Personal tools
Views
Toolbox

User manual/AllInOnePage

From MCRL2

Jump to: navigation, search

Contents

Introduction

mCRL2 stands for micro Common Representation Language 2. It is a specification language that can be used to specify and analyse the behaviour of distributed systems and protocols and is the successor to μCRL. Using its accompanying toolset systems can be analysed and verified automatically.

Philosophy

mCRL2 is based on the Algebra of Communicating Processes (ACP) which is extended to include data and time. Like in every process algebra, a fundamental concept in mCRL2 is the process. Processes can perform actions and can be composed to form new processes using algebraic operators. A system usually consists of several processes (or components) in parallel.

A process can carry data as its parameters. The state of a process is a specific combination of parameter values. This state may influence the possible actions that the process can perform. In turn, the execution of an action may result in a state change. Every process has a corresponding state space or Labelled Transition System (LTS) which contains all states that the process can reach, along with the possible transitions between those states.

Using the algebraic operators, very complex processes can be constructed containing, for example, lots of parallelism. A central notion in mCRL2 is the linear process. This is a process from which all parallelism has been removed to produce a series of condition - action - effect rules. Complex systems, consisting of hundreds or even thousands of processes, can be translated to a single linear process. Even for systems with an infinite state space, the linear process (being an abstract representation of that state space) is finite and can often be obtained very easily. Therefore, most tools in the mCRL2 toolset operate on linear processes rather than on state spaces.

Model checking is provided using Parameterised Boolean Equation Systems (PBES). Given a linear process and a formula that expresses some desired behaviour of the process, a PBES can be generated. The solution to this PBES indicates whether the formula holds on the process or not. An attempt can be made to remove data from a PBES in order to obtain a BES, which is often easier to solve.

History

Around 1980 many process algebras were designed to model behaviour. Most notably were CCS (Calculus of Communicating Processes, Milner), ACP (Algebra of Communicating Processes, Bergstra and Klop) and CSP (Communicating Sequential Processes, Hoare). These process algebras were mainly used as an object of study, mainly due to their lack of proper data types.

In order to use these languages for actual modelling of behaviour a number of process algebraic specifiation languages have been designed, which invariably were extended with equational datatypes. The most well known is LOTOS (Language of Temporal Ordering Specifications , Brinksma), but others are PSF (Process Specification Formalism, Mauw and Veltink) and μCRL (micro Common Representation Language, Groote and Ponse).

Unfortunately, the use of abstract data types made these languages unpleasant when it came to the specification of complex behaviour. Therefore, we designed the language mCRL2 (the successor of μCRL) to contain exactly those data types that one would expect when writing specifications, namely Bool, Pos, Nat, Int, Real, lists, sets, bags, functions and functional data types. These data types are machine independent. For instance there is no upperbound on natural numbers, sets are not necessarily finite, quantification can be used within boolean terms and lambda abstraction is part of the language. Furthermore, the language features time and multi-actions, which were not present in most of the process specification languages of the previous generation.

Note that mCRL2 is extremely rich and it is easy to express non-computable behavioural specifications in it. Typically, for those specifications, tool supported analysis will not be very fruitful. The advanced use of mCRL2 requires a good understanding of the language, the underlying notions and even of the implementation of the analysis tools. For more straightforward use this is not needed. An effective rule of thumb is that everything that could be done using languages such as LOTOS, PSF and μCRL, can be done without a problem using mCRL2.

Overview of this document

This user manual contains the following sections:


Installation instructions

Supported platforms for binary distributions

Currently the binary distributions are supported by following platforms:

Windows

Note: Other Microsoft Windows platforms may work, but have not been (thoroughly) tested.

Mac OS X

Linux

Installing a binary distribution

Unix/Linux

Binary distributions for some linux versions are available. See the Download page for more details.

For (manually) installing the mCRL2 toolset under other Unix/Linux variants, please follow the CMake build instructions.

Mac OS X

A binary distribution for Darwin is available. See the Download page for details.

For manually installing the mCRL2 toolset under Mac OS X, please follow the CMake build instructions.

Windows

These instructions are for installing the toolset on Windows.

  1. If a previous version of the toolset is installed, make sure to uninstall the toolset via "Add or Remove Programs" in the "Control Panel"
  2. Obtain a binary distribution from the download page.
  3. Install the toolset with the windows installer. The toolset will be installed to the chosen path.
  4. The tools can be found in the installation directory of your choice.
  5. NOTE: The toolset contains a number of command line tools. For effective use of these tools we advise you to add the installation directory to your PATH environment variable. This can be achieved by making the appropriate choice in the installer.

Installing a source distribution

To install a source distribution please follow the CMake build instructions.


Toolset overview

Introduction

An overview of the mCRL2 toolset is given in the picture below. It shows the main concepts that play a role (in blue) and the operations that can be performed on these concepts (in red). In the toolset, a file format is associated with every concept and operations are implemented in tools. In order to get a feeling for the relevant concepts and tools, we describe the workflow of a typical analysis using mCRL2 below.

All tools can be accessed via a command-line interface. Another possibility is to use the mcrl2-gui tool which provides access to the tools via a GUI.

Image:ToolsetOverview.png

mCRL2 specification and linearisation

Every analysis starts off by specifying the behaviour of the system being studied. This can be any kind of system, though the main application of mCRL2 is in distributed software systems. The specification can be seen as a model of the real system: it is a simplified, or abstracted version of reality. Obtaining a specification that is faithful to the real system is far from trivial and beyond the scope of this overview.

An mCRL2 specification is a plain-text file containing a model in the mCRL2 language. It can be created using any text editor. For a description of the mCRL2 language we refer to the Language reference.

Typically, the specification of a distributed system contains several processes that run in parallel. The first step in the mCRL2 analysis process is to linearise this specification to obtain a Linear Process Specification (LPS). This is an mCRL2 specification from which all parallelism has been removed. All that remains is a series of condition -- action -- effect rules that specify how the system as a whole reacts to certain stimuli given its current state. Because of its much simpler form, the LPS is much more suitable for automated analysis than an mCRL2 specification. Therefore, most tools in the mCRL2 toolset operate on LPSs.

The main tool for linearisation is mcrl22lps. Given an mCRL2 specification, it produces an equivalent LPS on which other tools can be run. We investigate these tools below.

LPS tools

An LPS is stored in a binary file format for efficiency. After having obtained an LPS, a very useful analysis method is by simulating the model. Starting from the initial state, sequences of actions can be performed which can quickly reveal unexpected or erroneous behaviour. It is also a good way of getting acquainted with the modelled behaviour.

The mCRL2 toolset contains two tools for simulation of an LPS: sim (command-line interface) and xsim (graphical user interface).

Some statistical information about an LPS can be collected using the lpsinfo tool. The LPS itself can also be printed in a pretty, human-readable format. The tool for this task is lpspp.

In essence, the LPS is a symbolic (or implicit) representation of the state space or labelled transition system (LTS) that describes the behaviour of the system explicitly. This LTS can be constructed from the LPS using a state space generator. In mCRL2 the tool that performs this task is lps2lts.

As state space generation can take a lot of time, it is often beneficial to reduce the LPS or make it more suitable for state space generation. Several tools are available for this, of which we mention a few here: lpssumelm, lpssuminst, lpsparelm, lpsconstelm and lpsrewr. Please refer to the manual pages of these tools for more information.

LTS tools

Once an LTS has been generated from an LPS, it can be visualised in several ways using interactive GUI tools. The most straightforward way of visualising an LTS is by showing it as a node-link diagram or graph. The ltsgraph tool performs this task. It can reorganise the produced image using a force-directed algorithm.

The picture produced by ltsgraph can become very cluttered for larger LTSs. Another LTS visualisation tool is ltsview which employs a clustering technique to reduce the complexity of the image. It produces a 3D visualisation of the LTS and aims to show symmetry in the behaviour of the system.

Diagraphica also clusters states to reduce complexity, producing a 2D image. It clusters states based on state parameter values, instead of on structural properties like ltsview.

Apart from these visualisation tools, a powerful tool is ltsconvert which can reduce an LTS modulo various equivalences. This often produces an LTS that is dramatically smaller than the original LTS, while important properties are maintained. The tool can also convert between various LTS file formats, some of which are textual, others binary.

An equally powerful tool is ltscompare which can check whether two LTSs are behaviourally equivalent or similar using various notions of equivalence/similarity.

The tool lts2lps can transform an LTS into an LPS, such that symbolic computation can be continued, e.g. after minimisation.

Model checking using PBESs

The aforementioned tools aid in getting more insight into the behaviour specified by an mCRL2 specification. However, a system's analysis often involves showing that the modelled system exhibits certain desired properties (or does not exhibit undesired ones). This can be done using model-checking techniques, which are very powerful verification methods.

In mCRL2, model checking is provided using parameterised boolean equation systems (PBESs). As mentioned before, the central notion in mCRL2 is the LPS. Not surprisingly, model checking also starts off with an LPS, which contains a symbolic specification of the system's behaviour.

The other input needed for model checking, is a formula expressing a desired property that the system should not violate (or satisfy). Such formulas are expressed in the regular modal μ-calculus (extended with data) and can be entered into a plain-text file using any text editor. The syntax of these formulas is described in the Language reference.

Given an LPS and a formula, the tool lps2pbes produces a PBES in which the model checking question of "does the formula hold for this LPS?" is encoded. The PBES is stored in a binary file format. By solving the PBES, an answer to this question can be found. The main tool for trying to solve a PBES is pbes2bool. It attempts to solve a given PBES and (if successful) returns either true or false.

Note that solving PBESs is generally undecidable, so the attempt may fail. In this case, more in-depth analysis of the PBES may be required. The tool pbespp is provided to pretty print a PBES in a human-readable format. Statistical information can be obtained using pbesinfo and the PBES can be simplified using pbesrewr. Furthermore some tools for simplifying the PBES are available, such as pbesparelm and pbesconstelm.

Import and export

The mCRL2 toolset also provides tools for converting system specifications in other languages to mCRL2. This can be done for Chi-models using chi2mcrl2, for Petri nets using pnml2mcrl2 and for typed LySa using lysa2mcrl2. Furthermore a μCRL linear process can be converted to an mCRL2 LPS using tbf2lps. Finally, an interface with the TorX tool is provided by lps2torx.


Tool manual pages

Release tools

Integrated tool environment
mcrl2-gui A graphical front-end for mCRL2-tools.
mCRL2 tools
grapemcrl2 Graphical editing environment for mCRL2 process specifications.
mcrl2i Interpreter for the mCRL2 data language.
LPS tools
formulacheck Check a boolean formula.
lps2lts Generate an LTS from an LPS.
lpsactionrename Rename actions of an LPS.
lpsbinary Replace finite sort variables by vectors of boolean variables in an LPS.
lpsconfcheck Mark confluent tau-summands of an LPS.
lpsconstelm Remove constant parameters from an LPS.
lpsinfo Display basic information about an LPS.
lpsinvelm Check invariants and use these to simplify or eliminate summands of an LPS.
lpsparelm Remove unused parameters from an LPS.
lpsparunfold Unfold process parameters in an LPS.
lpspp Pretty print an LPS.
lpsrewr Rewrite data expressions in an LPS.
lpssim Command-line simulation of an LPS.
lpssumelm Remove superfluous summations from an LPS.
lpssuminst Instantiate summation variables of an LPS.
lpsuntime Remove time from an LPS.
lpsxsim Graphical simulation of an LPS.
mcrl22lps Translate an mCRL2 specification to an LPS.
txt2lps Parse a textual description of a linear process specification.
PBES tools
lps2pbes Generate a PBES from an LPS and a state formula.
pbes2bool Solve a (P)BES.
pbes2bes Instantiate a PBES into a BES.
pbesconstelm Remove constant parameters from a PBES.
pbesinfo Display basic information about a PBES.
pbesparelm Remove unused parameters from a PBES.
pbespgsolve Solve a (P)BES using a parity game solver.
pbespp Pretty print a PBES.
pbesrewr Rewrite and simplify a PBES.
txt2pbes Parse a textual description of a PBES.
BES tools
besinfo Provide information of a BES.
bespp Pretty print a BES.
pbes2bool Solve a (P)BES.
pbespgsolve Solve a (P)BES using a parity game solver.
LTS tools
diagraphica Interactive visual analysis of an LTS.
lts2lps Convert an LTS to an LPS.
ltscompare Compare two LTSs.
ltsconvert Convert and optionally minimise an LTS.
ltsgraph Visualise an LTS as a graph and manipulate its layout.
ltsinfo Display basic information about an LTS.
ltsview 3D interactive visualisation of an LTS.
tracepp Convert and pretty print traces.
Import/Export
chi2mcrl2 Convert a Chi specification to a matching mCRL2 process specification.
lps2torx Provide TorX explorer interface to an LPS.
lysa2mcrl2 Convert a Typed LySa specification to an mCRL2 process specification.
pnml2mcrl2 Convert a Petri net to an mCRL2 process specification (removed from release March 2011).
tbf2lps Convert a µCRL LPE to an mCRL2 LPS.

Experimental tools

besconvert Simplify a BES using equivalences.
bessolve Solve a BES.
lpsbisim2pbes Compute a bisimulation relation between two LPSs.
lpsrealelm Remove Real numbers from an LPS.
lts2pbes Generate a PBES from an LTS and a state formula.
pbesabsinthe A form of abstract interpretation for PBESs.
pbesabstract A form of abstract interpretation for PBESs.
pbesinst Compute a (P)BES out of a PBES.
pbespareqelm Compute equivalence relations on parameters of a PBES.
txt2bes Parse a textual description of a BES.

Deprecated tools

squadt Interactive integration of software tools, including the tools mentioned above.
ltsmin Minimise an LTS.


chi2mcrl2

Convert a Chi specification to a matching mCRL2 process specification.

Synopsis

chi2mcrl2 [OPTION]... [INFILE [OUTFILE]]

Short description

chi2mcrl2 translates a Chi specification to a matching mCRL2 specification. For all the supported Chi operators individual translations to mCRL2 summands (with their associated data parameters) are constructed.

Currently, only non-timed/non-hybrid Chi specifications can be translated. If a specification is timed, e.g. the Chi statement delay, the time progress is translated to a "skip". If hybrid statements are used, e.g. the Chi Statement cont , the translation will fail to translate.

Options

OPTION can be any of the following:

-n, --no-state
no state parameters are generated when translating Chi processes

Standard options:

-q, --quiet
do not display warnings
-v, --verbose
display concise intermediate messages
-d, --debug
display detailed intermediate messages
-h, --help
display help message
--version
display version information

Detailed description

Supported Language Features

Like mCRL2, Chi also has a variety of tools for different translation and simulation purposes. Due to this variety it is hard to keep track of all the supported language features. We give an overview of the supported language features by chi2mcrl2, similar to the Chi Tools page. Note that the presented link shows a "Chi to μCRL translation", which is the predecessor of mCRL2.

In the tables below, a “+” means that the feature is supported and a “-” means that the language is not supported.

Variable Classes

Each variable in a Chi program belongs to a variable class. Below are the supported variable classes for chi2mcrl2.

Variable Class chi2mcrl2
cont vardecl -
alg vardecl -
var vardecl +
alg parameter -
alg parameter -

with the following footnotes:

Constant definitions

Constant definitions are not supported by chi2mcrl2.

Imports

Imports are a general concept in Chi. Library files can be imported but also other Chi specifications or even libraries written in other languages are considered useful. However the import feature is not supported in chi2mcrl2.

Enumerations

Enumeration definitions are not supported by chi2mcrl2.

Functions

Enumeration definitions are not supported by chi2mcrl2.

Processes

The following language features are supported.

Feature chi2mcrl2
time in guards -
folding -
alternative composition +
parallel composition #1
process instantiation #1
recdef instantiation -
deadlock +
inconsistent -
delay predicate -
action predicate #2
any delay -
signal emission -
delay operator #3
jump enable -
local variable scope -
local channel scope -
local recdef scope -
recdef -
urgent communication -
encapsulation -
guard +

with the following footnotes:

Data types

In the table below are the supported data types for chi2mcrl2.

Data type chi2mcrl2
booleans +
naturals +
reals -
lists +
sets +
dictionaries -
vectors -
records +
distributions -
matrices -

Author

Written by Frank Stappers.

Reporting bugs

Report bugs at our issue tracking system.


diagraphica

Interactive visual analysis of an LTS.

Synopsis

diagraphica [OPTION]... [INFILE]

Short description

The diagraphica tool offers multivariate state visualization and simulation analysis techniques for labelled transition systems (LTS's) in the FSM format. If INFILE is present, it will be loaded by the tool.

In the analysis mode, the tool allows the user to cluster states based on selected attributes. The clusters are visualized in a hierarchical pyramid structure were transitions between clusters are shown by arcs. The simulation view gives the user the facility to navigate through the transition graph and shows the effect of actions on the configuration. The integrated edit mode allows the user to create such a configuration. A configuration consists of geometric shapes. Each of the different shapes have a number of geometric and non-geometric degree of freedoms that can be adjusted for simulation purposes.

Options

OPTION can be any of the following standard options:

-q, --quiet
do not display warning messages
-v, --verbose
display short intermediate messages
-d, --debug
display detailed intermediate messages
-h, --help
display help information
--version
display version information

See also

A more elaborate description can be found here and in <ref> Bridging the semantic gap: visualization of transition graphs with user-defined diagrams A.J. Pretorius and J.J. van Wijk IEEE Computer Graphics and Applications, vol. 27, no. 5, pp. 58-66, 2007. </ref>.

References

<references />

Author

Written by Hannes Pretorius.

Bug reporting

Report bugs at our issue tracking system.


formulacheck

Check a boolean formula.

Synopsis

formulacheck [OPTION]... [INFILE]

Short description

The formulacheck tool checks the boolean formula (an mCRL2 data expression of sort Bool) in INFILE. If INFILE is not present, stdin is used.

The tool indicates whether or not the formula is a tautology or a contradiction.

In some cases, the tool is unable to determine whether a formula is a tautology or a contradiction. The option --verbose gives insight into what the prover used by the tool is doing and can be used to see if rewrite rules have to be added to the specification in order to enable the prover to determine that certain formulas are indeed tautologies or contradictions.

A BDD based prover is used to the check the formula. In some cases it may be useful to use an SMT solver to assist the prover. The SMT solver can further reduce BDDs by removing inconsistent paths. A specific SMT solver can be chosen using the option --smt-solver=SOLVER. Either the SMT solver Ario or CVC3 can be used. To use one of these solvers, the directory containing the corresponding executable must be in the path.

Example of use

The input file typically contains a single expression such as 

 3+3<4

When formulacheck would be applied to this file it would respond with 

'3 + 3 < 4': Contradiction

If the input formula holds, the following output would be 

'#[4, 5, 6] > 2': Tautology

If the input contains an expression which cannot be rewritten to true or false the response is 

'[1, 4, 7]': Undeterminable

It is not possible to use formulacheck for open terms. For this the interactive tool mcrl2i is more convenient.

Options

OPTION can be any of the following:

-c, --counter-example
display a valuation for which the formula does not hold, in case the current formula is neither a contradiction nor a tautology
-o, --induction
apply induction on lists
-pPREFIX, --print-dot=PREFIX
save a .dot file of the resulting BDD if it is impossible to determine whether a formula is a contradiction or a tautology; PREFIX will be used as prefix of the output files
-rNAME, --rewrite-strategy=NAME
use rewrite strategy NAME
-sSPECFILE, --spec=SPECFILE
check the formula against the data types from the LPS or PBES in SPECFILE
-tLIMIT, --time-limit=LIMIT
spend at most LIMIT seconds on proving the formula
-w, --witness
display a valuation for which the formula holds, in case the current formula is neither a contradiction nor a tautology
-zSOLVER, --smt-solver=SOLVER
use SOLVER to remove inconsistent paths from the internally used BDDs:
  • 'ario': the SMT solver Ario
  • 'cvc': the SMT solver CVC3
by default, no path elimination is applied

Standard options:

-q, --quiet
do not display warning messages
-v, --verbose
display short intermediate messages
-d, --debug
display detailed intermediate messages
-h, --help
display help information
--version
display version information

Author

Written by Luc Engelen.

Bug reporting

Report bugs at our issue tracking system.


grapemcrl2

Graphical editing environment for mCRL2 process specifications.

Synopsis

grapemcrl2 [OPTION]... [INFILE]

Short description

The grapemcrl2 tool allows users to create mCRL2 process specifications by means of a graphical editing environment. If INFILE is present, the corresponding file is loaded as a GraPE specification.

Detailed help is provided in the online manual, accessible from within the tool.

Options

OPTION can be any of the following standard options:

-q, --quiet
do not display warning messages
-v, --verbose
display short intermediate messages
-d, --debug
display detailed intermediate messages
-h, --help
display help information
--version
display version information

Author

Written by Remco Blewanus, Thorstin Crijns, Diana Koenraadt, Bas Luksenburg, Jonathan Nelisse, Hans Poppelaars and Bram Schoenmakers.

Bug reporting

Report bugs at our issue tracking system.


lps2lts

Generate an LTS from an LPS.

Synopsis

lps2lts [OPTION]... [INFILE [OUTFILE]]

Short description

The lps2lts tool generates a labelled transition system (LTS) from the linear process specification (LPS) in INFILE and saves the result to OUTFILE. If OUTFILE is not supplied, the LTS is not stored. If INFILE is not supplied, stdin is used.

The format of OUTFILE is determined by its extension (unless it is specified by an option). The supported formats are:

If the jittyc rewriter is used, then the MCRL2_COMPILEREWRITER environment variable (default value: mcrl2compilerewriter) determines the script that compiles the rewriter, and MCRL2_COMPILEDIR (default value: '.') determines where temporary files are stored.

Note that lps2lts can deliver multiple transitions with the same label between any pair of states. If this is not desired, such transitions can be removed by applying a strong bisimulation reducton using for instance the tool ltsconvert.

Options

OPTION can be any of the following:

-aNAMES, --action=NAMES
Detect and report actions in the transition system that have action names from the list NAMES. This is for instance useful to find (or prove the absence) of an action error. The list NAMES is a comma separated list of action names. A message is printed for every occurrence of an action with action names in the list. With the -t flag traces towards these actions are generated.
-b[NUM], --bit-hash[=NUM]
Make use of bit hashing to store states and store at most NUM states. This means that instead of keeping a full record of all states that have been visited, a bit array is used that indicate whether or not a hash of a state has been seen before. Although this means that this option may cause states to be mistaken for others (because they are mapped to the same hash), it can be useful to explore very large LTSs that are otherwise not explorable. If NUM is not supplied, then approximately 200 million is taken (this corresponds to about 25MB of memory).
-c[NAME], --confluence[=NAME]
Apply on-the-fly confluence reduction where action NAME is considered to denote a confluent silent step. If NAME is not supplied, ctau is assumed to be the confluent silent step.
-D, --deadlock
Detect deadlocks (i.e. for every deadlock a message is printed). A deadlock is a state from which no transitions are possible.
-F, --divergence
Detect divergences. For every state with a divergence (=tau loop) a message is printed. The algorithm to detect the divergences is linear for every state, and so state space exploration becomes quadratic with this option on. State space exploration can become slow with this option.
--error-trace
If an error occurs during exploration, a trace to the state that could not be explored is saved to a trace file.
-fNAME, --state-format=NAME
Store state internally in format NAME:
  • vector: for a vector (fastest, default in older versions of the toolset)
  • tree: for a tree (for memory efficiency, default in toolset versions from autumn 2011)
--init_tsize=NUM
Set the initial size of the internally used hash tables. The default size is 10000.
-lNUM, --max=NUM
Explore at most NUM states. After exploring of NUM states lps2lts will stop, having generated a partial LTS.
--no-info
Do not add state information to OUTFILE. Without this option lps2lts adds state vector to the LTS. This option causes this information to be discarded and states are only indicated by a sequence number. Explicit state information is useful for visualisation purposes, for instance, but can cause the OUTFILE to grow considerably. Note that this option is implicit when writing in the AUT format.
-oFORMAT, --out=FORMAT
Use FORMAT as the output format.
-rNAME, --rewriter=NAME
Use rewrite strategy NAME. lps2lts uses a term rewriting engine to manipulate data terms of the LPS. The choice of the rewriter can have influence on the performance.
-sNAME, --strategy=NAME
Explore the state space using strategy NAME:
b, breadth
breadth-first search (default)
d, depth
depth-first search
r, random
random simulation
--suppress
in verbose mode, do not print progress messages indicating the number of visited states and transitions. For large state spaces the number of progress messages can be quite horrendous. This feature helps to suppress those. Other verbose messages, such as the total number of states explored, just remain visible.
-t[NUM], --trace[=NUM]
Write a shortest trace to each state that is reached with an action from NAMES from option --action or is a deadlock detected with --deadlock to a file. No more than NUM traces will be written. If NUM is not supplied the number of traces is unbounded.
For each trace that is to be written a unique file with extension .trc (trace) will be created containing a shortest trace from the initial state to the deadlock state. The traces can be pretty printed and converted to other formats using tracepp.
--todo-max=NUM
Keep at most NUM states in todo lists; this option is only relevant for breadth-first search with bithashing, where NUM is the maximum number of states per level, and for depth first, where NUM is the maximum depth.
-u, --unused-data
Do not remove unused parts of the data specification.
-yBOOL, --dummy=BOOL
Replace free variables in the LPS with dummy values based on the value of BOOL: yes (default) or no.

Standard options:

-q, --quiet
Do not display warning messages.
-v, --verbose
Display short intermediate messages. This includes detailed status of the generation process. Once a level (in terms of breadth-first search) is completed, a message stating this is printed. After exploration of every 1000 states the following information is printed: current level, states explored, transitions explored, states seen. A state is explored if all its outgoing transitions have been explored. A state is seen if (at least) one of the transitions leading to it has been explored.
-d, --debug
Display detailed intermediate messages.
-h, --help
Display help information.
--version
Display version information.

Author

Written by Muck van Weerdenburg.

Reporting bugs

Report bugs at our issue tracking system.


lps2pbes

Synopsis

lps2pbes[OPTION]... --formula=FILE [INFILE [OUTFILE]]

Short Description

Convert the state formula in FILE and the LPS in INFILE to a parameterised boolean equation system (PBES) and save it to OUTFILE. If OUTFILE is not present, stdout is used. If INFILE is not present, stdin is used.

The concrete syntax of state formulas can be found at <http://www.mcrl2.org/mcrl 2/wiki/index.php/Language_reference/mu-calculus_syntax>.

Options

OPTION can be any of the following:

-fFILE, --formula=FILE
use the state formula from FILE
-t, --timed
use the timed version of the algorithm, even for untimed LPS's
--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
-h, --help
display help information
--version
display version information

Author

Implemented by Wieger Wesselink, with contributions from Tim Willemse.

Reporting bugs

Report bugs at [1].


lps2torx

Provide TorX explorer interface to an LPS.

Synopsis

lps2torx [OPTION]... INFILE

Short description

The lps2torx tool provides a TorX explorer interface to the linear process equation (LPS) in INFILE.

The LPS can be explored using TorX as described in the TorX documentation.

Options

OPTION can be any of the following:

-fNAME, --state-format=NAME
store state internally in format NAME:
  • vector: for a vector (fastest, default)
  • tree: for a tree (for memory efficiency)
-rNAME, --rewriter=NAME
use rewrite strategy NAME
-u, --unused-data
do not remove unused parts of the data specification
-yBOOL, --dummy=BOOL
replace free variables in the LPS with dummy values based on the value of BOOL: yes (default) or no

Standard options:

-q, --quiet
do not display warning messages
-v, --verbose
display short intermediate messages
-d, --debug
display detailed intermediate messages
-h, --help
display help information
--version
display version information

Author

Written by Muck van Weerdenburg.

Bug reporting

Report bugs at our issue tracking system.


lpsactionrename

Rename actions of an LPS.

Synopsis

lpsactionrename [OPTION]... --file=RENAMEFILE [INFILE[OUTFILE]]

Short description

The lpsactionrename tool renames the actions that occur in the INFILE and saves the result to the OUTFILE. If no OUTFILE is specified stdout is used. If no INFILE is specified stdin is used. The rename rules are defined in the RENAMEFILE that is given as a mandatory argument.

Options

OPTION can be any of the following:

-fRENAMEFILE, --renamefile=RENAMEFILE
use the rename rules from RENAMEFILE; this argument is mandatory
-m, --no-sumelim
do not apply sum elimination to the final result
-o, --no-rewrite
do not rewrite data terms while renaming; useful when the rewrite system does not terminate
-pPHASE, --end-phase=PHASE
stop conversion and output the action rename specification after phase PHASE: 'pa' (parsing), 'tc' (type checking), or 'di' (data implementation)
-P, --pretty
return a pretty printed version of the output
-rNAME, --rewriter=NAME
use rewrite strategy NAME

Standard options:

-q, --quiet
do not display warning messages
-v, --verbose
display short intermediate messages
-d, --debug
display detailed intermediate messages
-h, --help
display help information
--version
display version information

Detailed description

Structure of rename files

The format of the RENAMEFILE can contain sort cons map eqn act sections as in a mcrl2 file. This is followed by a rename section to define the rename rules. The sections sort cons map eqn act are meant for new declarations that will be added to the LPS and can be used in the rename rules. The new declarations are not allowed to contain any conflicts with the declarations of the LPS. The rename section can be preceded by a var section, where variables can be declared for the rename rules.

The rename rules have the format: rename condition -> action1 => action2; where condition is a boolean expression that has to hold to rename an occurrence of action1 into action2. The condition can be left out, in which case all occurrences of action1 will be renamed. The actions action1 can contain arguments that can either be uniquely occurring variables or closed terms. The arguments of action2 can be arbitrary terms, but the variables occurring in it must also occur in action1. The condition is an expression of type "Bool" and likewise can only occur variables that also occur in "action1".

Besides an action, action2 can also be tau or delta. In case of tau then if action1 is a multi action then it will be removed and otherwise be replaced with tau. In case of delta, the action and the following process call are replaced by delta.

The renaming rules are applied from top to bottom to an linear process equation. If no value for the variables in a rename rule can be found to match an action, the next rule is applied. If no rule applies the action is left untouched. Variables in different rename rules with the same variable names are independent when being matched.

After the lps has been renamed, sum elimination and rewriting will be applied to simplify the result. This can be skipped using appropriate switches.

Rename rule conditions

Upon loading the rename file, lpsactionrename will check if the following conditions hold:

Example

Consider an LPS with the process specification: 

P(x:Bool) = sum y:Nat. (y < 6) -> a(x,y). P(!x);

and a rename file with the following rename rules: 

act b: Bool;
var v: Nat; w:Bool;
rename 
  w -> a(w,v) => b(v==5);
  (v==v*2)==w -> a(w,v) => tau;
  a(w,5) => delta;

The arguments of an action do not have to consist of a single variable, as is done in the second rename rule. In the second rename rule a(w,2*v), w and 2*v will be respectively equal to x and y from the LPS action a(x,y).

The result of applying the rename rules to the LPS without sum elimination will give: 

proc P(x_P0: Bool) =
       true ->
         delta
     + sum w: Bool,v,y_P0: Nat.
         ((y_P0 < 6 && w==x_P0 && v==y_P0) && w) -> b(v==5).P(!x_P0);
     + sum w00: Bool,v00: Nat,w: Bool,v,y_P0: Nat.
         ((((y_P0 < 6 && w==x_P0 && v==y_P0) && !w) && w00==x_P0 && v00==y_P0) && 
                   (v00==v00*2)==w00) -> tau.P(!x_P0)
     + sum w01,w00: Bool,v00: Nat,w: Bool,v,y_P0: Nat.
         ((((((y_P0 < 6 && w==x_P0 && v==y_P0) && !w) && w00==x_P0 && v00==y_P0) && 
                   !((v00==v00*2)==w00)) && w01==x_P0) && 5==y_P0) -> delta
     + sum w01,w00: Bool,v00: Nat,w: Bool,v,y_P0: Nat.
         ((((((y_P0 < 6 && w==x_P0 && v==y_P0) && !w) && w00==x_P0 && v00==y_P0) && 
                   !((v00==v00*2)==w00)) && w01==x_P0) && !(5==y_P0)) -> a(x_P0, y_P0).P(!x_P0)

Most of the introduced sum variables have a single point domain, namely: u, w, w_S00, w_s01, v_S00 and in the last two summands y. These variables can be eliminated by applying sum elimination. For example: in the first summand w is equal to x. Therefore w can be substituted by x. And w can be removed from the sum since it is no longer used.

Applying sum elimination will give the following result: 

proc P(x_P0: Bool) =
     true -> delta
     + sum y_P0: Nat.(y_P0 < 6 && x_P0) ->b(y_P0 == 5) .P(!x_P0);
     + sum y_P0: Nat.(y_P0 < 6 && !(y_P0 == y_P0 * 2)) ->tau.P(!(y_P0 == y_P0 * 2))
     + (!x_P0 && x_P0) ->delta
     + sum y_P0: Nat.(((y_P0 < 6 && !x_P0) && !((y_P0 == y_P0 * 2) == x_P0)) &&
                   !(5 == y_P0)) -> a(x_P0, y_P0) .P(!x_P0)

Authors

Written by Jan Friso Groote and Tom Haenen.

Bug reporting

Report bugs at our issue tracking system.


lpsbinary

Replace finite sort variables by vectors of boolean variables in an LPS.

Synopsis

lpsbinary [OPTION]... [INFILE [OUTFILE]]

Short description

The lpsbinary tool replaces finite sort variables by vectors of boolean variables in the linear process specification (LPS) INFILE and write the result to OUTFILE. If INFILE is not present, stdin is used. if OUTFILE is not present, stdout is used.

Options

OPTION can be any of the following:

-rNAME, --rewriter=NAME
use rewrite strategy NAME

Standard options:

-q, --quiet
do not display warning messages
-v, --verbose
displays short intermediate messages
-d, --debug
displays detailed intermediate messages
-h, --help
display help information
--version
display version information

Author

Written by Jeroen Keiren.

Bug reporting

Report bugs at our issue tracking system.


lpsbisim2pbes

Synopsis

lpsbisim2pbes[OPTION]... INFILE1 INFILE2 [OUTFILE]

Short Description

Reads two files containing an LPS, and computes a PBES that expresses bisimulation between the two. If OUTFILE is not present, standard output is used.

Options

OPTION can be any of the following:

-bNAME, --bisimulation=NAME
generate a PBES for the bisimulation type NAME:

'strong-bisim' for strong bisimilarity, 'weak-bisim' for weak bisimilarity,' 'branching-bisim' for branching bisimilarity, 'branching-sim' for branching simulation equivalence

-n, --normalize
normalize the result

Standard options:

-q, --quiet
do not display warning messages
-v, --verbose
display short intermediate messages
-d, --debug
display detailed intermediate messages
-h, --help
display help information
--version
display version information

Author

Implemented by Wieger Wesselink, with contributions from Tim Willemse and Bas Ploeger.

Reporting bugs

Report bugs at [2].


lpsconfcheck

Mark confluent tau-summands of an LPS.

Synopsis

lpsconfcheck [OPTION]... [INFILE [OUTFILE]]

Short description

The lpsconfcheck tool checks which tau-summands of the linear process specification (LPS) in INFILE are confluent and marks them by renaming their tau-actions to ctau. The resulting LPS is written to OUTFILE. If INFILE is not present, stdin is used. If OUTFILE is not present, stdout is used.

Options

OPTION can be any of the following:

-a, --check-all
check confluence of the tau-summands regarding all other summands, instead of continuing with the next tau-summand as soon as a summand is encountered that is not confluent with the current tau-summand
-c, --counter-example
display a valuation for which the confluence condition does not hold, in case the encountered condition is neither a contradiction nor a tautology
-g, --generate-invariants
try to prove that the reduced confluence condition is an invariant of the LPS, in case the confluence condition is not a tautology
-iINVFILE, --invariant=INVFILE
use the boolean formula (an mCRL2 data expression of sort Bool) in INVFILE as invariant
-m, --no-marking
do not mark the confluent tau-summands; since there are no changes made to the LPS, nothing is written to OUTFILE
-n, --no-check
do not check if the invariant holds before checking for confluence
-o, --induction
apply induction on lists
-pPREFIX, --print-dot=PREFIX
save a .dot file of the resulting BDD in case two summands cannot be proven confluent; PREFIX will be used as prefix of the output files
-rNAME, --rewrite-strategy=NAME
use rewrite strategy NAME
-sNUM, --summand=NUM
check the summand with number NUM only
-tLIMIT, --time-limit=LIMIT
spend at most LIMIT seconds on proving a single formula
-zSOLVER, --smt-solver=SOLVER
use SOLVER to remove inconsistent paths from BDDs:
  • 'ario' for the SMT solver Ario
  • 'cvc' for the SMT solver CVC3
by default, no path elimination is applied

Standard options:

-q, --quiet
do not display warning messages
-v, --verbose
display short intermediate messages
-d, --debug
display detailed intermediate messages
-h, --help
display help information
--version
display version information

Detailed description

Given an LPS:

\begin{array}{lll} P(d:D) &=& \ldots + \sum_{e_i:E_i} c_i(d,e_i) \to a_i(f_i(d,e_i)) \cdot P(g_i(d,e_i)) +\\ && \ldots + \sum_{e_j:E_j} c_j(d,e_j) \to \tau \cdot P(g_j(d,e_j)) + \ldots \end{array}

tau-summand j is confluent with summand i if the following condition holds:

\begin{array}{l} \forall d{:}D.\forall e_i{:}E_i. \forall e_j{:}E_j . (inv(d) \land c_i(d,e_i) \land c_j(d,e_j)) \Rightarrow\\ (c_i(g_j(d,e_j),e_i) \land c_j(g_i(d,e_i),e_j) \land\\ f_i(d,e_i) = f_i(g_j(d,e_j),e_i) \land g_i(g_j(d,e_j),e_i) = g_j(g_i(d,e_i),e_j)) \end{array}

where inv() is the invariant specified using the option --invariant. In case ai is also a tau-action, this formula can be weakened to the following:

\begin{array}{l} \forall d{:}D. \forall e_i{:}E_i. \forall e_j{:}E_j . (inv(d) \land c_i(d,e_i) \land c_j(d,e_j)) \Rightarrow\\ (g_i(d,e_i) = g_j(d,e_j) \lor (c_i(g_j(d,e_j),e_i) \land c_j(g_i(d, e_i),e_j) \land\\ g_i(g_j(d,e_j),e_i) = g_j(g_i(d,e_i),e_j))) \end{array}

If the option --invariant is not used, the invariant is equal to true.

The tool will generate these confluence conditions for all tau-summands and tries to prove that they are tautologies using a BDD based prover for propositional formulas. In some cases lpsconfcheck indicates that a tau-summand is not confluent even though it is. The option --verbose gives insight into what the prover is doing and can be used to see if rewrite rules have to be added to the specification in order to enable the prover to determine that certain condition are indeed tautologies.

In some cases it may be useful to use an SMT solver to assist the prover. The SMT solver can further reduce BDDs by removing inconsistent paths. A specific SMT solver can be chosen using the option --smt-solver=SOLVER. Either the SMT solver Ario or CVC3 can be used. To use one of these solvers, the directory containing the corresponding executable must be in the path.

The tool can determine whether two summands are confluent in three ways and will indicate which of the methods was used while proving confluence. The three ways of determining confluence are as follows:

If two summands are confluent because of syntactic disjointness, lpsconfcheck indicates this by printing a colon (':').

If there already is an action named ctau present in the LPS as found in INFILE, an error will be reported.

Author

Written by Luc Engelen.

Bug reporting

Report bugs at our issue tracking system.


lpsconstelm

Synopsis

lpsconstelm[OPTION]... [INFILE [OUTFILE]]

Short Description

Remove constant process parameters from the LPS in INFILE and write the result to OUTFILE. If INFILE is not present, standard input is used. If OUTFILE is not present, standard output is used.


If it can be determined that certain parameters of this LPS remain constant throughout any run of the process, all occurrences of these process parameter are replaced by the initial value and the process parameters are removed from the LPS.

If the initial value of a process parameter is a global variable and remains a global variable throughout the run of the process, the process variable is considered constant.

If the initial value of a process parameter is a global variable and is only changed once to a certain value, the process parameter is constant and the specific value is used for substitution.

Options

OPTION can be any of the following:

-c, --ignore-conditions
ignore conditions by assuming they evaluate to true
-f, --instantiate-free-variables
allow free variables to be instantiated as a side effect of the algorithm

NOTE: this functionality is untested!

-s, --remove-singleton-sorts
remove parameters with single element sorts
-t, --remove-trivial-summands
remove summands with condition false
-rNAME, --rewriter=NAME
use rewrite strategy NAME: 
 'jitty' for jitty rewriting (default),
 'jittyp' for jitty rewriting with prover,
 'jittyc' for compiled jitty rewriting,
 'inner' for innermost rewriting,
 'innerp' for innermost rewriting with prover, or
 'innerc' for compiled innermost rewriting
--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
-h, --help
display help information
--version
display version information

Author

Implemented by Wieger Wesselink, with contributions from Frank Stappers.

Reporting bugs

Report bugs at [3].


lpsinfo

Synopsis

lpsinfo[OPTION]... [INFILE]

Short Description

Print basic information on the linear process specification (LPS) in INFILE.


By default, the following information about the LPS is shown:

Options

OPTION can be any of the following:

--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
-h, --help
display help information
--version
display version information

Author

Implemented by Wieger Wesselink and Frank Stappers.

Reporting bugs

Report bugs at [4].


lpsinvelm

Check invariants and use these to simplify or eliminate summands of an LPS.

Synopsis

lpsinvelm [OPTION]... --invariant=INVFILE [INFILE [OUTFILE]]

Short description

The lpsinvelm tool checks whether the boolean formula (an mCRL2 data expression of sort Bool) in INVFILE is an invariant of the linear process specification (LPS) in INFILE. If this is the case, the tool eliminates all summands of the LPS whose condition violates the invariant, and writes the result LPS to OUTFILE. If INFILE is not present, stdin is used. If OUTFILE is not present, stdout is used.

The tool can also be used to simplify the conditions of the summands of the given LPS.


Options

OPTION can be any of the following:

-c, --counter-example
display a valuation indicating why the invariant could possibly be violated if it is uncertain whether a summand violates the invariant
-e, --no-elimination
do not eliminate or simplify summands
-iINVFILE, --invariant=INVFILE
use the boolean formula (an mCRL2 data expression of sort Bool) in INVFILE as invariant
-l, --simplify-all
simplify the conditions of all summands, instead of just eliminating the summands whose conditions in conjunction with the invariant are contradictions
-n, --no-check
do not check if the invariant holds before eliminating unreachable summands
-o, --induction
apply induction on lists
-pPREFIX, --print-dot=PREFIX
save a .dot file of the resulting BDD if it is impossible to determine whether a summand violates the invariant; PREFIX will be used as prefix of the output files
-rNAME, --rewrite-strategy=NAME
use rewrite strategy NAME
-sNUM, --summand=NUM
eliminate or simplify the summand with number NUM only
-tLIMIT, --time-limit=LIMIT
spend at most the LIMIT seconds on proving a single expression
-y, --all-violations
do not terminate as soon as a violation of the invariant is found, but report all violations instead
-zSOLVER, --smt-solver=SOLVER
use the SOLVER to remove inconsistent paths from BDDs:
  • 'cvc' for the SMT solver CVC3
by default, no path elimination is applied

Standard options:

-q, --quiet
do not display warning messages
-v, --verbose
display short intermediate messages
-d, --debug
display detailed intermediate messages
-h, --help
display help information
--version
display version information

Example of use

Consider a linear process specification 

act a:Nat; b,c;
act a, b, c;
proc X(b1,b2:Bool) = b1 -> a.X(!b1,b2)
                   + b2 ->b.X(true,b2 && b1)
                   + (b1 && b2)->c.X(false,false);
init X(false,true);

If the lineariser is applied to this process using mcrl22lps -D infile.mcrl2 outfile.lps, the resulting lps looks like 

act  c,b,a;
 
proc P(b1_X,b2_X: Bool) =
       b1_X ->
         a .
         P(b1_X = !b1_X)
     + b2_X ->
         b .
         P(b1_X = true, b2_X = b2_X && b1_X)
     + (b1_X && b2_X) ->
         c .
         P(b1_X = false, b2_X = false)
     + delta;
 
init P(false, true);

Inspection of this linear process shows that b1_X and b2_X cannot both be true at the same time. So, we can define this in a file invariant.inv. This linear process specification has as an invariant that 

!(b1_X && b2_X)

See below for a detailed definition of an invariant.

Using lpsinvelm -v -iinvariant.inv outfile.lps outfile1.lps it is possible to check the invariant. Moreover, by default the summand with conditions that in conjunction with the invariant are false are removed. In the example above, the summand with action c is removed. Using the -l flag, the invariant is put into conjunction with the condition of each summand, and the resulting condition is simplified using the eq-BDD prover. So, applying lpsinvelm -v -l -iinvariant.inv outfile.lps outfile1.lps yields the following: 

act  c,b,a;
 
proc P(b1_X,b2_X: Bool) =
       if(b1_X, if(b2_X, false, true), false) ->
         a .
         P(b1_X = !b1_X)
     + if(b1_X, false, if(b2_X, true, false)) ->
         b .
         P(b1_X = true, b2_X = b2_X && b1_X)
     + if(b1_X, if(b2_X, false, true), true) ->
         delta;
 
init P(false, true);

Note that the conditions now have an if-then-else structure, due to the eq-BDD prover. Also note that the summand with action c has been removed.

Sometimes, this result is unreadable or the simplifications of the conditions in conjunction with the invariant is extremely time consuming. This is for instance the case if many non-boolean data types are used. In such a case the application of the tool lpsbinary can be helpful, by replacing finite data domains by boolean data domains. Using the -e flag it is possible to add the invariants to the summands, without simplifying the summands. So, by applying lpsinvelm -v -e -iinvariant.inv outfile.lps outfile1.lps the result becomes 

act  c,b,a;
 
proc P(b1_X,b2_X: Bool) =
       (!(b1_X && b2_X) && b1_X) ->
         a .
         P(b1_X = !b1_X)
     + (!(b1_X && b2_X) && b2_X) ->
         b .
         P(b1_X = true, b2_X = b2_X && b1_X)
     + (!(b1_X && b2_X) && b1_X && b2_X) ->
         c .
         P(b1_X = false, b2_X = false)
     + !(b1_X && b2_X) ->
         delta;
 
init P(false, true);

Note that the c summand is now still present.

The usage of lpsinvelm can be useful as a preprocessing step for symbolic reduction tools. For instance lpsconfcheck or lpsrealelm.

When an invariant is being checked, but turns out to be false, then counterexamples are very helpful (use the -c flag. Counterexamples can also be presented in dot format.

When the data types that are used in a process are complex, the prover is not able to prove that the invariant is actually an invariant. This for instance happens when inequalities are used. In such a case, the flag -n can be used to skip the check that the invariant indeed satisfies the invariant properties.

Detailed description

Given an LPS:

P(d:D) = \ldots + \sum_{e_i:E_i} c_i(d,e_i) \to a_i(f_i(d,e_i)) \cdot P(g_i(d,e_i)) + \ldots

a formula of the form

inv(d) \land c_i(d,e_i) \Rightarrow inv(g_i(d,e_i))

is generated for each of the summands, where inv() is the expression passed using the option --invariant. This expression is an invariant of the LPS if it holds in the initial state and all the generated formulas are tautologies.

The invariant is used to eliminate summands as follows. A formula of the form

inv(d) \land c_i(d,e_i)

is generated for each of the summands or for the summand indicated using the option --summand only. The tool uses a BDD based prover for expressions of sort Bool to see if the generated formula is a contradiction. If the formula is a contradiction for some summand, this summand will be eliminated from the LPS. If the formula is not a contradiction, the summand remains unchanged unless the option --simplify-all is used.

The option --simplify-all will replace the conditions of all summands by the equivalent BDD of the condition in conjunction with the invariant passed using the option --invariant. This may enable other tools, like for instance lpsconstelm or lpsparelm, to simplify the LPS even further.

In some cases it may be useful to use an SMT solver to assist the prover. The SMT solver can further reduce BDDs by removing inconsistent paths. A specific SMT solver can be chosen using the option --smt-solver=SOLVER. Either the SMT solver Ario or CVC3 can be used. To use one of these solvers, the directory containing the corresponding executable must be in the path.

Without using the option --no-check, lpsinvelm will first check if the given expression is an invariant of the LPS. If this is not the case, no elimination or simplification will be done. In some cases the invariant may hold even though the prover is unable to determine this fact. In cases where an expression is an invariant of the LPS, but the prover is unable to determine this, the option --no-check can be used to eliminate or simplify summands anyway. Note that this also makes it possible to eliminate or simplify summands using an expression that is not an invariant of the LPS.

The option --verbose gives insight into what the prover is doing and can be used to see if rewrite rules have to be added to the specification, in order to enable the prover to determine the invariance of an expression.

Author

Written by Luc Engelen.

Bug reporting

Report bugs at our issue tracking system.


lpsparelm

Synopsis

lpsparelm[OPTION]... [INFILE [OUTFILE]]

Short Description

Remove unused parameters from the linear process specification (LPS) in INFILE and write the result to OUTFILE. If INFILE is not present, stdin is used. If OUTFILE is not present, stdout is used.

Options

OPTION can be any of the following:

--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
-h, --help
display help information
--version
display version information

Author

Implemented by Wieger Wesselink and Jeroen van der Wulp, with contributions from Frank Stappers and Tim Willemse.

Reporting bugs

Report bugs at [5].


lpsparunfold

Unfold process parameters in an LPS.

Synopsis

lpsparunfold [OPTION]... --index=NUM [INFILE [OUTFILE]]

Short description

The algorithm applies a transformation on data expressions of an linear process specification (LPS), by which other tools (such as lpsparelm, lpsconstelm) can apply their transformations more effectively. In concrete, this tool unfolds a sort with associated constructor functions to a set of process parameters in the LPS, in such a way that all behaviour is preserved. The LPS is specified by INFILE and writes the result to OUTFILE. If OUTFILE is not present stdout is used. If INFILE is not present stdin is used.

Options

OPTION can be any of the following:

-iNUM, --index=NUM
unfolds process parameter at given index NUM

Standard options:

-rNAME, --rewriter=NAME
Use rewrite strategy NAME. lps2parunfold uses a term rewriting engine to manipulate data terms of the LPS. The choice of the rewriter can have influence on the performance.
-q, --quiet
do not display warning messages
-v, --verbose
display short intermediate messages
-d, --debug
display detailed intermediate messages
-h, --help
display help information
--version
display version information

Author

Written by Frank Stappers.

Bug reporting

Report bugs at our issue tracking system.


lpspp

Pretty print an LPS.

Synopsis

lpspp [OPTION]... [INFILE [OUTFILE]]

Short description

The lpspp tool prints the linear process specification (LPS) from INFILE to OUTFILE in a human readable format. If OUTFILE is not present, stdout is used. If INFILE is not present, stdin is used.

Options

OPTION can be any of the following:

-fFORMAT, --format=FORMAT
print the LPS in the specified FORMAT:
  • default: for an mCRL2 specification (default)
  • debug: like default, with the following exceptions:
    • data expressions are printed in prefix notation using identifiers from the internal format
    • each data equation is put in a separate data equation section
    • next states of process references are printed in assignment notation
  • internal: for a textual ATerm representation of the internal format
  • internal-debug: like internal, with an indented layout

Standard options:

-q, --quiet
do not display warning messages
-v, --verbose
display short intermediate messages
-d, --debug
display detailed intermediate messages
-h, --help
display help information
--version
display version information

Author

Written by Aad Mathijssen.

Bug reporting

Report bugs at our issue tracking system.


lpsrealelm

Synopsis

lpsrewr[OPTION]... [INFILE [OUTFILE]]

Short Description

Rewrite data expressions of the LPS in INFILE and save the result to OUTFILE.If OUTFILE is not present, standard output is used. If INFILE is not present,standard input is used


The following data expressions are rewritten:

Rewriting LPS summands and the initial state is done to simplify these parts of the LPS. Rewriting data equations is done to speed up state space generation. In most cases, this results in a performance gain of at most 5%.

Options

OPTION can be any of the following:

-rNAME, --rewriter=NAME
use rewrite strategy NAME: 
 'jitty' for jitty rewriting (default),
 'jittyp' for jitty rewriting with prover,
 'jittyc' for compiled jitty rewriting,
 'inner' for innermost rewriting,
 'innerp' for innermost rewriting with prover, or
 'innerc' for compiled innermost rewriting
--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
-h, --help
display help information
--version
display version information

Author

Implemented by Wieger Wesselink and Muck van Weerdenburg.

Reporting bugs

Report bugs at [6].


lpsrewr

Synopsis

lpsrewr[OPTION]... [INFILE [OUTFILE]]

Short Description

Rewrite data expressions of the LPS in INFILE and save the result to OUTFILE.If OUTFILE is not present, standard output is used. If INFILE is not present,standard input is used


The following data expressions are rewritten:

Rewriting LPS summands and the initial state is done to simplify these parts of the LPS. Rewriting data equations is done to speed up state space generation. In most cases, this results in a performance gain of at most 5%.

Options

OPTION can be any of the following:

-rNAME, --rewriter=NAME
use rewrite strategy NAME: 
 'jitty' for jitty rewriting (default),
 'jittyp' for jitty rewriting with prover,
 'jittyc' for compiled jitty rewriting,
 'inner' for innermost rewriting,
 'innerp' for innermost rewriting with prover, or
 'innerc' for compiled innermost rewriting
--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
-h, --help
display help information
--version
display version information

Author

Implemented by Wieger Wesselink and Muck van Weerdenburg.

Reporting bugs

Report bugs at [7].


lpssim

Command-line simulation of an LPS.

Synopsis

lpssim [OPTION]... INFILE

Short description

The lpssim tool simulates the linear process specification (LPS) in INFILE using a command-line interface.

In the first screen, lpssim shows the state vector of the initial state and a list of all possible transitions that can be taken from this state. These transitions are numbered from 0 onwards. For each transition, the state vector of the state that is reached after taking that transition, is shown. When a transition has been taken, lpssim shows the action label of that transition, the state vector of the current state and (again) a list of numbered transitions that can be taken from the current state along with the state vector of the resulting state, respectively.

On the lpssim command-line - which starts with a question mark '?' - the following commands can be entered:

n
Execute the action with number n from the list of actions that are possible in the current state.
u, undo
Go to previous state in the trace.
r, redo
Go to next state in the trace.
i, initial
Go to initial state. Note that this preserves the trace; it is equivalent to goto 0.
g n, goto n
Go to position n of the trace.
t, trace
Print the current trace. The current position in the trace is indicated with >.
l filename, load filename
Load a trace from filename.
s filename, save filename
Save the current trace to filename.
h, help
Display a help message explaining the available commands.
q, quit, Ctrl-D
Quit lpssim.

Options

OPTION can be any of the following:

-rNAME, --rewriter=NAME
use rewrite strategy NAME
-y, --dummy
replace free variables in the LPS with dummy values

Standard options:

-q, --quiet
do not display warning messages
-v, --verbose
display short intermediate messages
-d, --debug
display detailed intermediate messages
-h, --help
display help information
--version
display version information

See also

For a simulator that uses a graphical user interface, see the lpsxsim tool.

Author

Written by Muck van Weerdenburg.

Bug reporting

Report bugs at our issue tracking system.


lpssumelm

Remove superfluous summations from an LPS.

Synopsis

lpssumelm [OPTION]... [INFILE [OUTFILE]]

Short description

The lpssumelm tool removes superfluous summations from the linear process specification (LPS) in INFILE and write the result to OUTFILE. If INFILE is not present, stdin is used. If OUTFILE is not present, stdout is used.

The simplest case this tool handles is that, whenever a summation variable does not occur in the other terms of the summand, this summation variable is plainly removed. There is however also a more complex situation where the summation variable occurs in an equality within the condition. There is an axiom that says that we may then substitute the other term of the equality for the summation variable. We can then remove both the summation variable and the condition in which it occurred.

Options

OPTION can be any of the following standard options:

-q, --quiet
do not display warning messages
-v, --verbose
display short intermediate messages
-d, --debug
display detailed intermediate messages
-h, --help
display help information
--version
display version information

Known issues

Lpssumelm is not applicable if types in an equality in a condition do not match directly, i.e. an implicit type cast is used in order to match the types. An example of this is the following process: 

proc P(i : Int) = sum n : Nat . (n == i) -> tau . P(i);
 
init P(5);

In this example an implicit cast Nat2Int (i.e. Nat2Int(n) == i) is used in order to have compatible types. Because of this, the tool is unable to remove the summation over n.

Author

Written by Jeroen Keiren.

Bug reporting

Report bugs at our issue tracking system.


lpssuminst

Instantiate summation variables of an LPS.

Synopsis

lpssuminst [OPTION]... [INFILE [OUTFILE]]

Short description

The lpssuminst tool instantiates summation variables of the linear process specification (LPS) in INFILE and writes the result to OUTFILE. If INFILE is not present, stdin is used. If OUTFILE, stdout is used.

Options

OPTION can be any of the following:

-f, --finite
only instantiate variables whose sorts are finite
-rNAME, --rewriter=NAME
use rewrite strategy NAME
-t, --tau
only instantiate variables in tau summands

Standard options:

-q, --quiet
do not display warning messages
-v, --verbose
display short intermediate messages
-d, --debug
display detailed intermediate messages
-h, --help
display help information
--version
display version information

Detailed description

Summation variables are instantiated by applying induction on the values of the sort of the variable. Take for example the following LPS: 

sort D = struct d1 | d2;
     E = struct e1(D) | e2;
 
act  a: D;
     b: E;
 
proc P = sum d: D. a(d) . P
       + sum e: E. b(e) . P
       ;
 
init P;

lpssuminst instantiates the variable 'd' to the constructors 'd1' and 'd2' of sort 'D', and variable 'e' to the constructors 'e1(d1)', 'e1(d2)' and 'e2': 

sort D = struct d1 | d2;
     E = struct e1(D) | e2;
 
act  a: D;
     b: E;
 
proc P = a(d1) . P
       + a(d2) . P
       + b(e1(d1)) . P
       + b(e1(d2)) . P
       + b(e2) . P
       ;
 
init P;

Author

Written by Jeroen Keiren.

Bug reporting

Report bugs at our issue tracking system.


lpsuntime

Remove time from an LPS.

Synopsis

lpsuntime [OPTION]... [INFILE [OUTFILE]]

Short description

The lpsuntime tool removes time from the linear process specification (LPS) in INFILE and writes the result to OUTFILE. IF INFILE is not present, stdin is used. If OUTFILE is not present, stdout is used.

The process equation section of an LPS is of the following form: 

proc P(d: D) = sum e_0: E_0. c_0(d,e_0) -> a_0(f_0(d,e_0)) @ t_0(d,e_0) . P(g_0(d,e_0))
             + sum e_1: E_1. c_1(d,e_1) -> a_1(f_1(d,e_1)) @ t_1(d,e_1) . P(g_1(d,e_1))
             + ...
             ;

The tool transforms this to the following equivalent untimed version: 

proc P(d: D, t: Real) = sum e_0: E_0. (c_0(d,e_0) && t_0(d,e_0)) -> a_0(f_0(d,e_0)) . P(g_0(d,e_0),t_0(d,e_0))
                      + sum e_1: E_1. (c_1(d,e_1) && t_1(d,e_1)) -> a_1(f_1(d,e_1)) . P(g_1(d,e_1),t_1(d,e_1))
                      + ...
                      ;

Options

OPTION can be any of the following standard options:

-q, --quiet
do not display warning messages
-v, --verbose
display short intermediate messages
-d, --debug
display detailed intermediate messages
-h, --help
display help information
--version
display version information

Author

Written by Jeroen Keiren.

Bug reporting

Report bugs at our issue tracking system.


lpsxsim

Graphical simulation of an LPS.

Synopsis

lpsxsim [OPTION]... [INFILE]

Short description

The lpsxsim tool simulates the linear process specification (LPS) in INFILE using a graphical user interface. If INFILE is not supplied the simulator starts without an LPS. The interface consists of two parts. In the top part every transition that is possible from the current state, is listed including the changes to the state vector that would result from executing that transition. A transition can be executed by double clicking it. In the bottom part, the state vector of the current state is shown.

Apart from basic simulation, lpsxsim provides the following additional functionalities:

Options

OPTION can be any of the following:

-rNAME, --rewriter=NAME
use rewrite strategy NAME
-y, --dummy
replace free variables in the LPS with dummy values

Standard options:

-q, --quiet
do not display warning messages
-v, --verbose
display short intermediate messages
-d, --debug
display detailed intermediate messages
-h, --help
display help information
--version
display version information

See also

For a simulator that uses a command-line interface, see the lpssim tool.

Authors

Written by Muck van Weerdenburg and Jeroen van der Wulp.

Bug reporting

Report bugs at our issue tracking system.


lts2lps

Synopsis

lts2lps[OPTION] [INFILE [OUTFILE]]

Short Description

Translates an LTS in INFILE and writes the resulting LPS to OUTFILE. If OUTFILE is not present, standard output is used. If INFILE is not present, standard input is used. This tool is useful when an labelled transition system in .aut, .svc, .fsm or .lts must be processed. Such processing tools are generally only available on linear processes. By transforming the transition system to a linear process, such processing can be performed. For processing one can typically think on model checking a process, or applying lpsactionrename to the process.

Note that if the labelled transition system does not provide information on the data types and has no action declarations, these must be provided separately. Only the .lts format contains such information. There are several ways to provide this extra required info.

Options

OPTION can be any of the following:

-DFILE, --data=FILE
use FILE as the data and action specification. FILE must be a .mcrl2 file which does not contain an init clause.
-lFILE, --lps=FILE
use FILE for the data and action specification. FILE must be a .lps file.
-mFILE, --mcrl2=FILE
use FILE as the data and action specification for the LTS. FILE must be a .mcrl2 file.

Standard options:

-q, --quiet
do not display warning messages
-v, --verbose
display short intermediate messages
-d, --debug
display detailed intermediate messages
-h, --help
display help information
--version
display version information

Author

Written by Frank Stappers; extended by Jan Friso Groote.

Reporting bugs

Report bugs at [8].


ltscompare

Compare two LTSs.

Synopsis

ltscompare [OPTION]... [INFILE1] INFILE2

Short description

The ltscompare tool determines whether or not the labelled transition systems (LTSs) in INFILE1 and INFILE2 are related by some equivalence or preorder. If INFILE1 is not supplied, stdin is used.

The input formats are determined by the content of INFILE1 and INFILE2. The options --in1 and --in2 can be used to force the format of INFILE1 and INFILE2, respectively. The supported formats are:

Options

OPTION can be any of the following:

-eNAME, --equivalence=NAME
use equivalence NAME:
  • bisim: for strong bisimilarity
  • branching-bisim: for branching bisimilarity
  • sim: for strong simulation equivalence
  • trace: for strong trace equivalence
  • weak-trace: for weak trace equivalence
Note: this option is not allowed in combination with -p/--preorder.
-iFORMAT, --in1=FORMAT
use FORMAT format as the format for INFILE1 (or stdin if INFILE1 is not supplied)
-jFORMAT, --in2=FORMAT
use FORMAT format as the format for INFILE2
-pNAME, --preorder=NAME
use preorder NAME:
  • sim: for strong simulation preorder
  • trace: for strong trace preorder
  • weak-trace: for weak trace preorder
Note: this option is not allowed in combination with -e/--equivalence.
--tau=ACTNAMES
consider actions with a name in the comma separated list ACTNAMES to be a internal (tau) actions in addition to those defined as such by the input; this means that before comparing the LTSs all specified actions are first replaced by tau actions

Standard options:

-q, --quiet
do not display warning messages
-v, --verbose
display short intermediate messages
-d, --debug
display detailed intermediate messages
-h, --help
display help information
--version
display version information

Author

Written by Muck van Weerdenburg.

Bug reporting

Report bugs at our issue tracking system.


ltsconvert

Convert and optionally minimise an LTS.

Synopsis

ltsconvert [OPTION]... [INFILE [OUTFILE]]

Short description

The ltsconvert tool converts the labelled transition system (LTS) in INFILE to OUTFILE in the requested format after applying the selected minimisation method to INFILE (default is no minimisation). If OUTFILE is not supplied, stdout is used. If INFILE is not supplied, stdin is used.

The output format is determined by the extension of OUTFILE, whereas the input format is determined by the content of INFILE. Options --in and --out can be used to force the input and output formats. The supported formats are:

In order to convert a non-mCRL2 LTS to a mCRL2 LTS one needs to supply the original LPS with --lps. This is because actions need to be stored in the internal mCRL2 format in mCRL2 and in non-mCRL2 LTSs are represented by strings (lacking essential information such as data types).

Note that tools that use the fsm format may depend on state information and parameter names. This requires that this information is available in the input LTS file or that the --lps option is used (see the options sections below).

Options

OPTION can be any of the following:

-a, --add
do not minimise but save a copy of the original LTS extended with a state parameter indicating the bisimulation class a state belongs to; this means that every state is extended with a number in such a way that (only) equivalent states have the same number (this option only works for mCRL2 LTSs)
-D, --determinise
determinise the LTS
-eNAME, --equivalence=NAME
generate an equivalent LTS, preserving equivalence NAME:
  • bisim: minimise modulo strong bisimilarity
  • branching-bisim: minimise modulo branching bisimilarity
  • sim: minimise modulo strong simulation equivalence
  • trace: determinise and then minimise modulo trace equivalence
  • weak-trace: determinise and then minimise modulo weak trace equivalence
-iFORMAT, --in=FORMAT
use FORMAT format as the input format
-lFILE, --lps=FILE
use FILE as the LPS from which the input LTS was generated; this is needed to store the correct parameter names of states when saving in fsm format and to convert non-mCRL2 LTSs to a mCRL2 LTS
-n, --no-state
leave out state information when saving in dot format
--no-reach
do not perform reachability check on the input LTS
--none
do not minimise the LTS (this is the default)
-oFORMAT, --out=FORMAT
use FORMAT format as the output format
--tau=ACTNAMES
consider actions with a name in the comma separated list ACTNAMES to be a internal (tau) actions in addition to those defined as such by the input; this means that before minimisation all specified actions are first replaced by tau actions; in the case --add is used, these tau actions will only used internally to compute the equivalence classes; the output will have the original actions

Standard options:

-q, --quiet
do not display warning messages
-v, --verbose
display short intermediate messages
-d, --debug
display detailed intermediate messages
-h, --help
display help information
--version
display version information

See also

In case ltsconvert requires too much memory for bisimulation reductions one can try the ltsmin tool. Note, however, that this tools is deprecated and can only handle files in the mCRL2 SVC format.

Author

Written by Muck van Weerdenburg.

Bug reporting

Report bugs at our issue tracking system.


ltsgraph

Visualise an LTS as a graph and manipulate its layout.

Synopsis

ltsgraph [OPTION]... [INFILE]

Short description

The ltsgraph tool draws the graph described by INFILE using a graphical user interface. If INFILE is not supplied the tool starts without a drawing. INFILE can have any one of the following extensions:

The main window of the tool shows the labelled transition system described by the input file as a directed, labelled graph. Using the dialogs found in the "Tools" menu, the graph's layout and several other visualization settings can be manipulated. The layout of the graph can also be manipulated by dragging vertices (states).

Options

OPTION can be any of the following standard options:

-q, --quiet
do not display warning messages
-v, --verbose
display short intermediate messages
-d, --debug
display detailed intermediate messages
-h, --help
display help information
--version
display version information

Detailed description

Theory

The ltsgraph tool uses a basic force directed layout method to position the vertices in a 2 dimensional space. In general such layout methods use a force system based on vertices and edges. The goal is to find an equilibrium state, where the sum of forces is 0. The method used by ltsgraph uses springs and electrical forces. vertices are modelled as electrically charged particles that repel each other more when they come closer together. Edges are modelled as springs that generate a force on both connected vertices depending on the zero-energy length of the spring. The spring exerts an repelling force when smaller than zero-energy length and a attractive force otherwise.

Write xu,yu for the x-coordinate respectively the y-coordinate of a vertex u. Let u and v be atbitrary vertices and d(u,v) be a distance measure (usually Euclidean distance). The x-component of the electrical (repelling) force that a vertex u exerts on vertex v is defined as follows:

F^{electric}_{x}(u,v) = \frac{e_{u,v}}{d(u,v)^{2}} * \frac{x_{v} - x_{u}}{d(u,v)}

Where eu,v represents the strength of the electrical repulsion between u and v. Let u and v be vertices such that (u,v) \in E. The x-component of the force exerted by the spring on v is:

F^{spring}_{x}(u,v) = s_{u,v} * log(\frac{d(v,u)}{l_{u,v}}) * \frac{x_{v} - x_{u}}{d(v,u)}

Where su,v is the stiffness of the spring and lu,v is the zero-energy length of the spring between points u and v. The observant reader may point out that the last definition does not follow Hook's law that describes how a spring works in the physical world. Instead we used the alternate spring model more suitable for the purpose of computing graph layouts <ref name=[Eades84]>P.A. Eades, “A heuristic for graph drawing”, Congressus Nutnerantiunt, vol. 42, pages 149–160, 1984</ref>.

An algorithm is needed to simulate these forces and apply them to generate new graph layouts. The input to the algorithm is a graph (V,E) and an arbitrary existing layout for a graph. The algorithm computes the sum of electric forces:

F^{total}_{x}(v) = \sum_{u \in V}F^{electric}_{x}(u,v) + \sum_{(u,v) \in E}F^{spring}_{x}(u,v)

The new position of a vertex v is then computed from the old coordinates by applying the total force:

(v_{x} + F^{total}_{x}(v), v_{y} + F^{total}_{y}(v))

A single run of the algorithm computes a new set of coordinates for all vertices: the new layout. Repeating this process until the sum of all forces is zero gives an optimal layout.

The ltsgraph tool offers three parameters e, s and l that can be used to interactively guide the positioning algorithm. There is a simple link between these three parameters and the force models described above. For all e = eu,v,s = su,v,l = lu,v for all u and v.

Functionality

The ltsgraph tool generates two dimensional graph layouts for transition systems and has some edit functionality. Apart from basic drawing, provides the following additional functionalities:

References

<references />

Author

Written by Carst Tankink.

Bug reporting

Report bugs at our issue tracking system.


ltsinfo

Display basic information about an LTS.

Synopsis

ltsinfo [OPTION]... [INFILE]

Short description

The ltsinfo tool prints information about the labelled transition system (LTS) in INFILE. If INFILE is not supplied, stdin is used.

The format of INFILE is determined by its contents. The option --in can be used to force the format for INFILE. The supported formats are:

Options

OPTION can be any of the following:

-eNAME, --equivalence=NAME
use equivalence NAME for deterministic check:
  • isomorph: for isomorphism (default)
  • bisim: for strong bisimilarity
  • branching-bisim: for branching bisimilarity
  • none: for not performing the check at all
-iFORMAT, --in=FORMAT
use FORMAT format as the input format

Standard options:

-q, --quiet
do not display warning messages
-v, --verbose
display short intermediate messages
-d, --debug
display detailed intermediate messages
-h, --help
display help information
--version
display version information

Author

Written by Muck van Weerdenburg.

Bug reporting

Report bugs at our issue tracking system.


ltsmin

Minimise an LTS in SVC format (DEPRECATED)

Synopsis

ltsmin [OPTION]... INFILE OUTFILE

Short description

The ltsmin tool minimises the labelled transition system (LTS) in the SVC format from INFILE using bisimulation reduction and saves the resulting LTS to OUTFILE.

The input SVC file must have been generated by lps2lts.

Note that this tools is deprecated and ltsconvert should be used where possible.

Options

OPTION can be any of the following:

-a, --add
do not minimise but save a copy of the original LTS extended with a state parameter indicating the bisimulation class a state belongs to
-eNAME, --equivalence=NAME
use equivalence NAME:
  • strong: for strong bisimulation (default)
  • branching: for branching bisimulation
--tau=ACTNAME
consider action with name ACTNAME to be an internal (tau) action

Standard options:

-q, --quiet
do not display warning messages
-v, --verbose
display short intermediate messages
-d, --debug
display detailed intermediate messages
-h, --help
display help information
--version
display version information

See also

For minimising other types of LTSs or transforming one type into another see the ltsconvert tool.

Author

Written by Muck van Weerdenburg.

Bug reporting

Report bugs at our issue tracking system.


ltsview

3D interactive visualisation of an LTS.

Synopsis

ltsview [OPTION]... [INFILE]

Description

The ltsview tool visualises the LTS in INFILE using a graphical user interface. If INFILE is not supplied, the tool starts with no file opened. The supported LTS formats are:

The tool clusters states based on structural properties. These clusters are then visualised to form a backbone of the LTS on which the states and transitions can be drawn. The tool provides functionalities to explore the visualisation (zooming, panning, rotating), mark deadlocks, mark states based on the values of their state vector parameters and mark transitions based on their labels. An image of the visualisation can also be saved in various bitmap formats.

Options

OPTION can be any of the following standard options:

-q, --quiet
do not display warning messages
-v, --verbose
display short intermediate messages
-d, --debug
display detailed intermediate messages
-h, --help
display help information
--version
display version information

See also

The visualisation techniques are based on the techniques described here and in <ref> F. van Ham, H. van de Wetering and J.J. van Wijk. Visualization of State Transition Graphs. In: Proc. IEEE Symp. Information Visualization 2001, IEEE CS Press, pp. 59-66, 2001. </ref>.

References

<references />

Author

Written by Bas Ploeger and Carst Tankink.

Bug reporting

Report bugs at our issue tracking system.


lysa2mcrl2

Convert a Typed LySa specification to an mCRL2 process specification. (EXPERIMENTAL)

Synopsis

lysa2mcrl2[OPTION]... [INFILE [OUTFILE]]

Short Description

Converts a security protocol specified in Typed LySa in INFILE into an mCRL2 process specification in OUTFILE. If OUTFILE is not present, stdout is used. If INFILE is not present, stdin is used.

Options

OPTION can be any of the following:

-aNUM, --attacker-index=NUM
Assume that the attacker may be a legitimate (but dishonest) agent participating in the protocol, corresponding to meta-level index number NUM. The effect of setting this option is that the attacker's crypto-point CPDY is added to all dest/orig clauses where one or more of the current meta-variables equal NUM. This option corresponds to the attackerIndex option of the LySa tool.
-l, --lysa
Converts a Typed LySa process to LySa and not to mCRL2. Makes all other non-standard options illegal.
-i[PREFIX], --prefix-idents[=PREFIX]
Prefixes all identifiers found in the Typed LySa process in INPUT with an underscore or with PREFIX to prevent clashes with mCRL2 keywords or identifiers used in the preamble.
-s[STRATEGY], --strategy[=STRATEGY]
Apply conversion using the specified strategy:
  • 'straightforward' for a straightforward conversion; most likely this yields an infinite state space.
  • 'symbolic' for a conversion in which symbolic representations are chosen to represent possibly infinite numbers of ciphertexts and names (default).
-z, --zero-action
Generates a 'zero' action before deadlocking when Typed LySa's empty process (0) is encountered. This is a valid action in the supplied preambles. This option may help to differentiate between a deadlock and a correct protocol run termination.

Standard options:

-q, --quiet
do not display warning messages
-v, --verbose
display short intermediate messages
-d, --debug
display detailed intermediate messages
-h, --help
display help information
--version
display version information

Author

Written by Egbert Teeselink.

Reporting bugs

Report bugs at [9].


mcrl22lps

Translate an mCRL2 specification to a linear process specification (LPS).

Synopsis

mcrl22lps [OPTION]... [INFILE [OUTFILE]]

Short description

The tool mcrl22lps translates an mCRL2 process specification to a linear process specification (LPS). The input is read from INFILE and the output is written to OUTFILE. If OUTFILE is not present, stdout is used. If INFILE is not present, stdin is used.

The input process specification should adhere to its syntax description (see also the language reference for more information).

The process in the input must be in parallel pCRL format. This means that it must consist of the parallel composition of a set of processes that are described using actions, conditions, sum operators, timing, sequential and alternative composition operators only. The parallel, communication and renaming operators can only be used on the outer level. Typical input examples are found in the directory examples of the mCRL2 repository.

For certain inputs, mcrl22lps can take a large amount of time. In some cases it will not terminate, for instance with a non terminating rewrite rules. The following options can be used to speed up the linearisation, at the expense of a less readable result.

The option --lin-method=stack avoids non termination if the process structure is not regular. The option --no-rewrite causes rewriting to be switched off, avoiding non termination due to non terminating rewrite rules. The option --no-sumelm avoids the use of sum elimination, which under certain circumstances may take a lot of time. Finally, the option --no-deltaelm avoids removal of spurious delta summands, which uses a quadratic algorithm in the number of summands, and therefore, may be very time consuming.

The option --timed assumes that the timing of the input is strict. By default it is assumed that time can always progress in the sense that each process p is interpreted as p+delta, which is incorrect as it does not preserve time. For instance the process a@1 is interpreted as a@1+delta, meaning that the a does not have to happen at time 1. If time is important, the option --timed is required. However, this may lead to substantially increased linearisation times and an increased size of the linear process.

Options

OPTION can be any of the following:

-a, --statenames
Using this option, the names of generated data parameters are extended with the name of the process in which they occur. In this way it is easier to determine where the parameter comes from.
-b, --binary
This option causes all generated finite sorts to be encoded using boolean. These finite sorts are generated when clustering and when generating state variables. See --cluster and --newstate.
-c, --cluster
This option causes the output linear process to be clustered. This option is not used by default. Clustering means that summands with the same action labels are taken together. For instance, a(f1)·P(g1) + a(f2)·P(g2) is replaced by ∑b:Bool a(if(b,f1,f2))·P(if(b,g1,g2)). The advantage is that the number of summands can be reduced substantially in this way. The disadvantage is that sum operators are introduced and new data sorts with auxiliary functions are generated. In order to avoid the generation of new sorts, the option --binary can be used which causes all new sorts to be encoded using booleans.
-D, --delta
With this option a (untimed) delta summand is added to each state of each process. This influences the behaviour of timed processes in the sense that processes can also choose to idle, without being forced to perform an action. For untimed processes this was already the case, and there is no effect on the semantics. The advantage of this option is that the delta can subsume all other conditional and timed delta's reducing the number of delta summands in the resulting linear process. Furthermore, as processing delta summands can be very time consuming, this option can make linearisation substantially faster.
-e, --check-only
Using this option mcrl22lps only checks the syntax and the static semantics of the input, but it will not execute the linearisation process. This is useful to check whether the input is proper mCRL2.
-f, --no-globvars
When linearising, there are several places where the values of data variables are irrelevant for the behaviour of the process. E.g. when linearising the process X = ∑d:D read(d)·send(d)·X, the value of the variable d has no meaning after the send action. In this case a 'global variable' is introduced to indicate that the value of this variable can be chosen freely. As the number of global variables can become quite large, the generation of such variables can be avoided by using this option. In this case a dummy value is chosen, which is the same for each sort.
-g, --no-deltaelm
With this option the linearisation will not attempt to remove spurious delta summands. Due to the existence of time, delta summands cannot be omitted. Due to the presence of multi-actions the number of summands can be huge. The algorithm for removing delta summands simply works by comparing each delta summand with each other summand to see whether the condition of the one implies the condition of the other. Clearly, this has quadratic complexity, and can take a long time.
-lNAME, --lin-method=NAME
Use linearisation method NAME:
  • stack: The LPS is generated using stack data types. The non parallel processes are transformed to restricted Greibach Normal Form and straightforwardly translated to linear processes using a stack. The resulting linear processes are then put in parallel. This works for any allowed input. Unfortunately, the linear process that is the result of this operation can basically only be used for state space generation. Symbolic operations on the stacks are generally not very effective, because the stack data type is too complex. For symbolic analysis, linearisation methods regular or regular2 can be used.
  • regular: The non parallel processes are translated to restricted Greibach Normal Form. Instead of using a stack, these processes are translated to an LPS with finite control variables. If some process has an infinite number of control states, the tool will attempt to generate all of them, causing it to run out of memory. In such a case the stack method can be used to produce a linear process.
The regular method is almost the same as regular2. The only difference is in the way new process variables are generated: regular generates less parameters in the linear process than regular2, but regular2 generates an LPS in a few cases where the use of regular leads to non-termination.
The difference between the two methods is explained best by an example. The tool sometimes has to replace a sequence of process variables by a single new variable. For instance, P1(f(x)) · P2(g(x)) must be replaced by a new process P. With the regular method, the new process has a single parameter x, matching the single free variable x. I.e. the definition of P is P(x) = P1(f(x)) · P2(g(x)). With the regular2 method a variable is introduced for every term. In this latter case P is defined by P(y,z) = P1(y) · P2(z) and the expression P1(f(x)) · P2(g(x)) is replaced by P(f(x),g(x)).
We give an example in which linearisation with regular fails to terminate and the use of regular2 succeeds. Consider the process definition P(n:Nat) = a·P(n+1) + b and let the initial process be P(0)·δ. Now with regular infinitely many new processes are generated, each of the following form: P(0)·δ, P(1)·δ, etc. With regular2 only one new process is generated, namely one for P(n)·δ.
The regular method is used by default.
  • regular2: See the explanation of regular. Note that with this option the number of parameters can be very large, and consequently, the number of global variables can be huge too. In this case, linearising using the option -f,--no-globvars is advisable.
-m, --no-sumelm
This option causes the linearisation to avoid sum elimination. If there is a condition or part of a condition of the form x = t with x a variable bound in a sum operator, then the term t can often be substituted for x, and the sum over x can be removed. Sometimes searching for equations x = t can be very time consuming. Using the flag --no-sumelm sum elimination can be switched off.
-n, --no-cluster
This option prevents clustering of linear processes before they are put in parallel. By default these processes are clustered to avoid a blow-up in the number of summands when transforming two parallel linear processes into a single linear process. If a linear process with M summands is put in parallel with a linear process with N summands the resulting process has M×N + M + N summands. Both M and N can be substantially reduced by clustering at the cost of introducing new sorts and functions. See --cluster, esp. for a short explanation of the clustering process.
-o, --no-rewrite
This option prevents intermediate rewriting of terms. This is especially useful when the equations in the input specification are not terminating, as in this case the lineariser will not terminate.
-rNAME, --rewriter=NAME
Use rewrite strategy NAME. mcrl22lps simplifies data expressions using the

rewriter. To prevent rewriting the option -o, --no-rewrite can be used.

-w, --newstate
The sort of state variables is by default Pos, i.e. positive natural numbers. By using this option new finite sorts named Enumk are generated where k is the size of the domain. Also, auxiliary case functions and equalities are defined. In combination with the option --binary the finite sorts are encoded by booleans.
-z, --no-alpha
By default mcrl22lps attempts to distribute communication, hiding and allow operators over the parallel composition operator as this reduces the size of intermediate linear processes. By using this option, this step can be avoided. The name stems from the alphabet axioms in process algebra.

Standard options:

-q, --quiet
Do not display warning messages.
-v, --verbose
Display short intermediate messages.
-d, --debug
Display detailed intermediate messages.
-h, --help
Display help information.
--version
Display version information.

Author

Written by Jan Friso Groote.

Bug reporting

Report bugs at our issue tracking system.


mcrl2-gui

Synopsis

mcrl2-gui[OPTION]...

Short Description

A graphical front-end for mCRL2 tools

Options

OPTION can be any of the following: Standard options:

-q, --quiet
do not display warning messages
-v, --verbose
display short intermediate messages
-d, --debug
display detailed intermediate messages
-h, --help
display help information
--version
display version information

Detailed Description

mCRL2-gui provides a graphical user interface for mCRL2 tools. It gives the user the ability to edit, analyze and apply transformations to files that are affiliated to mCRL2. Furthermore, it gives the user feedback on the tools that are applied for analysis and transformation.

Graphical User Interface

The interface is divided into three panels. Each panel serves a different purpose. Panels can be moved, re-sized, hidden or shown.

File Browser

The File Browser is a file manager application that provides a graphical user interface for accessing the file systems for non-hidden files on disk. The file browser uses a tree-view representation. Nodes display folders and volumes, leaves of the tree represent files on disk. Both nodes and leaves can be subjected to manipulation. The available manipulations can differ per node or leave. These manipulations be addressed by right-clicking on an element in the tree, pressing the "menu" button (when the File Browser has focus), or using a short-cut key. mCRL2-gui offers the possibility to analyze and transform files that have a matching extension recognized by tools within the mCRL2-toolset. Recognized extensions can be found in the File_formats section. The figure below shows the options that are available for a file that has the "lps" extension.

Options:

Executed commands

The executed commands panel shows the commands that have been executed during the analysis and transformation on files. Each line specifies a command that can be executed from a shell. This panel provides the user the possibility to select, deselect, copy, and save the executed commands.

Image:Mcrl2-gui-executed-commands-crop.png

Configuration panel

The configuration panel is used to configure and run tools. The configuration panel is displayed after selecting either the analysis or transformation option. The configuration panel shows a notebook. Each instance of a tool is displayed in a separate notebook tab. Each tab is divided into two sub-tabs. The first tab displays the tool specific options, whereas the other displays the output produced by a tool during execution. The tab that displays the tool specific options allows a user to configure and run a tool. The tab that displays the output of tool, can also be used to re-run the tool, copy the output to clipboard or save the output to a file.

Preferences

The preferences windows allows a user to customize mcrl2-gui. Currently, it only facilitates options for editing files. The preferences window can be accessed through Window->Preferences. The preferences hold after the "save" button has been pressed.

Editors are associated to file type extensions. To override system defined editors, or set a custom editor for a specific file type extension, a user should specify the command that is required to edit the file. The left column displays the extension, the right column display the invoked command. The string %s specifies the wildcard for the file invoked for editing.

For example, editing files with the "mcrl2" extension with open OpenOffice Writer requires a user to add or edit the mapping for "mcrl2" files. Say, OpenOffice Writer is located at: 

 /usr/bin/oowriter

then a user should specify the mapping as: 

 /usr/bin/oowriter %s

for files with the "mcrl2" extension.

Author

Written by Frank Stappers.

Reporting bugs

Report bugs at [10].


mcrl2i

Interpreter for the mCRL2 data language.

Synopsis

mcrl2i [OPTION]... [INFILE]

Short description

The mcrl2i tool provides a textual interface to experiment with data expressions. It evaluates mCRL2 data expressions via a text-based interface. If INFILE is present and if it contains an LPS or PBES, the data types of this specification may be used. If no input file is given, only the standard numeric datatypes are available. Stdin is ignored.

When mcrl2i is started a prompt is displayed. The following commands are available to manipulate mcrl2 data expressions. Essentially, there are commands to rewrite and type expressions, as well as generating the solutions for a boolean expression. The expressions can contain assigned or unassigned variables. Note that there are no bounds on the number of steps to evaluate or solve an expression, nor is the number of solutions bounded. Hence, the assign, eval solve commands can give rise to infinite loops.

h[elp]
print help message
q[uit]
quit mcrl2i
t[ype] EXPRESSION
print type of EXPRESSION
a[ssign] VAR=EXPRESSION
evaluate the EXPRESSION and assign it to the variable VAR.
v[ar] VARLIST
declare variables in VARLIST
r[ewriter] STRATEGY
use STRATEGY for rewriting (see rewrite strategies)
e[val] EXPRESSION
rewrite EXPRESSION and print result.
s[solve] <VARLIST> EXPRESSION
give all valuations of the variables in VARLIST that satisfy EXPRESSION

VARLIST is of the form x,y,...: S; ... v,w,...: T.

The interface has changed in svn revision 6088. For mcrl2i with revision number lower than 6088 the mcrl2i --help explains the old interface.

Options

OPTION can be any of the following:

-rNAME, --rewriter=NAME
use rewrite strategy NAME

Standard options:

-q, --quiet
do not display warning messages
-v, --verbose
display short intermediate messages
-d, --debug
display detailed intermediate messages
-h, --help
display help information
--version
display version information

Known Issues

Parsing of data expressions may lead to a new data specification which the rewriter knows nothing about. This could cause unexpected behaviour.

Author

Written by Muck van Weerdenburg. Changed by Jan Friso Groote (April 2009, revision 6088).

Bug reporting

Report bugs at our issue tracking system.


pbes2bes

Synopsis

pbes2bes[OPTION]... [INFILE [OUTFILE]]

Short Description

Reads the PBES from INFILE and writes an equivalent BES to OUTFILE. If INFILE is not present, stdin is used. If OUTFILE is not present, stdout is used.

Options

OPTION can be any of the following:

-H, --hashtables
use hashtables when substituting in bes equations, and translate internal

expressions to binary decision diagrams (discouraged, due to performance)

-oFORMAT, --output=FORMAT
use output format FORMAT: 
'vasy',
'pbes' (save as a PBES in internal format),
'cwi',
'bes' (default, save as a BES in internal format)
-p[NAME], --pbes-rewriter[=NAME]
use pbes rewrite strategy NAME: 
 'simplify' for simplification
 'quantifier-all' for eliminating all quantifiers
 'quantifier-finite' for eliminating finite quantifier variables
 'pfnf' for rewriting into PFNF normal form
-rNAME, --rewriter=NAME
use rewrite strategy NAME: 
 'jitty' for jitty rewriting (default),
 'jittyp' for jitty rewriting with prover,
 'jittyc' for compiled jitty rewriting,
 'inner' for innermost rewriting,
 'innerp' for innermost rewriting with prover, or
 'innerc' for compiled innermost rewriting
-sSTRAT, --strategy=STRAT
use strategy STRAT (default '0'); 
0) Compute all boolean equations which can be reached from the initial state, 
without optimization (default). This is is the most data efficient option per 
generated equation.
1) Optimize by immediately substituting the right hand sides for already 
investigated variables that are true or false when generating an expression. 
This is as memory efficient as 0.
2) In addition to 1, also substitute variables that are true or false into an 
already generated right hand side. This can mean that certain variables become 
unreachable (e.g. X0 in X0 and X1, when X1 becomes false, assuming X0 does not 
occur elsewhere. It will be maintained which variables have become unreachable 
as these do not have to be investigated. Depending on the PBES, this can 
reduce the size of the generated BES substantially but requires a larger 
memory footprint.
3) In addition to 2, investigate for generated variables whether they occur on 
a loop, such that they can be set to true or false, depending on the fixed 
point symbol. This can increase the time needed to generate an equation 
substantially
--timings[=FILE]
append timing measurements to FILE. Measurements are written to standard

error if no FILE is provided

-t, --tree
store state in a tree (for memory efficiency)
-u, --unused_data
do not remove unused parts of the data specification

Standard options:

-q, --quiet
do not display warning messages
-v, --verbose
display short intermediate messages
-d, --debug
display detailed intermediate messages
-h, --help
display help information
--version
display version information

Author

Implemented by Jan Friso Groote.

Reporting bugs

Report bugs at [11].


pbes2bool

Determine whether a PBES is valid by translating it to a BES.

Synopsis

pbes2bool [OPTIONS]... [[INFILE] [OUTFILE]]

Short description

The tool pbes2bool computes a boolean equation system (BES) of the parameterised boolean equation system (PBES) in INFILE. Unless indicated otherwise, pbes2bool subsequently tries to solve the BES.

Options

OPTION can be any of the following:

-c --counter
print at the end a tree labelled with instantiations of the left hand side of equations; this tree is an indication of how pbes2bool came to the validity/invalidity of the PBES
-H --hashtables
use hashtables when substituting in bes equations, and translate internal expressions to binary decision diagrams (the use of this flag is discouraged, due to heavy performance penalties)
-oFORMAT --output=FORMAT
use output format FORMAT:
  • 'none': no output is printed, and the BES is solved within pbes2bool (default)
  • 'cwi': output is printed is a very straightforward BES format to be used by tools developed at CWI; the BES is not solved
  • 'vasy': output BES is printed for use within the CADP toolset; the BES is not solved
  • 'pbes': output BES in internal PBES format suitable for further processing in the toolset; the BES is not solved
-p --precompile
precompile the pbes for faster rewriting; does not work when the toolset is compiled in debug mode
-rNAME --rewriter=NAME
use rewrite strategy NAME
-sNUMBER --strategy=NUMBER
use strategy NUMBER (default '0') to generate the BES:
  • '0': Compute all boolean equations which can be reached from the initial state, without any optimization. This is is the most data efficient option per generated equation. (default)
  • '1': Optimize by immediately substituting the right hand sides for already investigated variables that are true or false when generating an expression. This is as memory efficient as strategy 0.
  • '2': In addition to '1', also substitute variables that are true or false into an already generated right hand sides. This can mean that certain variables become unreachable (e.g. X0 in X0 && X1,when X1 becomes false, assuming X0 does not occur elsewhere. It will be maintained which variables have become unreachable as these do not have to be investigated. Depending on the PBES, this can reduce the size of the generated BES substantially, but requires a larger memory footstamp.
  • '3': In addition to '2', investigate for generated variables whether they occur on a loop, such that they can be set to true or false, depending on the fixed point symbol. This can increase the time needed to generate an equation substantially.
-t --tree
store state in a tree (for memory efficiency, comes with a small performance penalty)
-u --unused-data
do not remove unused parts of the data specification

Standard options:

-q, --quiet
do not display warning messages
-v, --verbose
display short intermediate messages
-d, --debug
display detailed intermediate messages
-h, --help
display help information
--version
display version information

Known issues

The counter example generated when the approximation algorithm of boolean equations is being used is in general huge and not very helpful. This algorithm is always employed with strategies 0 and 1. With strategies 2 and 3 it can be that when generating the boolean equation system from a PBES, it is already detected that the initial instantiated variable is either true or false and the approximation algorithm is not necessary. Counter examples in this case are compact (although we have no proof that the counter examples are always optimal) and also very helpful.

Detailed description

Generation of a BES

A BES is generated as follows. First the initial instantiated variable is considered. The instantiated right hand side for this variable is calculated, where all expressions without PBES variables are eliminated. Expressions are reduced to true or false and quantifiers are eliminated by enumerating its elements. As an example consider the PBES (where we use natural numbers as parameters, but these could be different of course). 

pbes mu X(n:Nat)=(n<5)||(forall m:Nat.(m<=n+1) => X(m));
init X(0);

The initial instantiated variable is X(0). The right hand side belonging to X(0) is 

(0<5)||(forall m:Nat.(m<=0+1) => X(m))

which using rewriting reduces to: 

(forall m:Nat.(m<=1) => X(m))

The variable m can either be 0 or 1. Using that natural numbers are defined by constructors, a technique called narrowing is used, using which it is calculated that 0 and 1 are the only useful values for m. The expression reduces to: 

X(0) && X(1)

So, the first boolean equation that results is 

mu X(0)=X(0) && X(1)

The next step is to calculate the equation for X(1).

Strategies

There are different strategies to generate the equations. In strategy 0, all equations are generated in a breadth first search. The equations generated in the order the instantiated variables are encountered.

In strategy 1, a small improvement is made. If an equation of the form 

nu X(17)=(X(10) && X(18)) || X(19)

is encountered and the right hand side for X(10) is false, then by substitution false for X(10) the equation reduces to 

nu X(17)=X(19)

Note that the instantiated variable X(18) disappears. It can be that X(18) does not have to be investigated at all, saving work compared to strategy 0.

The idea of substituting true and false and avoiding unnecessary work is taken one step further in strategy 2. Here, whenever a right hand side of an instantiated bes variable is true or false, this value is substituted for the instantiated variable every where. The advantage of strategy 2 is that when the validity of a modal formula can be detected by only investigating parts of the state space, this is detected. The costs of strategy 2 is a higher memory footprint than for strategy 0 and 1.

Consider the following partially generated BES from some PBES, which typically is the result of a deadlock check on a transition system with a deadlock. 

nu X(0)=X(1) && X(2) && X(3)
nu X(1)=X(4) && X(5) 
nu X(2)=X(6)
nu X(3)=false

With strategy 2, the value for X(3) will be substituted. The result is that X(0) becomes false. Furthermore, the instantiated variables X(1) and X(2) cannot be reached and have become superfluous. Using strategy 2, a garbage collection algorithm prevents such variables from being investigated.

Strategy 3 is very comparable to strategy 2, except that when a dependency loop of instantiated variables is detected, it attempts to set all the variables in the loop to true in case the fixpoint symbol is a nu, or false if it is a mu. For example 

nu X(38)=X(39)
nu X(39)=X(38)

it can set both X(38) and X(39) to true. Moreover, following strategy 2, it can subsequently substitute true for X(38) and X(39) in the generated equations.

Solving a BES

After the BES is generated, it can be solved. For this a backward approximation technique is followed. First all instantiated BES variables of the highest alternation depth are calculated. The variables are all simultaneously set to true or false depending on the fixpoint symbol at this depth. By a normal fixpoint iteration, a stable solution is calculated. This process must be symbolic, as variables at lower alternation depths can still occur in the approximation.

The results of this approximation are substituted in all equations of lower alternation depth, just as in Gauss-elimination. In a sense this is the ordinary Gauss elimination process, except that it treats all variables at the same alternation depth at once. For instance when the alternation depth is 0, i.e. there is no alternation, this approximation process converges in linear time. For arbitrary nesting depths, this procedure is exponential.

Generation of counter examples

It is possible to let pbes2bool generate a counter example. As it stands, counterexamples are most useful when generated with strategy 2. A counterexample is a tree with the initial instantiated pbes variable as its root. The branches of each node are printed as lines with two extra spaces of indentation. These branches are labelled with instantiated pbes variables of which the value determined the value of our node. Typically a counter example looks like: 

Solving the BES with 10 equations.
The pbes is not valid
Below the justification for this outcome is listed
1: X(0)
  2: Subst:false X(2)
    4: Subst:false X(5)
  3: Subst:false X(9)

This says that when solving X(0), it could be determined that it had solution false, because X(2) and X(9) where also false. The instantiated variable X(2) was false because X(5) was false. Apparently, X(5) and X(9) where invalid by itself.

The phrase Subst:false indicates the reason why a substitution was made. The following indications exist:

Mu Cycle
the variable is set to false because it is part of a cycle in a class of variables that all have the same alternation depth, and are preceded by a mu (strategy 3).
Nu Cycle
as in a Mu Cycle, except that the variable is set to true and the variables are preceded by nu (strategy 3).
Subst:false
false is substituted using back or forward substitution (strategy 2).
Subst:true
the value true is substituted using back or forward substitution (strategy 2).
FSubst:false
the value false is substituted by forward substition (strategy 1).
FSubst:true
the value true is substituted by backward substitution (strategy 1).
Set:false
variable is set to false (currently not used).
Set:true
variable is set to true (currently not used).
Appr:false
false is substitued for the variable when solving it using approximation.
Appr:true
true is substituted for the variable when solving it using approximation.
Approxim
a value not equal to true or false is substituted when solving the BES using approximation.

Sometimes the counterexample is recursive, or has re-occuring parts. these parts are only given once in the counterexample. A * at the end of a line in the counterexample indicates that this instantiated variable did already occur earlier in the counterexample and therefore, the reasons why it is true or false are not printed again.

Author

Written by Jan Friso Groote.

Bug reporting

Report bugs at our issue tracking system.


pbesconstelm

Synopsis

pbesconstelm[OPTION]... [INFILE [OUTFILE]]

Short Description

Reads a file containing a PBES, and applies constant parameter elimination to it. If OUTFILE is not present, standard output is used. If INFILE is not present, standard input is used.

Options

OPTION can be any of the following:

-c, --compute-conditions
compute propagation conditions
-p[NAME], --pbes-rewriter[=NAME]
use pbes rewrite strategy NAME: 
 'simplify' for simplification
 'quantifier-all' for eliminating all quantifiers
 'quantifier-finite' for eliminating finite quantifier variables
 'pfnf' for rewriting into PFNF normal form
-e, --remove-equations
remove redundant equations
-rNAME, --rewriter=NAME
use rewrite strategy NAME: 
 'jitty' for jitty rewriting (default),
 'jittyp' for jitty rewriting with prover,
 'jittyc' for compiled jitty rewriting,
 'inner' for innermost rewriting,
 'innerp' for innermost rewriting with prover, or
 'innerc' for compiled innermost rewriting
--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
-h, --help
display help information
--version
display version information

Author

Implemented by Wieger Wesselink, with contributions from Simon Janssen and Tim Willemse.

Reporting bugs

Report bugs at [12].


pbesinfo

Synopsis

pbesinfo[OPTION]... [INFILE]

Short Description

Print basic information about the PBES in INFILE. If INFILE is not present, standard input is used.


By default, the following information about the PBES is shown:

Options

OPTION can be any of the following:

-f, --full
display the predicate variables and their signature
--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
-h, --help
display help information
--version
display version information

Author

Implemented by Wieger Wesselink, with contributions from Alexander van Dam.

Reporting bugs

Report bugs at [13].


pbesparelm

Synopsis

pbesparelm[OPTION]... [INFILE [OUTFILE]]

Short Description

Reads a file containing a PBES, and applies parameter elimination to it. If OUTFILE is not present, standard output is used. If INFILE is not present, standard input is used.

Options

OPTION can be any of the following:

--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
-h, --help
display help information
--version
display version information

Author

Implemented by Wieger Wesselink, with contributions from Simon Janssen and Tim Willemse.

Reporting bugs

Report bugs at [14].


pbespp

Pretty print a PBES.

Synopsis

pbespp [OPTION]... [INFILE [OUTFILE]]

Short description

The pbespp tool prints the parameterised boolean equation system (PBES) from INFILE to OUTFILE in a human readable format. If OUTFILE is not present, stdout is used. If INFILE is not present, stdin is used.

Options

OPTION can be any of the following:

-fFORMAT, --format=FORMAT
print the PBES in the specified FORMAT:
  • default: for a PBES specification (default)
  • debug: like default, with the following exceptions:
    • data expressions are printed in prefix notation using identifiers from the internal format
    • each data equation is put in a separate data equation section
  • internal: for a textual ATerm representation of the internal format
  • internal-debug: like internal, with an indented layout


Standard options:

-q, --quiet
do not display warning messages
-v, --verbose
display short intermediate messages
-d, --debug
display detailed intermediate messages
-h, --help
display help information
--version
display version information

Author

Written by Aad Mathijssen.

Bug reporting

Report bugs at our issue tracking system.


pbesrewr

Synopsis

pbesrewr[OPTION]... [INFILE [OUTFILE]]

Short Description

Rewrite the PBES in INFILE, remove quantified variables and write the resulting PBES to OUTFILE. If INFILE is not present, stdin is used. If OUTFILE is not present, stdout is used.

Options

OPTION can be any of the following:

-p[NAME], --pbes-rewriter[=NAME]
use pbes rewrite strategy NAME: 
 'simplify' for simplification
 'quantifier-all' for eliminating all quantifiers
 'quantifier-finite' for eliminating finite quantifier variables
 'pfnf' for rewriting into PFNF normal form
-rNAME, --rewriter=NAME
use rewrite strategy NAME: 
 'jitty' for jitty rewriting (default),
 'jittyp' for jitty rewriting with prover,
 'jittyc' for compiled jitty rewriting,
 'inner' for innermost rewriting,
 'innerp' for innermost rewriting with prover, or
 'innerc' for compiled innermost rewriting
--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
-h, --help
display help information
--version
display version information

Author

Implemented by Jan Friso Groote and Wieger Wesselink.

Reporting bugs

Report bugs at [15].


pnml2mcrl2

Convert a Petri net to an mCRL2 process specification.

Synopsis

pnml2mcrl2 [OPTION]... [INFILE [OUTFILE]]

Short description

The pnml2mcrl2 tool converts a Petri net in EPNML format to a matching mCRL2 specification. It does so without looking into the structure of the Petri net. Instead, it translates each place, transition and arc to (one or more) processes and/or variables, corresponding to that place, transition or arc.

Only classical Petri nets are translated, i.e. places, transitions and arcs. Other constructs, such as timing, coloring, inhibitor arcs and hierarchy will simply be ignored while translating.

Options

OPTION can be any of the following:

-e[NUM], --error[=NUM]
an __error action will happen if a place gets NUM or more tokens (default is 2)
-i, --hide
hide (rename to tau) all transition monitoring actions to hide all but one action edit the generated file and remove that action from the hide list
-p, --no-rec-par
generate non-recursive mCRL2 processes for the places, and enable the translation of inhibitor arcs and reset arcs

Standard options:

-q, --quiet
do not display warning messages
-v, --verbose
display concise intermediate messages
-d, --debug
displays detailed intermediate messages
-h, --help
display help message
--version
display version information

Authors

Written by Johfra Kamphuis and Yaroslav S. Usenko.

Bug reporting

Please report bugs at out issue tracking system.


squadt

Interactive integration of software tools

Synopsis

squadt [OPTION]... [PATH]

Short description

By default SQuADT starts and draws the graphical user interface, after which it waits for user interaction. Alternatively, when PATH is provided, it tries to open an existing project in PATH.

Options

OPTION can be any of the following:

-c, --create
create new project in PATH
-pPORT, --port=PORT
listen on TCP port number PORT

Standard options:

-q, --quiet
do not display warning messages
-v, --verbose
display short intermediate messages
-d, --debug
display detailed intermediate messages
-h, --help
display help message
--version
display version information

Detailed description

Overview

The SQuADT application provides a framework for tool integration. In the current version it is only possible to run tools that are present on the same machine that SQuADT is running on. The current setup does just this but in the future it should not matter on what machine the tools are running, as long as a tool can be started and can connect to SQuADT.

A custom build protocol based on XML-formatted messages is used for communication between tools and the SQuADT application across a TCP connection. This should allow almost any tool written in almost any programming language to connect and operate within this framework.

Projects

All operations occur within a project context, which is used by the system to collect and store information that can be used to automate certain tasks for the user. Creation of a new project consists of choosing a separate directory called project store. Associated with the project are all files that are assigned to it by the user or that are generated as part of tool operation.

The SQuADT application manages the contents of the project store. Files added to a project by the user are copied to this directory and erased when they are removed from the project. As part of the protocol the tool communicates what files have been used as input and what files have been produced during a tool run. The next section that discusses the data view tells how files can become part of a project.

Graphical User Interface

The main screen is split into two views, a view on the data in the project, and an activity view.

Data view

The data view shows sources of data and their main interdependencies. Below is a screenshot that shows the data view in SQuADT. Every icon represents a source of data, meaning a single file in the store. The colours indicate status. For instance a tool can be actively generating a file, or data in a file can be corrupted because a tool crashed while it was generating the data. To give the user a clue as to what is happening and what has happened the status is interactively updated while tools run in the background.

It is important to realise that the view only displays files in the project store that have been added to the project by the user, or files that can be created by running tools on other files in the project. Copying files to and from the project store has no effect, the system will ignore them or a tool may overwrite them if file names collide. Also note that not every object in the data view needs to actually correspond to a file in the project store. The data view (partly) visualises dependencies among data sources. It shows that the system `knows' what tools it must apply to what input in order to obtain each data object. The colours in the data view should be interpreted as follows:

Image:Document_white.png  
file contents is authentic (added by the user), so it is always up-to-date
Image:Document_green.png  
file contents is derived from other data and up-to-date
Image:Document_blue.png  
file contents is derived from other data, present in the project store but not up-to-date with respect to the data sources it depends on
Image:Document_red.png  
file contents is derived from other data and is not available in the project store or is considered corrupt
Image:Document_yellow.png 
file contents is being generated

As hinted at before here are two ways in which a file can become part of a project. The first is when a user manually adds it to a project. These files are called original or authentic because once lost they cannot be recreated without user intervention. Adding an original file is performed by selecting the appropriate option in the `Project' menu, as illustrated below.

The second way that files become part of a project is when they are produced by running a tool from the project store. The tool may require input from other files in the project. Such files are called the (input) dependencies. It is assumed that SQuADT is aware of all input dependencies in a project and one of its tasks is to make sure that all non-authentic files are up-to-date with respect to the files on which they depend (recursively). This means that changes propagate inversely across dependencies.

Note that there is an important restriction with regard to interfile dependencies. A tool may not depend for input on it's own output, or any file derived from it. Or equivalently cycles are not allowed in the dependency graph. The consequence is that there is only one way to generate each derived data source. This ensures that if all tools can process input and produce output in a finite amount of time, then all files in a project can be reproduced from the authentic files in a finite amount of time as well.

The data view is not just a passive visualisation of data in the project store. In addition it also functions as an interface for managing the project store. The following picture shows the operations that can be performed on a single file.

The context menu can be obtained by activating (right/double clicking) the object in the data view. From top to bottom. Rename can be used to edit the name of an object (and the associated file). Remove deletes the object and every object that depends on it (transitive-closure). Refresh brings the object and all objects it depends on in up-to-date status (transitive-closure). Configure starts a tool and reconfigures the tool that was used to generate the object. Clean removes the associated file from the project store, but retains the information on how it can be produced by running tools. The menu options between the separators are categories that characterise functionality of the set of known tools that take as (main) input a file with a type that corresponds with the type of the selected object. Finally the menu-option details shows a dialog that contains details on how the file was created (or how it can be recreated).

Activity view

The activity view shows activity of running tools as well as tools that might have already finished. Each tool instance is associated to a sub-window in the activity view associated. Such a window is called a `tool display' and is hidden by default. The tool display is not visible unless a tool activates it in some way.

The tool display represents a specific task that is being performed or has been performed. The task is performed by a single tool that is running in the background or has terminated already. Using the tool display the user can configure the tool to perform a task or see task progress information. The tool display is a communication channel between a tool instance and the user. For richer user-interaction the tool can also communicate with a user through its own graphical user interface.

Editing

Files can be manipulated by all kinds of tools that connected to SQuADT. An important class of useful tools namely editors are not available. To still be able to use such tools it is possible to invoke custom edit action on any file in a project. The inner workings are as follows. A command that performs the desired operation is associated with a file type. The command is executed in the default shell when the edit action is invoked.

The preferences menu gives access to the list of type/command associations. The list contains the types that are known to SQuADT after it's initialisation. The types are gathered by querying known tools. If initialisation fails for some tools then some types may not be in the list. It is possible to manually add a type/command pair, or to edit existing pairs. As an example the following command can be used to pretty print an mCRL2 linear process specification (LPS) and view the result in the editor vim. 

/bin/sh -c '/usr/bin/lpspp $ | /usr/bin/gvim -'

The command looks very complex for technical reasons, the goal is actually to execute '/usr/bin/lpspp $ | /usr/bin/gvim'. The shell (/bin/sh) is used to set up communication channels between the lpspp and programs gvim. Notice that the $ will be replaced by the target of the edit operation. For a file abp.lps, the result will look as follows: 

/bin/sh -c '/usr/bin/lpspp abp.lps | /usr/bin/gvim -'

For this mechanism to work as expected it is very important that the type of a file is known to SQuADT. This should be the case for any file generated by a tool. In this case the type is communicated as part of the message that a tool sends to inform SQuADT about the existence of the file. Of course a tool may communicate a bogus type and SQuADT will never know about it (considered a bug in the tool). For files added to a project by the user the type is guessed from the name of the file.

Author

Written by Jeroen van der Wulp.

Bug reporting

Report bugs at our issue tracking system.


tbf2lps

Convert a μCRL LPE to an mCRL2 LPS.

Synopsis

tbf2lps [OPTION]... [INFILE [OUTFILE]]

Short description

The tbf2lps tool translates linear process equations (LPEs) from the μCRL format (.tbf) to the mCRL2 format (.lps).

This translation assumes that Bool is the boolean sort with constructors T and F. Additionally, the following conversions on the data specification will be applied:

The conversions of and and eq are not necessary, but allow for elimination of sum variables (which can significantly speed up state space generation).

Options

OPTION can be any of the following:

-n, --no-conv-maps
do not apply conversions of mappings and and eq


Standard options:

-q, --quiet
do not display warning messages
-v, --verbose
display concise intermediate messages
-d, --debug
display detailed intermediate messages
-h, --help
display help message
--version
display version information

Author

Written by Muck van Weerdenburg.

Bug reporting

Report bugs at our issue tracking system.


tracepp

Convert and pretty print traces.

Synopsis

tracepp [OPTION]... [INFILE [OUTFILE]]

Short description

The tracepp tool converts the trace from INFILE to OUTFILE in another (possibly human readable) format. If OUTFILE is not present, stdout is used. If INFILE is not present, stdin is used.

Input should be in either plain format, which means a text file with one action on each line, or the mCRL2 trace format (as generated by lps2lts, for example).

Options

OPTION can be any of the following:

-fFORMAT, --format=FORMAT
print the trace in the specified FORMAT:
  • plain for plain text (default)
  • mcrl2 for the mCRL2 format
  • aut for the Aldebaran format
  • dot for the GraphViz format

Standard options:

-q, --quiet
do not display warning messages
-v, --verbose
display short intermediate messages
-d, --debug
display detailed intermediate messages
-h, --help
display help information
--version
display version information

Author

Written by Muck van Weerdenburg.

Bug reporting

Report bugs at our issue tracking system.


txt2lps

Synopsis

txt2lps[OPTION]... [INFILE [OUTFILE]]

Short Description

Translates the mCRL2 specification in INFILE and writes the resulting LPS to OUTFILE. If OUTFILE is not present, standard output is used. If INFILE is not present, standard input is used.

Options

OPTION can be any of the following:

--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
-h, --help
display help information
--version
display version information

Author

Implemented by Wieger Wesselink.

Reporting bugs

Report bugs at [16].


txt2pbes

Synopsis

txt2pbes[OPTION]... [INFILE [OUTFILE]]

Short Description

Parse the textual description of a PBES from INFILE and write it to OUTFILE. If INFILE is not present, stdin is used. If OUTFILE is not present, stdout is used.

The textual description should adhere to the BNF syntax description at <http://www.mcrl2.org/mcrl2/wiki/index.php/Language_reference/PBES_syntax>.


The textual description should adhere to the following BNF syntax description.

Options

OPTION can be any of the following:

--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
-h, --help
display help information
--version
display version information

Author

Implemented by Aad Mathijssen.

Reporting bugs

Report bugs at [17].


FAQ

Tools

Odd crashes on linux

On linux it is advised to set the stacksize to unlimited. This can be done by using a command limit stacksize unlimited. If the stack is limited tools will crash without warning when the stack is full.

mcrl22lps: Linearising an untimed mCRL2 file yields an LPS with time

This issue is caused by the use of the conditional operator c -> p. The default semantics of this operator is c -> p <> delta@0, which introduces time by means of the time stamp 0. When a specification does not contain time, it usually is more sensible to use the alternative semantics c -> p <> delta, that is without the introduction of a time stamp. To use this alternative semantics, the command line option -D/--delta may be used (or you can manually append <> delta to all expressions of the form c -> p).

mcrl22lps: Linearising takes excessively long

There are many potential reasons. First of all, the data equations -- that are considered as rewrite rules (from left to right) -- may not be terminating. Solution is to use the -o/--no-rewrite flag. A second reason can be that removing delta summands is too costly. This is avoided by using the -D/--delta option, which also eliminates timed delta summands. It is also possible that sum elimination is too costly, avoid this using the -m/--no-sumelm flag. The generation of large enumerated data types can also be expensive, which is avoided using the option -b/--binary (this encodes finite datatypes using booleans). Finally, it can be that the translation to regular form is very time consuming. Try to use -lstack/--lin-method=stack option instead of the default -1regular/--lin-method=regular. Also, the use of -lregular2/--lin-method=regular2 results in mcrl22lps terminating more often than the default.

LPS tools: "Cannot enumerate Real" error but no Reals are being used

This issue is most likely caused by the fact that linearisation of an untimed mCRL2 file yielded an LPS with time.

LPS tools: Performing tool operations on an LPS created by tbf2lps fails with an assertion

Currently tbf2lps does not check whether invalid identifiers are inserted into an LPS. Therefore, some tools may fail, as they render an LPS invalid because of this. This issue has at least been seen in lpsactionrename.

lpspp: Can I pass the output of lpspp to mcrl22lps?

Until svn revision 6655, mcrl22lps was not able to read linear process specifications that were pretty printed by lpspp, when the proc or init sections of the resulting specification contained free variable declarations denoted by var. This problem could be circumvented by running mcrl22lps with the -f/--no-freevars option, but it was not recommended when running other LPS tools. As of revision 6656, mcrl22lps is able to handle global variables, which replace the notion of free variables.

LTS tools do not work on very large SVC files

When using lps2lts the default mCRL2 (SVC-based) format can only be used when storing state spaces that fit into 4GiB. Files containing state spaces larger than that become unusable by any of the tools.

SQuADT: some tools are missing in the interface

When SQuADT is executed for the first time, it tries to find the required tools. If they cannot be found automatically, a pop-up appears which asks a user to guide SQuADT to the tools, by selecting a required one.

When tools are missing in SQuADT, please remove the .squadt/tool_catalog file in your "home" directory and restart SQuADT.

  1. On Linux/Unix: $HOME/.squadt/tool_catalog
  2. On Windows XP: C:\Documents and Settings\user\.squadt\tool_catalog
  3. On Mac OS X: /Users/user/.squadt/tool_catalog

Prior to the installation of a new version of the toolset, we advise users to remove .squadt directory.

SQuADT: Windows asks to unblock SQuADT in the firewall

SQuADT internally uses socket communication to connect to the specific mCRL2 tools. This causes the Windows firewall to ask to unblock SQuADT. By default SQuADT will only connect to localhost (127.0.0.1), and will never connect to the internet. Failing to unblock SQuADT in the firewall may lead to malfunction.

SQuADT: ltsgraph, ltsview and diagraphica crash when started from SQuADT

It is currently known that ltsgraph, ltsview and diagraphica crash when they are started from SQuADT in Windows Vista and Windows 7. A proper fix for this is currently not available. To work around this issue you can manually start the tools (from the start menu -> mCRL2 -> { ltsgraph, ltsview, diagraphica }), and manually open the file you want to display.

SQuADT

SQuADT is an alpha-tool, that may display inconsistent behavior. This may result in wrong user feedback, e.g. wrongful coloring of files, no feedback when tools are started or exit unexpectedly. Known issues are listed here.

Installation

After `svn update' the toolset no longer builds

Sometimes changes to the build system that are imported when running svn update cause build failures. Some different causes:

When the configure has changed, CMake should automatically trigger a new configuration. It is possible to trigger it manually by executing `cmake ." from the build-tree. If the problem persists, it is possible to remove the build target by executing `make clean'. This will preserve the current configuration. As a last resort it is possible to create a new build tree. This will require you to configure the build tree from scratch.

Linux: Visualization tools do not work properly

OpenGL tools do not work properly on X servers that use a Composite window manager (like Compiz or Beryl). Unfortunately this is a widespread issue that affects all OpenGL applications in general, not just the mCRL2 tools. We know of no workaround for this problem other than disabling your Composite window manager.

Linux: Diagraphica crashes with a segmentation fault at startup

With ATI cards diagraphica can terminate with a segmentation fault during initialization. Possible solutions:

Language

Support for quantifiers

As it stands, the implementation of quantifiers (exists and forall) in the language is not very advanced. This means that they can be used, but in general, simulating an mCRL2 model, or generating a state space for an mCRL2 model with quantifiers will most likely not succeed.

Support for Reals

The implementation of reals is currently the same as the implementation of integers, which explains the current lack of specific operators on reals.

Support for sets and bags

Sets over sort A are internally represented using functions of sort A -> Bool, and bags are represented by functions of sort A -> Nat. Currently, sets and bags are not normalized, meaning that two equal sets can have different denotations. For instance the empty set {} and the empty set to which an element is added that is subsequently removed again are not syntactically the same objects in memory. This means that sets and bags are suitable for simulation of processes, but as it stands not yet suited for state space generation. For state space generation it is generally better to use lists.

Known compilation issues

LTSview will produce a segmentation fault when loading a file if being compiled with MSVC9. Compiling LTSview with either MinGW or MSVC10 resolves the segmentation fault.


Retrieved from "http://www.mcrl2.org/mcrl2/wiki/index.php/User_manual/AllInOnePage"
This page was last modified on 26 August 2010, at 14:40. This page has been accessed 2,946 times.
Copyright © 2005-2012 Technische Universiteit Eindhoven.
Powered by MediaWiki