open SBCDES_Partial_Observation[StateSpace, EventSet, 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, s0s1, s0tn, s0s5, s0s6, s0s7, s1s0, s1s1, s1tn, s1s5, s1s6, s1s7, tns0, tns1, tntn, tns5, tns6, tns7, s5s0, s5s1, s5tn, s5s5, s5s6, s5s7, s6s0, s6s1, s6tn, s6s5, s6s6, s6s7, s7s0, s7s1, s7tn, s7s5, s7s6, s7s7 } enum EventSet { 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, firstTrain : set StateSpace -> LocalStateSpace, secondTrain : 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 firstTrain = (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) secondTrain = (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 + s0s1 + s0tn + s0s5 + s0s6 + s0s7 + s1s0 + s1s1 + s1tn + s1s5 + s1s6 + s1s7 + tns0 + tns1 + tntn + tns5 + tns6 + tns7 + s5s0 + s5s1 + s5tn + s5s5 + s5s6 + s5s7 + s6s0 + s6s1 + s6tn + s6s5 + s6s6 + s6s7 + s7s0 + s7s1 + s7tn + s7s5 + s7s6 + s7s7 tunnel = (s0_s0->s0s0) + (s0_s1->s0s1) + (s0_s2->s0tn) + (s0_s3->s0tn) + (s0_s4->s0tn) + (s0_s5->s0s5) + (s0_s6->s0s6) + (s0_s7->s0s7) + (s1_s0->s1s0) + (s1_s1->s1s1) + (s1_s2->s1tn) + (s1_s3->s1tn) + (s1_s4->s1tn) + (s1_s5->s1s5) + (s1_s6->s1s6) + (s1_s7->s1s7) + (s2_s0->tns0) + (s2_s1->tns1) + (s2_s2->tntn) + (s2_s3->tntn) + (s2_s4->tntn) + (s2_s5->tns5) + (s2_s6->tns6) + (s2_s7->tns7) + (s3_s0->tns0) + (s3_s1->tns1) + (s3_s2->tntn) + (s3_s3->tntn) + (s3_s4->tntn) + (s3_s5->tns5) + (s3_s6->tns6) + (s3_s7->tns7) + (s4_s0->tns0) + (s4_s1->tns1) + (s4_s2->tntn) + (s4_s3->tntn) + (s4_s4->tntn) + (s4_s5->tns5) + (s4_s6->tns6) + (s4_s7->tns7) + (s5_s0->s5s0) + (s5_s1->s5s1) + (s5_s2->s5tn) + (s5_s3->s5tn) + (s5_s4->s5tn) + (s5_s5->s5s5) + (s5_s6->s5s6) + (s5_s7->s5s7) + (s6_s0->s6s0) + (s6_s1->s6s1) + (s6_s2->s6tn) + (s6_s3->s6tn) + (s6_s4->s6tn) + (s6_s5->s6s5) + (s6_s6->s6s6) + (s6_s7->s6s7) + (s7_s0->s7s0) + (s7_s1->s7s1) + (s7_s2->s7tn) + (s7_s3->s7tn) + (s7_s4->s7tn) + (s7_s5->s7s5) + (s7_s6->s7s6) + (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 = s1_s7 markedStates = s1_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.firstTrain) = x.(twoTrains8.secondTrain) } pred OnAdjacentSections[x: one twoTrains8.states] { (twoTrains8.nextSection[x.(twoTrains8.firstTrain)] = x.(twoTrains8.secondTrain)) or (twoTrains8.prevSection[x.(twoTrains8.firstTrain)] = x.(twoTrains8.secondTrain)) } 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