open BasicProperties[StateSpace, EventSet]

-- The LRCrane 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 { aLnV, aLpA, aLV, aLlA, aRnV, aRpA, aRV, aRlA,
                  m2lnV, m2lpA, m2lV, m2llA, m2rnV, m2rpA, m2rV, m2rlA,
                  yaLnV, yaLpA, yaLV, yaRnV, yaRV,
                  yaRlA, ym2lnV, ym2rnV, ym2rV }
enum EventSet { move2left, move2right, eoml, eomr,
                grab, release, wpGrabbed, wpReleased }

one sig G extends CtrlAutomaton { }
{
 states = aLnV + aLpA + aLV + aLlA + aRnV + aRpA + aRV + aRlA
        + m2lnV + m2lpA + m2lV + m2llA + m2rnV + m2rpA + m2rV + m2rlA
 events = move2left + move2right + eoml + eomr
        + grab + release + wpGrabbed + wpReleased
 controllableEvents = move2left + move2right + grab + release
 transition = aLnV->move2right->m2rnV
            + aLnV->grab->aLpA
            + aLpA->move2right->m2rpA
            + aLpA->wpGrabbed->aLV
            + aLV->move2right->m2rV
            + aLV->release->aLlA
            + aLlA->move2right->m2rlA
            + aLlA->wpReleased->aLnV
            + aRnV->move2left->m2lnV
            + aRnV->grab->aRpA
            + aRpA->move2left->m2lpA
            + aRpA->wpGrabbed->aRV
            + aRV->move2left->m2lV
            + aRV->release->aRlA
            + aRlA->move2left->m2llA
            + aRlA->wpReleased->aRnV
            + m2lnV->eoml->aLnV
            + m2lnV->grab->m2lpA
            + m2lpA->eoml->aLpA
            + m2lpA->wpGrabbed->m2lV
            + m2lV->eoml->aLV
            + m2lV->release->m2llA
            + m2llA->eoml->aLlA
            + m2llA->wpReleased->m2lnV
            + m2rnV->eomr->aRnV
            + m2rnV->grab->m2rpA
            + m2rpA->eomr->aRpA
            + m2rpA->wpGrabbed->m2rV
            + m2rV->eomr->aRV
            + m2rV->release->m2rlA
            + m2rlA->eomr->aRlA
            + m2rlA->wpReleased->m2rnV
 initialState = aRnV
 markedStates = aRnV
}

one sig H extends CtrlAutomaton { }
{
 states = yaLnV + yaLpA + yaLV + yaRnV + yaRV
        + yaRlA + ym2lnV + ym2rnV + ym2rV
 events = move2left + move2right + eoml + eomr
        + grab + release + wpGrabbed + wpReleased
 controllableEvents = move2left + move2right + grab + release
 transition = yaLnV->move2right->ym2rnV
            + yaLnV->grab->yaLpA
            + yaLpA->wpGrabbed->yaLV
            + yaLV->move2right->ym2rV
            + yaRnV->move2left->ym2lnV
            + yaRV->release->yaRlA
            + yaRlA->wpReleased->yaRnV
            + ym2lnV->eoml->yaLnV
            + ym2rnV->eomr->yaRnV
            + ym2rV->eomr->yaRV
 initialState = yaRnV
 markedStates = yaRnV
}

fun f: H.states->G.states
{
   yaLnV->aLnV + yaLpA->aLpA + yaLV->aLV + yaRnV->aRnV + yaRV->aRV
 + yaRlA->aRlA + ym2lnV->m2lnV + ym2rnV->m2rnV + ym2rV->m2rV
}

run { }

check IsGtrimmed { IsTrim[G] }
check IsHtrimmed { IsTrim[H] }
check IsHcontrollable { controllability[G, H, f] }