lpsreach

This is a symbolic state space exploration tool for linear process specifications (.lps extension) largely based on the work presented in [1] and [2]. Similarly to lps2lts it can take any lps as input and produce a finite state space output. The main difference when compared to lps2lts is that lpsreach uses so-called symbolic representations internally to represent the set of states and transitions of the labelled transition system. Note that the symbolic representations in this tool are limited to finite sets, unlike the symbolic representations used in pbessymbolicbisim.

A typically use for lpsreach is as follows:

lpsreach --verbose infile.lps outfile.sym

This prints the number of states in the state space and saves the resulting symbolic state space in an internal file format for symbolic representations. The –verbose causes progress information to be printed as well. Currently, the resulting outfile.sym is not very useful, but in the future other tools will be introduced to convert it into a concrete LTS and reduce it modulo the standard equivalence relations such as bisimulation.

There are a number of tool options that can typically lead to large speedups. These can be tried in combination with –max-iterations to limit exploration depth to quickly benchmark their impact. First of all, –cached uses additional memory to reduce the amount of rewriting required. Next, –groups=simple is a simple, but often effective, heuristic to merge so-called transition groups, which correspond to the summands of the linear process and are explained in more detail below. There are two orthogonal exploration strategies implemented under options –chaining and –saturation that also often have a large impact on exploration performance.

To further guide the effectiveness of the exploration we need some additional background information.

Symbolic Exploration

The effectiveness of the symbolic representation is mostly determined by the size (in the number of nodes shown by –print-nodesize) of the symbolic data structures during intermediate computations. This size relies heavily on the order of the process parameters in the linear process and the dependencies of its summands on these process parameters. Intuitively, each summand is a condition-action-effect statement, where syntactic occurrences of process parameters in conditions, action and effects induce read dependencies and non-trivial effect statements induce write dependencies. Trivial being of the shape \(x := x\).

Currently, there are no heuristics implemented to compute the parameter order and the order provided by the linear process is used, but the –reorder option can be used to manually change the order. Ideally, parameters that depend (in some sense) on eachother, because for example one parameter occurs in the effect of another parameter, should be located close to eachother. To inspect these dependencies use the option –info. This will show a matrix under read/write patterns compacted where every column corresponds a parameter (in order) and every row corresponds to a transition group (in order), which are the summands by default.

Furthermore, the symbolic representation uses the process parameters as they are provided, which means that for complex data types (such as lists) the structure of the list is not used and it is represented as a set of values. Here, we can use lpsparunfold to introduce new parameters that allow a more structured symbolic representation.

Besides the order of the process parameters we also have to take into account the order of transition groups. By default there is one transition group for each summand in order of the summands of the linear process (as stored on disk). Use options -d –info to print the summands for every transition group for inspection. The order in which transition groups are applied can affect the size (in particular for the additional exploration strategies), where transition groups that write parameters that are read dependencies of other transition groups should generally be ordered first. Again, there are no heuristics for this and an order can be manually specified using –groups.

Transition groups can also be merged to reduce the amount of symbolic operations required, but doing so will over-approximate their dependencies (except for the –groups=simple) and this can be disadvantageous. Finally, to understand the consequences of the symbolic representation we explain it in more detail.

Symbolic Representation

For the state space of a linear process the set of states is typically a set of vectors, where every element in the vector corresponds to a process parameter. In lps2lts the states are represented as a set of (maximally shared) balanced binary trees. However, in lpsreach these set of vectors are represented by a so-called decision diagram based on function decomposition. This representation allows for maximally sharing equivalent sets and sharing prefixes. Furthermore, it allows for efficient implementation of various set and relational operations.

A set of vectors can be represented by the following function similar to how \(\mathbb{N} \rightarrow \mathbb{B}\) represents a set of natural numbers.

\[\begin{equation*} f: \mathbb{N} \times \cdots \times \mathbb{N} \rightarrow \mathbb{B} \end{equation*}\]

Note that we assume that all process parameters are bounded natural numbers since we can always bidirectionally map from natural numbers to abstract data. Now, the we can decompose \(f\) on the first argument as follows.

\[\begin{split}\begin{equation*} f(x_0, \ldots, x_n) = \begin{cases} f'_0(x_1, \ldots, x_n) &\textsf{if } x_0 = 0 \\ f'_1(x_1, \ldots, x_n) &\textsf{if } x_0 = 1 \\ \cdots \\ f'_{\|x_0\|}(x_1, \ldots, x_n) &\textsf{if } x_0 = \|x_0\| \\ \end{cases} \end{equation*}\end{split}\]

Such that \(f(x_0, x_1, \ldots, x_n) = f'_{x_0}(x_1, \ldots, x_n)\) for all \(0 \leq x_0 \leq \|x_0\|, \ldots, 0 \leq x_n \leq \|x_n\|\), where \(\|x_0\|\) indicates the maximum value of \(x_0\).

The decision diagram for this decomposed function consists of vertices and edges where vertices represent the functions, such as \(f\) and \(f'_0\), and edges the decisions, for example \(x_0 = 0\). The vertices are maximally shared such that if \(f'_0 = f'_1\) then there is a unique vertex in memory representing this function. Furthermore, we always decompose on the first argument, so the decision diagram is a tree of height \(n+1\).

The resulting decision diagram is called a quasi-reduced multi-valued decision diagrams, which is quasi-reduced since every path from the root to a leaf is exactly \(n+1\) long, because it never skips levels. For the implementation we use Sylvan [3], which implements list decision diagrams. These are unfolded multi-valued decision diagrams where every vertex has exactly two edges, one being the decision and the other being the next element in the list.

References

  • [1] Stefan Blom and Jan Cornelis van de Pol. Symbolic reachability for process algebras with recursive data types. In J.S. Fitzgerald, A.E. Haxthausen, and H. Yenigun, editors, Theoretical Aspects of Computing - ICTAC 2008, number Supplement in Lecture Notes in Computer Science, pages 81–95. Springer, August 2008.

  • [2] Jeroen Meijer. Efficient learning and analysis of system behavior. PhD thesis, University of Twente, Netherlands, September 2019.

  • [3] Tom van Dijk, Jaco van de Pol. Sylvan: multi-core framework for decision diagrams. Int. J. Softw. Tools Technol. Transf. 19(6): 675-696 (2017)

Manual page for lpsreach

Usage

lpsreach   [OPTION]... [INFILE [OUTFILE]]

Description

Read an LPS from INFILE and write a symbolic labelled transition system to OUTFILE. If OUTFILE is not present, no symbolic LTS is written. If INFILE is not present, stdin is used.

Command line options

--cached

use transition group caching to speed up state space exploration

--chaining

reduce the amount of breadth-first iterations by applying the transition groups consecutively

--deadlock

report the number of deadlocks (i.e. states with no outgoing transitions).

--groups[=GROUPS]

‘none’ (default) no summand groups

‘used’ summands with the same variables are joined ‘simple’ summands with the same read/write variables are joined a user defined list of summand groups separated by semicolons, e.g. ‘0; 1 3 4; 2 5’

--info

print read/write information of the summands

--initial-ratio[=NUM]

power-of-two ratio of initial and maximum table size (default 16)

--lace-dqsize[=NUM]

set length of Lace task queue (default 1024*1024*4)

--lace-stacksize[=NUM]

set size of program stack in kilobytes (0=default stack size)

--lace-workers[=NUM]

set number of Lace workers (threads for parallelization), (0=autodetect, default 1)

--max-iterations[=NUM]

limit number of breadth-first iterations to NUM

-m[NUM] , --memory-limit[=NUM]

Sylvan memory limit in gigabytes (default 3)

--print-nodesize

print the number of LDD nodes in addition to the number of elements represented as ‘elements[nodes]’

-QNUM , --qlimit=NUM

limit enumeration of quantifiers to NUM iterations. (Default NUM=1000, NUM=0 for unlimited).

--reorder[=ORDER]

‘none’ (default) no variable reordering

‘random’ variables are put in a random order ‘a user defined permutation e.g. ‘1 3 2 0 4’

-rNAME , --rewriter=NAME

use rewrite strategy NAME:

jitty

jitty rewriting

jittyc

compiled jitty rewriting

jittyp

jitty rewriting with prover

--saturation

reduce the amount of breadth-first iterations required by applying the transition groups until fixed point is reached

--table-ratio[=NUM]

power-of-two ratio of node table and cache table (default 1)

--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 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

Author

Wieger Wesselink