202307.1.18ca8a1307

Home

Introduction to mCRL2
Download mCRL2
Support
Publications
Showcases

Using mCRL2

mCRL2 tutorial
mCRL2 language reference
Tool documentation
- List of the common tools
  - besinfo
  - bespp
  - bessolve
  - diagraphica
    - References
  - lps2lts
  - lps2pbes
  - lpsactionrename
  - lpsbinary
  - lpsbisim2pbes
  - lpsconfcheck
  - lpsconstelm
  - lpsinfo
  - lpsinvelm
    - Example of use
  - lpsparelm
  - lpsparunfold
  - lpspp
  - lpsreach
  - lpsrewr
  - lpssim
  - lpsstategraph
  - lpssumelm
    - Known issues
  - lpssuminst
    - Example
  - lpsuntime
  - lpsxsim
  - lts2lps
  - lts2pbes
  - ltscompare
  - ltsconvert
  - ltsgraph
  - ltsinfo
  - ltspbisim
  - ltspcompare
  - ltsview
    - References
  - mcrl2-gui
  - mcrl22lps
    - Linearisation methods
  - mcrl2i
  - mcrl2ide
  - mcrl2xi
  - pbes2bes
    - Generation of a BES
    - Strategies
  - pbes2bool
  - pbes2booldeprecated
  - pbesconstelm
  - pbesinfo
  - pbesinst
  - pbesparelm
  - pbespgsolve
  - pbespp
  - pbesrewr
  - pbessolve
  - pbessolvesymbolic
    - Limitations
  - pbesstategraph
  - tracepp
  - txt2bes
  - txt2lps
  - txt2pbes
- List of the experimental tools
  - besconvert
  - lps2torx
  - lpscleave
    - Compositional Minimisation
    - References
  - lpscombine
  - lpsrealelm
    - Example
  - lpssymbolicbisim
    - Limitations
  - pbes2cvc4
  - pbes2yices
  - pbesabsinthe
  - pbesabstract
    - Example
  - pbespareqelm
  - pbespor
  - pbessymbolicbisim
  - symbolic_exploration
- File formats
  - Formats for Labelled Transition Systems
- External tools
mCRL2 fundamentals

Development

Contributing
Build instructions
Development guidelines
mCRL2 library documentation
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

mCRL2

mCRL2 library documentation
Modal formulas
View page source

Modal formulas

The modal formulas library contains classes and algorithms to represent and manipulate modal formulas using the modal mu-calculus with data and time. The code in this library is contained in the namespaces action_formulas, state_formulas and regular formulas.

Previous Next

© Copyright 2011-2023, Technische Universiteit Eindhoven.

Built with Sphinx using a theme provided by Read the Docs.