open SBCDES_Total_Observation[StateSpace, EventSet] -- The suction cup of the MPS from: -- D. Cote, -- Conception par composants de controleurs d'usines modulaires -- utilisant la theorie du controle supervise, -- Ph.D. thesis, Universite de Sherbrooke, 2011. -- copyright Richard St-Denis, Universite de Sherbrooke, 2013. enum StateSpace { x0, x1, x2, x3, bad } enum EventSet { fY0rY1, fY1rY0, rX0, fX0 } one sig G extends Automaton { } { states = x0 + x1 + x2 + x3 + bad -- x0 = Y0nY1nX0 -- x1 = nY0Y1nX0 -- x2 = nY0Y1X0 -- x3 = Y0nY1X0 events = fY0rY1 + fY1rY0 + rX0 + fX0 controllableEvents = fY0rY1 + fY1rY0 transition = x0->fY0rY1->x1 + x0->fY1rY0->bad + x1->rX0->x2 + x1->fY1rY0->bad + x1->fY0rY1->bad + x2->fY1rY0->x3 + x2->fY0rY1->bad + x3->fX0->x0 + x3->fY0rY1->bad + x3->fY1rY0->bad initialState = x0 markedStates = x0 } fun Q[X: G.states] : G.states { { x : X | not x = bad } } one sig SFBCsuctionCup { f = SFBCEnabled[G,Q[G.states]] } run { } for 1 check solution { Q[G.states] = NBC[G, Q[G.states]] } for 1