open SBCDES_Total_Observation[StateSpace, EventSet]

-- Two trains on a circular railway composed of 10 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, 2013.

enum StateSpace { s0_s0, s0_s1, s0_s2, s0_s3, s0_s4,
                  s0_s5, s0_s6, s0_s7, s0_s8, s0_s9,
                  s1_s0, s1_s1, s1_s2, s1_s3, s1_s4,
                  s1_s5, s1_s6, s1_s7, s1_s8, s1_s9,
                  s2_s0, s2_s1, s2_s2, s2_s3, s2_s4,
                  s2_s5, s2_s6, s2_s7, s2_s8, s2_s9,
                  s3_s0, s3_s1, s3_s2, s3_s3, s3_s4,
                  s3_s5, s3_s6, s3_s7, s3_s8, s3_s9,
                  s4_s0, s4_s1, s4_s2, s4_s3, s4_s4,
                  s4_s5, s4_s6, s4_s7, s4_s8, s4_s9,
                  s5_s0, s5_s1, s5_s2, s5_s3, s5_s4,
                  s5_s5, s5_s6, s5_s7, s5_s8, s5_s9,
                  s6_s0, s6_s1, s6_s2, s6_s3, s6_s4,
                  s6_s5, s6_s6, s6_s7, s6_s8, s6_s9,
                  s7_s0, s7_s1, s7_s2, s7_s3, s7_s4,
                  s7_s5, s7_s6, s7_s7, s7_s8, s7_s9,
                  s8_s0, s8_s1, s8_s2, s8_s3, s8_s4,
                  s8_s5, s8_s6, s8_s7, s8_s8, s8_s9,
                  s9_s0, s9_s1, s9_s2, s9_s3, s9_s4,
                  s9_s5, s9_s6, s9_s7, s9_s8, s9_s9 }

enum LocalStateSpace { s0, s1, s2, s3, s4, s5, s6, s7, s8, s9 }

enum EventSet { t1_s0TOs1, t1_s1TOs2, t1_s2TOs3, t1_s3TOs4, t1_s4TOs5,
                t1_s5TOs6, t1_s6TOs7, t1_s7TOs8, t1_s8TOs9, t1_s9TOs0,
                t2_s0TOs1, t2_s1TOs2, t2_s2TOs3, t2_s3TOs4, t2_s4TOs5,
                t2_s5TOs6, t2_s6TOs7, t2_s7TOs8, t2_s8TOs9, t2_s9TOs0 }

one sig twoTrains10 extends Automaton
{
 localStates   : set LocalStateSpace,
 firstProcess  : set StateSpace -> LocalStateSpace,
 secondProcess : set StateSpace -> LocalStateSpace,
 nextSection   : set LocalStateSpace -> LocalStateSpace,
 prevSection   : set LocalStateSpace -> LocalStateSpace
}
{
 states = s0_s0 + s0_s1 + s0_s2 + s0_s3 + s0_s4
        + s0_s5 + s0_s6 + s0_s7 + s0_s8 + s0_s9
        + s1_s0 + s1_s1 + s1_s2 + s1_s3 + s1_s4
        + s1_s5 + s1_s6 + s1_s7 + s1_s8 + s1_s9
        + s2_s0 + s2_s1 + s2_s2 + s2_s3 + s2_s4
        + s2_s5 + s2_s6 + s2_s7 + s2_s8 + s2_s9
        + s3_s0 + s3_s1 + s3_s2 + s3_s3 + s3_s4
        + s3_s5 + s3_s6 + s3_s7 + s3_s8 + s3_s9
        + s4_s0 + s4_s1 + s4_s2 + s4_s3 + s4_s4
        + s4_s5 + s4_s6 + s4_s7 + s4_s8 + s4_s9
        + s5_s0 + s5_s1 + s5_s2 + s5_s3 + s5_s4
        + s5_s5 + s5_s6 + s5_s7 + s5_s8 + s5_s9
        + s6_s0 + s6_s1 + s6_s2 + s6_s3 + s6_s4
        + s6_s5 + s6_s6 + s6_s7 + s6_s8 + s6_s9
        + s7_s0 + s7_s1 + s7_s2 + s7_s3 + s7_s4
        + s7_s5 + s7_s6 + s7_s7 + s7_s8 + s7_s9
        + s8_s0 + s8_s1 + s8_s2 + s8_s3 + s8_s4
        + s8_s5 + s8_s6 + s8_s7 + s8_s8 + s8_s9
        + s9_s0 + s9_s1 + s9_s2 + s9_s3 + s9_s4
        + s9_s5 + s9_s6 + s9_s7 + s9_s8 + s9_s9
 localStates = s0 + s1 + s2 + s3 + s4 + s5 + s6 + s7 + s8 + s9
 firstProcess = (s0_s0 -> s0) + (s0_s1 -> s0) + (s0_s2 -> s0) + (s0_s3 -> s0) + (s0_s4 -> s0)
              + (s0_s5 -> s0) + (s0_s6 -> s0) + (s0_s7 -> s0) + (s0_s8 -> s0) + (s0_s9 -> s0)
              + (s1_s0 -> s1) + (s1_s1 -> s1) + (s1_s2 -> s1) + (s1_s3 -> s1) + (s1_s4 -> s1)
              + (s1_s5 -> s1) + (s1_s6 -> s1) + (s1_s7 -> s1) + (s1_s8 -> s1) + (s1_s9 -> s1)
              + (s2_s0 -> s2) + (s2_s1 -> s2) + (s2_s2 -> s2) + (s2_s3 -> s2) + (s2_s4 -> s2)
              + (s2_s5 -> s2) + (s2_s6 -> s2) + (s2_s7 -> s2) + (s2_s8 -> s2) + (s2_s9 -> s2)
              + (s3_s0 -> s3) + (s3_s1 -> s3) + (s3_s2 -> s3) + (s3_s3 -> s3) + (s3_s4 -> s3)
              + (s3_s5 -> s3) + (s3_s6 -> s3) + (s3_s7 -> s3) + (s3_s8 -> s3) + (s3_s9 -> s3)
              + (s4_s0 -> s4) + (s4_s1 -> s4) + (s4_s2 -> s4) + (s4_s3 -> s4) + (s4_s4 -> s4)
              + (s4_s5 -> s4) + (s4_s6 -> s4) + (s4_s7 -> s4) + (s4_s8 -> s4) + (s4_s9 -> s4)
              + (s5_s0 -> s5) + (s5_s1 -> s5) + (s5_s2 -> s5) + (s5_s3 -> s5) + (s5_s4 -> s5)
              + (s5_s5 -> s5) + (s5_s6 -> s5) + (s5_s7 -> s5) + (s5_s8 -> s5) + (s5_s9 -> s5)
              + (s6_s0 -> s6) + (s6_s1 -> s6) + (s6_s2 -> s6) + (s6_s3 -> s6) + (s6_s4 -> s6)
              + (s6_s5 -> s6) + (s6_s6 -> s6) + (s6_s7 -> s6) + (s6_s8 -> s6) + (s6_s9 -> s6)
              + (s7_s0 -> s7) + (s7_s1 -> s7) + (s7_s2 -> s7) + (s7_s3 -> s7) + (s7_s4 -> s7)
              + (s7_s5 -> s7) + (s7_s6 -> s7) + (s7_s7 -> s7) + (s7_s8 -> s7) + (s7_s9 -> s7)
              + (s8_s0 -> s8) + (s8_s1 -> s8) + (s8_s2 -> s8) + (s8_s3 -> s8) + (s8_s4 -> s8)
              + (s8_s5 -> s8) + (s8_s6 -> s8) + (s8_s7 -> s8) + (s8_s8 -> s8) + (s8_s9 -> s8)
              + (s9_s0 -> s9) + (s9_s1 -> s9) + (s9_s2 -> s9) + (s9_s3 -> s9) + (s9_s4 -> s9)
              + (s9_s5 -> s9) + (s9_s6 -> s9) + (s9_s7 -> s9) + (s9_s8 -> s9) + (s9_s9 -> s9)
 secondProcess = (s0_s0 -> s0) + (s0_s1 -> s1) + (s0_s2 -> s2) + (s0_s3 -> s3) + (s0_s4 -> s4)
               + (s0_s5 -> s5) + (s0_s6 -> s6) + (s0_s7 -> s7) + (s0_s8 -> s8) + (s0_s9 -> s9)
               + (s1_s0 -> s0) + (s1_s1 -> s1) + (s1_s2 -> s2) + (s1_s3 -> s3) + (s1_s4 -> s4)
               + (s1_s5 -> s5) + (s1_s6 -> s6) + (s1_s7 -> s7) + (s1_s8 -> s8) + (s1_s9 -> s9)
               + (s2_s0 -> s0) + (s2_s1 -> s1) + (s2_s2 -> s2) + (s2_s3 -> s3) + (s2_s4 -> s4)
               + (s2_s5 -> s5) + (s2_s6 -> s6) + (s2_s7 -> s7) + (s2_s8 -> s8) + (s2_s9 -> s9)
               + (s3_s0 -> s0) + (s3_s1 -> s1) + (s3_s2 -> s2) + (s3_s3 -> s3) + (s3_s4 -> s4)
               + (s3_s5 -> s5) + (s3_s6 -> s6) + (s3_s7 -> s7) + (s3_s8 -> s8) + (s3_s9 -> s9)
               + (s4_s0 -> s0) + (s4_s1 -> s1) + (s4_s2 -> s2) + (s4_s3 -> s3) + (s4_s4 -> s4)
               + (s4_s5 -> s5) + (s4_s6 -> s6) + (s4_s7 -> s7) + (s4_s8 -> s8) + (s4_s9 -> s9)
               + (s5_s0 -> s0) + (s5_s1 -> s1) + (s5_s2 -> s2) + (s5_s3 -> s3) + (s5_s4 -> s4)
               + (s5_s5 -> s5) + (s5_s6 -> s6) + (s5_s7 -> s7) + (s5_s8 -> s8) + (s5_s9 -> s9)
               + (s6_s0 -> s0) + (s6_s1 -> s1) + (s6_s2 -> s2) + (s6_s3 -> s3) + (s6_s4 -> s4)
               + (s6_s5 -> s5) + (s6_s6 -> s6) + (s6_s7 -> s7) + (s6_s8 -> s8) + (s6_s9 -> s9)
               + (s7_s0 -> s0) + (s7_s1 -> s1) + (s7_s2 -> s2) + (s7_s3 -> s3) + (s7_s4 -> s4)
               + (s7_s5 -> s5) + (s7_s6 -> s6) + (s7_s7 -> s7) + (s7_s8 -> s8) + (s7_s9 -> s9)
               + (s8_s0 -> s0) + (s8_s1 -> s1) + (s8_s2 -> s2) + (s8_s3 -> s3) + (s8_s4 -> s4)
               + (s8_s5 -> s5) + (s8_s6 -> s6) + (s8_s7 -> s7) + (s8_s8 -> s8) + (s8_s9 -> s9)
               + (s9_s0 -> s0) + (s9_s1 -> s1) + (s9_s2 -> s2) + (s9_s3 -> s3) + (s9_s4 -> s4)
               + (s9_s5 -> s5) + (s9_s6 -> s6) + (s9_s7 -> s7) + (s9_s8 -> s8) + (s9_s9 -> s9)

 nextSection = (s0 -> s1) + (s1 -> s2) + (s2 -> s3) + (s3 -> s4) + (s4 -> s5)
             + (s5 -> s6) + (s6 -> s7) + (s7 -> s8) + (s8 -> s9) + (s9 -> s0)
 prevSection = (s0 -> s9) + (s1 -> s0) + (s2 -> s1) + (s3 -> s2) + (s4 -> s3)
             + (s5 -> s4) + (s6 -> s5) + (s7 -> s6) + (s8 -> s7) + (s9 -> s8)
 events = t1_s0TOs1 + t1_s1TOs2 + t1_s2TOs3 + t1_s3TOs4 + t1_s4TOs5
        + t1_s5TOs6 + t1_s6TOs7 + t1_s7TOs8 + t1_s8TOs9 + t1_s9TOs0
        + t2_s0TOs1 + t2_s1TOs2 + t2_s2TOs3 + t2_s3TOs4 + t2_s4TOs5
        + t2_s5TOs6 + t2_s6TOs7 + t2_s7TOs8 + t2_s8TOs9 + t2_s9TOs0
 controllableEvents = t1_s1TOs2 + t1_s3TOs4 + t1_s5TOs6 + t1_s7TOs8 + t1_s9TOs0
                    + t2_s1TOs2 + t2_s3TOs4 + t2_s5TOs6 + t2_s7TOs8 + t2_s9TOs0
 initialState = s1_s3
 markedStates = s1_s3
 transition = s0_s0->t1_s0TOs1->s1_s0 + s0_s0->t2_s0TOs1->s0_s1 + s0_s1->t1_s0TOs1->s1_s1
            + s0_s1->t2_s1TOs2->s0_s2 + s0_s2->t1_s0TOs1->s1_s2 + s0_s2->t2_s2TOs3->s0_s3
            + s0_s3->t1_s0TOs1->s1_s3 + s0_s3->t2_s3TOs4->s0_s4 + s0_s4->t1_s0TOs1->s1_s4
            + s0_s4->t2_s4TOs5->s0_s5 + s0_s5->t1_s0TOs1->s1_s5 + s0_s5->t2_s5TOs6->s0_s6
            + s0_s6->t1_s0TOs1->s1_s6 + s0_s6->t2_s6TOs7->s0_s7 + s0_s7->t1_s0TOs1->s1_s7
            + s0_s7->t2_s7TOs8->s0_s8 + s0_s8->t1_s0TOs1->s1_s8 + s0_s8->t2_s8TOs9->s0_s9
            + s0_s9->t1_s0TOs1->s1_s9 + s0_s9->t2_s9TOs0->s0_s0
            + s1_s0->t1_s1TOs2->s2_s0 + s1_s0->t2_s0TOs1->s1_s1 + s1_s1->t1_s1TOs2->s2_s1
            + s1_s1->t2_s1TOs2->s1_s2 + s1_s2->t1_s1TOs2->s2_s2 + s1_s2->t2_s2TOs3->s1_s3
            + s1_s3->t1_s1TOs2->s2_s3 + s1_s3->t2_s3TOs4->s1_s4 + s1_s4->t1_s1TOs2->s2_s4
            + s1_s4->t2_s4TOs5->s1_s5 + s1_s5->t1_s1TOs2->s2_s5 + s1_s5->t2_s5TOs6->s1_s6
            + s1_s6->t1_s1TOs2->s2_s6 + s1_s6->t2_s6TOs7->s1_s7 + s1_s7->t1_s1TOs2->s2_s7
            + s1_s7->t2_s7TOs8->s1_s8 + s1_s8->t1_s1TOs2->s2_s8 + s1_s8->t2_s8TOs9->s1_s9
            + s1_s9->t1_s1TOs2->s2_s9 + s1_s9->t2_s9TOs0->s1_s0
            + s2_s0->t1_s2TOs3->s3_s0 + s2_s0->t2_s0TOs1->s2_s1 + s2_s1->t1_s2TOs3->s3_s1
            + s2_s1->t2_s1TOs2->s2_s2 + s2_s2->t1_s2TOs3->s3_s2 + s2_s2->t2_s2TOs3->s2_s3
            + s2_s3->t1_s2TOs3->s3_s3 + s2_s3->t2_s3TOs4->s2_s4 + s2_s4->t1_s2TOs3->s3_s4
            + s2_s4->t2_s4TOs5->s2_s5 + s2_s5->t1_s2TOs3->s3_s5 + s2_s5->t2_s5TOs6->s2_s6
            + s2_s6->t1_s2TOs3->s3_s6 + s2_s6->t2_s6TOs7->s2_s7 + s2_s7->t1_s2TOs3->s3_s7
            + s2_s7->t2_s7TOs8->s2_s8 + s2_s8->t1_s2TOs3->s3_s8 + s2_s8->t2_s8TOs9->s2_s9
            + s2_s9->t1_s2TOs3->s3_s9 + s2_s9->t2_s9TOs0->s2_s0
            + s3_s0->t1_s3TOs4->s4_s0 + s3_s0->t2_s0TOs1->s3_s1 + s3_s1->t1_s3TOs4->s4_s1
            + s3_s1->t2_s1TOs2->s3_s2 + s3_s2->t1_s3TOs4->s4_s2 + s3_s2->t2_s2TOs3->s3_s3
            + s3_s3->t1_s3TOs4->s4_s3 + s3_s3->t2_s3TOs4->s3_s4 + s3_s4->t1_s3TOs4->s4_s4
            + s3_s4->t2_s4TOs5->s3_s5 + s3_s5->t1_s3TOs4->s4_s5 + s3_s5->t2_s5TOs6->s3_s6
            + s3_s6->t1_s3TOs4->s4_s6 + s3_s6->t2_s6TOs7->s3_s7 + s3_s7->t1_s3TOs4->s4_s7
            + s3_s7->t2_s7TOs8->s3_s8 + s3_s8->t1_s3TOs4->s4_s8 + s3_s8->t2_s8TOs9->s3_s9
            + s3_s9->t1_s3TOs4->s4_s9 + s3_s9->t2_s9TOs0->s3_s0
            + s4_s0->t1_s4TOs5->s5_s0 + s4_s0->t2_s0TOs1->s4_s1 + s4_s1->t1_s4TOs5->s5_s1
            + s4_s1->t2_s1TOs2->s4_s2 + s4_s2->t1_s4TOs5->s5_s2 + s4_s2->t2_s2TOs3->s4_s3
            + s4_s3->t1_s4TOs5->s5_s3 + s4_s3->t2_s3TOs4->s4_s4 + s4_s4->t1_s4TOs5->s5_s4
            + s4_s4->t2_s4TOs5->s4_s5 + s4_s5->t1_s4TOs5->s5_s5 + s4_s5->t2_s5TOs6->s4_s6
            + s4_s6->t1_s4TOs5->s5_s6 + s4_s6->t2_s6TOs7->s4_s7 + s4_s7->t1_s4TOs5->s5_s7
            + s4_s7->t2_s7TOs8->s4_s8 + s4_s8->t1_s4TOs5->s5_s8 + s4_s8->t2_s8TOs9->s4_s9
            + s4_s9->t1_s4TOs5->s5_s9 + s4_s9->t2_s9TOs0->s4_s0
            + s5_s0->t1_s5TOs6->s6_s0 + s5_s0->t2_s0TOs1->s5_s1 + s5_s1->t1_s5TOs6->s6_s1
            + s5_s1->t2_s1TOs2->s5_s2 + s5_s2->t1_s5TOs6->s6_s2 + s5_s2->t2_s2TOs3->s5_s3
            + s5_s3->t1_s5TOs6->s6_s3 + s5_s3->t2_s3TOs4->s5_s4 + s5_s4->t1_s5TOs6->s6_s4
            + s5_s4->t2_s4TOs5->s5_s5 + s5_s5->t1_s5TOs6->s6_s5 + s5_s5->t2_s5TOs6->s5_s6
            + s5_s6->t1_s5TOs6->s6_s6 + s5_s6->t2_s6TOs7->s5_s7 + s5_s7->t1_s5TOs6->s6_s7
            + s5_s7->t2_s7TOs8->s5_s8 + s5_s8->t1_s5TOs6->s6_s8 + s5_s8->t2_s8TOs9->s5_s9
            + s5_s9->t1_s5TOs6->s6_s9 + s5_s9->t2_s9TOs0->s5_s0
            + s6_s0->t1_s6TOs7->s7_s0 + s6_s0->t2_s0TOs1->s6_s1 + s6_s1->t1_s6TOs7->s7_s1
            + s6_s1->t2_s1TOs2->s6_s2 + s6_s2->t1_s6TOs7->s7_s2 + s6_s2->t2_s2TOs3->s6_s3
            + s6_s3->t1_s6TOs7->s7_s3 + s6_s3->t2_s3TOs4->s6_s4 + s6_s4->t1_s6TOs7->s7_s4
            + s6_s4->t2_s4TOs5->s6_s5 + s6_s5->t1_s6TOs7->s7_s5 + s6_s5->t2_s5TOs6->s6_s6
            + s6_s6->t1_s6TOs7->s7_s6 + s6_s6->t2_s6TOs7->s6_s7 + s6_s7->t1_s6TOs7->s7_s7
            + s6_s7->t2_s7TOs8->s6_s8 + s6_s8->t1_s6TOs7->s7_s8 + s6_s8->t2_s8TOs9->s6_s9
            + s6_s9->t1_s6TOs7->s7_s9 + s6_s9->t2_s9TOs0->s6_s0
            + s7_s0->t1_s7TOs8->s8_s0 + s7_s0->t2_s0TOs1->s7_s1 + s7_s1->t1_s7TOs8->s8_s1
            + s7_s1->t2_s1TOs2->s7_s2 + s7_s2->t1_s7TOs8->s8_s2 + s7_s2->t2_s2TOs3->s7_s3
            + s7_s3->t1_s7TOs8->s8_s3 + s7_s3->t2_s3TOs4->s7_s4 + s7_s4->t1_s7TOs8->s8_s4
            + s7_s4->t2_s4TOs5->s7_s5 + s7_s5->t1_s7TOs8->s8_s5 + s7_s5->t2_s5TOs6->s7_s6
            + s7_s6->t1_s7TOs8->s8_s6 + s7_s6->t2_s6TOs7->s7_s7 + s7_s7->t1_s7TOs8->s8_s7
            + s7_s7->t2_s7TOs8->s7_s8 + s7_s8->t1_s7TOs8->s8_s8 + s7_s8->t2_s8TOs9->s7_s9
            + s7_s9->t1_s7TOs8->s8_s9 + s7_s9->t2_s9TOs0->s7_s0
            + s8_s0->t1_s8TOs9->s9_s0 + s8_s0->t2_s0TOs1->s8_s1 + s8_s1->t1_s8TOs9->s9_s1
            + s8_s1->t2_s1TOs2->s8_s2 + s8_s2->t1_s8TOs9->s9_s2 + s8_s2->t2_s2TOs3->s8_s3
            + s8_s3->t1_s8TOs9->s9_s3 + s8_s3->t2_s3TOs4->s8_s4 + s8_s4->t1_s8TOs9->s9_s4
            + s8_s4->t2_s4TOs5->s8_s5 + s8_s5->t1_s8TOs9->s9_s5 + s8_s5->t2_s5TOs6->s8_s6
            + s8_s6->t1_s8TOs9->s9_s6 + s8_s6->t2_s6TOs7->s8_s7 + s8_s7->t1_s8TOs9->s9_s7
            + s8_s7->t2_s7TOs8->s8_s8 + s8_s8->t1_s8TOs9->s9_s8 + s8_s8->t2_s8TOs9->s8_s9
            + s8_s9->t1_s8TOs9->s9_s9 + s8_s9->t2_s9TOs0->s8_s0
            + s9_s0->t1_s9TOs0->s0_s0 + s9_s0->t2_s0TOs1->s9_s1 + s9_s1->t1_s9TOs0->s0_s1
            + s9_s1->t2_s1TOs2->s9_s2 + s9_s2->t1_s9TOs0->s0_s2 + s9_s2->t2_s2TOs3->s9_s3
            + s9_s3->t1_s9TOs0->s0_s3 + s9_s3->t2_s3TOs4->s9_s4 + s9_s4->t1_s9TOs0->s0_s4
            + s9_s4->t2_s4TOs5->s9_s5 + s9_s5->t1_s9TOs0->s0_s5 + s9_s5->t2_s5TOs6->s9_s6
            + s9_s6->t1_s9TOs0->s0_s6 + s9_s6->t2_s6TOs7->s9_s7 + s9_s7->t1_s9TOs0->s0_s7
            + s9_s7->t2_s7TOs8->s9_s8 + s9_s8->t1_s9TOs0->s0_s8 + s9_s8->t2_s8TOs9->s9_s9
            + s9_s9->t1_s9TOs0->s0_s9 + s9_s9->t2_s9TOs0->s9_s0
}

pred OnSameSection[x: one twoTrains10.states]
{
 x.(twoTrains10.firstProcess) = x.(twoTrains10.secondProcess)
}

pred OnAdjacentSections[x: one twoTrains10.states]
{
    (twoTrains10.nextSection[x.(twoTrains10.firstProcess)] = x.(twoTrains10.secondProcess))
 or (twoTrains10.prevSection[x.(twoTrains10.firstProcess)] = x.(twoTrains10.secondProcess))
}

fun Q[X : set twoTrains10.states] : twoTrains10.states
{ -- The two trains must be separated by at least one section.
 { x : X | not (OnSameSection[x] or OnAdjacentSections[x]) }
}

run { } for 1

sig NBCQ in StateSpace { }

fact
{
 NBCQ in twoTrains10.states
}

/*
fun Q1st1[X :twoTrains10.states] : twoTrains10.states
{ -- predicate obtained after one iteration
   s0_s3 + s0_s4 + s0_s5 + s0_s6 + s0_s7
 + s1_s3 + s1_s4 + s1_s5 + s1_s6 + s1_s7 + s1_s8 + s1_s9
 + s2_s5 + s2_s6 + s2_s7 + s2_s8 + s2_s9
 + s3_s0 + s3_s1 + s3_s5 + s3_s6 + s3_s7 + s3_s8 + s3_s9
 + s4_s0 + s4_s1 + s4_s7 + s4_s8 + s4_s9
 + s5_s0 + s5_s1 + s5_s2 + s5_s3 + s5_s7 + s5_s8 + s5_s9
 + s6_s0 + s6_s1 + s6_s2 + s6_s3 + s6_s9
 + s7_s0 + s7_s1 + s7_s2 + s7_s3 + s7_s4 + s7_s5 + s7_s9
 + s8_s1 + s8_s2 + s8_s3 + s8_s4 + s8_s5
 + s9_s1 + s9_s2 + s9_s3 + s9_s4 + s9_s5 + s9_s6 + s9_s7
}
*/

run generateStrongerPredicate1stStrategy
{  -- use successively with Q and Q1st1
 NBCQ = NBC[twoTrains10, Q[twoTrains10.states]]
}

/*
fun Q2nd1[X :twoTrains10.states] : twoTrains10.states
{ -- NCQ predicate obtained after zero iteration
 s1_s3
}

fun Q2nd2[X :twoTrains10.states] : twoTrains10.states
{ -- NCQ predicate obtained after zero iteration
   s0_s3 + s0_s4 + s0_s5 + s0_s6 + s0_s7
 + s1_s3 + s1_s4 + s1_s5 + s1_s6 + s1_s7
 + s2_s5 + s2_s7
 + s3_s5 + s3_s6 + s3_s7
 + s4_s7
 + s5_s0 + s5_s1 + s5_s7 + s5_s8 + s5_s9
 + s6_s1
 + s7_s1
 + s8_s1
 + s9_s1 + s9_s2 + s9_s3
}

fun Q2nd3[X :twoTrains10.states] : twoTrains10.states
{ -- NCQ predicate obtained after zero iteration
   s0_s3 + s0_s4 + s0_s5 + s0_s6 + s0_s7
 + s1_s3 + s1_s4 + s1_s5 + s1_s6 + s1_s7
 + s2_s5 + s2_s6 + s2_s7
 + s3_s5 + s3_s6 + s3_s7
 + s4_s7
 + s5_s0 + s5_s1 + s5_s7 + s5_s8 + s5_s9
 + s6_s1
 + s7_s1
 + s8_s1
 + s9_s1 + s9_s2 + s9_s3
}

fun Q2nd4[X :twoTrains10.states] : twoTrains10.states
{ -- NCQ predicate obtained after zero iteration
   s0_s3 + s0_s4 + s0_s5 + s0_s6 + s0_s7
 + s1_s3 + s1_s4 + s1_s5 + s1_s6 + s1_s7
 + s2_s5 + s2_s6 + s2_s7
 + s3_s5 + s3_s6 + s3_s7 + s3_s8 + s3_s9
 + s4_s7 + s4_s9
 + s5_s0 + s5_s1 + s5_s7 + s5_s8 + s5_s9
 + s6_s1
 + s7_s1
 + s8_s1
 + s9_s1 + s9_s2 + s9_s3
}

fun Q2nd5[X :twoTrains10.states] : twoTrains10.states
{ -- NCQ predicate obtained after zero iteration
   s0_s3 + s0_s4 + s0_s5 + s0_s6 + s0_s7
 + s1_s3 + s1_s4 + s1_s5 + s1_s6 + s1_s7 + s1_s8 + s1_s9
 + s2_s5 + s2_s6 + s2_s7 + s2_s9
 + s3_s5 + s3_s6 + s3_s7 + s3_s8 + s3_s9
 + s4_s7 + s4_s9
 + s5_s0 + s5_s1 + s5_s7 + s5_s8 + s5_s9
 + s6_s1
 + s7_s1
 + s8_s1
 + s9_s1 + s9_s2 + s9_s3
}

fun Q2nd6[X :twoTrains10.states] : twoTrains10.states
{ -- NCQ predicate obtained after zero iteration
   s0_s3 + s0_s4 + s0_s5 + s0_s6 + s0_s7
 + s1_s3 + s1_s4 + s1_s5 + s1_s6 + s1_s7 + s1_s8 + s1_s9
 + s2_s5 + s2_s6 + s2_s7 + s2_s9
 + s3_s0 + s3_s1 + s3_s5 + s3_s6 + s3_s7 + s3_s8 + s3_s9
 + s4_s1 + s4_s7 + s4_s9
 + s5_s0 + s5_s1 + s5_s7 + s5_s8 + s5_s9
 + s6_s1
 + s7_s1
 + s8_s1
 + s9_s1 + s9_s2 + s9_s3
}

fun Q2nd7[X :twoTrains10.states] : twoTrains10.states
{ -- NCQ predicate obtained after zero iteration
   s0_s3 + s0_s4 + s0_s5 + s0_s6 + s0_s7
 + s1_s3 + s1_s4 + s1_s5 + s1_s6 + s1_s7 + s1_s8 + s1_s9
 + s2_s5 + s2_s6 + s2_s7 + s2_s8 + s2_s9
 + s3_s0 + s3_s1 + s3_s5 + s3_s6 + s3_s7 + s3_s8 + s3_s9
 + s4_s1 + s4_s7 + s4_s9
 + s5_s0 + s5_s1 + s5_s7 + s5_s8 + s5_s9
 + s6_s1
 + s7_s1
 + s8_s1
 + s9_s1 + s9_s2 + s9_s3
}

fun Q2nd8[X :twoTrains10.states] : twoTrains10.states
{ -- NCQ predicate obtained after zero iteration
   s0_s3 + s0_s4 + s0_s5 + s0_s6 + s0_s7
 + s1_s3 + s1_s4 + s1_s5 + s1_s6 + s1_s7 + s1_s8 + s1_s9
 + s2_s5 + s2_s6 + s2_s7 + s2_s8 + s2_s9
 + s3_s0 + s3_s1 + s3_s5 + s3_s6 + s3_s7 + s3_s8 + s3_s9
 + s4_s0 + s4_s1 + s4_s7 + s4_s9
 + s5_s0 + s5_s1 + s5_s7 + s5_s8 + s5_s9
 + s6_s1
 + s7_s1
 + s8_s1
 + s9_s1 + s9_s2 + s9_s3
}

fun Q2nd9[X :twoTrains10.states] : twoTrains10.states
{ -- NCQ predicate obtained after zero iteration
   s0_s3 + s0_s4 + s0_s5 + s0_s6 + s0_s7
 + s1_s3 + s1_s4 + s1_s5 + s1_s6 + s1_s7 + s1_s8 + s1_s9
 + s2_s5 + s2_s6 + s2_s7 + s2_s8 + s2_s9
 + s3_s0 + s3_s1 + s3_s5 + s3_s6 + s3_s7 + s3_s8 + s3_s9
 + s4_s0 + s4_s1 + s4_s7 + s4_s8 + s4_s9
 + s5_s0 + s5_s1 + s5_s7 + s5_s8 + s5_s9
 + s6_s1
 + s7_s1
 + s8_s1
 + s9_s1 + s9_s2 + s9_s3
}

fun Q2nd10[X :twoTrains10.states] : twoTrains10.states
{ -- NCQ predicate obtained after zero iteration
   s0_s3 + s0_s4 + s0_s5 + s0_s6 + s0_s7
 + s1_s3 + s1_s4 + s1_s5 + s1_s6 + s1_s7 + s1_s8 + s1_s9
 + s2_s5 + s2_s6 + s2_s7 + s2_s8 + s2_s9
 + s3_s0 + s3_s1 + s3_s5 + s3_s6 + s3_s7 + s3_s8 + s3_s9
 + s4_s0 + s4_s1 + s4_s7 + s4_s8 + s4_s9
 + s5_s0 + s5_s1 + s5_s7 + s5_s8 + s5_s9
 + s6_s0 + s6_s1
 + s7_s0 + s7_s1
 + s8_s1
 + s9_s1 + s9_s2 + s9_s3
}

fun Q2nd11[X :twoTrains10.states] : twoTrains10.states
{ -- NCQ predicate obtained after zero iteration
   s0_s3 + s0_s4 + s0_s5 + s0_s6 + s0_s7
 + s1_s3 + s1_s4 + s1_s5 + s1_s6 + s1_s7 + s1_s8 + s1_s9
 + s2_s5 + s2_s6 + s2_s7 + s2_s8 + s2_s9
 + s3_s0 + s3_s1 + s3_s5 + s3_s6 + s3_s7 + s3_s8 + s3_s9
 + s4_s0 + s4_s1 + s4_s7 + s4_s8 + s4_s9
 + s5_s0 + s5_s1 + s5_s7 + s5_s8 + s5_s9
 + s6_s0 + s6_s1
 + s7_s0 + s7_s1 + s7_s2 + s7_s3
 + s8_s1 + s8_s3
 + s9_s1 + s9_s2 + s9_s3
}

fun Q2nd12[X :twoTrains10.states] : twoTrains10.states
{ -- NCQ predicate obtained after zero iteration
   s0_s3 + s0_s4 + s0_s5 + s0_s6 + s0_s7
 + s1_s3 + s1_s4 + s1_s5 + s1_s6 + s1_s7 + s1_s8 + s1_s9
 + s2_s5 + s2_s6 + s2_s7 + s2_s8 + s2_s9
 + s3_s0 + s3_s1 + s3_s5 + s3_s6 + s3_s7 + s3_s8 + s3_s9
 + s4_s0 + s4_s1 + s4_s7 + s4_s8 + s4_s9
 + s5_s0 + s5_s1 + s5_s2 + s5_s3 + s5_s7 + s5_s8 + s5_s9
 + s6_s0 + s6_s1 + s6_s3
 + s7_s0 + s7_s1 + s7_s2 + s7_s3
 + s8_s1 + s8_s3
 + s9_s1 + s9_s2 + s9_s3
}

fun Q2nd13[X :twoTrains10.states] : twoTrains10.states
{ -- NCQ predicate obtained after zero iteration
   s0_s3 + s0_s4 + s0_s5 + s0_s6 + s0_s7
 + s1_s3 + s1_s4 + s1_s5 + s1_s6 + s1_s7 + s1_s8 + s1_s9
 + s2_s5 + s2_s6 + s2_s7 + s2_s8 + s2_s9
 + s3_s0 + s3_s1 + s3_s5 + s3_s6 + s3_s7 + s3_s8 + s3_s9
 + s4_s0 + s4_s1 + s4_s7 + s4_s8 + s4_s9
 + s5_s0 + s5_s1 + s5_s2 + s5_s3 + s5_s7 + s5_s8 + s5_s9
 + s6_s0 + s6_s1 + s6_s2 + s6_s3
 + s7_s0 + s7_s1 + s7_s2 + s7_s3
 + s8_s1 + s8_s3
 + s9_s1 + s9_s2 + s9_s3
}

fun Q2nd14[X :twoTrains10.states] : twoTrains10.states
{ -- NCQ predicate obtained after zero iteration
   s0_s3 + s0_s4 + s0_s5 + s0_s6 + s0_s7
 + s1_s3 + s1_s4 + s1_s5 + s1_s6 + s1_s7 + s1_s8 + s1_s9
 + s2_s5 + s2_s6 + s2_s7 + s2_s8 + s2_s9
 + s3_s0 + s3_s1 + s3_s5 + s3_s6 + s3_s7 + s3_s8 + s3_s9
 + s4_s0 + s4_s1 + s4_s7 + s4_s8 + s4_s9
 + s5_s0 + s5_s1 + s5_s2 + s5_s3 + s5_s7 + s5_s8 + s5_s9
 + s6_s0 + s6_s1 + s6_s2 + s6_s3 + s6_s9
 + s7_s0 + s7_s1 + s7_s2 + s7_s3 + s7_s9
 + s8_s1 + s8_s3
 + s9_s1 + s9_s2 + s9_s3
}

fun Q2nd15[X :twoTrains10.states] : twoTrains10.states
{ -- NCQ predicate obtained after zero iteration
   s0_s3 + s0_s4 + s0_s5 + s0_s6 + s0_s7
 + s1_s3 + s1_s4 + s1_s5 + s1_s6 + s1_s7 + s1_s8 + s1_s9
 + s2_s5 + s2_s6 + s2_s7 + s2_s8 + s2_s9
 + s3_s0 + s3_s1 + s3_s5 + s3_s6 + s3_s7 + s3_s8 + s3_s9
 + s4_s0 + s4_s1 + s4_s7 + s4_s8 + s4_s9
 + s5_s0 + s5_s1 + s5_s2 + s5_s3 + s5_s7 + s5_s8 + s5_s9
 + s6_s0 + s6_s1 + s6_s2 + s6_s3 + s6_s9
 + s7_s0 + s7_s1 + s7_s2 + s7_s3 + s7_s9
 + s8_s1 + s8_s2 + s8_s3
 + s9_s1 + s9_s2 + s9_s3
}

fun Q2nd16[X :twoTrains10.states] : twoTrains10.states
{ -- NCQ predicate obtained after zero iteration
   s0_s3 + s0_s4 + s0_s5 + s0_s6 + s0_s7
 + s1_s3 + s1_s4 + s1_s5 + s1_s6 + s1_s7 + s1_s8 + s1_s9
 + s2_s5 + s2_s6 + s2_s7 + s2_s8 + s2_s9
 + s3_s0 + s3_s1 + s3_s5 + s3_s6 + s3_s7 + s3_s8 + s3_s9
 + s4_s0 + s4_s1 + s4_s7 + s4_s8 + s4_s9
 + s5_s0 + s5_s1 + s5_s2 + s5_s3 + s5_s7 + s5_s8 + s5_s9
 + s6_s0 + s6_s1 + s6_s2 + s6_s3 + s6_s9
 + s7_s0 + s7_s1 + s7_s2 + s7_s3 + s7_s9
 + s8_s1 + s8_s2 + s8_s3
 + s9_s1 + s9_s2 + s9_s3 + s9_s4 + s9_s5
}

fun Q2nd17[X :twoTrains10.states] : twoTrains10.states
{ -- NCQ predicate obtained after zero iteration
   s0_s3 + s0_s4 + s0_s5 + s0_s6 + s0_s7
 + s1_s3 + s1_s4 + s1_s5 + s1_s6 + s1_s7 + s1_s8 + s1_s9
 + s2_s5 + s2_s6 + s2_s7 + s2_s8 + s2_s9
 + s3_s0 + s3_s1 + s3_s5 + s3_s6 + s3_s7 + s3_s8 + s3_s9
 + s4_s0 + s4_s1 + s4_s7 + s4_s8 + s4_s9
 + s5_s0 + s5_s1 + s5_s2 + s5_s3 + s5_s7 + s5_s8 + s5_s9
 + s6_s0 + s6_s1 + s6_s2 + s6_s3 + s6_s9
 + s7_s0 + s7_s1 + s7_s2 + s7_s3 + s7_s4 + s7_s5 + s7_s9
 + s8_s1 + s8_s2 + s8_s3 + s8_s5
 + s9_s1 + s9_s2 + s9_s3 + s9_s4 + s9_s5
}

fun Q2nd18[X :twoTrains10.states] : twoTrains10.states
{ -- NCQ predicate obtained after zero iteration
   s0_s3 + s0_s4 + s0_s5 + s0_s6 + s0_s7
 + s1_s3 + s1_s4 + s1_s5 + s1_s6 + s1_s7 + s1_s8 + s1_s9
 + s2_s5 + s2_s6 + s2_s7 + s2_s8 + s2_s9
 + s3_s0 + s3_s1 + s3_s5 + s3_s6 + s3_s7 + s3_s8 + s3_s9
 + s4_s0 + s4_s1 + s4_s7 + s4_s8 + s4_s9
 + s5_s0 + s5_s1 + s5_s2 + s5_s3 + s5_s7 + s5_s8 + s5_s9
 + s6_s0 + s6_s1 + s6_s2 + s6_s3 + s6_s9
 + s7_s0 + s7_s1 + s7_s2 + s7_s3 + s7_s4 + s7_s5 + s7_s9
 + s8_s1 + s8_s2 + s8_s3 + s8_s4 + s8_s5
 + s9_s1 + s9_s2 + s9_s3 + s9_s4 + s9_s5
}

fun Q2nd19[X :twoTrains10.states] : twoTrains10.states
{ -- NCQ predicate obtained after zero iteration
   s0_s3 + s0_s4 + s0_s5 + s0_s6 + s0_s7
 + s1_s3 + s1_s4 + s1_s5 + s1_s6 + s1_s7 + s1_s8 + s1_s9
 + s2_s5 + s2_s6 + s2_s7 + s2_s8 + s2_s9
 + s3_s0 + s3_s1 + s3_s5 + s3_s6 + s3_s7 + s3_s8 + s3_s9
 + s4_s0 + s4_s1 + s4_s7 + s4_s8 + s4_s9
 + s5_s0 + s5_s1 + s5_s2 + s5_s3 + s5_s7 + s5_s8 + s5_s9
 + s6_s0 + s6_s1 + s6_s2 + s6_s3 + s6_s9
 + s7_s0 + s7_s1 + s7_s2 + s7_s3 + s7_s4 + s7_s5 + s7_s9
 + s8_s1 + s8_s2 + s8_s3 + s8_s4 + s8_s5
 + s9_s1 + s9_s2 + s9_s3 + s9_s4 + s9_s5 + s9_s6 + s9_s7
}
*/

run generateWeakerPredicate2ndStrategy
{ -- use successively with none, Q2nd1, Q2nd2, Q2nd3, Q2nd4, Q2nd5,
  --                       Q2nd6, Q2nd7, Q2nd8, Q2nd9, Q2nd10, Q2nd11,
  --                       Q2nd12, Q2nd13, Q2nd14, Q2nd15, Q2nd16,
  --                       Q2nd17, Q2nd18 and Q2nd19
 NBCQ.IsWeakerNBC[none, twoTrains10, Q[twoTrains10.states]]
} for 1

run generateWeakerPredicate3rdStrategy
{ -- generate {}, {s1_s3} and ... with next
 NBCQ.IsNBC[twoTrains10, Q[twoTrains10.states]]
} for 1