open Component[StateSpace, Input, Output, Agent, Interface] as Injector -- 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, I, R, W, H } enum Input { rX0, fX0, rX1, fX1, rX2, fX2, rY0, fY0 } enum Output { wpa, inject, eoi, rearm, epsilon } fact { no Injector/A/SilentEvents epsilon = Injector/I/SilentEvents } one sig lrX0, lfX0, lrX1, lfX1, lrX2, lfX2, lrY0, lfY0 extends Injector/Label { } fact { -- causal map Sigma = lrX0->rX0 + lfX0->fX0 + lrX1->rX1 + lfX1->fX1 + lrX2->rX2 + lfX2->fX2 + lrY0->rY0 + lfY0->fY0 T = lrX0->epsilon + lfX0->wpa + lrX1->epsilon + lfX1->epsilon + lfX2->epsilon + lrX2->eoi + lrY0->inject + lfY0->rearm } one sig Agent extends Injector/A/CtrlAutomaton { } { states = x0 + x1 + x2 + x3 + x4 + x5 + x6 + x7 events = lrX0 + lfX0 + lrX1 + lfX1 + lrX2 + lfX2 + lrY0 + lfY0 controllableEvents = lrY0 + lfY0 transition = x0->lfX0->x1 + x1->lrY0->x2 + x2->lfX1->x3 + x3->lrX2->x4 + x4->lfY0->x5 + x5->lfX2->x6 + x6->lrX0->x7 + x7->lrX1->x0 initialState = x0 markedStates = x0 } one sig Interface extends Injector/I/CtrlAutomaton { } { states = I + R + W + H events = wpa + inject + eoi + rearm controllableEvents = inject + rearm transition = I->wpa->R + R->inject->W + W->eoi->H + H->rearm->I initialState = I finalStates = I } run { } for 1 but 10 SeqIdx, 1 Injector/A/Walk, 1 Injector/I/Walk check consistencyOfMarking {Injector/consistencyOfMarking} for 1 but 10 SeqIdx, 1 Injector/A/Walk, 1 Injector/I/Walk check observer {Injector/observer} for 1 but 10 SeqIdx, 1 Injector/A/Walk, 2 Injector/I/Walk check conditionOnSCT {Injector/conditionOnSCT} for 1 but 10 SeqIdx, 1 Injector/A/Walk, 1 Injector/I/Walk