This website contains the formal semantics of Lingua Franca defined by using the MoCCML approach in the Gemoc studio.
This is still a work in progess but it is already possible to debug LF models like shown in the following screenshot:
It is also possible to do some exhaustive simulation to explore all the state space of a LF program. Resulting state spaces are amenable to model checking in the CADP tool:
- Demo of the omniscient debugger (video) for LF, allowing to navigate forward and backward in time
- Demo of the check of assertions (video) for a specific LF program. Assertions are written in CCSL
- Demo of model checking (video) LF program and injection of the counter example back into the debugging environment
this work is based on this fork of the LF tooling: https://github.com/jdeantoni/lingua-franca