open SBCDES_Total_Observation[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 }
enum EventSet { move2left, move2right, eoml, eomr,
                grab, release, wpGrabbed, wpReleased }

one sig G extends Automaton { }
{
 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
}

fun Q[X: G.states] : G.states
{
 { x : X | not x in aLlA + aRpA + m2lpA + m2lV + m2llA + m2rpA + m2rlA}
}

one sig SFBCLRCrane
{
 f = SFBCEnabled[G, Q[G.states]]
}

run { } for 1

check solution
{
 Q[G.states] = NBC[G, Q[G.states]]
} for 1