User manual/lpssuminst

From MCRL2

Instantiate summation variables of an LPS.

Synopsis

lpssuminst [OPTION]... [INFILE [OUTFILE]]

Short description

The lpssuminst tool instantiates summation variables of the linear process specification (LPS) in INFILE and writes the result to OUTFILE. If INFILE is not present, stdin is used. If OUTFILE, stdout is used.

Options

OPTION can be any of the following:

-f, --finite

only instantiate variables whose sorts are finite

-rNAME, --rewriter=NAME

use rewrite strategy NAME

-t, --tau

only instantiate variables in tau summands

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

--version

display version information

Detailed description

Summation variables are instantiated by applying induction on the values of the sort of the variable. Take for example the following LPS:

sort D = struct d1 | d2;
     E = struct e1(D) | e2;
 
act  a: D;
     b: E;
 
proc P = sum d: D. a(d) . P
       + sum e: E. b(e) . P
       ;
 
init P;

lpssuminst instantiates the variable 'd' to the constructors 'd1' and 'd2' of sort 'D', and variable 'e' to the constructors 'e1(d1)', 'e1(d2)' and 'e2':

sort D = struct d1 | d2;
     E = struct e1(D) | e2;
 
act  a: D;
     b: E;
 
proc P = a(d1) . P
       + a(d2) . P
       + b(e1(d1)) . P
       + b(e1(d2)) . P
       + b(e2) . P
       ;
 
init P;

Author

Written by Jeroen Keiren.

Bug reporting

Report bugs at our issue tracking system.

lpssumelm

lpsuntime