open BasicProperties[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,
                  y0, y1, y2, y3 }
enum EventSet { fY0rY1, fY1rY0, rX0, fX0 }

one sig G extends CtrlAutomaton { }
{
 states = x0 + x1 + x2 + x3
 -- x0 = Y0nY1nX0
 -- x1 = nY0Y1nX0
 -- x2 = nY0Y1X0
 -- x3 = Y0nY1X0
 -- Y0Y1. and nY0nY1. are physically impossible because these commands
 --                   are exclusive.
 events = fY0rY1 + fY1rY0 + rX0 + fX0
 controllableEvents = fY0rY1 + fY1rY0
 transition = x0->fY0rY1->x1 + x0->fY1rY0->x0
            + x1->rX0->x2    + x1->fY1rY0->x0 + x1->fY0rY1->x1
            + x2->fY1rY0->x3 + x2->fY0rY1->x2
            + x3->fX0->x0    + x3->fY0rY1->x2 + x3->fY1rY0->x3
            -- example of uncontrollabled transitions almost impossible
            -- (statistically validated): x0->rX0, x1->fX0
 initialState = x0
 markedStates = x0
}

one sig H extends CtrlAutomaton { }
{
 states = y0 + y1 + y2 + y3
 events = fY0rY1 + fY1rY0 + rX0 + fX0
 controllableEvents = fY0rY1 + fY1rY0
 transition = y0->fY0rY1->y1
            + y1->rX0->y2
            + y2->fY1rY0->y3
            + y3->fX0->y0
 initialState = y0
 markedStates = y0
}

fun f: H.states->G.states
{
   y0->x0 + y1->x1 + y2->x2 + y3->x3
}

run { }

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