open SBCDES_Total_Observation[StateSpace, Events] -- The distribution station of the MPS from: -- D. Cote, -- Conception par composants de controleurs d'usines modulaires -- utilisant la theorie du controle supervise, -- Ph.D. thesis, Universite de Sherbrooke, 2011. -- copyright Richard St-Denis, Universite de Sherbrooke, 2014. enum StateSpace { IaRnVx0, RaRnVx1, WaRnVx1, HaRnVx2, Hm2lnVx2, HaLnVx3, HaLpAx3, Hm2rnVx3, HaLVx4, HaRnVx3, IaLVx5, Hm2rVx4, RaLVx6, Im2rVx5, HaRVx4, WaLVx6, Rm2rVx6, IaRVx7, IaRVx5, HaRlAx4, HaLVx6, Wm2rVx6, RaRVx8, IaRlAx7, RaRVx6, IaRlAx5, HaRnVx4, Hm2rVx6, WaRVx8, RaRlAx8, IaRnVx7, WaRVx6, RaRlAx6, IaRnVx5, HaRVx8, HaRVx9, WaRlAx8, RaRnVx8, Im2lnVx11, HaRVx6, WaRlAx6, RaRnVx6, HaRlAx8, HaRlAx9, WaRnVx8, Rm2lnVx12, IaLnVx13, HaRlAx6, WaRnVx6, HaRnVx8, HaRnVx9, Wm2lnVx12, RaLnVx14, IaLpAx13, Im2rnVx13, IaLnVx16, HaRnVx6, Hm2lnVx9, Hm2lnVx12, WaLnVx14, RaLpAx14, Rm2rnVx14, RaLnVx15, IaLVx13, IaLpAx16, IaRnVx13, Im2rnVx16, HaLnVx10, HaLnVx14, WaLpAx14, Wm2rnVx14, WaLnVx15, RaLVx14, RaLpAx15, RaRnVx14, Rm2rnVx15, Im2rVx13, IaLVx16, IaRnVx16, HaLpAx10, Hm2rnVx10, HaLpAx14, Hm2rnVx14, HaLnVx15, WaLVx14, WaLpAx15, WaRnVx14, Wm2rnVx15, Rm2rVx14, RaLVx15, RaRnVx15, IaRVx13, Im2rVx16, HaLVx10, HaRnVx10, HaLVx14, HaLpAx15, HaRnVx14, Hm2rnVx15, Wm2rVx14, WaLVx15, WaRnVx15, RaRVx14, Rm2rVx15, IaRlAx13, IaRVx16, IaRVx0, Hm2rVx10, HaLVx3, Hm2rVx14, HaLVx15, HaRnVx15, HaRnVx1, WaRVx14, Wm2rVx15, RaRlAx14, RaRVx15, RaRVx1, IaRlAx16, IaRlAx0, HaRVx10, Hm2rVx3, HaRVx14, Hm2rVx15, WaRlAx14, WaRVx15, WaRVx1, RaRlAx15, RaRlAx1, HaRlAx10, HaRVx3, HaRlAx14, HaRVx15, HaRVx1, WaRlAx15, HaRVx2, WaRlAx1, HaRlAx3, HaRlAx15, HaRlAx1, HaRlAx2 } enum LocalStateSpace { I, R, W, H, aLnV, aLpA, aLV, aRnV, aRV, aRlA, m2lnV, m2rnV, m2rV, x0, x1, x2, x3, x4, x5, x6, x7, x8, x9, x10, x11, x12, x13, x14, x15, x16 } enum Events { wpa, inject, eoi, rearm, ch, eoch, oh, eooh, gr, eogr, gl, eogl, rst } one sig distribution extends Automaton { localStates : set LocalStateSpace, injector : set StateSpace -> LocalStateSpace, crane : set StateSpace -> LocalStateSpace, sequencer : set StateSpace -> LocalStateSpace } { states = IaRnVx0 + RaRnVx1 + WaRnVx1 + HaRnVx2 + Hm2lnVx2 + HaLnVx3 + HaLpAx3 + Hm2rnVx3 + HaLVx4 + HaRnVx3 + IaLVx5 + Hm2rVx4 + RaLVx6 + Im2rVx5 + HaRVx4 + WaLVx6 + Rm2rVx6 + IaRVx7 + IaRVx5 + HaRlAx4 + HaLVx6 + Wm2rVx6 + RaRVx8 + IaRlAx7 + RaRVx6 + IaRlAx5 + HaRnVx4 + Hm2rVx6 + WaRVx8 + RaRlAx8 + IaRnVx7 + WaRVx6 + RaRlAx6 + IaRnVx5 + HaRVx8 + HaRVx9 + WaRlAx8 + RaRnVx8 + Im2lnVx11 + HaRVx6 + WaRlAx6 + RaRnVx6 + HaRlAx8 + HaRlAx9 + WaRnVx8 + Rm2lnVx12 + IaLnVx13 + HaRlAx6 + WaRnVx6 + HaRnVx8 + HaRnVx9 + Wm2lnVx12 + RaLnVx14 + IaLpAx13 + Im2rnVx13 + IaLnVx16 + HaRnVx6 + Hm2lnVx9 + Hm2lnVx12 + WaLnVx14 + RaLpAx14 + Rm2rnVx14 + RaLnVx15 + IaLVx13 + IaLpAx16 + IaRnVx13 + Im2rnVx16 + HaLnVx10 + HaLnVx14 + WaLpAx14 + Wm2rnVx14 + WaLnVx15 + RaLVx14 + RaLpAx15 + RaRnVx14 + Rm2rnVx15 + Im2rVx13 + IaLVx16 + IaRnVx16 + HaLpAx10 + Hm2rnVx10 + HaLpAx14 + Hm2rnVx14 + HaLnVx15 + WaLVx14 + WaLpAx15 + WaRnVx14 + Wm2rnVx15 + Rm2rVx14 + RaLVx15 + RaRnVx15 + IaRVx13 + Im2rVx16 + HaLVx10 + HaRnVx10 + HaLVx14 + HaLpAx15 + HaRnVx14 + Hm2rnVx15 + Wm2rVx14 + WaLVx15 + WaRnVx15 + RaRVx14 + Rm2rVx15 + IaRlAx13 + IaRVx16 + IaRVx0 + Hm2rVx10 + HaLVx3 + Hm2rVx14 + HaLVx15 + HaRnVx15 + HaRnVx1 + WaRVx14 + Wm2rVx15 + RaRlAx14 + RaRVx15 + RaRVx1 + IaRlAx16 + IaRlAx0 + HaRVx10 + Hm2rVx3 + HaRVx14 + Hm2rVx15 + WaRlAx14 + WaRVx15 + WaRVx1 + RaRlAx15 + RaRlAx1 + HaRlAx10 + HaRVx3 + HaRlAx14 + HaRVx15 + HaRVx1 + WaRlAx15 + HaRVx2 + WaRlAx1 + HaRlAx3 + HaRlAx15 + HaRlAx1 + HaRlAx2 localStates = I + R + W + H + aLnV + aLpA + aLV + aRnV + aRV + aRlA + m2lnV + m2rnV + m2rV + x0 + x1 + x2 + x3 + x4 + x5 + x6 + x7 + x8 + x9 + x10 + x11 + x12 + x13 + x14 + x15 + x16 injector = (IaRnVx0 -> I) + (RaRnVx1 -> R) + (WaRnVx1 -> W) + (HaRnVx2 -> H) + (Hm2lnVx2 -> H) + (HaLnVx3 -> H) + (HaLpAx3 -> H) + (Hm2rnVx3 -> H) + (HaLVx4 -> H) + (HaRnVx3 -> H) + (IaLVx5 -> I) + (Hm2rVx4 -> H) + (RaLVx6 -> R) + (Im2rVx5 -> I) + (HaRVx4 -> H) + (WaLVx6 -> W) + (Rm2rVx6 -> R) + (IaRVx7 -> I) + (IaRVx5 -> I) + (HaRlAx4 -> H) + (HaLVx6 -> H) + (Wm2rVx6 -> W) + (RaRVx8 -> R) + (IaRlAx7 -> I) + (RaRVx6 -> R) + (IaRlAx5 -> I) + (HaRnVx4 -> H) + (Hm2rVx6 -> H) + (WaRVx8 -> W) + (RaRlAx8 -> R) + (IaRnVx7 -> I) + (WaRVx6 -> W) + (RaRlAx6 -> R) + (IaRnVx5 -> I) + (HaRVx8 -> H) + (HaRVx9 -> H) + (WaRlAx8 -> W) + (RaRnVx8 -> R) + (Im2lnVx11 -> I) + (HaRVx6 -> H) + (WaRlAx6 -> W) + (RaRnVx6 -> R) + (HaRlAx8 -> H) + (HaRlAx9 -> H) + (WaRnVx8 -> W) + (Rm2lnVx12 -> R) + (IaLnVx13 -> I) + (HaRlAx6 -> H) + (WaRnVx6 -> W) + (HaRnVx8 -> H) + (HaRnVx9 -> H) + (Wm2lnVx12 -> W) + (RaLnVx14 -> R) + (IaLpAx13 -> I) + (Im2rnVx13 -> I) + (IaLnVx16 -> I) + (HaRnVx6 -> H) + (Hm2lnVx9 -> H) + (Hm2lnVx12 -> H) + (WaLnVx14 -> W) + (RaLpAx14 -> R) + (Rm2rnVx14 -> R) + (RaLnVx15 -> R) + (IaLVx13 -> I) + (IaLpAx16 -> I) + (IaRnVx13 -> I) + (Im2rnVx16 -> I) + (HaLnVx10 -> H) + (HaLnVx14 -> H) + (WaLpAx14 -> W) + (Wm2rnVx14 -> W) + (WaLnVx15 -> W) + (RaLVx14 -> R) + (RaLpAx15 -> R) + (RaRnVx14 -> R) + (Rm2rnVx15 -> R) + (Im2rVx13 -> I) + (IaLVx16 -> I) + (IaRnVx16 -> I) + (HaLpAx10 -> H) + (Hm2rnVx10 -> H) + (HaLpAx14 -> H) + (Hm2rnVx14 -> H) + (HaLnVx15 -> H) + (WaLVx14 -> W) + (WaLpAx15 -> W) + (WaRnVx14 -> W) + (Wm2rnVx15 -> W) + (Rm2rVx14 -> R) + (RaLVx15 -> R) + (RaRnVx15 -> R) + (IaRVx13 -> I) + (Im2rVx16 -> I) + (HaLVx10 -> H) + (HaRnVx10 -> H) + (HaLVx14 -> H) + (HaLpAx15 -> H) + (HaRnVx14 -> H) + (Hm2rnVx15 -> H) + (Wm2rVx14 -> W) + (WaLVx15 -> W) + (WaRnVx15 -> W) + (RaRVx14 -> R) + (Rm2rVx15 -> R) + (IaRlAx13 -> I) + (IaRVx16 -> I) + (IaRVx0 -> I) + (Hm2rVx10 -> H) + (HaLVx3 -> H) + (Hm2rVx14 -> H) + (HaLVx15 -> H) + (HaRnVx15 -> H) + (HaRnVx1 -> H) + (WaRVx14 -> W) + (Wm2rVx15 -> W) + (RaRlAx14 -> R) + (RaRVx15 -> R) + (RaRVx1-> R) + (IaRlAx16 -> I) + (IaRlAx0 -> I) + (HaRVx10 -> H) + (Hm2rVx3 -> H) + (HaRVx14 -> H) + (Hm2rVx15 -> H) + (WaRlAx14 -> W) + (WaRVx15 -> W) + (WaRVx1 -> W) + (RaRlAx15 -> R) + (RaRlAx1 -> R) + (HaRlAx10 -> H) + (HaRVx3 -> H) + (HaRlAx14 -> H) + (HaRVx15 -> H) + (HaRVx1 -> H) + (WaRlAx15 -> W) + (HaRVx2 -> H) + (WaRlAx1 -> W) + (HaRlAx3 -> H) + (HaRlAx15 -> H) + (HaRlAx1 -> H) + (HaRlAx2 -> H) crane = (IaRnVx0 -> aRnV) + (RaRnVx1 -> aRnV) + (WaRnVx1 -> aRnV) + (HaRnVx2 -> aRnV) + (Hm2lnVx2 -> m2lnV) + (HaLnVx3 -> aLnV) + (HaLpAx3 -> aLpA) + (Hm2rnVx3 -> m2rnV) + (HaLVx4 -> aLV) + (HaRnVx3 -> aRnV) + (IaLVx5 -> aLV) + (Hm2rVx4 -> m2rV) + (RaLVx6 -> aLV) + (Im2rVx5 -> m2rV) + (HaRVx4 -> aRV) + (WaLVx6 -> aLV) + (Rm2rVx6 -> m2rV) + (IaRVx7 -> aRV) + (IaRVx5 -> aRV) + (HaRlAx4 -> aRlA) + (HaLVx6 -> aLV) + (Wm2rVx6 -> m2rV) + (RaRVx8 -> aRV) + (IaRlAx7 -> aRlA) + (RaRVx6 -> aRV) + (IaRlAx5 -> aRlA) + (HaRnVx4 -> aRnV) + (Hm2rVx6 -> m2rV) + (WaRVx8 -> aRV) + (RaRlAx8 -> aRlA) + (IaRnVx7 -> aRnV) + (WaRVx6 -> aRV) + (RaRlAx6 -> aRlA) + (IaRnVx5 -> aRnV) + (HaRVx8 -> aRV) + (HaRVx9 -> aRV) + (WaRlAx8 -> aRlA) + (RaRnVx8 -> aRnV) + (Im2lnVx11 -> m2lnV) + (HaRVx6 -> aRV) + (WaRlAx6 -> aRlA) + (RaRnVx6 -> aRnV) + (HaRlAx8 -> aRlA) + (HaRlAx9 -> aRlA) + (WaRnVx8 -> aRnV) + (Rm2lnVx12 -> m2lnV) + (IaLnVx13 -> aLnV) + (HaRlAx6 -> aRlA) + (WaRnVx6 -> aRnV) + (HaRnVx8 -> aRnV) + (HaRnVx9 -> aRnV) + (Wm2lnVx12 -> m2lnV) + (RaLnVx14 -> aLnV) + (IaLpAx13 -> aLpA) + (Im2rnVx13 -> m2rnV) + (IaLnVx16 -> aLnV) + (HaRnVx6 -> aRnV) + (Hm2lnVx9 -> m2lnV) + (Hm2lnVx12 -> m2lnV) + (WaLnVx14 -> aLnV) + (RaLpAx14 -> aLpA) + (Rm2rnVx14 -> m2rnV) + (RaLnVx15 -> aLnV) + (IaLVx13 -> aLV) + (IaLpAx16 -> aLpA) + (IaRnVx13 -> aRnV) + (Im2rnVx16 -> m2rnV) + (HaLnVx10 -> aLnV) + (HaLnVx14 -> aLnV) + (WaLpAx14 -> aLpA) + (Wm2rnVx14 -> m2rnV) + (WaLnVx15 -> aLnV) + (RaLVx14 -> aLV) + (RaLpAx15 -> aLpA) + (RaRnVx14 -> aRnV) + (Rm2rnVx15 -> m2rnV) + (Im2rVx13 -> m2rV) + (IaLVx16 -> aLV) + (IaRnVx16 -> aRnV) + (HaLpAx10 -> aLpA) + (Hm2rnVx10 -> m2rnV) + (HaLpAx14 -> aLpA) + (Hm2rnVx14 -> m2rnV) + (HaLnVx15 -> aLnV) + (WaLVx14 -> aLV) + (WaLpAx15 -> aLpA) + (WaRnVx14 -> aRnV) + (Wm2rnVx15 -> m2rnV) + (Rm2rVx14 -> m2rV) + (RaLVx15 -> aLV) + (RaRnVx15 -> aRnV) + (IaRVx13 -> aRV) + (Im2rVx16 -> m2rV) + (HaLVx10 -> aLV) + (HaRnVx10 -> aRnV) + (HaLVx14 -> aLV) + (HaLpAx15 -> aLpA) + (HaRnVx14 -> aRnV) + (Hm2rnVx15 -> m2rnV) + (Wm2rVx14 -> m2rV) + (WaLVx15 -> aLV) + (WaRnVx15 -> aRnV) + (RaRVx14 -> aRV) + (Rm2rVx15 -> m2rV) + (IaRlAx13 -> aRlA) + (IaRVx16 -> aRV) + (IaRVx0 -> aRV) + (Hm2rVx10 -> m2rV) + (HaLVx3 -> aLV) + (Hm2rVx14 -> m2rV) + (HaLVx15 -> aLV) + (HaRnVx15 -> aRnV) + (HaRnVx1 -> aRnV) + (WaRVx14 -> aRV) + (Wm2rVx15 -> m2rV) + (RaRlAx14 -> aRlA) + (RaRVx15 -> aRV) + (RaRVx1-> aRV) + (IaRlAx16 -> aRlA) + (IaRlAx0 -> aRlA) + (HaRVx10 -> aRV) + (Hm2rVx3 -> m2rV) + (HaRVx14 -> aRV) + (Hm2rVx15 -> m2rV) + (WaRlAx14 -> aRlA) + (WaRVx15 -> aRV) + (WaRVx1 -> aRV) + (RaRlAx15 -> aRlA) + (RaRlAx1 -> aRlA) + (HaRlAx10 -> aRlA) + (HaRVx3 -> aRV) + (HaRlAx14 -> aRlA) + (HaRVx15 -> aRV) + (HaRVx1 -> aRV) + (WaRlAx15 -> aRlA) + (HaRVx2 -> aRV) + (WaRlAx1 -> aRlA) + (HaRlAx3 -> aRlA) + (HaRlAx15 -> aRlA) + (HaRlAx1 -> aRlA) + (HaRlAx2 -> aRlA) sequencer = (IaRnVx0 -> x0) + (RaRnVx1 -> x1) + (WaRnVx1 -> x1) + (HaRnVx2 -> x2) + (Hm2lnVx2 -> x2) + (HaLnVx3 -> x3) + (HaLpAx3 -> x3) + (Hm2rnVx3 -> x3) + (HaLVx4 -> x4) + (HaRnVx3 -> x3) + (IaLVx5 -> x5) + (Hm2rVx4 -> x4) + (RaLVx6 -> x6) + (Im2rVx5 -> x5) + (HaRVx4 -> x4) + (WaLVx6 -> x6) + (Rm2rVx6 -> x6) + (IaRVx7 -> x7) + (IaRVx5 -> x5) + (HaRlAx4 -> x4) + (HaLVx6 -> x6) + (Wm2rVx6 -> x6) + (RaRVx8 -> x8) + (IaRlAx7 -> x7) + (RaRVx6 -> x6) + (IaRlAx5 -> x5) + (HaRnVx4 -> x4) + (Hm2rVx6 -> x6) + (WaRVx8 -> x8) + (RaRlAx8 -> x8) + (IaRnVx7 -> x7) + (WaRVx6 -> x6) + (RaRlAx6 -> x6) + (IaRnVx5 -> x5) + (HaRVx8 -> x8) + (HaRVx9 -> x9) + (WaRlAx8 -> x8) + (RaRnVx8 -> x8) + (Im2lnVx11 -> x11) + (HaRVx6 -> x6) + (WaRlAx6 -> x6) + (RaRnVx6 -> x6) + (HaRlAx8 -> x8) + (HaRlAx9 -> x9) + (WaRnVx8 -> x8) + (Rm2lnVx12 -> x12) + (IaLnVx13 -> x13) + (HaRlAx6 -> x6) + (WaRnVx6 -> x6) + (HaRnVx8 -> x8) + (HaRnVx9 -> x9) + (Wm2lnVx12 -> x12) + (RaLnVx14 -> x14) + (IaLpAx13 -> x13) + (Im2rnVx13 -> x13) + (IaLnVx16 -> x16) + (HaRnVx6 -> x6) + (Hm2lnVx9 -> x9) + (Hm2lnVx12 -> x12) + (WaLnVx14 -> x14) + (RaLpAx14 -> x14) + (Rm2rnVx14 -> x14) + (RaLnVx15 -> x15) + (IaLVx13 -> x13) + (IaLpAx16 -> x16) + (IaRnVx13 -> x13) + (Im2rnVx16 -> x16) + (HaLnVx10 -> x10) + (HaLnVx14 -> x14) + (WaLpAx14 -> x14) + (Wm2rnVx14 -> x14) + (WaLnVx15 -> x15) + (RaLVx14 -> x14) + (RaLpAx15 -> x15) + (RaRnVx14 -> x14) + (Rm2rnVx15 -> x15) + (Im2rVx13 -> x13) + (IaLVx16 -> x16) + (IaRnVx16 -> x16) + (HaLpAx10 -> x10) + (Hm2rnVx10 -> x10) + (HaLpAx14 -> x14) + (Hm2rnVx14 -> x14) + (HaLnVx15 -> x15) + (WaLVx14 -> x14) + (WaLpAx15 -> x15) + (WaRnVx14 -> x14) + (Wm2rnVx15 -> x15) + (Rm2rVx14 -> x14) + (RaLVx15 -> x15) + (RaRnVx15 -> x15) + (IaRVx13 -> x13) + (Im2rVx16 -> x16) + (HaLVx10 -> x10) + (HaRnVx10 -> x10) + (HaLVx14 -> x14) + (HaLpAx15 -> x15) + (HaRnVx14 -> x14) + (Hm2rnVx15 -> x15) + (Wm2rVx14 -> x14) + (WaLVx15 -> x15) + (WaRnVx15 -> x15) + (RaRVx14 -> x14) + (Rm2rVx15 -> x15) + (IaRlAx13 -> x13) + (IaRVx16 -> x16) + (IaRVx0 -> x0) + (Hm2rVx10 -> x10) + (HaLVx3 -> x3) + (Hm2rVx14 -> x14) + (HaLVx15 -> x15) + (HaRnVx15 -> x15) + (HaRnVx1 -> x1) + (WaRVx14 -> x14) + (Wm2rVx15 -> x15) + (RaRlAx14 -> x14) + (RaRVx15 -> x15) + (RaRVx1-> x1) + (IaRlAx16 -> x16) + (IaRlAx0 -> x10) + (HaRVx10 -> x10) + (Hm2rVx3 -> x3) + (HaRVx14 -> x14) + (Hm2rVx15 -> x15) + (WaRlAx14 -> x14) + (WaRVx15 -> x15) + (WaRVx1 -> x1) + (RaRlAx15 -> x15) + (RaRlAx1 -> x1) + (HaRlAx10 -> x10) + (HaRVx3 -> x3) + (HaRlAx14 -> x14) + (HaRVx15 -> x15) + (HaRVx1 -> x1) + (WaRlAx15 -> x15) + (HaRVx2 -> x2) + (WaRlAx1 -> x1) + (HaRlAx3 -> x3) + (HaRlAx15 -> x15) + (HaRlAx1 -> x1) + (HaRlAx2 -> x2) events = wpa + inject + eoi + rearm + ch + eoch + oh + eooh + gr + eogr + gl + eogl + rst controllableEvents = inject + rearm + ch + oh + gr + gl + rst initialState = IaRnVx0 markedStates = IaRnVx0 transition = (IaRnVx0 -> wpa -> RaRnVx1) + (RaRnVx1 -> inject -> WaRnVx1) + (WaRnVx1 -> eoi -> HaRnVx2) + (HaRnVx2 -> gl -> Hm2lnVx2) + (Hm2lnVx2 -> eogl -> HaLnVx3) + (HaLnVx3 -> ch -> HaLpAx3) + (HaLnVx3 -> gr -> Hm2rnVx3) + (HaLpAx3 -> eoch -> HaLVx4) + (Hm2rnVx3 -> eogr -> HaRnVx3) + (HaLVx4 -> rearm -> IaLVx5) + (HaLVx4 -> gr -> Hm2rVx4) + (IaLVx5 -> wpa -> RaLVx6) + (IaLVx5 -> gr -> Im2rVx5) + (Hm2rVx4 -> rearm -> Im2rVx5) + (Hm2rVx4 -> eogr -> HaRVx4) + (RaLVx6 -> inject -> WaLVx6) + (RaLVx6 -> gr -> Rm2rVx6) + (Im2rVx5 -> wpa -> Rm2rVx6) + (Im2rVx5 -> eogr -> IaRVx7) + (HaRVx4 -> rearm -> IaRVx5) + (HaRVx4 -> oh -> HaRlAx4) + (WaLVx6 -> eoi -> HaLVx6) + (WaLVx6 -> gr -> Wm2rVx6) + (Rm2rVx6 -> inject -> Wm2rVx6) + (Rm2rVx6 -> eogr -> RaRVx8) + (IaRVx7 -> wpa -> RaRVx8) + (IaRVx7 -> oh -> IaRlAx7) + (IaRVx5 -> wpa -> RaRVx6) + (IaRVx5 -> oh -> IaRlAx5) + (HaRlAx4 -> rearm -> IaRlAx5) + (HaRlAx4 -> eooh -> HaRnVx4) + (HaLVx6 -> gr -> Hm2rVx6) + (Wm2rVx6 -> eoi -> Hm2rVx6) + (Wm2rVx6 -> eogr -> WaRVx8) + (RaRVx8 -> inject -> WaRVx8) + (RaRVx8 -> oh -> RaRlAx8) + (IaRlAx7 -> wpa -> RaRlAx8) + (IaRlAx7 -> eooh -> IaRnVx7) + (RaRVx6 -> inject -> WaRVx6) + (RaRVx6 -> oh -> RaRlAx6) + (IaRlAx5 -> wpa -> RaRlAx6) + (IaRlAx5 -> eooh -> IaRnVx5) + (HaRnVx4 -> rearm -> IaRnVx5) + (Hm2rVx6 -> eogr -> HaRVx8) + (WaRVx8 -> eoi -> HaRVx9) + (WaRVx8 -> oh -> WaRlAx8) + (RaRlAx8 -> inject -> WaRlAx8) + (RaRlAx8 -> eooh -> RaRnVx8) + (IaRnVx7 -> wpa -> RaRnVx8) + (IaRnVx7 -> gl -> Im2lnVx11) + (WaRVx6 -> eoi -> HaRVx6) + (WaRVx6 -> oh -> WaRlAx6) + (RaRlAx6 -> inject -> WaRlAx6) + (RaRlAx6 -> eooh -> RaRnVx6) + (IaRnVx5 -> wpa -> RaRnVx6) + (HaRVx8 -> oh -> HaRlAx8) + (HaRVx9 -> oh -> HaRlAx9) + (WaRlAx8 -> eoi -> HaRlAx9) + (WaRlAx8 -> eooh -> WaRnVx8) + (RaRnVx8 -> inject -> WaRnVx8) + (Im2lnVx11 -> wpa -> Rm2lnVx12) + (Im2lnVx11 -> eogl -> IaLnVx13) + (HaRVx6 -> oh -> HaRlAx6) + (WaRlAx6 -> eoi -> HaRlAx6) + (WaRlAx6 -> eooh -> WaRnVx6) + (RaRnVx6 -> inject -> WaRnVx6) + (HaRlAx8 -> eooh -> HaRnVx8) + (HaRlAx9 -> eooh -> HaRnVx9) + (WaRnVx8 -> eoi -> HaRnVx9) + (Rm2lnVx12 -> inject -> Wm2lnVx12) + (Rm2lnVx12 -> eogl -> RaLnVx14) + (IaLnVx13 -> wpa -> RaLnVx14) + (IaLnVx13 -> ch -> IaLpAx13) + (IaLnVx13 -> gr -> Im2rnVx13) + (IaLnVx13 -> rst -> IaLnVx16) + (HaRlAx6 -> eooh -> HaRnVx6) + (WaRnVx6 -> eoi -> HaRnVx6) + (HaRnVx9 -> gl -> Hm2lnVx9) + (Wm2lnVx12 -> eoi -> Hm2lnVx12) + (Wm2lnVx12 -> eogl -> WaLnVx14) + (RaLnVx14 -> inject -> WaLnVx14) + (RaLnVx14 -> ch -> RaLpAx14) + (RaLnVx14 -> gr -> Rm2rnVx14) + (RaLnVx14 -> rst -> RaLnVx15) + (IaLpAx13 -> wpa -> RaLpAx14) + (IaLpAx13 -> eoch -> IaLVx13) + (IaLpAx13 -> rst -> IaLpAx16) + (Im2rnVx13 -> wpa -> Rm2rnVx14) + (Im2rnVx13 -> eogr -> IaRnVx13) + (Im2rnVx13 -> rst -> Im2rnVx16) + (IaLnVx16 -> wpa -> RaLnVx15) + (IaLnVx16 -> ch -> IaLpAx16) + (IaLnVx16 -> gr -> Im2rnVx16) + (Hm2lnVx9 -> eogl -> HaLnVx10) + (Hm2lnVx12 -> eogl -> HaLnVx14) + (WaLnVx14 -> eoi -> HaLnVx14) + (WaLnVx14 -> ch -> WaLpAx14) + (WaLnVx14 -> gr -> Wm2rnVx14) + (WaLnVx14 -> rst -> WaLnVx15) + (RaLpAx14 -> inject -> WaLpAx14) + (RaLpAx14 -> eoch -> RaLVx14) + (RaLpAx14 -> rst -> RaLpAx15) + (Rm2rnVx14 -> inject -> Wm2rnVx14) + (Rm2rnVx14 -> eogr -> RaRnVx14) + (Rm2rnVx14 -> rst -> Rm2rnVx15) + (RaLnVx15 -> inject -> WaLnVx15) + (RaLnVx15 -> ch -> RaLpAx15) + (RaLnVx15 -> gr -> Rm2rnVx15) + (IaLVx13 -> wpa -> RaLVx14) + (IaLVx13 -> gr -> Im2rVx13) + (IaLVx13 -> rst -> IaLVx16) + (IaLpAx16 -> wpa -> RaLpAx15) + (IaLpAx16 -> eoch -> IaLVx16) + (IaRnVx13 -> wpa -> RaRnVx14) + (IaRnVx13 -> rst -> IaRnVx16) + (Im2rnVx16 -> wpa -> Rm2rnVx15) + (Im2rnVx16 -> eogr -> IaRnVx0) + (HaLnVx10 -> ch -> HaLpAx10) + (HaLnVx10 -> gr -> Hm2rnVx10) + (HaLnVx10 -> rst -> HaLnVx3) + (HaLnVx14 -> ch -> HaLpAx14) + (HaLnVx14 -> gr -> Hm2rnVx14) + (HaLnVx14 -> rst -> HaLnVx15) + (WaLpAx14 -> eoi -> HaLpAx14) + (WaLpAx14 -> eoch -> WaLVx14) + (WaLpAx14 -> rst -> WaLpAx15) + (Wm2rnVx14 -> eoi -> Hm2rnVx14) + (Wm2rnVx14 -> eogr -> WaRnVx14) + (Wm2rnVx14 -> rst -> Wm2rnVx15) + (WaLnVx15 -> eoi -> HaLnVx15) + (WaLnVx15 -> ch -> WaLpAx15) + (WaLnVx15 -> gr -> Wm2rnVx15) + (RaLVx14 -> inject -> WaLVx14) + (RaLVx14 -> gr -> Rm2rVx14) + (RaLVx14 -> rst -> RaLVx15) + (RaLpAx15 -> inject -> WaLpAx15) + (RaLpAx15 -> eoch -> RaLVx15) + (RaRnVx14 -> inject -> WaRnVx14) + (RaRnVx14 -> rst -> RaRnVx15) + (Rm2rnVx15 -> inject -> Wm2rnVx15) + (Rm2rnVx15 -> eogr -> RaRnVx1) + (Im2rVx13 -> wpa -> Rm2rVx14) + (Im2rVx13 -> eogr -> IaRVx13) + (Im2rVx13 -> rst -> Im2rVx16) + (IaLVx16 -> wpa -> RaLVx15) + (IaLVx16 -> gr -> Im2rVx16) + (IaRnVx16 -> wpa -> RaRnVx15) + (HaLpAx10 -> eoch -> HaLVx10) + (HaLpAx10 -> rst -> HaLpAx3) + (Hm2rnVx10 -> eogr -> HaRnVx10) + (Hm2rnVx10 -> rst -> Hm2rnVx3) + (HaLpAx14 -> eoch -> HaLVx14) + (HaLpAx14 -> rst -> HaLpAx15) + (Hm2rnVx14 -> eogr -> HaRnVx14) + (Hm2rnVx14 -> rst -> Hm2rnVx15) + (HaLnVx15 -> ch -> HaLpAx15) + (HaLnVx15 -> gr -> Hm2rnVx15) + (WaLVx14 -> eoi -> HaLVx14) + (WaLVx14 -> gr -> Wm2rVx14) + (WaLVx14 -> rst -> WaLVx15) + (WaLpAx15 -> eoi -> HaLpAx15) + (WaLpAx15 -> eoch -> WaLVx15) + (WaRnVx14 -> eoi -> HaRnVx14) + (WaRnVx14 -> rst -> WaRnVx15) + (Wm2rnVx15 -> eoi -> Hm2rnVx15) + (Wm2rnVx15 -> eogr -> WaRnVx1) + (Rm2rVx14 -> inject -> Wm2rVx14) + (Rm2rVx14 -> eogr -> RaRVx14) + (Rm2rVx14 -> rst -> Rm2rVx15) + (RaLVx15 -> inject -> WaLVx15) + (RaLVx15 -> gr -> Rm2rVx15) + (RaRnVx15 -> inject -> WaRnVx15) + (IaRVx13 -> wpa -> RaRVx14) + (IaRVx13 -> oh -> IaRlAx13) + (IaRVx13 -> rst -> IaRVx16) + (Im2rVx16 -> wpa -> Rm2rVx15) + (Im2rVx16 -> eogr -> IaRVx0) + (HaLVx10 -> gr -> Hm2rVx10) + (HaLVx10 -> rst -> HaLVx3) + (HaRnVx10 -> rst -> HaRnVx3) + (HaLVx14 -> gr -> Hm2rVx14) + (HaLVx14 -> rst -> HaLVx15) + (HaLpAx15 -> eoch -> HaLVx15) + (HaRnVx14 -> rst -> HaRnVx15) + (Hm2rnVx15 -> eogr -> HaRnVx1) + (Wm2rVx14 -> eoi -> Hm2rVx14) + (Wm2rVx14 -> eogr -> WaRVx14) + (Wm2rVx14 -> rst -> Wm2rVx15) + (WaLVx15 -> eoi -> HaLVx15) + (WaLVx15 -> gr -> Wm2rVx15) + (WaRnVx15 -> eoi -> HaRnVx15) + (RaRVx14 -> inject -> WaRVx14) + (RaRVx14 -> oh -> RaRlAx14) + (RaRVx14 -> rst -> RaRVx15) + (Rm2rVx15 -> inject -> Wm2rVx15) + (Rm2rVx15 -> eogr -> RaRVx1) + (IaRlAx13 -> wpa -> RaRlAx14) + (IaRlAx13 -> eooh -> IaRnVx13) + (IaRlAx13 -> rst -> IaRlAx16) + (IaRVx16 -> wpa -> RaRVx15) + (IaRVx16 -> oh -> IaRlAx16) + (IaRVx0 -> wpa -> RaRVx1) + (IaRVx0 -> oh -> IaRlAx0) + (Hm2rVx10 -> eogr -> HaRVx10) + (Hm2rVx10 -> rst -> Hm2rVx3) + (HaLVx3 -> gr -> Hm2rVx3) + (Hm2rVx14 -> eogr -> HaRVx14) + (Hm2rVx14 -> rst -> Hm2rVx15) + (HaLVx15 -> gr -> Hm2rVx15) + (WaRVx14 -> eoi -> HaRVx14) + (WaRVx14 -> oh -> WaRlAx14) + (WaRVx14 -> rst -> WaRVx15) + (Wm2rVx15 -> eoi -> Hm2rVx15) + (Wm2rVx15 -> eogr -> WaRVx1) + (RaRlAx14 -> inject -> WaRlAx14) + (RaRlAx14 -> eooh -> RaRnVx14) + (RaRlAx14 -> rst -> RaRlAx15) + (RaRVx15 -> inject -> WaRVx15) + (RaRVx15 -> oh -> RaRlAx15) + (RaRVx1 -> inject -> WaRVx1) + (RaRVx1 -> oh -> RaRlAx1) + (IaRlAx16 -> wpa -> RaRlAx15) + (IaRlAx16 -> eooh -> IaRnVx16) + (IaRlAx0 -> wpa -> RaRlAx1) + (IaRlAx0 -> eooh -> IaRnVx0) + (HaRVx10 -> oh -> HaRlAx10) + (HaRVx10 -> rst -> HaRVx3) + (Hm2rVx3 -> eogr -> HaRVx3) + (HaRVx14 -> oh -> HaRlAx14) + (HaRVx14 -> rst -> HaRVx15) + (Hm2rVx15 -> eogr -> HaRVx1) + (WaRlAx14 -> eoi -> HaRlAx14) + (WaRlAx14 -> eooh -> WaRnVx14) + (WaRlAx14 -> rst -> WaRlAx15) + (WaRVx15 -> eoi -> HaRVx15) + (WaRVx15 -> oh -> WaRlAx15) + (WaRVx1 -> eoi -> HaRVx2) + (WaRVx1 -> oh -> WaRlAx1) + (RaRlAx15 -> inject -> WaRlAx15) + (RaRlAx15 -> eooh -> RaRnVx15) + (RaRlAx1 -> inject -> WaRlAx1) + (RaRlAx1 -> eooh -> RaRnVx1) + (HaRlAx10 -> eooh -> HaRnVx10) + (HaRlAx10 -> rst -> HaRlAx3) + (HaRVx3 -> oh -> HaRlAx3) + (HaRlAx14 -> eooh -> HaRnVx14) + (HaRlAx14 -> rst -> HaRlAx15) + (HaRVx15 -> oh -> HaRlAx15) + (HaRVx1 -> oh -> HaRlAx1) + (WaRlAx15 -> eoi -> HaRlAx15) + (WaRlAx15 -> eooh -> WaRnVx15) + (HaRVx2 -> oh -> HaRlAx2) + (WaRlAx1 -> eoi -> HaRlAx2) + (WaRlAx1 -> eooh -> WaRnVx1) + (HaRlAx3 -> eooh -> HaRnVx3) + (HaRlAx15 -> eooh -> HaRnVx15) + (HaRlAx1 -> eooh -> HaRnVx1) + (HaRlAx2 -> eooh -> HaRnVx2) } fun Q[X : distribution.states] : distribution.states { { x : X | (not ( x.(distribution.injector) = W and (x.(distribution.crane) = m2lnV or x.(distribution.crane) = aLnV or x.(distribution.crane) = m2rnV or x.(distribution.crane) = aLpA or x.(distribution.crane) = aLV or x.(distribution.crane) = m2rV))) and (not ( x.(distribution.injector) = H and (x.(distribution.crane) = m2rnV or x.(distribution.crane) = m2rV))) and (not ( x.(distribution.crane) = aLpA and (x.(distribution.injector) = I or x.(distribution.injector) = R or x.(distribution.injector) = W))) and (not ( (x.(distribution.sequencer) = x0 or x.(distribution.sequencer) = x7 or x.(distribution.sequencer) = x13) and (x.(distribution.injector) = W or x.(distribution.crane) = m2lnV or x.(distribution.crane) = m2rnV or x.(distribution.crane) = aLpA or x.(distribution.crane) = m2rV))) and (not ( (x.(distribution.sequencer) = x1 or x.(distribution.sequencer) = x8) and (x.(distribution.injector) = I or x.(distribution.crane) = m2lnV or x.(distribution.crane) = m2rnV or x.(distribution.crane) = aLpA or x.(distribution.crane) = m2rV))) and (not ( (x.(distribution.sequencer) = x2 or x.(distribution.sequencer) = x9 or x.(distribution.sequencer) = x12) and (x.(distribution.injector) = I or x.(distribution.injector) = W or x.(distribution.crane) = m2rnV or x.(distribution.crane) = aLpA or x.(distribution.crane) = m2rV))) and (not ( x.(distribution.sequencer) = x3 and (x.(distribution.injector) = I or x.(distribution.injector) = W or x.(distribution.crane) = m2lnV or x.(distribution.crane) = m2rnV or x.(distribution.crane) = m2rV))) and (not ( (x.(distribution.sequencer) = x4 or x.(distribution.sequencer) = x10 or x.(distribution.sequencer) = x14) and (x.(distribution.injector) = I or x.(distribution.injector) = W or x.(distribution.crane) = m2lnV or x.(distribution.crane) = m2rnV or x.(distribution.crane) = aLpA or x.(distribution.crane) = m2rV))) and (not ( (x.(distribution.sequencer) = x5 or x.(distribution.sequencer) = x16) and (x.(distribution.injector) = W or x.(distribution.crane) = m2lnV or x.(distribution.crane) = aLpA))) and (not ( (x.(distribution.sequencer) = x6 or x.(distribution.sequencer) = x15) and (x.(distribution.injector) = I or x.(distribution.injector) = W or x.(distribution.crane) = m2lnV or x.(distribution.crane) = aLpA))) and (not ( x.(distribution.sequencer) = x11 and (x.(distribution.injector) = W or x.(distribution.crane) = m2rnV or x.(distribution.crane) = aLpA or x.(distribution.crane) = m2rV))) } } sig NBCQ in StateSpace {} fact{NBCQ in distribution.states} fun Q1[X : distribution.states] : distribution.states { -- first predicate obtained after one iteration HaLVx4 + HaLnVx10 + HaLnVx3 + HaLpAx3 + HaRVx9 + HaRlAx9 + HaRnVx2 + HaRnVx9 + Hm2lnVx2 + Hm2lnVx9 + IaLVx5 + IaLnVx13 + IaLnVx16 + IaRVx7 + IaRlAx7 + IaRnVx0 + IaRnVx7 + Im2lnVx11 + Im2rVx5 + Im2rnVx16 + RaLVx6 + RaLnVx14 + RaLnVx15 + RaRVx8 + RaRlAx8 + RaRnVx1 + RaRnVx8 + Rm2lnVx12 + Rm2rVx6 + Rm2rnVx15 + WaRVx8 + WaRlAx8 + WaRnVx1 + WaRnVx8 } run { } for 1 run generate { -- generate {} with next NBCQ.IsNBC[distribution, Q[distribution.states]] } for 1