lpscleave [OPTION]... [INFILE] OUTFILE1 OUTFILE2
Decomposes the data parameters of the linear process specification (LPS) in INFILE and write the result of the left component to OUTFILE1 and the rightcomponent to OUTFILE2. If INFILE is not present, stdin is used.
-iFILE
, --invariantFILE
A FILE which contains a data expression to strengthen the condition expressions.
-m
, --merge-heuristic
Enable heuristics to merge synchronization indices of summands.
-pPARAMS
, --parametersPARAMS
A comma separated list of PARAMS that are used for the left process of the cleave.
-fPREFIX
, --prefixPREFIX
Add a prefix to the synchronisation action labels to ensure that do not already occur in the specification
-sPARAMS
, --sharedPARAMS
A comma separated list of shared PARAMS that occur in both processes of the cleave.
-a
, --split-action
Enable heuristics to split the action expression of each summand, where the indices in INDICES are used as a fallback (if no optimal choice is available).
-c
, --split-condition
Enable heuristics to split the condition expression of each summand.
-t
, --split-summands
Split each summand with a disjunctive condition into one summand per clause
-lINDICES
, --summandsINDICES
A comma separated list of INDICES of summands where the left process generates the action.
--timings[FILE]
append timing measurements to FILE. Measurements are written to standard error if no FILE is provided
-u
, --use-next-state
Apply the invariant to the parameter values after the update instead of the current value
-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
Maurice Laveaux