open SBCDES_Total_Observation[StateSpace, EventSet]

-- The jack211r 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, x4, x5, bad }
enum EventSet { fY0rY1, fY1rY0, rX0, fX0, rX1, fX1 }

one sig G extends Automaton { }
{
 states = x0 + x1 + x2 + x3 + x4 + x5 + bad
 -- x0 = nY0Y1nX0X1
 -- x1 = Y0nY1nX0X1
 -- x2 = Y0nY1nX0nX1
 -- x3 = Y0nY1X0nX1
 -- x4 = nY0Y1X0nX1
 -- x5 = nY0Y1nX0nX1
 events = fY0rY1 + fY1rY0 + rX0 + fX0 + rX1 + fX1
 controllableEvents = fY0rY1 + fY1rY0
 transition = x0->fY1rY0->x1 + x0->fY0rY1->bad
            + x1->fX1->x2    + x1->fY0rY1->bad + x1->fY1rY0->bad
            + x2->rX0->x3    + x2->fY0rY1->bad + x2->fY1rY0->bad
            + x3->fY0rY1->x4 + x3->fY1rY0->bad
            + x4->fX0->x5    + x4->fY1rY0->bad + x4->fY0rY1->bad
            + x5->rX1->x0    + x5->fY1rY0->bad + x5->fY0rY1->bad
 initialState = x0
 markedStates = x0
}

fun Q[X: G.states] : G.states
{
 { x : X | not x = bad }
}

one sig SFBCjack211r
{
 f = SFBCEnabled[G,Q[G.states]]
}

run { } for 1

check solution
{
 Q[G.states] = NBC[G, Q[G.states]]
} for 1