lpscleave

A tool that can be used to split (or cleave) a linear process (.lps extension) based on a parameter partitioning and various heuristics. The main goal is that the resulting components can be used to perform compositional minimisation to obtain a smaller state space that is strongly bisimilar to the original LPS with the corresponding tool lpscombine.

A typically use for lpscleave is as follows:

lpscleave --verbose infile.lps left.lps right.lps

The left.lps and right.lps are the two components generated by the tool based on the given options whose summands are derived from infile.lps. The options –parameters and –shared are the most important options that allow the user to define how the parameters are cleaved. First of all, parameters passed to –parameters occur exclusively in left.lps, parameters passed to –shared occur in both left.lps and right.lps and the remaining parameters occur exclusively in right.lps. The option –summands can be used to define summands where the action expression is put in left.lps.

There are various heuristics implemented by the tool to refine the choices made when generating the summands of both components. Two rather safe and useful heuristics are enabled by options –split-action and –split-condition that allow splitting multi-actions into individual actions and to split conjunctive conditions into individual clauses. The –merge-heuristic option is useful, but generally quite expensive to compute.

Compositional Minimisation

The general approach for compositional minimisation is the following. First ,we generate both state spaces:

lps2lts --verbose --no-info left.lps left.lts
lps2lts --verbose --no-info right.lps right.lts

Next, we reduce both state spaces modulo bisimulation (or any other equivalence):

ltsconvert -ebisim left.lts left_reduced.lts
ltsconvert -ebisim right.lts right_reduced.lts

Finally, we combine the resulting minimised state spaces using lpscombine as follows:

lpscombine --lts --verbose left_reduced.lts right_reduced.lts result.lts

Cleaving can also again be performed on left.lps (or right.lps) before combining the results again, but in that case we must ensure that the actions introduced by the tool are unique. For this purpose we can use the –prefix option to prefix all introduced action names. In that case we must also pass –prefix to lpscombine when combining them again.

The main difficulty in applying this technique is ensuring that left.lts and right.lts are finite (and smaller than the original state space), which depends strongly on the heuristics and user-defined choice of parameter partitioning and where the actions are generated in the presence of infinite data types and summations. The lpsreach tool can often be used to quickly figure out whether the state spaces are at least finite.

References

[1] Maurice Laveaux, Tim A. C. Willemse. Decomposing Monolithic Processes in a Process Algebra with Multi-actions. ICE 2021: 57-76.

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 , --invariant=FILE

A FILE which contains a data expression to strengthen the condition expressions.

-m , --merge-heuristic

Enable heuristics to merge synchronization indices of summands.

-pPARAMS , --parameters=PARAMS

A comma separated list of PARAMS that are used for the left process of the cleave.

-fPREFIX , --prefix=PREFIX

Add a prefix to the synchronisation action labels to ensure that do not already occur in the specification

-sPARAMS , --shared=PARAMS

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 , --summands=INDICES

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-level=LEVEL

display intermediate messages up to and including level

-h , --help

display help information

--version

display version information

--help-all

display help information, including hidden and experimental options

Author

Maurice Laveaux