Wieger Wesselink: About the Design and Implementation of State Space Exploration in the mCRL2 toolset

Event Details

An important use case of the mCRL2 tool set is state space exploration. An efficient and feature-rich implementation is available that works quite well in practice. Unfortunately the design of this implementation is quite complicated, and there is insufficient documentation. This makes it very hard to make any changes, or to add new functionality. During the last couple of months I have implemented a completely new version of state space exploration. In this talk I will explain its design and implementation. The new design contains pseudo code descriptions of the underlying algorithms. I consider it very important to have pseudo code descriptions at the right level of abstraction, and an implementation that closely matches the pseudo code. Another aspect that I will discuss is how to keep the code for all different features separate.