open BasicProperties[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,
                  y0, y1, y2, y3, y4, y5, y6, y7 }
enum EventSet { rX0, fX0, rX1, fX1, rX2, fX2, rY0, fY0 }

one sig G extends CtrlAutomaton { }
{
 states = x0 + x1 + x2 + x3 + x4 + x5 + x6 + x7
 -- x0 = X0nY0X1nX2
 -- x1 = nX0nY0X1nX2
 -- x2 = nX0Y0X1nX2
 -- x3 = nX0Y0nX1nX2
 -- x4 = nX0Y0nX1X2
 -- x5 = nX0nY0nX1X2
 -- x6 = nX0nY0nX1nX2
 -- x7 = X0nY0nX1nX2
 -- ..X1X2 is physically impossible:
 --        the cylinder at the far beginning and the far end at the same time
 -- X0Y0.. is physically impossible in the normal operation mode because
 --        the cylinder, when extended, blocks the beam of light
 events = rX0 + fX0 + rX1 + fX1 + rX2 + fX2 + rY0 + fY0
 controllableEvents = rY0 + fY0
 transition = x0->fX0->x1 + x0->fY0->x0
            + x1->rY0->x2 + x1->fY0->x1
            + x2->fX1->x3 + x2->fY0->x1 + x2->rY0->x2
            + x3->rX2->x4 + x3->fY0->x6 + x3->rY0->x3
            + x4->fY0->x5 + x4->rY0->x4
            + x5->fX2->x6 + x5->rY0->x4 + x5->fY0->x5
            + x6->rX0->x7 + x6->rY0->x3 + x6->fY0->x6
            + x7->rX1->x0 + x7->fY0->x7
            -- example of uncontrollabled transitions almost impossible
            -- (statistically validated): x0->rX2, x0-fX1->x7
            -- example of controllable transitions that are inconsistent
            -- with the normal operation mode : x1->rY0
 initialState = x0
 markedStates = x0
}

one sig H extends CtrlAutomaton { }
{
 states = y0 + y1 + y2 + y3 + y4 + y5 + y6 + y7
 events = rX0 + fX0 + rX1 + fX1 + rX2 + fX2 + rY0 + fY0
 controllableEvents = rY0 + fY0
 transition = y0->fX0->y1 + y1->rY0->y2 + y2->fX1->y3
            + y3->rX2->y4 + y4->fY0->y5 + y5->fX2->y6
            + y6->rX0->y7 + y7->rX1->y0
 initialState = y0
 markedStates = y0
}

fun f: H.states->G.states
{
   y0->x0 + y1->x1 + y2->x2 + y3->x3
 + y4->x4 + y5->x5 + y6->x6 + y7->x7
}

run { }

check IsGtrimmed { IsTrim[G] }
check IsHtrimmed { IsTrim[H] }
check IsHcontrollable { controllability[G, H, f] }