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

-- The distribution station 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, 2014.

enum StateSpace { IaRnVx0,   RaRnVx1,   WaRnVx1,  HaRnVx2,   Hm2lnVx2, HaLnVx3,
                  HaLpAx3,   HaLVx4,    IaLVx5,   RaLVx6,    Im2rVx5,  Rm2rVx6,
                  IaRVx7,    RaRVx8,    IaRlAx7,  WaRVx8,    RaRlAx8,  IaRnVx7,
                  HaRVx9,    WaRlAx8,   RaRnVx8,  Im2lnVx11, HaRlAx9,  WaRnVx8,
                  Rm2lnVx12, IaLnVx13,  HaRnVx9,  RaLnVx14,  IaLnVx16, Hm2lnVx9,
                  RaLnVx15,  Im2rnVx16, HaLnVx10, Rm2rnVx15,
                  x0, x1, x2, x3, x4 }
enum Input { wpa, inject, eoi, rearm, ch, eoch, oh, eooh, gr, eogr, gl, eogl, rst }
enum Output { dwpa, deogl, drst, epsilon }
fact
{
 no Distribution/A/SilentEvents
 epsilon = Distribution/I/SilentEvents
}

one sig lwpa, linject, leoi, lrearm,
        lch, leoch, loh, leooh, lgr, leogr, lgl, leogl, leogleps,
        lrst extends Distribution/Label { }

fact
{ -- causal map
 Sigma = lwpa->wpa      + linject->inject + leoi->eoi + lrearm->rearm
       + lch->ch        + leoch->eoch     + loh->oh   + leooh->eooh
       + lgr->gr        + leogr->eogr     + lgl->gl   + leogl->eogl
       + leogleps->eogl + lrst->rst
     T = lwpa->dwpa        + linject->epsilon + leoi->epsilon + lrearm->epsilon
       + lch->epsilon      + leoch->epsilon   + loh->epsilon  + leooh->epsilon
       + lgr->epsilon      + leogr->epsilon   + lgl->epsilon  + leogl->deogl
       + leogleps->epsilon + lrst->drst
}

one sig Agent extends Distribution/A/CtrlAutomaton { }
{
 states = IaRnVx0   + RaRnVx1   + WaRnVx1   + HaRnVx2   + Hm2lnVx2  + HaLnVx3
        + HaLpAx3   + HaLVx4    + IaLVx5    + RaLVx6    + Im2rVx5   + Rm2rVx6
        + IaRVx7    + RaRVx8    + IaRlAx7   + WaRVx8    + RaRlAx8   + IaRnVx7
        + HaRVx9    + WaRlAx8   + RaRnVx8   + Im2lnVx11 + HaRlAx9   + WaRnVx8
        + Rm2lnVx12 + IaLnVx13  + HaRnVx9   + RaLnVx14  + IaLnVx16  + Hm2lnVx9  
        + RaLnVx15  + Im2rnVx16 + HaLnVx10  + Rm2rnVx15
 events = lwpa + linject + leoi + lrearm
        + lch + leoch + loh + leooh + lgr + leogr + lgl + leogl + leogleps
        + lrst
 controllableEvents = linject + lrearm + lch + loh + lgr + lgl + lrst
 transition = IaRnVx0->lwpa->RaRnVx1
            + RaRnVx1->linject->WaRnVx1
            + WaRnVx1->leoi->HaRnVx2
            + HaRnVx2->lgl->Hm2lnVx2
            + Hm2lnVx2->leogleps->HaLnVx3
            + HaLnVx3->lch->HaLpAx3
            + HaLpAx3->leoch->HaLVx4
            + HaLVx4->lrearm->IaLVx5
            + IaLVx5->lwpa->RaLVx6
            + IaLVx5->lgr->Im2rVx5
            + RaLVx6->lgr->Rm2rVx6
            + Im2rVx5->lwpa->Rm2rVx6
            + Im2rVx5->leogr->IaRVx7
            + Rm2rVx6->leogr->RaRVx8
            + IaRVx7->lwpa->RaRVx8
            + IaRVx7->loh->IaRlAx7
            + RaRVx8->linject->WaRVx8
            + RaRVx8->loh->RaRlAx8
            + IaRlAx7->lwpa->RaRlAx8
            + IaRlAx7->leooh->IaRnVx7
            + WaRVx8->leoi->HaRVx9
            + WaRVx8->loh->WaRlAx8
            + RaRlAx8->linject->WaRlAx8
            + RaRlAx8->leooh->RaRnVx8
            + IaRnVx7->lwpa->RaRnVx8
            + IaRnVx7->lgl->Im2lnVx11
            + HaRVx9->loh->HaRlAx9
            + WaRlAx8->leoi->HaRlAx9
            + WaRlAx8->leooh->WaRnVx8
            + RaRnVx8->linject->WaRnVx8
            + Im2lnVx11->lwpa->Rm2lnVx12
            + Im2lnVx11->leogl->IaLnVx13
            + HaRlAx9->leooh->HaRnVx9
            + WaRnVx8->leoi->HaRnVx9
            + Rm2lnVx12->leogl->RaLnVx14
            + IaLnVx13->lwpa->RaLnVx14
            + IaLnVx13->lrst->IaLnVx16
            + HaRnVx9->lgl->Hm2lnVx9
            + RaLnVx14->lrst->RaLnVx15
            + IaLnVx16->lwpa->RaLnVx15
            + IaLnVx16->lgr->Im2rnVx16
            + Hm2lnVx9->leogl->HaLnVx10
            + RaLnVx15->lgr->Rm2rnVx15
            + Im2rnVx16->lwpa->Rm2rnVx15
            + Im2rnVx16->leogr->IaRnVx0
            + HaLnVx10->lrst->HaLnVx3
            + Rm2rnVx15->leogr->RaRnVx1
 initialState = IaRnVx0
 markedStates = IaRnVx0
}

one sig Interface extends Distribution/I/CtrlAutomaton { }
{
 states = x0 + x1 + x2 + x3 + x4
 events = dwpa + deogl + drst
 controllableEvents = drst
 transition = x0->dwpa->x4
            + x1->drst->x4
            + x2->drst->x0  + x2->dwpa->x1
            + x3->deogl->x1
            + x4->deogl->x2 + x4->dwpa->x3
 initialState = x0
 finalStates = x0
}

run { } for 1 but 50 SeqIdx, 1 Distribution/A/Walk, 1 Distribution/I/Walk

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