202407.1.168e85a571
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
lpsfununfold
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
Options
Background
lpspp
Usage
Description
Command line options
Author
lpsreach
Symbolic Exploration
Symbolic Representation
Limitations
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
lps2pres
Usage
Description
Command line options
Author
lps2torx
lpscleave
Compositional Minimisation
References
lpscombine
Usage
Description
Command line options
Author
lpsrealelm
Example
lpssymbolicbisim
Limitations
lts2pres
Usage
Description
Command line options
Author
ltscombine
Usage
Description
Command line options
Author
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
presconstelm
Usage
Description
Command line options
Author
presinfo
Usage
Description
Command line options
Author
presinst
Usage
Description
Command line options
Author
presparelm
Usage
Description
Command line options
Author
prespp
Usage
Description
Command line options
Author
presrewr
Usage
Description
Command line options
Author
pressolve
Usage
Description
Command line options
Author
resinfo
Usage
Description
Command line options
Author
respp
Usage
Description
Command line options
Author
symbolic_exploration
Usage
Description
Command line options
Author
txt2pres
Usage
Description
Command line options
Author
txt2res
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
Python dependencies
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
Code coverage
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
mCRL2 fundamentals
View page source
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