Discrete Event Controller Synthesis

MTSA supports a synthesising behaviour models that control a given plant to satisfy a given property. The plant is defined using an FSP composite process. The property is defined using the controllerSpec keyword.

controller ||CONTROLLER = (PLANT)~{SPECIFICATIONS}.

The specification includes various items, some are optional:

Safety properties. These are process names that describe bad behaviour with error states. They may have been constructed using the property or ltl_property keyword)
Assumptions. These are names of assertions that must be boolean formulae (i.e., no temporal operators). An assertion A is interpreted by the synthesis procedure as []<>A.
Liveness. As with assumptions, they are boolean formulae and are interpreted as being g preceded by []<>.
Controllable alphabet. This is the set of events that are controllable by the controller to be synthesised.

controllerSpec NAME = {
    safety = { COMMA SEPARATED PROCESS NAMES }
    assumption = { COMMA SEPARATED ASSERTION NAMES }
    liveness = { COMMA SEPARATED ASSERTION NAMES }
    controllable = { NAME OF SET OF LABELS }
}

To check if the assumptions are compatible use:

check compatibility ||CONTROLLERNAME = (PLANTNAME)~{CONTROLLERSPECNAME}.