4mmuse24m(n)                                                                4mmuse24m(n)

1mNAME0m
       selt  - SE-MMC model checker

       Part of Tina Toolbox for analysis of Petri nets and Time Petri nets.


1mSYNOPSIS0m
       1mmuse 22m[-4mh24melp]

       1mmuse  22m[-prelude  mmcfile] [-q | -v] [-b | -c | -s | -m] [-limit n] [-wp
       n]
            ktzfile [-f formula | formfile] [outfile] [errorfile]

       1mmuse 22m[-prelude mmcfile] [-q | -v] [-b | -c | -s | -m] [-limit  n]  [-wp
       n]
            -script formfile ktzfile [outfile] [errorfile]


1mDESCRIPTION0m
       muse  model-checks  state-event  modal  mu-calculus (MMC) formulas on a
       kripke transition system given in ktz format. Muse is  a  global  model
       checker; the result of a query is a set of states or transitions.

       If  some  formula is specified (by  flag -f or by  providing formfile),
       then  the result  of  evaluation  of  the formula  is  printed  accord-
       ing to the output mode and verbosity flags, and muse exits.

       If  no  formula file is  specified,  then  muse  starts an  interactive
       session, evaluating commands entered by the user on standard input (see
       "muse se-mmc language and commands" below).



1mOPTIONS0m
       -4mh24melp  Recalls options.



       1mKtz input:0m


       ktzfile
              The kripke transition system on which formula are model-checked,
              in ktz format (extension .ktz).


       -wp (0|1|2)
              This  flag  removes (0), preserves (1),  or forces at each state
              (2) the temporal divergence  property possibly  present  in  the
              kts file (see tina's -wp flag for details).


       -script
              For using muse as a script interpreter: The first file is then a
              file  of  muse declarations and the second is a ktzfile, Evalua-
              tions of property  declarations  are  silent  and  formulas  are
              printed before their values.



       1mMMC input:0m


       -f formula
              Passes to muse the formula to be verified.


       formfile
              Specifies  a file holding the formulas to be verified. Must have
              extension .mmc


       -prelude mmcfile
              Specifies a  file containing muse  commands to be evaluated   on
              entry,  before   any formula  provided by  -f, by  formfile,  or
              interactively.  This  flag  is   useful  to   load   SE-MMC  li-
              braries.   mmcfile must  have extension .mmc.



       1mVerbosity level:0m


       -v     prints banner and evaluation times for MMC commands (default).


       -q     No   banner  nor times  are  printed. This  flag  is  useful for
              batch operation.


       -limit n
              Limits to n the number of items printed if -s or -m. No limit if
              n=0.



       1mOutput mode flags:0m


       -b     When evaluating a state (resp.  event) formula, prints its truth
              value for state (resp. transition) numbered 0.


       -c     When evaluating a state (resp.  event) formula, prints the  num-
              ber of states (resp. transitions) satisfying the formula.


       -s     When  evaluating  a state (resp.  event) formula, prints the set
              of states numbers (resp. transition numbers) satisfying the for-
              mula.  States (resp. transitions) are numbered in their order of
              occurrence in the ktz file.


       -m     When evaluating a state (resp. transition)  formula,  prints  in
              clear the set of state values (resp. transition values) satisfy-
              ing the formula.


       1mOutput destination:0m


       outfile
              Where results are written.



       1mErrors destination:0m


       errorfile
              Where error messages are written. By default, errors are printed
              on standard error.



1mMUSE SE-MMC LANGUAGE AND COMMANDS0m
1m1. 4m22mLexical24m 4mmatters24m:
       - A identifier is either:

       Any   place   or  transition  identifier   allowed  in  .net   or  .ndr
       descriptions, that  is: any  sequence of letters,  digits,  underscores
       "_"  and primes  "'", or any sequence of  characters enclosed in braces
       in which "{", "}" (except the outer ones) and "\" are prefixed by "\"

       Any sequence of symbols from the list ~ ` ! @ # $ % ^ & * - + = :  ?  |
        / < > [ ];

       A qualified identifier: an identifier prefixed by S., E. or L.

       e.g.    hello,  _p4'_,  123,  >=<, or {variable x45}, are legal identi-
       fiers.

       - The commands are: op, infix, prefix, forget,  verb,  output,  source,
       quit, assert.  Command names  may not be used  as operator or  variable
       names.

       -  When  analyzing  identifiers,  the  scanner  advances  as  right  as
       possible.  So, in a juxtaposition  of identifiers, two symbolic or  two
       alphanumeric  unbraced identifiers,  or e.g. an alphanumeric identifier
       and a  command name, must  be separated by  a space.  But no  space  is
       necessary   between  identifiers  of   different  kinds  or  between  a
       parenthesis (or ";") and an identifier.

       - justaposition bind  tighter than infixes and associate  to the  left,
       infixes  and prefixes associate to the  right. That is, if f is a 3-ary
       operator in functional notation, A,  B, -, are prefixes,  and  /\,  \/,
       are infixes:

                      A p1 => B - p3 /\ f u v w
         parses as (A p1) => ((B (- p3)) /\ (f u v wp))

                      f - B p1 (f p0 p1 (p4 /\ p5)) \/ f u v w
         parses as (f (- B p1) (f p0 p1 (p4 /\ p5))) \/ (f u v w)

         and       f - B p1 f p0 p1 p4 \/ f u v w
         parses as      (f (- B p1) f p0 p1 p4) \/ (f u v w)
         which is ill-typed

       -  infixes  have precedence in  0..5 (see  below). Infixes  with higher
       precedence bind tighter than those with lower precedence.



1m2. 4m22mThe24m 4minitial24m 4menvironment24m:
       It is made up of (pushed in that order):

       - The  atomic  state  and  event  propositions. They  have  the   names
       captured in the .ktz file,  i.e. those of the places and transitions of
       the Petri net if the .ktz file was generated by tina.

       - Then, the logic and arithmetic primitives, constituted of:

          constants:     T (true), F (false),
                    in some rare cases you may need to specify the kind of T or F,
                    this can be done by suffixing them with either :S (for states)
                    or :E (for transitions).
                 div (temporal divergence property),
                 sub (partially defined state or transition)

          prefixes: - (logic negation), ~ (arithmetic negation),
                 modal operators <f>_ and [f]_, for each transition formula f,
                 ` followed by an integer, designating a state or transition by its rank in the ktz input file,
                 the MEC4 primitives src, tgt, rsrc, rtgt

          infixes:  => (implies), <=> (equivalent), of precedence 1
                    /\ (and), \/ (or), of precedence 2
                 <=, >=, =, le, lt, ge, gt, of precedence 3
                 +, of precedence 4
                 *, of precedence 5
                  - Then the user defined operators.

       Since  the syntactic classes of atomic state propositions, atomic event
       propositions, logic primitives,  integer,  and user defined  operators,
       overlap,   we must have  some way  of disambiguating  identifiers.  For
       this:

       - unqualified identifiers are bound to  the command with than name,  if
       any,  or  otherwise  to  the last bound user defined operator with that
       name.

       - identifiers  qualified by  S (e.g.  S.p1)  are bound  to the   atomic
       state proposition with that name with the qualifier removed (e.g. p1);

       -  identifiers  qualified by  E (e.g.  E.t1)  are bound  to the  atomic
       event proposition with that name with the qualifier removed (e.g. t1);

       - identifiers  qualified by  L  (e.g.  L./\) are  bound  to the   logic
       primitive with that name with the qualifier removed (e.g. /\);

       So,  atomic  propositions (found  in the ktz  file) sharing  their name
       with some atomic propositions in a different group (state or event)  or
       with  some command  (e.g. op), or some logical  primitive (e.g.  -), or
       the name  of which  is an integer  (e.g.  3),  must be referred  to  in
       formulas by their qualified form (e.g.  S.op, E.-, or S.3);



1m3. 4m22mDerived24m 4mforms24m 4mand24m 4mfixpoint24m 4mnotation24m:
       The modalities of the mu-calculus are derived from the MEC4 primitives,
       as  follows.  They  benefit however of a specific concrete syntax. Muse
       supports both future and past modalities:

          <p>q   stands for   src (p /\ rtgt q)
          [p]q   stands for   -<p>(-q)

          q<p>   stands for   tgt (p /\ rsrc q)
          q[p]   stands for   -(-q)<p>

       Whether p is a transition formula and q is a state formula.

       Note: In <p>q (resp. q<p>), the muse type system assumes that p denotes
       a set of events and that q denotes a set of  states.  This  restriction
       will be dropped in a forthcoming release supporting polymorphic modali-
       ties.

       Modal mu-calculus makes use of fixpoint expressions:

       - Minimal fixpoint expressions make use of keywords "min" or "mu", fol-
       lowed  by the bound variable and a bar separating the variable from the
       body of the expression, as in  "min x | p \/ <q>x".

       - Maximal fixpoints makes use of keywords "max" or "nu".

       Note: muse does not perform yet any polarity checks on fixpoint expres-
       sions, this check is left to the user's responsability. Hence  termina-
       tion  of  evaluation  is not guaranteed (ill-formed expressions may di-
       verge).

       (more derived notations to come)


1m4. 4m22mFixity24m:
       Identifiers declared  infix (binary  logic primitives or  user  defined
       operators declared by "infix") must be used in infix notation;

       Identifiers  declared  prefix (unary  logic primitives or  user defined
       operators declared by "prefix") must  be used in prefix notation (in  a
       juxtaposition   of  identifiers, prefix  operators  associate with  the
       right expression);

       Other operators  or primitives accessed by their  qualified names  must
       be  used in functional notation.   E.g. if a1, a2, a3 are parenthesized
       expressions, and f has arity 3, then:

            a1 /\ a2 and L./\ a1 a2 are legal (and equivalent)
           but a1 L./\ a2 is ill-typed

            f - a1 a2 a3 is legal (parses as ((f (- a1)) a2) a3)
           but f L.- a1 a2 a3 T is ill-typed (parses as (((f L.-) a1) a2) a3)


1m4. 4m22mCommands24m 4mand24m 4meffects24m:
       Commands must terminate with ";".  In formula files, the final ";"  may
       be   omitted (EOF  plays that  role). The  effects of  commands  are as
       follows ("exp" is any MMC expression, x, y, f, xi are identifiers):

       exp;
            evaluates MMC expression exp;
            The result of evaluation of the last expression is always bound
            to identifier "it";

       assert exp "whentrue" "whenfalse";
              in bool output mode, evaluates exp then prints string whentrue
              (resp. whenfalse) if exp holds (resp. does not) instead of the
              default message TRUE (resp. FALSE). Equivalent to exp in other
              modes.

       op f x1 ... xn = exp;
            declares an  operator f  or arity n  (n >=  0), to be  used in
            functional notation;

       infix [n] x f y = exp;
            declares a binary operator f in infix notation. n is an
            optional integer in 0..5 specifying precedence.

       prefix f x = exp;
            declares a unary operator f in prefix notation;

       forget f1 ... fn;
            Removed items names f1 ...  fn from the environment, and their
            fixity information;

       source [file | "file"];
            reads at toplevel the contents of file. The file name is
            optionally surrounded  by string quotes (this  is necessary if
            the name includes spaces);

       verb [true | false | debug];
            verbosity level. Tne initial  setting follows from the command
            line flags -v | -q (default -v);

            true  (default):  prints   the  banner,  prompts,  results  of
            commands, and evaluation times;

            false:  just   prints  the   results  of  evaluation   of  MMC
            expressions (useful in batch mode);

            debug: may print extra information (mainly for developper);

       output [bool | card | set | values];
            specify   effects   and   results   of  evaluations   of   MMC
            expressions.  The  command  line  flags  -b, -c, -s,
            specifie the initial setting (default -c);

            If the expression evaluated is a state (resp. transition) expression:

            bool: evaluation prints the truth value (TRUE or FALSE) of the
            expression at state 0 (resp. transition 0);

            card (default): evaluation prints the number of states (resp. transitions)
            satisfying the expression;

            set: evaluation prints the set of states (resp. transitions)
            satisfying the expression;

            values: if muse was launched with option -m, evaluation prints
            the set of state values (markings) (resp. transition values (events))
            satisfying the expression.
            The command fails if option -m was not passed on the muse command line.

       which exp;
               Like exp; but overrides the default output option by "set";

       card exp;
               Like exp; but overrides the default output option by "card";

       quit
            leaves muse (also ^D on Unix targets).




1m5. 4m22mExample24m 4mcommands24m:
       # CTL. (All | Some) state along (Every | Some) path
       prefix AF g = min x | g \/ (<T>T /\ [T]x);
       prefix wAF g = min x | g \/ [T]x;
       prefix EF g = min x | g \/ <T>x;
       prefix AG g = max x | g /\ [T]x;
       prefix EG g = max x | g /\ ([T]F \/ <T>x);




1mEXAMPLES0m
       muse abp.ktz -b -prelude ctl.mmc -f "AG EF p1"
       muse abp.ktz



1mSEE ALSO0m
       nd(n),  tina(n),  plan(n),  struct(n),  ktzio(n),  ndrio(n),   tedd(n),
       selt(n), sift(n), pathto(n), scan(n), play(n), walk(n), reduce(n), for-
       mats(n), stan(n)


1mAUTHORS0m
       Bernard Berthomieu LAAS/CNRS,  2000-2026, Bernard.Berthomieu@laas.fr


Tina Tools                       Version 4.0.0                         4mmuse24m(n)
