202307.1.18ca8a1307
Home
Introduction to mCRL2
Philosophy
History
Toolset overview
mCRL2 specification and linearisation
LPS tools
LTS tools
Model checking using PBESs
Integration with other tools
Download mCRL2
Latest release
Nightly build
Previous releases
Support
Publications
General
Research
Applications
Course material
Presentations
Showcases
AIA ITP load-balancer
Technical details
Publications
Atacama Large Millimeter Array
Technical details
Publications
Automated parking garage
Technical details
Publications
Automatic Document Feeder
Technical details
Publications
Links
Control Software of the CMS Experiment at CERN’s Large Hadron Collider
Formalisation
Bugs Detected
Future
Technical details
Publications
DAF Trucks Vehicle Function Architecture
Technical Details
Distributed system for lifting trucks
Technical details
Publications
Links
Dogfooding the structural operational semantics of mCRL2
Technical details
Publications
FlexRay communication protocol
Technical details
Publications
Generic Driving Actuator
Technical details
Publications
IEEE 1394 link layer
Technical details
Publications
LedSync communication protocol
Technical details
PCB Printer
Technical details
Publications
Pacemaker
Approach
Technical details
Publications
Patient support platform
System description
Context
Purpose
System architecture
Requirements
Validation
Technical details
Stella Solar Car
Technical details
Using mCRL2
mCRL2 tutorial
A Vending Machine
First variation
Second variation
Third variation
Water cans
Towers of Hanoi
Optimal strategy
The Rope Bridge
A Telephone Book
Gossips
Probabilistic processes
Using mcrl2-gui
Obtaining a linear process specification
Generating a labelled transition system
ltsgraph
and
ltsconvert
ltsview
and
diagraphica
Simulating a linear process specification
Setting an external editor in mcrl2-gui
Concluding remarks
References
mCRL2 language reference
mCRL2 specification
Lexical elements
Comments
Data specifications
Specifying sorts
Data expressions
Specifying mappings
Predefined mappings
Predefined sorts
Constructed sorts
Global variables
Process syntax
Process specifications
Actions
Process algebra
Adding data
Parallel composition
Communication and allow
Rename and hide
Time
Specification syntax
Linear Process Specifications
µ-Calculus
Multi-actions
Action formulas
Regular formulas
State formulas
Relations between symbols
Examples
Boolean Equation Systems
BES expression
BES equation
BES specification
References
Parameterised Boolean Equation Systems
PBES expression
PBES equation
PBES specification
Transforming PBESs
Solving PBESs
Symbolic approximation + Gauß elimination
Enumerative
References
Tool documentation
List of the common tools
besinfo
Usage
Description
Command line options
Author
bespp
Usage
Description
Command line options
Author
bessolve
Usage
Description
Command line options
Author
diagraphica
References
lps2lts
Usage
Description
Command line options
Author
lps2pbes
Usage
Description
Command line options
Author
lpsactionrename
Structure of rename files
Rename rule conditions
Example
Regular Expressions
Examples
lpsbinary
Usage
Description
Command line options
Author
lpsbisim2pbes
Usage
Description
Command line options
Author
lpsconfcheck
Usage
Description
Command line options
Author
lpsconstelm
Usage
Description
Command line options
Author
lpsinfo
Usage
Description
Command line options
Author
lpsinvelm
Example of use
lpsparelm
Usage
Description
Command line options
Author
lpsparunfold
Usage
Description
Command line options
Author
lpspp
Usage
Description
Command line options
Author
lpsreach
Symbolic Exploration
Symbolic Representation
References
lpsrewr
Usage
Description
Command line options
Author
lpssim
Usage
Description
Command line options
Author
lpsstategraph
Usage
Description
Command line options
Author
lpssumelm
Known issues
lpssuminst
Example
lpsuntime
Usage
Description
Command line options
Author
lpsxsim
Usage
Description
Command line options
Author
lts2lps
Usage
Description
Command line options
Author
lts2pbes
Usage
Description
Command line options
Author
ltscompare
Usage
Description
Command line options
Author
ltsconvert
Usage
Description
Command line options
Author
ltsgraph
Usage
Description
Command line options
Author
ltsinfo
Usage
Description
Command line options
Author
ltspbisim
Usage
Description
Command line options
Author
ltspcompare
Usage
Description
Command line options
Author
ltsview
References
mcrl2-gui
Usage
Description
Command line options
Author
mcrl22lps
Linearisation methods
mcrl2i
Usage
Description
Command line options
Author
mcrl2ide
Projects
Simulation and state space generation
Properties
Running tools
Known issues
Usage
Description
Command line options
Author
mcrl2xi
Usage
Description
Command line options
Author
pbes2bes
Generation of a BES
Strategies
pbes2bool
Usage
Description
Command line options
Author
pbes2booldeprecated
Generation of a BES
Solving a BES
Generation of counter examples
Known issues
pbesconstelm
Usage
Description
Command line options
Author
pbesinfo
Usage
Description
Command line options
Author
pbesinst
Usage
Description
Command line options
Author
pbesparelm
Usage
Description
Command line options
Author
pbespgsolve
Usage
Description
Command line options
Author
pbespp
Usage
Description
Command line options
Author
pbesrewr
Usage
Description
Command line options
Author
pbessolve
Usage
Description
Command line options
Author
pbessolvesymbolic
Limitations
pbesstategraph
Usage
Description
Command line options
Author
tracepp
Usage
Description
Command line options
Author
txt2bes
Usage
Description
Command line options
Author
txt2lps
Usage
Description
Command line options
Author
txt2pbes
Usage
Description
Command line options
Author
List of the experimental tools
besconvert
Usage
Description
Command line options
Author
lps2torx
Usage
Description
Command line options
Author
lpscleave
Compositional Minimisation
References
lpscombine
Usage
Description
Command line options
Author
lpsrealelm
Example
lpssymbolicbisim
Limitations
pbes2cvc4
Usage
Description
Command line options
Author
pbes2yices
Usage
Description
Command line options
Author
pbesabsinthe
Usage
Description
Command line options
Author
pbesabstract
Example
pbespareqelm
Usage
Description
Command line options
Author
pbespor
Usage
Description
Command line options
Author
pbessymbolicbisim
Usage
Description
Command line options
Author
symbolic_exploration
Usage
Description
Command line options
Author
File formats
Formats for Labelled Transition Systems
mCRL2 LTS format
The aut format
The FSM file format
External tools
mCRL2 fundamentals
Basic modelling with mCRL2
Behaviour and transition systems
Sequences and choices
Specifying systems
Comparing systems
A dash of infinity
Recursion
Regular HML
The modal µ-calculus
Using the µ-calculus
Data
The first-order µ-calculus
Compositionality
Operators
Communicating systems
Labelled transition systems
Internal actions
State values
Equivalences
Trace equivalence
Weak trace equivalence
Strong bisimilarity
Branching bisimilarity
Isomorphism
Determinism
Development
Contributing
Build instructions
Windows instructions
MacOS instructions
Ubuntu instructions
Documentation
CMake configuration flags
Development guidelines
File hierarchy
Libraries
Tools
Programming
Preamble
Naming conventions
Header policy
Exception handling
Standards compliance
Regression tests
Usability
Platform independence
Committing changes
Documentation guidelines
Tools
User manual
Libraries
User manual
Reference manual
General
Acknowledgements
mCRL2 library documentation
Atermpp
Introduction to the atermpp library
What is an aterm?
Atermpp types
Aterm properties
Programming with aterms
Aterm creation
Aterm manipulation
Aterms and the C++ Standard Library
Aterm algorithms
BES
Core
Introduction
Concepts
Structure
Tutorial
Dependencies
The specification
The program
Manipulating the specification
Alphabet reduction
References
Common functionality
Traversal functions
Generic programming techniques
Static polymorphism
Concepts
Data
Introduction
Data specifications
Expressions
Sort expressions
Data expressions
Predefined sorts
Operations on data expressions
Creating data expressions
Sort aliases and sort normalisation
Data rewriters
Rewriter Concept
Algorithms using a rewriter
Data enumerator
GUI
The GUI library
The qt_tool class
LPS
Linear process specifications
Definitions
Specification
Linear processes
Classes in the LPS library
Correctness checks
LTS
Introduction
Structure
Creating and accessing an LTS
The standard labelled transition systems
Reducing and comparing labelled transition systems
Some utility functions
Traces
Modal formula
Modal formulas
PBES
Parameterised Boolean Equation Systems
PBES equation systems
PBES expressions
Algorithms
Algorithms on PBESs
Search and Replace functions
Rewriters for PBES expressions
Process
Introduction
Process expressions
Algorithms on processes
Search and Replace functions
SMT
SMT Interface library
Utilities
Introduction
Structure
CLI Library
Introduction
Concepts
Library interface
Tutorial
Tool classes
Tool interface guidelines
Available tool classes
Example
Logging Library
Introduction
Concepts
Library interface
Tutorial
Source code reference
Code generation
Testing
Regression tests
Random Testing
Performance measurements
Benchmarks
Setup
Maintainers
Git workflow
Regression testing with TeamCity
Setup
TeamCity project configuration
Build steps
Configure
Build
Test
CPack
Setup VS Env
Release and packaging procedure
Versioning scheme
Creating an official release
Creating release branch
Testing
Updating release number and copyright information
Tagging
Source release
Debian/Ubuntu packages
Windows release
Mac OS-X installer for 10.5+
Checking the installers
mCRL2
Index
Index
Symbols
|
A
|
B
|
C
|
D
|
E
|
F
|
G
|
H
|
I
|
L
|
M
|
N
|
O
|
P
|
R
|
S
|
T
|
U
|
V
|
W
Symbols
!
bag complement
logical not
set complement
#
list length
&&
logical and
()
function application
*
bag intersection
mathematical multiplication
set intersection
+
bag union
mathematical addition
set union
++
list concatenation
-
bag difference
mathematical negation
mathematical subtraction
set difference
->
.
list element extraction
<
less than
lexicographical ordering
subset
<=
less than or equal to
lexicographical ordering
subset or equal to
<|
list snoc
==
equality
=>
logical implication
>
greater than
lexicographical ordering
superset
>=
greater than or equal to
lexicographical ordering
subset or equal to
[]
list constructor
list enumeration
{}
bag comprehension
bag constructor
bag enumeration
set comprehension
set constructor
set enumeration
|>
list constructor
||
logical or
A
addition
+, mathematical
and
&&, logical
B
Bag
bag
complement !
comprehension {}
constructor {}
difference -
enumeration {}
intersection *
union +
Bag2Set
besconvert
besinfo
bespp
bessolve
Bool
BOOST_ROOT
BUILD_SHARED_LIBS
C
Casts
Int2Nat
Int2Pos
Int2Real
Nat2Int
Nat2Pos
Nat2Real
Pos2Int
Pos2Nat
Pos2Real
Real2Int
Real2Nat
Real2Pos
ceil
CMAKE_BUILD_TYPE
CMAKE_INSTALL_PREFIX
complement
!, bag
!, set
comprehension
{}, bag
{}, set
concatenation
++, list
cons
constructor
[], list
{}, bag
{}, set
|>, list
count
D
data
expression
specification
diagraphica
difference
-, bag
-, set
div
E
element extraction
., list
empty
bag
list
set
enumeration
[], list
{}, bag
{}, set
eqn
exists
exp
F
false
floor
forall
function application
G
glob
H
head
I
if(_,_,_)
implication
=>, logical
in
Int
intersection
*, bag
*, set
L
lambda
length
#, list
List
list
concatenation ++
constructor []
constructor |>
element extraction .
enumeration []
length #
snoc <|
logical
and &&
implication =>
not !
or ||
lps2lts
lps2pbes
lps2torx
lpsactionrename
lpsbinary
lpsbisim2pbes
lpscleave
lpscombine
lpsconfcheck
lpsconstelm
lpsinfo
lpsinvelm
lpsparelm
lpsparunfold
lpspp
lpsreach
lpsrealelm
lpsrewr
lpssim
lpsstategraph
lpssumelm
lpssuminst
lpssymbolicbisim
lpsuntime
lpsxsim
lts2lps
lts2pbes
ltscompare
ltsconvert
ltsgraph
ltsinfo
ltspbisim
ltspcompare
ltsview
M
map
mathematical
addition +
multiplication *
negation -
subtraction -
max
mcrl2-gui
mcrl22lps
MCRL2_ENABLE_EXPERIMENTAL
mcrl2i
mcrl2ide
mcrl2xi
min
mod
multiplication
*, mathematical
N
Nat
negation
-, mathematical
not
!, logical
O
or
||, logical
P
pbes2bes
pbes2bool
pbes2booldeprecated
pbes2cvc4
pbes2yices
pbesabsinthe
pbesabstract
pbesconstelm
pbesinfo
pbesinst
pbesparelm
pbespareqelm
pbespgsolve
pbespor
pbespp
pbesrewr
pbessolve
pbessolvesymbolic
pbesstategraph
pbessymbolicbisim
Pos
pred
R
Real
rhead
round
rtail
S
Set
set
complement !
comprehension {}
constructor {}
difference -
enumeration {}
intersection *
union +
Set2Bag
snoc
<|, list
sort
subtraction
-, mathematical
succ
symbolic_exploration
T
tail
tracepp
true
txt2bes
txt2lps
txt2pbes
U
union
+, bag
+, set
V
var
W
where clause
whr