Man Linux: Main Page and Category List


       mcrl22lps - translate an mCRL2 specification to an LPS


       mcrl22lps [OPTION]... [INFILE [OUTFILE]]


       Linearises  the  mCRL2 specification in INFILE and writes the resulting
       LPS to OUTFILE. If OUTFILE is not present, stdout is used. If INFILE is
       not present, stdin is used.


       OPTION can be any of the following:

       -b, --binary
              when  clustering  use binary case functions instead of n-ary; in
              the presence of -w/--newstate, state variables are encoded by  a
              vector of boolean variables

       -e, --check-only
              check syntax and static semantics; do not linearise

       -c, --cluster
              all actions in the final LPS are clustered

       -D, --delta
              add  a true->delta summands to each state in each process; these
              delta’s subsume all other conditional timed delta’s, effectively
              reducing  the  number  of  delta  summands  drastically  in  the
              resulting linear process; speeds up linearisation

       -lNAME, --lin-method=NAME
              use linearisation method NAME:
                ’regular’ for generating an LPS in regular form
                (specification should be regular, default),
                ’regular2’ for a variant of  ’regular’  that  uses  more  data
                (useful when ’regular’ does not work), or
                ’stack’ for using stack data types
                (useful when ’regular’ and ’regular2’ do not work)

       -w, --newstate
              state  variables  are  encoded  using enumerated types (requires
              linearisation method  ’regular’  or  ’regular2’);  without  this
              option numbers are used

       -z, --no-alpha
              alphabet reductions are not applied

       -n, --no-cluster
              the  actions  in  intermediate  LPSs  are not clustered (default
              behaviour is that intermediate LPSs are clustered and the  final
              LPS is not clustered)

       -g, --no-deltaelm
              avoid removing spurious delta summands

       -f, --no-globvars
              instantiate  don’t care values with arbitrary constants, instead
              of modelling them by global  variables.  This  has  no  effecton
              global variable that are declared in the specification.

       -o, --no-rewrite
              do  not  rewrite  data  terms while linearising; useful when the
              rewrite system does not terminate

       -m, --no-sumelm
              avoid applying sum elimination in parallel composition

       -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

       -a, --statenames
              the names of state variables are derived from the specification

       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 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

mcrl22lps mCRL2 toolset July 2010 (Maye2010ent)