NAME

       mcrl2i - Interpreter for the mCRL2 data language

SYNOPSIS

       mcrl2i [OPTION]... [INFILE]

DESCRIPTION

       Evaluate mCRL2 data expressions via a text-based interface. If INFILE is present and if it
       contains an LPS or PBES, the data types of this specification may be  used.  If  no  input
       file  is  given,  only  the standard numeric datatypes are available. Stdin is ignored.The
       following commands are available to manipulate mcrl2 data expressions. Essentially,  there
       are  commands  to  rewrite and type expressions, as well as generating the solutions for a
       boolean expression. The expressions can contain assigned  or  unassigned  variables.  Note
       that there are no bounds on the number of steps to evaluate or solve an expression, nor is
       the number of solutions bounded. Hence, the assign, eval solve commands can give  rise  to
       infinite loops.
         h[elp]                         print this help message.
         q[uit]                         quit.
         t[ype] EXPRESSION              print type of EXPRESSION.
         a[ssign] VAR=EXPRESSION        evaluate the expression and assign it to the
         variable.
         e[val] EXPRESSION              rewrite EXPRESSION and print result.
         v[ar] VARLIST                  declare variables in VARLIST.
         r[ewriter] STRATEGY            use STRATEGY for rewriting.
         s[solve] VARLIST. EXPRESSION   give all valuations of the variables in
                                             VARLIST  that satisfy EXPRESSION.  VARLIST is of the
       form x,y,...: S; ... v,w,...: T.

OPTIONS

       OPTION can be any of the following:

       -QNUM, --qlimit=NUM
              limit enumeration of quantifiers to NUM variables.  (Default  NUM=1000,  NUM=0  for
              unlimited).

       -rNAME, --rewriter=NAME
              use  rewrite  strategy  NAME:  'jitty'  jitty rewriting (default) 'jittyc' compiled
              jitty rewriting 'jittyp' jitty rewriting with prover

       --timings[=FILE]
              append timing measurements to FILE. Measurements are written to standard  error  if
              no FILE is provided

       Standard options:

       -q, --quiet
              do not display warning messages

       -v, --verbose
              display short intermediate messages

       -d, --debug
              display detailed intermediate messages

       --log-level=LEVEL
              display intermediate messages up to and including level

       -h, --help
              display help information

       --version
              display version information

AUTHOR

       Written by Muck van Weerdenburg; Jan Friso Groote.

REPORTING BUGS

       Report bugs at <http://www.mcrl2.org/issuetracker>.

COPYRIGHT

       Copyright © 2012 Technische Universiteit Eindhoven.
       This  is  free  software.   You may redistribute copies of it under the terms of the Boost
       Software License <http://www.boost.org/LICENSE_1_0.txt>.  There is  NO  WARRANTY,  to  the
       extent permitted by law.

SEE ALSO

       See also the manual at <http://www.mcrl2.org/release/user_manual/tools/mcrl2i.html>.