open BasicProperties[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, y0, y1, y2, y3, y4, y5 } enum EventSet { fY0rY1, fY1rY0, rX0, fX0, rX1, fX1 } one sig G extends CtrlAutomaton { } { states = x0 + x1 + x2 + x3 + x4 + x5 -- x0 = nY0Y1nX0X1 -- x1 = Y0nY1nX0X1 -- x2 = Y0nY1nX0nX1 -- x3 = Y0nY1X0nX1 -- x4 = nY0Y1X0nX1 -- x5 = nY0Y1nX0nX1 -- ..X0X1 is physically impossible: -- the cylinder at the far beginning and the far end at the same time -- Y0Y1.. and nY0nY1.. are physically impossible because these commands -- are exclusive. events = fY0rY1 + fY1rY0 + rX0 + fX0 + rX1 + fX1 controllableEvents = fY0rY1 + fY1rY0 transition = x0->fY1rY0->x1 + x0->fY0rY1->x0 + x1->fX1->x2 + x1->fY0rY1->x0 + x1->fY1rY0->x1 + x2->rX0->x3 + x2->fY0rY1->x5 + x2->fY1rY0->x2 + x3->fY0rY1->x4 + x3->fY1rY0->x3 + x4->fX0->x5 + x4->fY1rY0->x3 + x4->fY0rY1->x4 + x5->rX1->x0 + x5->fY1rY0->x2 + x5->fY0rY1->x5 -- 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 + y4 + y5 events = fY0rY1 + fY1rY0 + rX0 + fX0 + rX1 + fX1 controllableEvents = fY0rY1 + fY1rY0 transition = y0->fY1rY0->y1 + y1->fX1->y2 + y2->rX0->y3 + y3->fY0rY1->y4 + y4->fX0->y5 + y5->rX1->y0 initialState = y0 markedStates = y0 } fun f: H.states->G.states { y0->x0 + y1->x1 + y2->x2 + y3->x3 + y4->x4 + y4->x4 } run { } check IsGtrimmed { IsTrim[G] } check IsHtrimmed { IsTrim[H] } check IsHcontrollable { controllability[G, H, f] }