lpsconstelm

This tool removes constant process parameters from the LPS. If it can be determined that certain parameters of this LPS remain constant throughout any run of the process, all occurrences of these process parameter are replaced by the initial value and the process parameters are removed from the LPS. After substitution expressions are simplified using a rewriter. Note that summands of which the conditions are false are only removed with the --remove-trivial-summands flag.

If the initial value of a process parameter is a global variable and remains a global variable throughout the run of the process, the process variable is considered constant.

If the initial value of a process parameter is a global variable and is only changed once to a certain value, the process parameter is constant and the specific value is used for substitution.

A typical example of lpsconstelm is the following. Consider the linear process:

act a:Nat;
proc P(m,n:Nat)=
        a(m).P(m,n+1) +
        (m>0) -> a(m).P(m+1,n);
init P(0,0);

It is determined that m can only have the value 0, and the second summand can never take place. The result is:

act  a: Nat;
proc P(n: Nat) =
       a(0) .
         P(n+1);
init P(0);

Note that lpsconstelm is very useful in simplifying linear processes. Its application does not reduce the size of generated state spaces. But its application can enable other tools, such as lpsparelm to become more effective.

In some cases lpsconstelm can reduce the number of summands quite dramatically. For instance when dealing with similar communicating processes, such as in:

proc P(id:Nat,...)= ....;
init allow({...},comm({...},P(0,...)||P(1,...)||...||P(10,...)));

the variables id for each processes are replaced by the concrete ids. When processes send messages to other processes indexed by numbers (e.g., send(message,sender_id,receiver_id)) then summands with communication that are not possible due to mismatching id’s are removed from the lps by lpsconstelm. For a typical example such as Milner’s scheduler, this reduces the number of summands from quadratic to linear in the number of participating processes.

Manual page for lpsconstelm

Usage

lpsconstelm   [OPTION]... [INFILE [OUTFILE]]

Description

Remove constant process parameters from the LPS in INFILE and write the result to OUTFILE. If INFILE is not present, standard input is used. If OUTFILE is not present, standard output is used.

Command line options

-c , --ignore-conditions

ignore conditions by assuming they evaluate to true

-f , --instantiate-free-variables

allow free variables to be instantiated as a side effect of the algorithm. This functionality is untested!

-QNUM , --qlimitNUM

limit enumeration of quantifiers to NUM variables. (Default NUM=1000, NUM=0 for unlimited).

-s , --remove-singleton-sorts

remove parameters with single element sorts

-t , --remove-trivial-summands

remove summands with condition false

-rNAME , --rewriterNAME

use rewrite strategy NAME:

jitty

jitty rewriting

jittyc

compiled jitty rewriting

jittyp

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

display intermediate messages up to and including level

-h , --help

display help information

--version

display version information

Author

Wieger Wesselink; Frank Stappers