open SBCDES_Partial_Observation[StateSpace, Alphabet, ObservationSpace] -- 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, 2013. enum StateSpace { s0_s0, s0_s1, s0_s2, s0_s3, s0_s4, s0_s5, s0_s6, s0_s7, s1_s0, s1_s1, s1_s2, s1_s3, s1_s4, s1_s5, s1_s6, s1_s7, s2_s0, s2_s1, s2_s2, s2_s3, s2_s4, s2_s5, s2_s6, s2_s7, s3_s0, s3_s1, s3_s2, s3_s3, s3_s4, s3_s5, s3_s6, s3_s7, s4_s0, s4_s1, s4_s2, s4_s3, s4_s4, s4_s5, s4_s6, s4_s7, s5_s0, s5_s1, s5_s2, s5_s3, s5_s4, s5_s5, s5_s6, s5_s7, s6_s0, s6_s1, s6_s2, s6_s3, s6_s4, s6_s5, s6_s6, s6_s7, s7_s0, s7_s1, s7_s2, s7_s3, s7_s4, s7_s5, s7_s6, s7_s7 } enum LocalStateSpace { s0, s1, s2, s3, s4, s5, s6, s7 } enum ObservationSpace { s0s0, s0t1, s0s3, s0s4, s0t2, s0s7, t1s0, t1t1, t1s3, t1s4, t1t2, t1s7, s3s0, s3t1, s3s3, s3s4, s3t2, s3s7, s4s0, s4t1, s4s3, s4s4, s4t2, s4s7, t2s0, t2t1, t2s3, t2s4, t2t2, t2s7, s7s0, s7t1, s7s3, s7s4, s7t2, s7s7 } enum Alphabet { 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 } one sig twoTrains8 extends Automaton { localStates : set LocalStateSpace, firstProcess : set StateSpace -> LocalStateSpace, secondProcess : set StateSpace -> LocalStateSpace, observationSpace : set ObservationSpace, tunnel : set StateSpace -> ObservationSpace, 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 + s1_s0 + s1_s1 + s1_s2 + s1_s3 + s1_s4 + s1_s5 + s1_s6 + s1_s7 + s2_s0 + s2_s1 + s2_s2 + s2_s3 + s2_s4 + s2_s5 + s2_s6 + s2_s7 + s3_s0 + s3_s1 + s3_s2 + s3_s3 + s3_s4 + s3_s5 + s3_s6 + s3_s7 + s4_s0 + s4_s1 + s4_s2 + s4_s3 + s4_s4 + s4_s5 + s4_s6 + s4_s7 + s5_s0 + s5_s1 + s5_s2 + s5_s3 + s5_s4 + s5_s5 + s5_s6 + s5_s7 + s6_s0 + s6_s1 + s6_s2 + s6_s3 + s6_s4 + s6_s5 + s6_s6 + s6_s7 + s7_s0 + s7_s1 + s7_s2 + s7_s3 + s7_s4 + s7_s5 + s7_s6 + s7_s7 localStates = s0 + s1 + s2 + s3 + s4 + s5 + s6 + s7 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) + (s1_s0 -> s1) + (s1_s1 -> s1) + (s1_s2 -> s1) + (s1_s3 -> s1) + (s1_s4 -> s1) + (s1_s5 -> s1) + (s1_s6 -> s1) + (s1_s7 -> 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) + (s3_s0 -> s3) + (s3_s1 -> s3) + (s3_s2 -> s3) + (s3_s3 -> s3) + (s3_s4 -> s3) + (s3_s5 -> s3) + (s3_s6 -> s3) + (s3_s7 -> 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) + (s5_s0 -> s5) + (s5_s1 -> s5) + (s5_s2 -> s5) + (s5_s3 -> s5) + (s5_s4 -> s5) + (s5_s5 -> s5) + (s5_s6 -> s5) + (s5_s7 -> 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) + (s7_s0 -> s7) + (s7_s1 -> s7) + (s7_s2 -> s7) + (s7_s3 -> s7) + (s7_s4 -> s7) + (s7_s5 -> s7) + (s7_s6 -> s7) + (s7_s7 -> s7) 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) + (s1_s0 -> s0) + (s1_s1 -> s1) + (s1_s2 -> s2) + (s1_s3 -> s3) + (s1_s4 -> s4) + (s1_s5 -> s5) + (s1_s6 -> s6) + (s1_s7 -> s7) + (s2_s0 -> s0) + (s2_s1 -> s1) + (s2_s2 -> s2) + (s2_s3 -> s3) + (s2_s4 -> s4) + (s2_s5 -> s5) + (s2_s6 -> s6) + (s2_s7 -> s7) + (s3_s0 -> s0) + (s3_s1 -> s1) + (s3_s2 -> s2) + (s3_s3 -> s3) + (s3_s4 -> s4) + (s3_s5 -> s5) + (s3_s6 -> s6) + (s3_s7 -> s7) + (s4_s0 -> s0) + (s4_s1 -> s1) + (s4_s2 -> s2) + (s4_s3 -> s3) + (s4_s4 -> s4) + (s4_s5 -> s5) + (s4_s6 -> s6) + (s4_s7 -> s7) + (s5_s0 -> s0) + (s5_s1 -> s1) + (s5_s2 -> s2) + (s5_s3 -> s3) + (s5_s4 -> s4) + (s5_s5 -> s5) + (s5_s6 -> s6) + (s5_s7 -> s7) + (s6_s0 -> s0) + (s6_s1 -> s1) + (s6_s2 -> s2) + (s6_s3 -> s3) + (s6_s4 -> s4) + (s6_s5 -> s5) + (s6_s6 -> s6) + (s6_s7 -> s7) + (s7_s0 -> s0) + (s7_s1 -> s1) + (s7_s2 -> s2) + (s7_s3 -> s3) + (s7_s4 -> s4) + (s7_s5 -> s5) + (s7_s6 -> s6) + (s7_s7 -> s7) observationSpace = s0s0 + s0t1 + s0s3 + s0s4 + s0t2 + s0s7 + t1s0 + t1t1 + t1s3 + t1s4 + t1t2 + t1s7 + s3s0 + s3t1 + s3s3 + s3s4 + s3t2 + s3s7 + s4s0 + s4t1 + s4s3 + s4s4 + s4t2 + s4s7 + t2s0 + t2t1 + t2s3 + t2s4 + t2t2 + t2s7 + s7s0 + s7t1 + s7s3 + s7s4 + s7t2 + s7s7 tunnel = (s0_s0->s0s0) + (s0_s1->s0t1) + (s0_s2->s0t1) + (s0_s3->s0s3) + (s0_s4->s0s4) + (s0_s5->s0t2) + (s0_s6->s0t2) + (s0_s7->s0s7) + (s1_s0->t1s0) + (s1_s1->t1t1) + (s1_s2->t1t1) + (s1_s3->t1s3) + (s1_s4->t1s4) + (s1_s5->t1t2) + (s1_s6->t1t2) + (s1_s7->t1s7) + (s2_s0->t1s0) + (s2_s1->t1t1) + (s2_s2->t1t1) + (s2_s3->t1s3) + (s2_s4->t1s4) + (s2_s5->t1t2) + (s2_s6->t1t2) + (s2_s7->t1s7) + (s3_s0->s3s0) + (s3_s1->s3t1) + (s3_s2->s3t1) + (s3_s3->s3s3) + (s3_s4->s3s4) + (s3_s5->s3t2) + (s3_s6->s3t2) + (s3_s7->s3s7) + (s4_s0->s4s0) + (s4_s1->s4t1) + (s4_s2->s4t1) + (s4_s3->s4s3) + (s4_s4->s4s4) + (s4_s5->s4t2) + (s4_s6->s4t2) + (s4_s7->s4s7) + (s5_s0->t2s0) + (s5_s1->t2t1) + (s5_s2->t2t1) + (s5_s3->t2s3) + (s5_s4->t2s4) + (s5_s5->t2t2) + (s5_s6->t2t2) + (s5_s7->t2s7) + (s6_s0->t2s0) + (s6_s1->t2t1) + (s6_s2->t2t1) + (s6_s3->t2s3) + (s6_s4->t2s4) + (s6_s5->t2t2) + (s6_s6->t2t2) + (s6_s7->t2s7) + (s7_s0->s7s0) + (s7_s1->s7t1) + (s7_s2->s7t1) + (s7_s3->s7s3) + (s7_s4->s7s4) + (s7_s5->s7t2) + (s7_s6->s7t2) + (s7_s7->s7s7) nextSection = (s0 -> s1) + (s1 -> s2) + (s2 -> s3) + (s3 -> s4) + (s4 -> s5) + (s5 -> s6) + (s6 -> s7) + (s7 -> s0) prevSection = (s0 -> s7) + (s1 -> s0) + (s2 -> s1) + (s3 -> s2) + (s4 -> s3) + (s5 -> s4) + (s6 -> s5) + (s7 -> s6) events = 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 controllableEvents = t1_s1TOs2 + t1_s3TOs4 + t1_s5TOs6 + t1_s7TOs0 + t2_s1TOs2 + t2_s3TOs4 + t2_s5TOs6 + t2_s7TOs0 initialState = s3_s7 markedStates = s3_s7 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_s7TOs0->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_s7TOs0->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_s7TOs0->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_s7TOs0->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_s7TOs0->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_s7TOs0->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_s7TOs0->s6_s0 + s7_s0->t1_s7TOs0->s0_s0 + s7_s0->t2_s0TOs1->s7_s1 + s7_s1->t1_s7TOs0->s0_s1 + s7_s1->t2_s1TOs2->s7_s2 + s7_s2->t1_s7TOs0->s0_s2 + s7_s2->t2_s2TOs3->s7_s3 + s7_s3->t1_s7TOs0->s0_s3 + s7_s3->t2_s3TOs4->s7_s4 + s7_s4->t1_s7TOs0->s0_s4 + s7_s4->t2_s4TOs5->s7_s5 + s7_s5->t1_s7TOs0->s0_s5 + s7_s5->t2_s5TOs6->s7_s6 + s7_s6->t1_s7TOs0->s0_s6 + s7_s6->t2_s6TOs7->s7_s7 + s7_s7->t1_s7TOs0->s0_s7 + s7_s7->t2_s7TOs0->s7_s0 } pred OnSameSection[x: one twoTrains8.states] { x.(twoTrains8.firstProcess) = x.(twoTrains8.secondProcess) } pred OnAdjacentSections[x: one twoTrains8.states] { (twoTrains8.nextSection[x.(twoTrains8.firstProcess)] = x.(twoTrains8.secondProcess)) or (twoTrains8.prevSection[x.(twoTrains8.firstProcess)] = x.(twoTrains8.secondProcess)) } fun Q[X : twoTrains8.states] : twoTrains8.states { -- The two trains must be separated by at least one section. { x : X | not (OnSameSection[x] or OnAdjacentSections[x]) } } fun NBCQ[X :twoTrains8.states] : twoTrains8.states { -- supremal nonblocking controllable predicate of Q 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 } one sig SFBC1 { f = SFBC_breveF[twoTrains8.tunnel, twoTrains8, R_breve[twoTrains8.tunnel, twoTrains8, NBCQ[twoTrains8.states]]] } one sig SFBC2 { f = SFBC_breve[twoTrains8.tunnel, twoTrains8, R_breve[twoTrains8.tunnel, twoTrains8, NBCQ[twoTrains8.states]]] } run { } for 1 check sameSFBC { SFBC1.f = SFBC2.f } for 1