Skip to content

Modular PlusCal feature: Interleaving

Jump to bottom
Do Nhat Minh edited this page Feb 1, 2019 · 3 revisions

Interleaving

Interleaving allows the developer to specify an action that is to be non-deterministically performed on each step of an archetype. For example, fail-stop fail semantics could be model-checked using interleavings as:

process (MainCoordinator \in COORDINATORS) == instance Coordinator(connection)
    interleaving { goto l1 };

The semantics of the process instantiation above is that, on each step of Coordinator, the algorithm may non-deterministically perform the goto l1 statement passed to interleaving. In other words, the interleaving constructs allow the modeling of fail-stop scenarios (where l1 is the first label in Coordinator), where processes may be restarted at arbitrary points in time.

The only type of statement supported on interleavings is PlusCal's goto.

Clone this wiki locally