open BasicProperties[StateSpace, EventSet] -- 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 EventSet { wpa, inject, eoi, rearm, ch, eoch, oh, eooh, gr, eogr, gl, eogl, rst } one sig G extends CtrlAutomaton { } { 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 events = wpa + inject + eoi + rearm + ch + eoch + oh + eooh + gr + eogr+ gl + eogl + rst controllableEvents = inject + rearm + ch + oh + gr + gl + rst 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) initialState = IaRnVx0 markedStates = IaRnVx0 } one sig H extends CtrlAutomaton { } { states = IaRnVx0 + RaRnVx1 + WaRnVx1 + HaRnVx2 + Hm2lnVx2 + HaLnVx3 + HaLpAx3 + HaLVx4 + IaLVx5 + RaLVx6 + Im2rVx5 + Rm2rVx6 + IaRVx7 + RaRVx8 + IaRlAx7 + WaRVx8 + RaRlAx8 + IaRnVx7 + HaRVx9 + WaRlAx8 + RaRnVx8 + Im2lnVx11 + HaRlAx9 + WaRnVx8 + Rm2lnVx12 + IaLnVx13 + HaRnVx9 + RaLnVx14 + IaLnVx16 + Hm2lnVx9 + RaLnVx15 + Im2rnVx16 + HaLnVx10 + Rm2rnVx15 events = wpa + inject + eoi + rearm + ch + eoch + oh + eooh + gr + eogr+ gl + eogl + rst controllableEvents = inject + rearm + ch + oh + gr + gl + rst transition = IaRnVx0->wpa->RaRnVx1 + RaRnVx1->inject->WaRnVx1 + WaRnVx1->eoi->HaRnVx2 + HaRnVx2->gl->Hm2lnVx2 + Hm2lnVx2->eogl->HaLnVx3 + HaLnVx3->ch->HaLpAx3 + HaLpAx3->eoch->HaLVx4 + HaLVx4->rearm->IaLVx5 + IaLVx5->wpa->RaLVx6 + IaLVx5->gr->Im2rVx5 + RaLVx6->gr->Rm2rVx6 + Im2rVx5->wpa->Rm2rVx6 + Im2rVx5->eogr->IaRVx7 + Rm2rVx6->eogr->RaRVx8 + IaRVx7->wpa->RaRVx8 + IaRVx7->oh->IaRlAx7 + RaRVx8->inject->WaRVx8 + RaRVx8->oh->RaRlAx8 + IaRlAx7->wpa->RaRlAx8 + IaRlAx7->eooh->IaRnVx7 + WaRVx8->eoi->HaRVx9 + WaRVx8->oh->WaRlAx8 + RaRlAx8->inject->WaRlAx8 + RaRlAx8->eooh->RaRnVx8 + IaRnVx7->wpa->RaRnVx8 + IaRnVx7->gl->Im2lnVx11 + HaRVx9->oh->HaRlAx9 + WaRlAx8->eoi->HaRlAx9 + WaRlAx8->eooh->WaRnVx8 + RaRnVx8->inject->WaRnVx8 + Im2lnVx11->wpa->Rm2lnVx12 + Im2lnVx11->eogl->IaLnVx13 + HaRlAx9->eooh->HaRnVx9 + WaRnVx8->eoi->HaRnVx9 + Rm2lnVx12->eogl->RaLnVx14 + IaLnVx13->wpa->RaLnVx14 + IaLnVx13->rst->IaLnVx16 + HaRnVx9->gl->Hm2lnVx9 + RaLnVx14->rst->RaLnVx15 + IaLnVx16->wpa->RaLnVx15 + IaLnVx16->gr->Im2rnVx16 + Hm2lnVx9->eogl->HaLnVx10 + RaLnVx15->gr->Rm2rnVx15 + Im2rnVx16->wpa->Rm2rnVx15 + Im2rnVx16->eogr->IaRnVx0 + HaLnVx10->rst->HaLnVx3 + Rm2rnVx15->eogr->RaRnVx1 initialState = IaRnVx0 markedStates = IaRnVx0 } run { } check IsGtrimmed { IsTrim[G] } check IsHtrimmed { IsTrim[H] } check IsHcontrollable { controllability[G, H, iden] }