MM2 tutorial: Reachability

MM2 Tutorial - Reachability

By Anneline Daggelinckx

Reachability is the task of determining which elements can be reached from an initial set by repeatedly applying a given relation. In this tutorial, we will explore various types of reachability tasks and demonstrate how to encode them in MM2.

Each example covers the goal and desired result, introduces the data, builds code stepwise, and walks through an execution trace showing how each statement affects the space.

At the end of each part, you’ll also find a few exercises to try on your own.

If any part of the code is unclear, it can be helpful to start with the execution trace: seeing how the space evolves often makes the intention of the rules easier to understand.

Part 1 - reachable set via fixed relations

Part 2 - reachable set via patterns

Part 3 - reachable with budget

Part 4 - path to reachable

Part 5 - putting it all together [WIP]