MCRL2I(1)							   User Commands							 MCRL2I(1)

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:

       -rNAME, --rewriter=NAME
	      use rewrite strategy NAME:
		'jitty' for jitty rewriting (default),
		'jittyc' for compiled jitty rewriting,
		'jittyp' for 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 (C) 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/mcrl2/wiki/index.php/User_manual/mcrl2i>.

mcrl2i mCRL2 toolset 201202.0 (Release) 			    April 2012								 MCRL2I(1)