under construction

MTSA implements discrete event controller synthesis for GR1 formulae.

To use this functionality first declare a controller goal using

controllerSpec NAME = { safety = { COMMA SEPARATED PROCESS NAMES (WITH ERROR STATES) } assumption = { COMMA SEPARATED ASSERTION NAMES} liveness = { COMMA SEPARATED ASSERTION NAMES}
controllable = { NAME OF SET OF LABELS} }

Then build the controller from a plant

controller ||CONTROLLERNAME = (PLANTNAME)~{CONTROLLERSPECNAME}.

To check if the assumptions are compatible use

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