open SBCDES_Total_Observation[StateSpace, EventSet] -- Maze for cat and mouse with five rooms 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 } enum LocalStateSpace { c0, c1, c2, c3, c4, m0, m1, m2, m3, m4 } enum EventSet { cd1, cd2, cd3, cd4, cd5, cd6, cd7, md1, md2, md3, md4, md5, md6 } one sig maze5 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 localStates = c0 + c1 + c2 + c3 + c4 + 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) 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) events = cd1 + cd2 + cd3 + cd4 + cd5 + cd6 + cd7 + md1 + md2 + md3 + md4 + md5 + md6 controllableEvents = 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 -> c3_m0) + (c1_m0 -> md1 -> c1_m2) + (c1_m0 -> md4 -> c1_m4) + (c1_m1 -> cd2 -> c2_m1) + (c1_m1 -> cd7 -> c3_m1) + (c1_m1 -> md3 -> c1_m0) + (c1_m2 -> cd2 -> c2_m2) + (c1_m2 -> cd7 -> c3_m2) + (c1_m2 -> md2 -> c1_m1) + (c1_m3 -> cd2 -> c2_m3) + (c1_m3 -> cd7 -> c3_m3) + (c1_m3 -> md6 -> c1_m0) + (c1_m4 -> cd2 -> c2_m4) + (c1_m4 -> cd7 -> c3_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 -> cd7 -> c1_m0) + (c3_m0 -> md1 -> c3_m2) + (c3_m0 -> md4 -> c3_m4) + (c3_m1 -> cd5 -> c4_m1) + (c3_m1 -> cd7 -> c1_m1) + (c3_m1 -> md3 -> c3_m0) + (c3_m2 -> cd5 -> c4_m2) + (c3_m2 -> cd7 -> c1_m2) + (c3_m2 -> md2 -> c3_m1) + (c3_m3 -> cd5 -> c4_m3) + (c3_m3 -> cd7 -> c1_m3) + (c3_m3 -> md6 -> c3_m0) + (c3_m4 -> cd5 -> c4_m4) + (c3_m4 -> cd7 -> 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) } fun Q[X: maze5.states] : maze5.states { -- The cat and mouse never occupy the same room simultaneously { x : X | not (x.(maze5.firstProcess) = c0 and x.(maze5.secondProcess) = m0) and not (x.(maze5.firstProcess) = c1 and x.(maze5.secondProcess) = m1) and not (x.(maze5.firstProcess) = c2 and x.(maze5.secondProcess) = m2) and not (x.(maze5.firstProcess) = c3 and x.(maze5.secondProcess) = m3) and not (x.(maze5.firstProcess) = c4 and x.(maze5.secondProcess) = m4) } } run { } for 1 sig NBCQ in StateSpace { } fact { NBCQ in maze5.states } /* fun Q1st1[X: maze5.states] : maze5.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 } fun Q1st2[X: maze5.states] : maze5.states { -- predicate obtained after two iterations (the solution) c0_m4 + c1_m4 + c2_m0 + c2_m3 + c2_m4 + c3_m4 } */ run generateStrongerPredicate1stStrategy { -- use successively with Q, Q1st1 and Q1st2 NBCQ = NBC[maze5, Q[maze5.states]] } /* fun Q2nd1[X: maze5.states] : maze5.states { -- predicate obtained after one iteration c2_m4 } fun Q2nd2[X: maze5.states] : maze5.states { -- predicate obtained after two iterations c2_m4 + c2_m0 + c2_m3 } fun Q2nd3[X: maze5.states] : maze5.states { -- predicate obtained after three iterations c0_m4 + c1_m4 + c2_m0 + c2_m3 + c2_m4 + c3_m4 } */ run generateWeakerPredicate2ndStrategy { -- use successively with none, Q2nd1, Q2nd2 and Q2nd3 NBCQ.IsWeakerNBC[none, maze5, Q[maze5.states]] } for 1 run generateWeakerPredicate3rdStrategy { -- generate {}, {c2_m4}, {c0_m4,c1_m4,c2_m4,c3_m4}, -- {c2_m0,c2_m3 c2_m4} and -- {c0_m4,c1_m4,c2_m0,c2_m3,c2_m4,c3_m4} with next NBCQ.IsNBC[maze5, Q[maze5.states]] } for 1