muse 3.8.0 release notes

muse is a global modal mu-calculus model checker.
It model checks the kripke transition systems built by the tina or sift tool against modal mu-calculus formula. Accepts a rich language allowing notably to declare new operators or redefine existing operators. Muse computes sets of states or transitions obeying some formula. A path to some state or transition can then be computed using the pathto and plan tools, and that path replayed on the model using tool play or the nd stepper.

muse can be used in batch mode: if some formula is passed by -f or if a mmc file is passed not following -prelude, or in interactive mode otherwise.

Some typical usage are as follows:

muse ktzfile [verbopt] [outopt] [-prelude mccfile] -f form

computes in batch mode the set of states in the state space represented by file ktzfile obeying formula form. If the prelude option is present, the commands in file mccfile are evaluated before formula form (file mccfile can be thought as a library).
verbopt is a verbosity option, one of -q or -v (default)
outopt is the output option, one of -b, -c (default), -s, -m.

muse ktzfile [verbopt] [outopt] mccfile

evaluates in batch mode the commands read in file mccfile.
muse ktzfile [verbopt] [outopt] [-prelude mccfile]
starts an interactive muse session loading first file mccfile, if present.

mccfile may contain declarations of formulas (those commands starting with keyword op, prefix or infix), muse commands (see the muse manual page) and evaluation requests (expressions, aka formulas).

In batch mode, the verbosity option -q suppresses printing of the muse banner and of computing times for commands.

Up to the September 17 2024 3.8.0 release (aka 3.8.0 early), declaration results in all modes, for declarations found in mccfiles, were printed.

muse 3.8.0 introduced options -m and -script

-m
When evaluating a state (resp. transition) formula, the result set of states (resp. transitions) are printed as the state values (resp. transition values) obeying the formula. Check the muse manual page for a description of The other output modes.
-script
For using muse as a script interpreter: The first file is then a file of muse declarations and the second is a ktzfile, Evaluations of property declarations are silent and formulas are printed before their values when evaluating expressions (according to the output option selected).

The latest revision of muse 3.8.0 (of October 22) introduced option -limit and brought slight changes in the printed results of option -m and declarations.

-limit n
Limits to n the number of items printed in output modes -s or -m. No limit if n=0 (default). Please note that ktzfles may capture millions of states/transitions or more, and that trying to print them might fail badly, hence the purpose of -limit.
-m output changes:
3.8.0 early printed state values as s:m: marking while 3.8.0 prints them as s: marking 3.8.0 early printed transitions values as labels (transition names for Petri nets) while 3.8.0 prints them as triples: (source state,label,target state)
Only expression results are printed in batch modes, while declaration results were also printed in 3.8.0 early. This brings more user control of muse outputs (outputs may be huge). Note that if "op G = ...;" is a declaration, then "G;" is an expression, so the former (3.8.0 early) printing effects can always be achieved by adding some expressions.

In paper deadlock studies, written with muse version 3.8.0 early in mind, tool muse is used to compute particular sets of states relevant to deadlock analysis (live zone, dead zone, etc). Four mcc files are used for that purpose: lz.mmc dz.mmc, fbm.mmc, zones.mmc; their contents are made precise in the paper.

files lz.mmc and dz.mmc print the same results in (early) 3.8.0 and in (final) 3.8.0, but files zones.mmc and fbm.mmc don't. To print results exactly as shown in the paper when using final 3.8.0, one should use the slightly updated files zones.mmc and fbm.mmc. Last updated: Thu Apr 25 18:09:00 CEST 2024