lpscleave

Manual page for lpscleave

Usage

lpscleave   [OPTION]... [INFILE] OUTFILE1 OUTFILE2

Description

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.

Command line options

-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

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

Maurice Laveaux