# Coobservability of discrete event systems. # copyright Richard St-Denis, Universite de Sherbrooke, 2016. # # References: # [1] A general architecture for decentralized supervisory control of # discrete event systems, # T.-S. Yoo and S. Lafortune, # Discrete Event Dynamic Systems: Theory and Applications, # 12 (3), 335-377, 2002. # # [2] Decentralized supervisory control with conditional decisions: # Supervisor exitence, # T.-S. Yoo and S. Lafortune, # IEEE Transactions on Atomatic Control, # 49 (11), 1886-1904, 2004. alloy_model :Coob do open Declaration abstract sig System [ nbrOfsup: Int, states: (set StateSpace), events: (set Labels), ctrlEvents: (set Labels), ctrlEventSets: (set Int ** Labels), obsEvents: (set Labels), obsEventSets: (set Int ** Labels), ctrlEventsE: (set Labels), ctrlEventsD: (set Labels) ] { ctrlEvents.in? events and (ctrlEventsE + ctrlEventsD).in? ctrlEvents and ctrlEventsE & ctrlEventsD == none and all(i: Int) { if i >= 1 and i <= nbrOfsup then (i.(ctrlEventSets)).in? ctrlEvents end } and all(i: Int) { if i >= 1 and i <= nbrOfsup then (i.(obsEventSets)).in? obsEvents end } } # ---------- Automaton and basic functions. abstract sig Automaton [ states: (set StateSpace), labels: (set Labels), initialState: (one StateSpace), finalStates: (set StateSpace), transition: (set StateSpace ** Labels ** StateSpace) ] { initialState.in? states and finalStates.in? states and transition.(this.states).(this.labels).in? states and labels.(states.(this.transition)).in? states and states.(this.transition).(this.states).in? labels } fun getTrs[a: (one Automaton), lbls: (set Labels)] [(set StateSpace ** StateSpace)] { (StateSpace ** StateSpace).select { |src, dst| some(l: lbls) { (src ** l ** dst).in? a.transition } } } fun target[a: (one Automaton), s: (one StateSpace), lbl: (one Labels)] [(set StateSpace)] { s.(getTrs(a,lbl)) } # ---------- Walk and basic functions and predicates. abstract sig Walk [ edges: (seq Labels), vertices: (seq StateSpace), stg: (one Automaton) ] { vertices[0] == stg.initialState and edges.size == vertices.size - 1 and all(k: Int) { if k >= 1 and k <= vertices.size - 1 then let(lbl: edges[k-1]) { let(s1: vertices[k-1]) { let(s2: vertices[k]) { s2.in? stg.target(s1, lbl) } } } end } } fact { all(w1, w2: Walk) { if (w1.stg == w2.stg and not w1 == w2) then ( (not w1.vertices == w2.vertices) or (not w1.edges == w2.edges) ) end } } fun lastVertex[w: (one Walk)] [(one StateSpace)] { (w.vertices)[w.vertices.size - 1] } fun labelInds[sq: (seq Labels)] [Int] { sq.inds } fun projectWalk[w: (one Walk), lbls: (set Labels)] [ (set Int ** Labels)] { (Int ** Labels).select { |j, lbl| some(k: labelInds(w.edges)) { w.edges[k].in? lbls and lbl == w.edges[k] and (w.edges.subseq(0,k).indsOf(lbls)).size == j + 1 } } } pred isAnExtension[w: (one Walk), lbl: (one Labels)] { some(s: StateSpace) { (lastVertex(w) ** lbl ** s).in? w.stg.transition } } # ---------- Observability properties. pred observability[arch: (one System), sys: (one Automaton), spec: (set Automaton)] { # observability property all(ws1: Walk, w1: Walk, sigma: arch.ctrlEvents) { if ws1.stg == spec and w1.stg == sys and ws1.edges == w1.edges and not isAnExtension(ws1, sigma) and isAnExtension(w1, sigma) then all(ws2: Walk) { if ws2.stg == spec and projectWalk(ws2, arch.obsEvents) == projectWalk(ws1, arch.obsEvents) then not isAnExtension(ws2, sigma) end } end } } pred cpCoobservability[arch: (one System), sys: (one Automaton), spec: (set Automaton), defaultEnablement: (set Labels) ] { # C&P co-observability property all(ws1: Walk, w1: Walk, sigma: defaultEnablement) { if ws1.stg == spec and w1.stg == sys and ws1.edges == w1.edges and not isAnExtension(ws1, sigma) and isAnExtension(w1, sigma) then some(i: Int) { i <= arch.nbrOfsup and sigma.in? ((i.(arch.ctrlEventSets)) & defaultEnablement) and all(ws2: Walk) { if ws2.stg == spec and projectWalk(ws2, i.(arch.obsEventSets)) == projectWalk(ws1, i.(arch.obsEventSets)) then not isAnExtension(ws2, sigma) end } } end } } pred daCoobservability[arch: (one System), sys: (one Automaton), spec: (set Automaton), defaultDisablement: (set Labels) ] { # D&A co-observability property all(ws1: Walk, sigma: defaultDisablement) { if ws1.stg == spec and isAnExtension(ws1, sigma) then some(i: Int) { i <= arch.nbrOfsup and sigma.in? ((i.(arch.ctrlEventSets)) & defaultDisablement) and all(ws2: Walk, w2: Walk) { if ws2.stg == spec and w2.stg == sys and ws2.edges == w2.edges and projectWalk(ws2, i.(arch.obsEventSets)) == projectWalk(ws1, i.(arch.obsEventSets)) then isAnExtension(w2, sigma) and not isAnExtension(ws2, sigma) end } } end } } end