open Component[StateSpace, Input, Output, Agent, Interface] as Boom -- The boom of the LRCrane 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, 2014. enum StateSpace { x0, x1, x2, x3, x4, x5, atLeft, atRight, moving2left, moving2right } enum Input { fY0rY1, fY1rY0, rX0, fX0, rX1, fX1 } enum Output { move2left, move2right, eoml, eomr, epsilon } fact { no Boom/A/SilentEvents epsilon = Boom/I/SilentEvents } one sig lfY0rY1, lfY1rY0, lrX0, lfX0, lrX1, lfX1 extends Boom/Label { } fact { -- causal map Sigma = lfY0rY1->fY0rY1 + lfY1rY0->fY1rY0 + lrX0->rX0 + lfX0->fX0 + lrX1->rX1 + lfX1->fX1 T = lfY0rY1->move2right + lfY1rY0->move2left + lrX0->eoml + lfX0->epsilon + lrX1->eomr + lfX1->epsilon } one sig Agent extends Boom/A/CtrlAutomaton { } { states = x0 + x1 + x2 + x3 + x4 + x5 events = lfY0rY1 + lfY1rY0 + lrX0 + lfX0 + lrX1 + lfX1 controllableEvents = lfY0rY1 + lfY1rY0 transition = x0->lfY1rY0->x1 + x1->lfX1->x2 + x2->lrX0->x3 + x3->lfY0rY1->x4 + x4->lfX0->x5 + x5->lrX1->x0 initialState = x0 markedStates = x0 } one sig Interface extends Boom/I/CtrlAutomaton { } { states = atLeft + atRight + moving2left + moving2right events = move2left + move2right + eoml + eomr controllableEvents = move2left + move2right transition = atRight->move2left->moving2left + moving2left->eoml->atLeft + atLeft->move2right->moving2right + moving2right->eomr->atRight initialState = atRight finalStates = atRight } run { } for 1 but 10 SeqIdx, 1 Boom/A/Walk, 1 Boom/I/Walk check consistencyOfMarking {Boom/consistencyOfMarking} for 1 but 10 SeqIdx, 1 Boom/A/Walk, 1 Boom/I/Walk check observer {Boom/observer} for 1 but 10 SeqIdx, 1 Boom/A/Walk, 2 Boom/I/Walk check conditionOnSCT {Boom/conditionOnSCT} for 1 but 10 SeqIdx, 1 Boom/A/Walk, 1 Boom/I/Walk