open Component[StateSpace, Input, Output, Agent, Interface] as Hook

-- The hook 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,
                  noVacuum, pumpingAir, vacuum, losingAir }
enum Input { fY0rY1, fY1rY0, rX0, fX0 }
enum Output { grab, release, wpGrabbed, wpReleased }

fact
{
 no Hook/A/SilentEvents
 no Hook/I/SilentEvents
}

one sig lfY0rY1, lfY1rY0, lrX0, lfX0
        extends Hook/Label { }

fact
{ -- causal map
 Sigma = lfY0rY1->fY0rY1 + lfY1rY0->fY1rY0 + lrX0->rX0 + lfX0->fX0
     T = lfY0rY1->grab + lfY1rY0->release + lrX0->wpGrabbed + lfX0->wpReleased
}

one sig Agent extends Hook/A/CtrlAutomaton { }
{
 states = x0 + x1 + x2 + x3
 events = lfY0rY1 + lfY1rY0 + lrX0 + lfX0
 controllableEvents = lfY0rY1 + lfY1rY0
 transition = x0->lfY0rY1->x1
            + x1->lrX0->x2
            + x2->lfY1rY0->x3
            + x3->lfX0->x0
 initialState = x0
 markedStates = x0
}

one sig Interface extends Hook/I/CtrlAutomaton { }
{
 states = noVacuum + pumpingAir + vacuum + losingAir
 events = grab + release + wpGrabbed + wpReleased
 controllableEvents = grab + release
 transition = noVacuum->grab->pumpingAir
            + pumpingAir->wpGrabbed->vacuum
            + vacuum->release->losingAir
            + losingAir->wpReleased->noVacuum
 initialState = noVacuum
 markedStates = noVacuum
}

run { } for 1 but 10 SeqIdx, 1 Hook/A/Walk, 1 Hook/I/Walk

check consistencyOfMarking {Hook/consistencyOfMarking} for 1
      but 10 SeqIdx, 1 Hook/A/Walk, 1 Hook/I/Walk
check observer {Hook/observer} for 1
      but 10 SeqIdx, 1 Hook/A/Walk, 2 Hook/I/Walk
check conditionOnSCT {Hook/conditionOnSCT} for 1
      but 10 SeqIdx, 1 Hook/A/Walk, 1 Hook/I/Walk