User manual/lpssumelm

From MCRL2

Remove superfluous summations from an LPS.

Synopsis

lpssumelm [OPTION]... [INFILE [OUTFILE]]

Short description

The lpssumelm tool removes superfluous summations from the linear process specification (LPS) in INFILE and write the result to OUTFILE. If INFILE is not present, stdin is used. If OUTFILE is not present, stdout is used.

The simplest case this tool handles is that, whenever a summation variable does not occur in the other terms of the summand, this summation variable is plainly removed. There is however also a more complex situation where the summation variable occurs in an equality within the condition. There is an axiom that says that we may then substitute the other term of the equality for the summation variable. We can then remove both the summation variable and the condition in which it occurred.

Options

OPTION can be any of the following 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

Known issues

Lpssumelm is not applicable if types in an equality in a condition do not match directly, i.e. an implicit type cast is used in order to match the types. An example of this is the following process:

proc P(i : Int) = sum n : Nat . (n == i) -> tau . P(i);
 
init P(5);

In this example an implicit cast Nat2Int (i.e. Nat2Int(n) == i) is used in order to have compatible types. Because of this, the tool is unable to remove the summation over n.

Author

Written by Jeroen Keiren.

Bug reporting

Report bugs at our issue tracking system.

lpssim

lpssuminst