Man Linux: Main Page and Category List


       mcrl2i - Interpreter for the mCRL2 data language


       mcrl2i [OPTION]... [INFILE]


       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
         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
                                             VARLIST  that satisfy EXPRESSION.
       VARLIST is of the form x,y,...: S; ... v,w,...: T.


       OPTION can be any of the following:

       -rNAME, --rewriter=NAME
              use rewrite strategy NAME:
                ’jitty’ for jitty rewriting (default),
                ’jittyp’ for jitty rewriting with prover,
                ’jittyc’ for compiled jitty rewriting,
                ’inner’ for innermost rewriting,
                ’innerp’ for innermost rewriting with prover, or
                ’innerc’ for compiled innermost rewriting

       Standard options:

       -q, --quiet
              do not display warning messages

       -v, --verbose
              display short intermediate messages

       -d, --debug
              display detailed intermediate messages

       -h, --help
              display help information

              display version information


       Written by Muck van Weerdenburg; Jan Friso Groote.


       Report bugs at <>.


       Copyright © 2010 Technische Universiteit Eindhoven.
       This is free software.  You may redistribute copies  of  it  under  the
       terms         of        the        Boost        Software        License
       <>.  There is NO WARRANTY,  to  the
       extent permitted by law.


       See              also             the             manual             at

mcrl2i mCRL2 toolset July 2010 (devMayp2010)