lpsparelm
The tool lpsparelm tries to find those parameters in a linear process that do not influence the behaviour and removes those. A parameter in a linear process does not influence the behaviour if it does not occur in an action or in a condition, either directly, or indirectly via other parameters. Removing parameters is very useful as it generally substantially reduces the state space, sometimes even from infinite to finite.
In the following example the parameter n does not influence the behaviour of the
process:
act a;
proc P(n: Nat) =
a.P(n+1);
init P(0);
After applying lpsparelm the linear process looks as follows:
act a;
proc P=a.P;
init P;
The state space has been reduced from an infinite one to a single state.
In the following example lpsparelm cannot remove any parameter:
act a:Nat;
proc P(m,n,p:Nat)=(n<10) -> a(m).P(n+p,m+1,p+1);
init P(0,0,0);
The parameter m occurs in an action, n occurs in a condition and p indirectly
influences the value of n.
It can be useful to remove parameters from actions (use lpsactionrename for this purpose)
as it may allow lpsparelm to remove more parameters. If in the previous example a(m)
is renamed to a, both parameters n and p can be removed.
Sometimes parameters of a process are of a complex datatype using constructors. E.g., a parameter can be of type list, but only the first element in the list influences the behaviour. Then the list can be unfolded in its first element and the rest using the tool lpsparunfold. Using lpsparelm the resulting parameter modelling the rest of the list can be removed. A typical application of the combination of these two tools are for board games, where the board is represented as a list of lists. Unfolding the board completely and removing redundant parameters can speed up the generation of the state space. Another typical application is the elimination of data from communication protocols. By unfolding the message frames in the protocol into their individual components, by preventing data to be delivered, lpsparelm can remove all the data from the protocol, allowing to investigate its full behaviour, independently of the nature of the data.
- orphan:
Usage
lpsparelm [OPTION]... [INFILE [OUTFILE]]
Description
Remove unused parameters 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.
Command line options
--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