open SBCDES_Total_Observation[StateSpace, EventSet]

-- The injector 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, x6, x7, bad }
enum EventSet { rX0, fX0, rX1, fX1, rX2, fX2, rY0, fY0 }

one sig G extends Automaton { }
{
 states = x0 + x1 + x2 + x3 + x4 + x5 + x6 + x7 + bad
 -- x0 = X0nY0X1nX2
 -- x1 = nX0nY0X1nX2
 -- x2 = nX0Y0X1nX2
 -- x3 = nX0Y0nX1nX2
 -- x4 = nX0Y0nX1X2
 -- x5 = nX0nY0nX1X2
 -- x6 = nX0nY0nX1nX2
 -- x7 = X0nY0nX1nX2
 events = rX0 + fX0 + rX1 + fX1 + rX2 + fX2 + rY0 + fY0
 controllableEvents = rY0 + fY0
 transition = x0->fX0->x1 + x0->fY0->bad
            + x1->rY0->x2 + x1->fY0->bad
            + x2->fX1->x3 + x2->fY0->bad + x2->rY0->bad
            + x3->rX2->x4 + x3->fY0->bad + x3->rY0->bad
            + x4->fY0->x5 + x4->rY0->bad
            + x5->fX2->x6 + x5->rY0->bad + x5->fY0->bad
            + x6->rX0->x7 + x6->rY0->bad + x6->fY0->bad
            + x7->rX1->x0 + x7->fY0->bad
 initialState = x0
 markedStates = x0
}

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

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

run { } for 1

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