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

-- 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 { aLnV, aLpA, aLV, aRnV, aRV,
                  aRlA, m2lnV, m2rnV, m2rV,
                  x0, x1, x2, x3, x4, x5 }
enum Input { move2left, move2right, eoml, eomr,
             grab, release, wpGrabbed, wpReleased }
enum Output { ch, eoch, gr, eogr, gl, eogl, epsilon }

fact
{
 no LRCrane/A/SilentEvents
 epsilon = LRCrane/I/SilentEvents
}

one sig lmove2left, lmove2right, leoml, leomr,
        lgrab, lrelease, lwpGrabbed, lwpReleased
        extends LRCrane/Label { }

fact
{ -- causal map
 Sigma = lmove2left->move2left + lmove2right->move2right + leoml->eoml
       + leomr->eomr + lgrab->grab + lrelease->release
       + lwpGrabbed->wpGrabbed + lwpReleased->wpReleased
     T = lmove2left->gl + lmove2right->gr + leoml->eogl + leomr->eogr
       + lgrab->ch + lrelease->epsilon + lwpGrabbed->eoch
       + lwpReleased->epsilon
}

one sig Agent extends LRCrane/A/CtrlAutomaton { }
{
 states = aLnV + aLpA + aLV + aRnV + aRV
        + aRlA + m2lnV + m2rnV + m2rV
 events = lmove2left + lmove2right + leoml + leomr
        + lgrab + lrelease + lwpGrabbed + lwpReleased
 controllableEvents = lmove2left + lmove2right + lgrab + lrelease
 transition = aLnV->lmove2right->m2rnV
            + aLnV->lgrab->aLpA
            + aLpA->lwpGrabbed->aLV
            + aLV->lmove2right->m2rV
            + aRnV->lmove2left->m2lnV
            + aRV->lrelease->aRlA
            + aRlA->lwpReleased->aRnV
            + m2lnV->leoml->aLnV
            + m2rnV->leomr->aRnV
            + m2rV->leomr->aRV
 initialState = aRnV
 markedStates = aRnV
}

one sig Interface extends LRCrane/I/CtrlAutomaton { }
{
 states = x0 + x1 + x2 + x3 + x4 + x5
 events = ch + eoch + gr + eogr + gl + eogl
 controllableEvents = ch + gr + gl
 transition = x0->gl->x1
            + x1->eogl->x2
            + x2->ch->x3
            + x2->gr->x5
            + x3->eoch->x4
            + x4->gr->x5
            + x5->eogr->x0
 initialState = x0
 markedStates = x0
}

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

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