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

-- Two trains on a circular railway composed of 8 sections from:
--   M. Makungu, M. Barbeau and R. St-Denis,
--   Synthesis of controllers of processes modeled as colored Petri nets,
--   Discrete Event Dynamic Systems: Theory and Applications,
--   9 (2), 1999, 147-169.
-- copyright Richard St-Denis, Universite de Sherbrooke, 2014.

enum StateSpace { s0_s3, s0_s4, s0_s5, s1_s3, s1_s4, s1_s5, s1_s6, s1_s7,
                  s2_s5, s2_s6, s2_s7, s3_s0, s3_s1, s3_s5, s3_s6, s3_s7,
                  s4_s0, s4_s1, s4_s7, s5_s0, s5_s1, s5_s2, s5_s3, s5_s7,
                  s6_s1, s6_s2, s6_s3, s7_s1, s7_s2, s7_s3, s7_s4, s7_s5,
                  x0, x1, x2, x3, x4 }
enum Input { t1_s0TOs1, t1_s1TOs2, t1_s2TOs3, t1_s3TOs4,
             t1_s4TOs5, t1_s5TOs6, t1_s6TOs7, t1_s7TOs0,
             t2_s0TOs1, t2_s1TOs2, t2_s2TOs3, t2_s3TOs4,
             t2_s4TOs5, t2_s5TOs6, t2_s6TOs7, t2_s7TOs0 }
enum Output { startup, stop, completed, epsilon }

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

one sig lt1_s0TOs1, lt1_s1TOs2, lt1_s2TOs3, lt1_s3TOs4,
        lt1_s4TOs5, lt1_s5TOs6, lt1_s6TOs7, lt1_s7TOs0,
        lt2_s0TOs1, lt2_s1TOs2, lt2_s2TOs3, lt2_s3TOs4,
        lt2_s4TOs5, lt2_s5TOs6, lt2_s6TOs7, lt2_s7TOs0 extends twoTrains/Label { }

fact
{ -- causal map
 Sigma = lt1_s0TOs1->t1_s0TOs1 + lt1_s1TOs2->t1_s1TOs2 + lt1_s2TOs3->t1_s2TOs3 + lt1_s3TOs4->t1_s3TOs4
       + lt1_s4TOs5->t1_s4TOs5 + lt1_s5TOs6->t1_s5TOs6 + lt1_s6TOs7->t1_s6TOs7 + lt1_s7TOs0->t1_s7TOs0
       + lt2_s0TOs1->t2_s0TOs1 + lt2_s1TOs2->t2_s1TOs2 + lt2_s2TOs3->t2_s2TOs3 + lt2_s3TOs4->t2_s3TOs4
       + lt2_s4TOs5->t2_s4TOs5 + lt2_s5TOs6->t2_s5TOs6 + lt2_s6TOs7->t2_s6TOs7 + lt2_s7TOs0->t2_s7TOs0
     T = lt1_s0TOs1->completed + lt1_s1TOs2->startup   + lt1_s2TOs3->epsilon   + lt1_s3TOs4->epsilon
       + lt1_s4TOs5->epsilon   + lt1_s5TOs6->epsilon   + lt1_s6TOs7->epsilon   + lt1_s7TOs0->stop
       + lt2_s0TOs1->epsilon   + lt2_s1TOs2->epsilon   + lt2_s2TOs3->epsilon   + lt2_s3TOs4->epsilon
       + lt2_s4TOs5->epsilon   + lt2_s5TOs6->epsilon   + lt2_s6TOs7->epsilon   + lt2_s7TOs0->epsilon
}

one sig Agent extends twoTrains/A/CtrlAutomaton { }
{
 states = s0_s3 + s0_s4 + s0_s5
        + s1_s3 + s1_s4 + s1_s5 + s1_s6 + s1_s7
        + s2_s5 + s2_s6 + s2_s7
        + s3_s0 + s3_s1 + s3_s5 + s3_s6 + s3_s7
        + s4_s0 + s4_s1 + s4_s7
        + s5_s0 + s5_s1 + s5_s2 + s5_s3 + s5_s7
        + s6_s1 + s6_s2 + s6_s3
        + s7_s1 + s7_s2 + s7_s3 + s7_s4 + s7_s5
 events = lt1_s0TOs1 + lt1_s1TOs2 + lt1_s2TOs3 + lt1_s3TOs4
        + lt1_s4TOs5 + lt1_s5TOs6 + lt1_s6TOs7 + lt1_s7TOs0
        + lt2_s0TOs1 + lt2_s1TOs2 + lt2_s2TOs3 + lt2_s3TOs4
        + lt2_s4TOs5 + lt2_s5TOs6 + lt2_s6TOs7 + lt2_s7TOs0
 controllableEvents = lt1_s1TOs2 + lt1_s3TOs4 + lt1_s5TOs6 + lt1_s7TOs0
                    + lt2_s1TOs2 + lt2_s3TOs4 + lt2_s5TOs6 + lt2_s7TOs0
 transition = s0_s3->lt1_s0TOs1->s1_s3 + s0_s3->lt2_s3TOs4->s0_s4 + s0_s4->lt1_s0TOs1->s1_s4
            + s0_s4->lt2_s4TOs5->s0_s5 + s0_s5->lt1_s0TOs1->s1_s5 
            + s1_s3->lt2_s3TOs4->s1_s4 + s1_s4->lt2_s4TOs5->s1_s5 + s1_s5->lt1_s1TOs2->s2_s5
            + s1_s5->lt2_s5TOs6->s1_s6 + s1_s6->lt1_s1TOs2->s2_s6 + s1_s6->lt2_s6TOs7->s1_s7
            + s1_s7->lt1_s1TOs2->s2_s7  
            + s2_s5->lt1_s2TOs3->s3_s5 + s2_s5->lt2_s5TOs6->s2_s6 + s2_s6->lt1_s2TOs3->s3_s6
            + s2_s6->lt2_s6TOs7->s2_s7 + s2_s7->lt1_s2TOs3->s3_s7
            + s3_s0->lt1_s3TOs4->s4_s0 + s3_s0->lt2_s0TOs1->s3_s1 + s3_s1->lt1_s3TOs4->s4_s1
            + s3_s5->lt2_s5TOs6->s3_s6 + s3_s6->lt2_s6TOs7->s3_s7 + s3_s7->lt1_s3TOs4->s4_s7
            + s3_s7->lt2_s7TOs0->s3_s0
            + s4_s0->lt1_s4TOs5->s5_s0 + s4_s0->lt2_s0TOs1->s4_s1 + s4_s1->lt1_s4TOs5->s5_s1
            + s4_s7->lt1_s4TOs5->s5_s7 + s4_s7->lt2_s7TOs0->s4_s0
            + s5_s0->lt2_s0TOs1->s5_s1 + s5_s1->lt1_s5TOs6->s6_s1 + s5_s1->lt2_s1TOs2->s5_s2
            + s5_s2->lt1_s5TOs6->s6_s2 + s5_s2->lt2_s2TOs3->s5_s3 + s5_s3->lt1_s5TOs6->s6_s3
            + s5_s7->lt2_s7TOs0->s5_s0
            + s6_s1->lt1_s6TOs7->s7_s1 + s6_s1->lt2_s1TOs2->s6_s2 + s6_s2->lt1_s6TOs7->s7_s2 
            + s6_s2->lt2_s2TOs3->s6_s3 + s6_s3->lt1_s6TOs7->s7_s3
            + s7_s1->lt2_s1TOs2->s7_s2 + s7_s2->lt2_s2TOs3->s7_s3 + s7_s3->lt1_s7TOs0->s0_s3
            + s7_s3->lt2_s3TOs4->s7_s4 + s7_s4->lt1_s7TOs0->s0_s4 + s7_s4->lt2_s4TOs5->s7_s5
            + s7_s5->lt1_s7TOs0->s0_s5
 initialState = s1_s7
 markedStates = s1_s7
}

one sig Interface extends twoTrains/I/CtrlAutomaton { }
{
 states = x0 + x1 + x2 + x3 + x4 
 events = startup + stop + completed
 controllableEvents = startup + stop
 transition = x0->startup->x1 + x1->stop->x2 + x2->completed->x3
            + x3->startup->x4 + x4->stop->x2
 initialState = x0
 finalStates = x0 + x3
}

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

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