open SBCDES_Total_Observation[StateSpace, EventSet] -- Maze for cat and mouse with eight rooms inspired from: -- P. J. G. Ramadge and W. M. Wonham, -- The control of discrete event systems, -- Proceedings of the IEEE, 77 (1): 81-98. -- copyright Richard St-Denis, Universite de Sherbrooke, 2013. enum StateSpace { c0_m0, c0_m1, c0_m2, c0_m3, c0_m4, c1_m0, c1_m1, c1_m2, c1_m3, c1_m4, c2_m0, c2_m1, c2_m2, c2_m3, c2_m4, c3_m0, c3_m1, c3_m2, c3_m3, c3_m4, c4_m0, c4_m1, c4_m2, c4_m3, c4_m4, c5_m0, c5_m1, c5_m2, c5_m3, c5_m4, c6_m0, c6_m1, c6_m2, c6_m3, c6_m4, c7_m0, c7_m1, c7_m2, c7_m3, c7_m4 } enum LocalStateSpace { c0, c1, c2, c3, c4, c5, c6, c7, m0, m1, m2, m3, m4 } enum EventSet { cd0, cd1, cd2, cd3, cd4, cd5, cd6, cd7, cd8, cd9, cd10, md1, md2, md3, md4, md5, md6 } one sig maze8 extends Automaton { localStates : set LocalStateSpace, firstProcess : set StateSpace -> LocalStateSpace, secondProcess : set StateSpace -> LocalStateSpace } { states = c0_m0 + c0_m1 + c0_m2 + c0_m3 + c0_m4 + c1_m0 + c1_m1 + c1_m2 + c1_m3 + c1_m4 + c2_m0 + c2_m1 + c2_m2 + c2_m3 + c2_m4 + c3_m0 + c3_m1 + c3_m2 + c3_m3 + c3_m4 + c4_m0 + c4_m1 + c4_m2 + c4_m3 + c4_m4 + c5_m0 + c5_m1 + c5_m2 + c5_m3 + c5_m4 + c6_m0 + c6_m1 + c6_m2 + c6_m3 + c6_m4 + c7_m0 + c7_m1 + c7_m2 + c7_m3 + c7_m4 localStates = c0 + c1 + c2 + c3 + c4 + c5 + c6 + c7 + m0 + m1 + m2 + m3 + m4 firstProcess = (c0_m0 -> c0) + (c0_m1 -> c0) + (c0_m2 -> c0) + (c0_m3 -> c0) + (c0_m4 -> c0) + (c1_m0 -> c1) + (c1_m1 -> c1) + (c1_m2 -> c1) + (c1_m3 -> c1) + (c1_m4 -> c1) + (c2_m0 -> c2) + (c2_m1 -> c2) + (c2_m2 -> c2) + (c2_m3 -> c2) + (c2_m4 -> c2) + (c3_m0 -> c3) + (c3_m1 -> c3) + (c3_m2 -> c3) + (c3_m3 -> c3) + (c3_m4 -> c3) + (c4_m0 -> c4) + (c4_m1 -> c4) + (c4_m2 -> c4) + (c4_m3 -> c4) + (c4_m4 -> c4) + (c5_m0 -> c5) + (c5_m1 -> c5) + (c5_m2 -> c5) + (c5_m3 -> c5) + (c5_m4 -> c5) + (c6_m0 -> c6) + (c6_m1 -> c6) + (c6_m2 -> c6) + (c6_m3 -> c6) + (c6_m4 -> c6) + (c7_m0 -> c7) + (c7_m1 -> c7) + (c7_m2 -> c7) + (c7_m3 -> c7) + (c7_m4 -> c7) secondProcess = (c0_m0 -> m0) + (c0_m1 -> m1) + (c0_m2 -> m2) + (c0_m3 -> m3) + (c0_m4 -> m4) + (c1_m0 -> m0) + (c1_m1 -> m1) + (c1_m2 -> m2) + (c1_m3 -> m3) + (c1_m4 -> m4) + (c2_m0 -> m0) + (c2_m1 -> m1) + (c2_m2 -> m2) + (c2_m3 -> m3) + (c2_m4 -> m4) + (c3_m0 -> m0) + (c3_m1 -> m1) + (c3_m2 -> m2) + (c3_m3 -> m3) + (c3_m4 -> m4) + (c4_m0 -> m0) + (c4_m1 -> m1) + (c4_m2 -> m2) + (c4_m3 -> m3) + (c4_m4 -> m4) + (c5_m0 -> m0) + (c5_m1 -> m1) + (c5_m2 -> m2) + (c5_m3 -> m3) + (c5_m4 -> m4) + (c6_m0 -> m0) + (c6_m1 -> m1) + (c6_m2 -> m2) + (c6_m3 -> m3) + (c6_m4 -> m4) + (c7_m0 -> m0) + (c7_m1 -> m1) + (c7_m2 -> m2) + (c7_m3 -> m3) + (c7_m4 -> m4) events = cd0 + cd1 + cd2 + cd3 + cd4 + cd5 + cd6 + cd7 + cd8 + cd9 + cd10 + md1 + md2 + md3 + md4 + md5 + md6 controllableEvents = cd0 + cd1 + cd2 + cd3 + cd4 + cd5 + cd6 + md1 + md2 + md3 + md4 + md5 + md6 initialState = c2_m4 markedStates = c2_m4 transition = (c0_m0 -> cd1 -> c1_m0) + (c0_m0 -> cd4 -> c3_m0) + (c0_m0 -> md1 -> c0_m2) + (c0_m0 -> md4 -> c0_m4) + (c0_m1 -> cd1 -> c1_m1) + (c0_m1 -> cd4 -> c3_m1) + (c0_m1 -> md3 -> c0_m0) + (c0_m2 -> cd1 -> c1_m2) + (c0_m2 -> cd4 -> c3_m2) + (c0_m2 -> md2 -> c0_m1) + (c0_m3 -> cd1 -> c1_m3) + (c0_m3 -> cd4 -> c3_m3) + (c0_m3 -> md6 -> c0_m0) + (c0_m4 -> cd1 -> c1_m4) + (c0_m4 -> cd4 -> c3_m4) + (c0_m4 -> md5 -> c0_m3) + (c1_m0 -> cd2 -> c2_m0) + (c1_m0 -> cd7 -> c5_m0) + (c1_m0 -> md1 -> c1_m2) + (c1_m0 -> md4 -> c1_m4) + (c1_m1 -> cd2 -> c2_m1) + (c1_m1 -> cd7 -> c5_m1) + (c1_m1 -> md3 -> c1_m0) + (c1_m2 -> cd2 -> c2_m2) + (c1_m2 -> cd7 -> c5_m2) + (c1_m2 -> md2 -> c1_m1) + (c1_m3 -> cd2 -> c2_m3) + (c1_m3 -> cd7 -> c5_m3) + (c1_m3 -> md6 -> c1_m0) + (c1_m4 -> cd2 -> c2_m4) + (c1_m4 -> cd7 -> c5_m4) + (c1_m4 -> md5 -> c1_m3) + (c2_m0 -> cd3 -> c0_m0) + (c2_m0 -> md1 -> c2_m2) + (c2_m0 -> md4 -> c2_m4) + (c2_m1 -> cd3 -> c0_m1) + (c2_m1 -> md3 -> c2_m0) + (c2_m2 -> cd3 -> c0_m2) + (c2_m2 -> md2 -> c2_m1) + (c2_m3 -> cd3 -> c0_m3) + (c2_m3 -> md6 -> c2_m0) + (c2_m4 -> cd3 -> c0_m4) + (c2_m4 -> md5 -> c2_m3) + (c3_m0 -> cd5 -> c4_m0) + (c3_m0 -> cd10 -> c1_m0) + (c3_m0 -> md1 -> c3_m2) + (c3_m0 -> md4 -> c3_m4) + (c3_m1 -> cd5 -> c4_m1) + (c3_m1 -> cd10 -> c1_m1) + (c3_m1 -> md3 -> c3_m0) + (c3_m2 -> cd5 -> c4_m2) + (c3_m2 -> cd10 -> c1_m2) + (c3_m2 -> md2 -> c3_m1) + (c3_m3 -> cd5 -> c4_m3) + (c3_m3 -> cd10 -> c1_m3) + (c3_m3 -> md6 -> c3_m0) + (c3_m4 -> cd5 -> c4_m4) + (c3_m4 -> cd10 -> c1_m4) + (c3_m4 -> md5 -> c3_m3) + (c4_m0 -> cd6 -> c0_m0) + (c4_m0 -> md1 -> c4_m2) + (c4_m0 -> md4 -> c4_m4) + (c4_m1 -> cd6 -> c0_m1) + (c4_m1 -> md3 -> c4_m0) + (c4_m2 -> cd6 -> c0_m2) + (c4_m2 -> md2 -> c4_m1) + (c4_m3 -> cd6 -> c0_m3) + (c4_m3 -> md6 -> c4_m0) + (c4_m4 -> cd6 -> c0_m4) + (c4_m4 -> md5 -> c4_m3) + (c5_m0 -> cd8 -> c6_m0) + (c5_m0 -> md1 -> c5_m2) + (c5_m0 -> md4 -> c5_m4) + (c5_m1 -> cd8 -> c6_m1) + (c5_m1 -> md3 -> c5_m0) + (c5_m2 -> cd8 -> c6_m2) + (c5_m2 -> md2 -> c5_m1) + (c5_m3 -> cd8 -> c6_m3) + (c5_m3 -> md6 -> c5_m0) + (c5_m4 -> cd8 -> c6_m4) + (c5_m4 -> md5 -> c5_m3) + (c6_m0 -> cd0 -> c7_m0) + (c6_m0 -> cd9 -> c3_m0) + (c6_m0 -> md1 -> c6_m2) + (c6_m0 -> md4 -> c6_m4) + (c6_m1 -> cd0 -> c7_m1) + (c6_m1 -> cd9 -> c3_m1) + (c6_m1 -> md3 -> c6_m0) + (c6_m2 -> cd0 -> c7_m2) + (c6_m2 -> cd9 -> c3_m2) + (c6_m2 -> md2 -> c6_m1) + (c6_m3 -> cd0 -> c7_m3) + (c6_m3 -> cd9 -> c3_m3) + (c6_m3 -> md6 -> c6_m0) + (c6_m4 -> cd0 -> c7_m4) + (c6_m4 -> cd9 -> c3_m4) + (c6_m4 -> md5 -> c6_m3) } fun Q[X: maze8.states] : maze8.states { -- The cat and mouse never occupy the same room simultaneously { x : X | not (x.(maze8.firstProcess) = c0 and x.(maze8.secondProcess) = m0) and not (x.(maze8.firstProcess) = c1 and x.(maze8.secondProcess) = m1) and not (x.(maze8.firstProcess) = c2 and x.(maze8.secondProcess) = m2) and not (x.(maze8.firstProcess) = c3 and x.(maze8.secondProcess) = m3) and not (x.(maze8.firstProcess) = c4 and x.(maze8.secondProcess) = m4) } } run { } for 1 sig NBCQ in StateSpace { } fact { NBCQ in maze8.states } /* fun Q1st1[X: maze8.states] : maze8.states { -- predicate obtained after one iteration c0_m1 + c0_m2 + c0_m3 + c0_m4 + c1_m0 + c1_m2 + c1_m4 + c2_m0 + c2_m3 + c2_m4 + c3_m0 + c3_m2 + c3_m4 + c4_m0 + c4_m1 + c4_m2 + c5_m0 + c5_m2 + c5_m4 + c6_m0 + c6_m2 + c6_m4 } fun Q1st2[X: maze8.states] : maze8.states { -- predicate obtained after two iterations (the solution) c0_m4 + c1_m4 + c2_m0 + c2_m3 + c2_m4 + c3_m4 + c5_m4 + c6_m4 } */ run generateStrongerPredicate1stStrategy { -- use successively with Q, Q1st1 and Q1st2 NBCQ = NBC[maze8, Q[maze8.states]] } /* fun Q2nd1[X: maze8.states] : maze8.states { -- predicate obtained after one iteration c2_m4 } fun Q2nd2[X: maze8.states] : maze8.states { -- predicate obtained after two iterations c2_m4 + c2_m0 + c2_m3 } fun Q2nd3[X: maze8.states] : maze8.states { -- predicate obtained after three iterations c0_m4 + c1_m4 + c2_m0 + c2_m3 + c2_m4 + c3_m4 + c5_m4 + c6_m4 } */ run generateWeakerPredicate2ndStrategy { -- use successively with none, Q2nd1, Q2nd2 and Q2nd3 NBCQ.IsWeakerNBC[none, maze8, Q[maze8.states]] } for 1 run generateWeakerPredicate3rdStrategy { -- generate {}, {c2_m4}, {c0_m4,c1_m4,c2_m4,c3_m4,c5_m4,c6_m4}, -- {c2_m0,c2_m3 c2_m4} and -- {c0_m4,c1_m4,c2_m0,c2_m3,c2_m4,c3_m4,c5_m4,c6_m4} with next NBCQ.IsNBC[maze8, Q[maze8.states]] } for 1