ScenarioTools implements an on-the-fly synthesis algorithm that, based on the same play-out execution logic as the simulation, can synthesize a global finite-state controller for an MSD specifications, or show that a specification is inconsistent, i.e., no controller exists for the specification.
On-the-fly Synthesis Algorithm
The play-out-based execution logic of ScenarioTools can be also used to build a model of all or some of the states reachable in an execution. Based on this state-exploration capability, ScenarioTools implements an algorithm for synthesizing controllers for MSD specifications, or showing that there does not exist one, which implies that there does not exist a controller that implements the specification. The synthesis problem can be viewed as an infinite game with a Büchi winning condition. The game-solving algorithm used by ScenarioTools is an on-the-fly algorithm, which means that it can find winning strategies without necessarily exploring all possibly reachable states.
The figure below shows part of a state graph that is explored by the ScenarioTools synthesis. Each state represents is a particular set of active MSDs in a particular cut, lifeline bindings, etc. The green states are winning states, which are essentially states where the system has no liveness obligation and waits for the next environment event. In a nutshell, the ScenarioTools synthesis then tries to find a strategy that allows the system to reach such states infinitely often, although the environment tries everything to keep the system from doing so.
Part of a state space diagram explored by the ScenarioTools synthesis
From the explored state space and the winning states, a controller can then be extracted that contains for every possible sequence of environment events the admissible actions of the system to “win”, i.e., to satisfy the MSD specification. The figure below shows part of such a controller.
Part of a controller extracted from the state space explored by the game-solving algorithm.
The two diagrams shown above are state space resp. controller diagram created for the production cell example. The full diagrams can be downloaded here: