.. index:: lpscleave

.. _tool-lpscleave:

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 :ref:`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 :ref:`tool-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.

.. include:: man/lpscleave.rst