open SBCDES_Total_Observation[StateSpace, EventSet] -- Two trains on a circular railway composed of 6 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, s1_s0, s1_s1, s1_s2, s1_s3, s1_s4, s1_s5, s2_s0, s2_s1, s2_s2, s2_s3, s2_s4, s2_s5, s3_s0, s3_s1, s3_s2, s3_s3, s3_s4, s3_s5, s4_s0, s4_s1, s4_s2, s4_s3, s4_s4, s4_s5, s5_s0, s5_s1, s5_s2, s5_s3, s5_s4, s5_s5 } enum LocalStateSpace { s0, s1, s2, s3, s4, s5 } enum EventSet { t1_s0TOs1, t1_s1TOs2, t1_s2TOs3, t1_s3TOs4, t1_s4TOs5, t1_s5TOs0, t2_s0TOs1, t2_s1TOs2, t2_s2TOs3, t2_s3TOs4, t2_s4TOs5, t2_s5TOs0 } one sig twoTrains6 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 + s1_s0 + s1_s1 + s1_s2 + s1_s3 + s1_s4 + s1_s5 + s2_s0 + s2_s1 + s2_s2 + s2_s3 + s2_s4 + s2_s5 + s3_s0 + s3_s1 + s3_s2 + s3_s3 + s3_s4 + s3_s5 + s4_s0 + s4_s1 + s4_s2 + s4_s3 + s4_s4 + s4_s5 + s5_s0 + s5_s1 + s5_s2 + s5_s3 + s5_s4 + s5_s5 localStates = s0 + s1 + s2 + s3 + s4 + s5 firstProcess = (s0_s0 -> s0) + (s0_s1 -> s0) + (s0_s2 -> s0) + (s0_s3 -> s0) + (s0_s4 -> s0) + (s0_s5 -> s0) + (s1_s0 -> s1) + (s1_s1 -> s1) + (s1_s2 -> s1) + (s1_s3 -> s1) + (s1_s4 -> s1) + (s1_s5 -> s1) + (s2_s0 -> s2) + (s2_s1 -> s2) + (s2_s2 -> s2) + (s2_s3 -> s2) + (s2_s4 -> s2) + (s2_s5 -> s2) + (s3_s0 -> s3) + (s3_s1 -> s3) + (s3_s2 -> s3) + (s3_s3 -> s3) + (s3_s4 -> s3) + (s3_s5 -> s3) + (s4_s0 -> s4) + (s4_s1 -> s4) + (s4_s2 -> s4) + (s4_s3 -> s4) + (s4_s4 -> s4) + (s4_s5 -> s4) + (s5_s0 -> s5) + (s5_s1 -> s5) + (s5_s2 -> s5) + (s5_s3 -> s5) + (s5_s4 -> s5) + (s5_s5 -> s5) secondProcess = (s0_s0 -> s0) + (s0_s1 -> s1) + (s0_s2 -> s2) + (s0_s3 -> s3) + (s0_s4 -> s4) + (s0_s5 -> s5) + (s1_s0 -> s0) + (s1_s1 -> s1) + (s1_s2 -> s2) + (s1_s3 -> s3) + (s1_s4 -> s4) + (s1_s5 -> s5) + (s2_s0 -> s0) + (s2_s1 -> s1) + (s2_s2 -> s2) + (s2_s3 -> s3) + (s2_s4 -> s4) + (s2_s5 -> s5) + (s3_s0 -> s0) + (s3_s1 -> s1) + (s3_s2 -> s2) + (s3_s3 -> s3) + (s3_s4 -> s4) + (s3_s5 -> s5) + (s4_s0 -> s0) + (s4_s1 -> s1) + (s4_s2 -> s2) + (s4_s3 -> s3) + (s4_s4 -> s4) + (s4_s5 -> s5) + (s5_s0 -> s0) + (s5_s1 -> s1) + (s5_s2 -> s2) + (s5_s3 -> s3) + (s5_s4 -> s4) + (s5_s5 -> s5) nextSection = (s0 -> s1) + (s1 -> s2) + (s2 -> s3) + (s3 -> s4) + (s4 -> s5) + (s5 -> s0) prevSection = (s0 -> s5) + (s1 -> s0) + (s2 -> s1) + (s3 -> s2) + (s4 -> s3) + (s5 -> s4) events = t1_s0TOs1 + t1_s1TOs2 + t1_s2TOs3 + t1_s3TOs4 + t1_s4TOs5 + t1_s5TOs0 + t2_s0TOs1 + t2_s1TOs2 + t2_s2TOs3 + t2_s3TOs4 + t2_s4TOs5 + t2_s5TOs0 controllableEvents = t1_s1TOs2 + t1_s3TOs4 + t1_s5TOs0 + t2_s1TOs2 + t2_s3TOs4 + t2_s5TOs0 initialState = s3_s5 markedStates = s3_s5 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_s5TOs0->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_s5TOs0->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_s5TOs0->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_s5TOs0->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_s5TOs0->s4_s0 + s5_s0->t1_s5TOs0->s0_s0 + s5_s0->t2_s0TOs1->s5_s1 + s5_s1->t1_s5TOs0->s0_s1 + s5_s1->t2_s1TOs2->s5_s2 + s5_s2->t1_s5TOs0->s0_s2 + s5_s2->t2_s2TOs3->s5_s3 + s5_s3->t1_s5TOs0->s0_s3 + s5_s3->t2_s3TOs4->s5_s4 + s5_s4->t1_s5TOs0->s0_s4 + s5_s4->t2_s4TOs5->s5_s5 + s5_s5->t1_s5TOs0->s0_s5 + s5_s5->t2_s5TOs0->s5_s0 } pred OnSameSection[x: one twoTrains6.states] { x.(twoTrains6.firstProcess) = x.(twoTrains6.secondProcess) } pred OnAdjacentSections[x: one twoTrains6.states] { (twoTrains6.nextSection[x.(twoTrains6.firstProcess)] = x.(twoTrains6.secondProcess)) or (twoTrains6.prevSection[x.(twoTrains6.firstProcess)] = x.(twoTrains6.secondProcess)) } fun Q[X : set twoTrains6.states] : twoTrains6.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 twoTrains6.states } /* fun Q1st1[X :twoTrains6.states] : twoTrains6.states { -- predicate obtained after one iteration (the solution) s0_s3 + s1_s3 + s1_s4 + s1_s5 + s2_s5 + s3_s0 + s3_s1 + s3_s5 + s4_s1 + s5_s1 + s5_s2 + s5_s3 } */ run generateStrongerPredicate1stStrategy { -- use successively with Q and Q1st1 NBCQ = NBC[twoTrains6, Q[twoTrains6.states]] } /* fun Q2nd1[X :twoTrains6.states] : twoTrains6.states { -- predicate obtained after one iteration s3_s5 } */ fun Q2nd2[X :twoTrains6.states] : twoTrains6.states { -- predicate obtained after two iteration s0_s3 + s1_s3 + s1_s4 + s1_s5 + s2_s5 + s3_s0 + s3_s1 + s3_s5 + s4_s1 + s5_s1 + s5_s2 + s5_s3 } run generateWeakerPredicate2ndStrategy { -- use successively with none, Q2nd1 and Q2nd2 NBCQ.IsWeakerNBC[none, twoTrains6, Q[twoTrains6.states]] } for 1 run generateWeakerPredicate3rdStrategy { -- generate {}, {s3_s5} and {s0_s3, s1_s3, s1_s4, s1_s5, -- s2_s5, s3_s0, s3_s1, s3_s5, -- s4_s1, s5_s1, s5_s2, s5_s3} with next NBCQ.IsNBC[twoTrains6, Q[twoTrains6.states]] } for 1