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