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



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


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 , --qlimit=NUM

limit enumeration of universal and existential quantifiers in data expressions to NUM iterations (default NUM=10, NUM=0 for unlimited).

-s , --remove-singleton-sorts

remove parameters with single element sorts

-t , --remove-trivial-summands

remove summands with condition false

-rNAME , --rewriter=NAME

use rewrite strategy NAME:


jitty rewriting


compiled jitty rewriting


jitty rewriting with prover


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

-d , --debug

display detailed log messages


display log messages up to and including level; either warn, verbose, debug or trace

-h , --help

display help information


display version information


display help information, including hidden and experimental options


Wieger Wesselink; Frank Stappers