MBP tool along with plan synthesis allows to synthesize (maximally permissive) controllers. It takes as the input a plant (or domain; a state-transition system) written in SMV language, and requirements as CTL formulae. Also, MBP allows one to simulate behaviours of both the uncontrolled plant (domain) and the controlled one. Finally, it benefits from the common language with NuSMV Symbolic Model Checker. Once a plant is implemented in SMV, it can be verified using this model checker. Such a verification might be useful to ensure the correctness of the complex plants' models.
To synthesize the controller, run
MBP <smv_file>Run "MBP -h" for many other options.
With MBP it is possible to simulate both controlled and uncontrolled plant. For uncontrolled plant (domain) simulation run
MBP -dsimulate <smv_file>For controlled plant (plan) simulation run
MBP -simulate_plan <smv_file>
Here you can download the binary version of MBP, modified to allow for (maximally permissive) controller synthesis. Binary is compiled for PCs supporting Linux.
STL consists of two machines M1 and M2, followed by a test unit TU, linked by buffers B1 and B2. A workpiece tested by TU may be accepted or rejected; if accepted, it is released from the system; if rejected, it is returned to B1 for reprocessing by M2. The capacities of B1 and B2 are assumed to be 3 and 1 respectively. For detailed description see, for example Prof. Wonham's notes on Supervisory Control of Discrete-Event Systems.
In order to increase complexity of the problem, authors of the paper on STCT proposed two axis of extensions for the Simple Transfer Line example. One possibility is to allow all components to handle M workpieces. The second is to connect L Transfer Lines in a sequence with additional buffers between each pair of M-extended Tranfer Lines. Thus, we obtain an (L,M)-extended Transfer Line.