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.
- orphan:
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 , --qlimit=NUM
limit enumeration of quantifiers to NUM iterations. (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 , --rewriter=NAME
use rewrite strategy NAME:
jittyjitty rewriting
jittyccompiled jitty rewriting
jittypjitty 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 log messages
-d , --debug
display detailed log messages
--log-level=LEVEL
display log messages up to and including level; either warn, verbose, debug or trace
-h , --help
display help information
--version
display version information
--help-all
display help information, including hidden and experimental options