superior inferior
ENROL/rsp-req <-- i1 :a1
disruption I XXX a1 :z
I1 :A1 <----------------------ENROL/rsp-req
A1 :A1 XXX disruption 0
A1 :Z XXX disruption I
Nothing happens (:)
superior inferior
I1 :A1 <-----------------------------ENROL/rsp-req <-- i1 :a1
disruption I XXX a1 :z
A1 :Z XXX disruption I
Nothing happens (:)
superior inferior
ENROL/rsp-req <-- i1 :a1
detect problem === a1 :m2
I1 :A1 <----------------------ENROL/rsp-req
A1 :M0 <------------------------------------HAZARD <-- m2 :m2
disruption I XXX m2 :z
M0 :Z XXX disruption I
Superior nothing, unreported hazard (:?)
superior inferior
I1 :A1 <-----------------------------ENROL/rsp-req <-- i1 :a1
A1 :A1 <------------------------INF_STATE/active/y <-- a1 :a1
disruption I XXX a1 :z
A1 :Z XXX disruption I
Nothing happens (:)
superior inferior
I1 :A1 <-----------------------------ENROL/rsp-req <-- i1 :a1
A1 :B1 --> ENROLLED
B1 :Z XXX disruption I
ENROLLED---X
disruption I XXX a1 :z
Nothing happens (:)
superior inferior
ENROL/no-rsp-req <-- i1 :b1
RESIGN/no-rsp-req <-- b1 :z
I1 :B1 <-------------------ENROL/no-rsp-req
B1 :G1 === decide to cancel
G1 :Z <------------------RESIGN/no-rsp-req
Superior cancels, inferior never decided (-:)
superior inferior
ENROL/no-rsp-req <-- i1 :b1
CANCELLED <-- b1 :z
I1 :B1 <-------------------ENROL/no-rsp-req
B1 :D1 === decide to prepare
D1 :Z <--------------------------CANCELLED
Nothing happens (:)
superior inferior
I1 :B1 <--------------------------ENROL/no-rsp-req <-- i1 :b1
CANCELLED <-- b1 :z
B1 :B1 XXX disruption 0
B1 :Z <--------------------------CANCELLED
Nothing happens (:)
superior inferior
ENROL/no-rsp-req <-- i1 :b1
RESIGN/no-rsp-req <-- b1 :z
I1 :B1 <-------------------ENROL/no-rsp-req
B1 :Z XXX disruption I
X---RESIGN/no-rsp-req
Nothing happens (:)
superior inferior
ENROL/no-rsp-req <-- i1 :b1
CANCELLED <-- b1 :z
I1 :B1 <-------------------ENROL/no-rsp-req
B1 :Z <--------------------------CANCELLED
Nothing happens (:)
superior inferior
ENROL/no-rsp-req <-- i1 :b1
decide to be prepared === b1 :e1
decide to confirm autonomously === e1 :h1
CONFIRMED/auto <-- h1 :h1
I1 :B1 <-------------------ENROL/no-rsp-req
B1 :H1 <---------------------CONFIRMED/auto
H1 :L0 === decide to cancel
L0 :L1 === record contradiction
L1 :Z --> CONTRADICTION-----------------------------> h1 :z
Superior cancels, inferior confirmed - contradiction reported (-!:#)
superior inferior
ENROL/no-rsp-req <-- i1 :b1
detect problem === b1 :m2
I1 :B1 <-------------------ENROL/no-rsp-req
B1 :M0 <------------------------------------HAZARD <-- m2 :m2
disruption I XXX m2 :z
M0 :Z XXX disruption I
Superior nothing, unreported hazard (:?)
superior inferior
I1 :B1 <--------------------------ENROL/no-rsp-req <-- i1 :b1
B1 :B1 --> SUP_STATE/active/y------------------------> b1 :b1
B1 :B1 <--------------------------INF_STATE/active <-- b1 :b1
B1 :Z <---------------------------------CANCELLED <-- b1 :z
Nothing happens (:)
superior inferior
ENROL/no-rsp-req <-- i1 :b1
INF_STATE/active/y <-- b1 :b1
RESIGN/no-rsp-req <-- b1 :z
I1 :B1 <-------------------ENROL/no-rsp-req
B1 :B1 <-----------------INF_STATE/active/y
B1 :Z <------------------RESIGN/no-rsp-req
Nothing happens (:)
superior inferior
ENROL/no-rsp-req <-- i1 :b1
RESIGN/rsp-req <-- b1 :c1
disruption I XXX c1 :z
X---RESIGN/rsp-req
I1 :B1 <-------------------ENROL/no-rsp-req
B1 :B1 --> SUP_STATE/active/y------------------------> z :y1
B1 :Z <-------------------------INF_STATE/unknown <-- y1 :z
Nothing happens (:)
superior inferior
I1 :B1 <--------------------------ENROL/no-rsp-req <-- i1 :b1
decide to be prepared === b1 :e1
B1 :E1 <----------------------------------PREPARED <-- e1 :e1
E1 :N1 --> REQUEST_CONFIRM
decide to cancel autonomously === e1 :j1
REQUEST_CONFIRM--------------------> j1 :n3
N1 :Z <---------------------------------CANCELLED <-- n3 :z
Superior requested confirm, inferior cancelled (=:-)
superior inferior
ENROL/no-rsp-req <-- i1 :b1
decide to be prepared/cancel === b1 :e2
PREPARED/cancel <-- e2 :e2
I1 :B1 <-------------------ENROL/no-rsp-req
decide to cancel autonomously === e2 :z1
B1 :E2 <--------------------PREPARED/cancel
E2 :Z === decide to cancel
Both cancel (-:-)
superior inferior
I1 :B1 <--------------------------ENROL/no-rsp-req <-- i1 :b1
B1 :Z <-------------------------RESIGN/no-rsp-req <-- b1 :z
Nothing happens (:)
superior inferior
ENROL/no-rsp-req <-- i1 :b1
RESIGN/rsp-req <-- b1 :c1
I1 :B1 <-------------------ENROL/no-rsp-req
B1 :C1 <---------------------RESIGN/rsp-req
C1 :Z <-------------------------RESIGN/no-rsp-req <-- c1 :z
Nothing happens (:)
superior inferior
ENROL/no-rsp-req <-- i1 :b1
CANCELLED <-- b1 :z
I1 :B1 <-------------------ENROL/no-rsp-req
B1 :N1 --> REQUEST_CONFIRM
disruption 0 XXX z :z
REQUEST_CONFIRM---X
N1 :Z <--------------------------CANCELLED
Superior requested confirm, inferior never decided (=:)
superior inferior
ENROL/no-rsp-req <-- i1 :b1
INF_STATE/active/y <-- b1 :b1
CANCELLED <-- b1 :z
I1 :B1 <-------------------ENROL/no-rsp-req
B1 :B1 <-----------------INF_STATE/active/y
B1 :B1 --> SUP_STATE/active
B1 :Z <--------------------------CANCELLED
SUP_STATE/active-------------------> z :z
Nothing happens (:)
superior inferior
I1 :B1 <--------------------------ENROL/no-rsp-req <-- i1 :b1
B1 :B1 --> SUP_STATE/active/y
RESIGN/no-rsp-req <-- b1 :z
B1 :Z XXX disruption I
SUP_STATE/active/y---X
X---RESIGN/no-rsp-req
Nothing happens (:)
superior inferior
I1 :B1 <--------------------------ENROL/no-rsp-req <-- i1 :b1
B1 :C1 <----------------------------RESIGN/rsp-req <-- b1 :c1
C1 :C1 XXX disruption 0
C1 :Z --> RESIGNED----------------------------------> c1 :z
Nothing happens (:)
superior inferior
ENROL/no-rsp-req <-- i1 :b1
RESIGN/rsp-req <-- b1 :c1
I1 :B1 <-------------------ENROL/no-rsp-req
B1 :C1 <---------------------RESIGN/rsp-req
C1 :Z XXX disruption I
disruption I XXX c1 :z
Nothing happens (:)
superior inferior
ENROL/no-rsp-req <-- i1 :b1
RESIGN/rsp-req <-- b1 :c1
disruption I XXX c1 :z
I1 :B1 <-------------------ENROL/no-rsp-req
B1 :N1 --> REQUEST_CONFIRM
N1 :C1 <---------------------RESIGN/rsp-req
REQUEST_CONFIRM--------------------> z :y1
C1 :Z <-------------------------INF_STATE/unknown <-- y1 :z
Superior requested confirm, inferior never decided (=:)
superior inferior
ENROL/no-rsp-req <-- i1 :b1
RESIGN/rsp-req <-- b1 :c1
I1 :B1 <-------------------ENROL/no-rsp-req
B1 :C1 <---------------------RESIGN/rsp-req
C1 :Z <-------------------------RESIGN/no-rsp-req <-- c1 :z
Nothing happens (:)
superior inferior
ENROL/no-rsp-req <-- i1 :b1
RESIGN/rsp-req <-- b1 :c1
I1 :B1 <-------------------ENROL/no-rsp-req
B1 :C1 <---------------------RESIGN/rsp-req
C1 :C1 <----------------------------RESIGN/rsp-req <-- c1 :c1
C1 :Z --> RESIGNED----------------------------------> c1 :z
Nothing happens (:)
superior inferior
ENROL/no-rsp-req <-- i1 :b1
RESIGN/rsp-req <-- b1 :c1
I1 :B1 <-------------------ENROL/no-rsp-req
B1 :C1 <---------------------RESIGN/rsp-req
C1 :Z --> RESIGNED----------------------------------> c1 :z
Nothing happens (:)
superior inferior
I1 :B1 <--------------------------ENROL/no-rsp-req <-- i1 :b1
B1 :D1 === decide to prepare
RESIGN/no-rsp-req <-- b1 :z
D1 :G1 === decide to cancel
G1 :Z <------------------RESIGN/no-rsp-req
Superior cancels, inferior never decided (-:)
superior inferior
I1 :B1 <--------------------------ENROL/no-rsp-req <-- i1 :b1
B1 :D1 === decide to prepare
D1 :D1 XXX disruption 0
D1 :Z <---------------------------------CANCELLED <-- b1 :z
Nothing happens (:)
superior inferior
I1 :B1 <--------------------------ENROL/no-rsp-req <-- i1 :b1
RESIGN/no-rsp-req <-- b1 :z
B1 :D1 === decide to prepare
D1 :Z XXX disruption I
X---RESIGN/no-rsp-req
Nothing happens (:)
superior inferior
ENROL/no-rsp-req <-- i1 :b1
CANCELLED <-- b1 :z
I1 :B1 <-------------------ENROL/no-rsp-req
B1 :D1 === decide to prepare
D1 :Z <--------------------------CANCELLED
Nothing happens (:)
superior inferior
I1 :B1 <--------------------------ENROL/no-rsp-req <-- i1 :b1
decide to be prepared === b1 :e1
decide to confirm autonomously === e1 :h1
CONFIRMED/auto <-- h1 :h1
B1 :D1 === decide to prepare
D1 :H1 <---------------------CONFIRMED/auto
H1 :L0 === decide to cancel
L0 :L1 === record contradiction
L1 :Z --> CONTRADICTION-----------------------------> h1 :z
Superior cancels, inferior confirmed - contradiction reported (-!:#)
superior inferior
ENROL/no-rsp-req <-- i1 :b1
detect problem === b1 :m2
I1 :B1 <-------------------ENROL/no-rsp-req
B1 :D1 === decide to prepare
D1 :M0 <------------------------------------HAZARD <-- m2 :m2
disruption I XXX m2 :z
M0 :Z XXX disruption I
Superior nothing, unreported hazard (:?)
superior inferior
I1 :B1 <--------------------------ENROL/no-rsp-req <-- i1 :b1
B1 :B1 --> SUP_STATE/active/y------------------------> b1 :b1
B1 :D1 === decide to prepare
INF_STATE/active <-- b1 :b1
RESIGN/no-rsp-req <-- b1 :z
D1 :D1 <-------------------INF_STATE/active
D1 :Z <------------------RESIGN/no-rsp-req
Nothing happens (:)
superior inferior
ENROL/no-rsp-req <-- i1 :b1
INF_STATE/active/y <-- b1 :b1
CANCELLED <-- b1 :z
I1 :B1 <-------------------ENROL/no-rsp-req
B1 :D1 === decide to prepare
D1 :D1 <-----------------INF_STATE/active/y
D1 :Z <--------------------------CANCELLED
Nothing happens (:)
superior inferior
ENROL/no-rsp-req <-- i1 :b1
detect problem === b1 :m2
I1 :B1 <-------------------ENROL/no-rsp-req
B1 :D1 === decide to prepare
disruption I XXX m2 :z
D1 :D1 --> PREPARE-----------------------------------> z :y1
D1 :Z <-------------------------INF_STATE/unknown <-- y1 :z
Superior nothing, unreported hazard (:?)
superior inferior
I1 :B1 <--------------------------ENROL/no-rsp-req <-- i1 :b1
decide to be prepared === b1 :e1
B1 :D1 === decide to prepare
PREPARED <-- e1 :e1
decide to confirm autonomously === e1 :h1
D1 :E1 <---------------------------PREPARED
E1 :N1 --> REQUEST_CONFIRM---------------------------> h1 :n2
N1 :Z <------------------------CONFIRMED/response <-- n2 :z
Superior requested confirm, inferior confirmed (=:#)
superior inferior
ENROL/no-rsp-req <-- i1 :b1
decide to be prepared/cancel === b1 :e2
I1 :B1 <-------------------ENROL/no-rsp-req
PREPARED/cancel <-- e2 :e2
decide to cancel autonomously === e2 :z1
B1 :D1 === decide to prepare
D1 :E2 <--------------------PREPARED/cancel
E2 :Z === decide to cancel
Both cancel (-:-)
superior inferior
I1 :B1 <--------------------------ENROL/no-rsp-req <-- i1 :b1
B1 :D1 === decide to prepare
D1 :Z <-------------------------RESIGN/no-rsp-req <-- b1 :z
Nothing happens (:)
superior inferior
I1 :B1 <--------------------------ENROL/no-rsp-req <-- i1 :b1
B1 :D1 === decide to prepare
D1 :C1 <----------------------------RESIGN/rsp-req <-- b1 :c1
C1 :Z <-------------------------RESIGN/no-rsp-req <-- c1 :z
Nothing happens (:)
superior inferior
I1 :B1 <--------------------------ENROL/no-rsp-req <-- i1 :b1
B1 :D1 === decide to prepare
D1 :D1 --> PREPARE-----------------------------------> b1 :d1
D1 :Z <-------------------------RESIGN/no-rsp-req <-- d1 :z
Nothing happens (:)
superior inferior
ENROL/no-rsp-req <-- i1 :b1
decide to be prepared === b1 :e1
PREPARED <-- e1 :e1
decide to cancel autonomously === e1 :j1
I1 :B1 <-------------------ENROL/no-rsp-req
B1 :E1 <---------------------------PREPARED
E1 :G1 === decide to cancel
G1 :G2 --> CANCEL
G2 :Z <---------------------------------CANCELLED <-- j1 :j2
CANCEL-----------------------------> j2 :z
Both cancel (-:-)
superior inferior
I1 :B1 <--------------------------ENROL/no-rsp-req <-- i1 :b1
decide to be prepared === b1 :e1
B1 :E1 <----------------------------------PREPARED <-- e1 :e1
E1 :F1 === decide to confirm
decide to confirm autonomously === e1 :h1
F1 :F1 --> CONFIRM-----------------------------------> h1 :h2
F1 :Z0 <------------------------CONFIRMED/response <-- h2 :z
Both confirm (+:#)
superior inferior
I1 :B1 <--------------------------ENROL/no-rsp-req <-- i1 :b1
decide to be prepared === b1 :e1
B1 :E1 <----------------------------------PREPARED <-- e1 :e1
E1 :E1 === decide to prepare
E1 :N1 --> REQUEST_CONFIRM
decide to cancel autonomously === e1 :j1
REQUEST_CONFIRM--------------------> j1 :n3
N1 :Z <---------------------------------CANCELLED <-- n3 :z
Superior requested confirm, inferior cancelled (=:-)
superior inferior
ENROL/no-rsp-req <-- i1 :b1
decide to be prepared === b1 :e1
PREPARED <-- e1 :e1
decide to cancel autonomously === e1 :j1
I1 :B1 <-------------------ENROL/no-rsp-req
B1 :D1 === decide to prepare
D1 :E1 <---------------------------PREPARED
E1 :E1 XXX disruption 0
E1 :J1 <---------------------------------CANCELLED <-- j1 :j2
CANCELLED <-- j2 :j2
J1 :J2 === decide to cancel
J2 :J2 <--------------------------CANCELLED
J2 :Z --> CANCEL------------------------------------> j2 :z
Both cancel (-:-)
superior inferior
ENROL/no-rsp-req <-- i1 :b1
decide to be prepared === b1 :e1
PREPARED <-- e1 :e1
decide to cancel autonomously === e1 :j1
I1 :B1 <-------------------ENROL/no-rsp-req
B1 :E1 <---------------------------PREPARED
E1 :Z XXX disruption I
CANCELLED <-- j1 :j2
CANCELLED <-- j2 :j2
Z :Y1 <--------------------------CANCELLED
Y1 :Z --> SUP_STATE/unknown
Z :Y1 <--------------------------CANCELLED
SUP_STATE/unknown------------------> j2 :z
Y1 :Z --> SUP_STATE/unknown-------------------------> z :z
superior never decided, inferior cancelled (:-)
superior inferior
ENROL/no-rsp-req <-- i1 :b1
decide to be prepared === b1 :e1
I1 :B1 <-------------------ENROL/no-rsp-req
B1 :E1 <----------------------------------PREPARED <-- e1 :e1
E1 :E1 --> PREPARE
decide to cancel autonomously === e1 :j1
E1 :D1 XXX disruption II
PREPARE---X
D1 :G1 === decide to cancel
G1 :G2 --> CANCEL------------------------------------> j1 :j3
G2 :Z <---------------------------------CANCELLED <-- j3 :z
Both cancel (-:-)
superior inferior
I1 :B1 <--------------------------ENROL/no-rsp-req <-- i1 :b1
B1 :D1 === decide to prepare
decide to be prepared === b1 :e1
PREPARED <-- e1 :e1
decide to cancel autonomously === e1 :j1
D1 :E1 <---------------------------PREPARED
E1 :B1 XXX disruption III
B1 :N1 --> REQUEST_CONFIRM---------------------------> j1 :n3
N1 :Z <---------------------------------CANCELLED <-- n3 :z
Superior requested confirm, inferior cancelled (=:-)
superior inferior
ENROL/no-rsp-req <-- i1 :b1
decide to be prepared === b1 :e1
PREPARED <-- e1 :e1
decide to cancel autonomously === e1 :j1
CANCELLED <-- j1 :j2
I1 :B1 <-------------------ENROL/no-rsp-req
B1 :E1 <---------------------------PREPARED
E1 :J1 <--------------------------CANCELLED
J1 :J2 === decide to cancel
J2 :Z --> CANCEL------------------------------------> j2 :z
Both cancel (-:-)
superior inferior
ENROL/no-rsp-req <-- i1 :b1
decide to be prepared === b1 :e1
I1 :B1 <-------------------ENROL/no-rsp-req
PREPARED <-- e1 :e1
decide to confirm autonomously === e1 :h1
CONFIRMED/auto <-- h1 :h1
B1 :E1 <---------------------------PREPARED
E1 :H1 <---------------------CONFIRMED/auto
H1 :L0 === decide to cancel
L0 :L1 === record contradiction
L1 :Z --> CONTRADICTION-----------------------------> h1 :z
Superior cancels, inferior confirmed - contradiction reported (-!:#)
superior inferior
ENROL/no-rsp-req <-- i1 :b1
decide to be prepared === b1 :e1
PREPARED <-- e1 :e1
detect problem === e1 :m3
I1 :B1 <-------------------ENROL/no-rsp-req
B1 :E1 <---------------------------PREPARED
E1 :M0 <------------------------------------HAZARD <-- m3 :m3
M0 :M3 === record contradiction
M3 :Z --> CONTRADICTION-----------------------------> m3 :z
Inferior detected problem, contradiction reported (!:?)
superior inferior
ENROL/no-rsp-req <-- i1 :b1
decide to be prepared === b1 :e1
I1 :B1 <-------------------ENROL/no-rsp-req
PREPARED <-- e1 :e1
PREPARED <-- e1 :e1
decide to confirm autonomously === e1 :h1
B1 :E1 <---------------------------PREPARED
E1 :E1 <---------------------------PREPARED
E1 :N1 --> REQUEST_CONFIRM---------------------------> h1 :n2
N1 :Z <------------------------CONFIRMED/response <-- n2 :z
Superior requested confirm, inferior confirmed (=:#)
superior inferior
ENROL/no-rsp-req <-- i1 :b1
decide to be prepared === b1 :e1
PREPARED <-- e1 :e1
detect problem === e1 :m3
I1 :B1 <-------------------ENROL/no-rsp-req
B1 :E1 <---------------------------PREPARED
E1 :E1 --> PREPARE
E1 :N1 --> REQUEST_CONFIRM
PREPARE----------------------------> m3 :m3
REQUEST_CONFIRM--------------------> m3 :n5
N1 :Z <------------------------------------HAZARD <-- n5 :z
Confirm requested, inferior detected problem, contradiction not reported (=:?)
superior inferior
ENROL/no-rsp-req <-- i1 :b1
decide to be prepared === b1 :e1
I1 :B1 <-------------------ENROL/no-rsp-req
B1 :E1 <----------------------------------PREPARED <-- e1 :e1
E1 :N1 --> REQUEST_CONFIRM
detect problem === e1 :m3
REQUEST_CONFIRM--------------------> m3 :n5
N1 :Z <------------------------------------HAZARD <-- n5 :z
Confirm requested, inferior detected problem, contradiction not reported (=:?)
superior inferior
I1 :B1 <--------------------------ENROL/no-rsp-req <-- i1 :b1
INF_STATE/active/y <-- b1 :b1
decide to be prepared === b1 :e1
B1 :B1 <-----------------INF_STATE/active/y
PREPARED <-- e1 :e1
decide to confirm autonomously === e1 :h1
B1 :E1 <---------------------------PREPARED
E1 :E1 --> SUP_STATE/preparedreceived
E1 :E1 === decide to prepare
SUP_STATE/preparedreceived---------> h1 :h1
E1 :N1 --> REQUEST_CONFIRM---------------------------> h1 :n2
N1 :Z <------------------------CONFIRMED/response <-- n2 :z
Superior requested confirm, inferior confirmed (=:#)
superior inferior
ENROL/no-rsp-req <-- i1 :b1
decide to be prepared === b1 :e1
PREPARED <-- e1 :e1
I1 :B1 <-------------------ENROL/no-rsp-req
B1 :E1 <---------------------------PREPARED
decide to cancel autonomously === e1 :j1
E1 :E1 --> SUP_STATE/preparedreceived/y
E1 :N1 --> REQUEST_CONFIRM
SUP_STATE/preparedreceived/y-------> j1 :j1
REQUEST_CONFIRM--------------------> j1 :n3
N1 :Z <---------------------------------CANCELLED <-- n3 :z
Superior requested confirm, inferior cancelled (=:-)
superior inferior
I1 :B1 <--------------------------ENROL/no-rsp-req <-- i1 :b1
decide to be prepared/cancel === b1 :e2
B1 :E2 <---------------------------PREPARED/cancel <-- e2 :e2
E2 :Z === decide to cancel
decide to cancel autonomously === e2 :z1
Both cancel (-:-)
superior inferior
ENROL/no-rsp-req <-- i1 :b1
decide to be prepared/cancel === b1 :e2
PREPARED/cancel <-- e2 :e2
I1 :B1 <-------------------ENROL/no-rsp-req
B1 :E2 <--------------------PREPARED/cancel
E2 :F1 === decide to confirm
F1 :F1 --> CONFIRM-----------------------------------> e2 :f1
apply ordered confirmation === f1 :f2
F1 :Z0 <------------------------CONFIRMED/response <-- f2 :z
Confirm ordered and applied (+:+)
superior inferior
ENROL/no-rsp-req <-- i1 :b1
decide to be prepared/cancel === b1 :e2
PREPARED/cancel <-- e2 :e2
I1 :B1 <-------------------ENROL/no-rsp-req
B1 :E2 <--------------------PREPARED/cancel
decide to cancel autonomously === e2 :z1
E2 :E2 === decide to prepare
E2 :Z === decide to cancel
Both cancel (-:-)
superior inferior
ENROL/no-rsp-req <-- i1 :b1
decide to be prepared/cancel === b1 :e2
PREPARED/cancel <-- e2 :e2
decide to cancel autonomously === e2 :z1
I1 :B1 <-------------------ENROL/no-rsp-req
B1 :E2 <--------------------PREPARED/cancel
E2 :E2 XXX disruption 0
E2 :Z === decide to cancel
Both cancel (-:-)
superior inferior
ENROL/no-rsp-req <-- i1 :b1
decide to be prepared/cancel === b1 :e2
PREPARED/cancel <-- e2 :e2
I1 :B1 <-------------------ENROL/no-rsp-req
decide to cancel autonomously === e2 :z1
B1 :E2 <--------------------PREPARED/cancel
E2 :Z XXX disruption I
superior never decided, inferior cancelled (:-)
superior inferior
disruption 0 XXX i1 :i1
I1 :B1 <--------------------------ENROL/no-rsp-req <-- i1 :b1
decide to be prepared/cancel === b1 :e2
PREPARED/cancel <-- e2 :e2
B1 :D1 === decide to prepare
decide to cancel autonomously === e2 :z1
D1 :D1 --> PREPARE
D1 :E2 <--------------------PREPARED/cancel
PREPARE----------------------------> z1 :z1
E2 :D1 XXX disruption II
D1 :G1 === decide to cancel
G1 :Z XXX disruption I
Both cancel (-:-)
superior inferior
I1 :A1 <-----------------------------ENROL/rsp-req <-- i1 :a1
A1 :B1 --> ENROLLED----------------------------------> a1 :b1
decide to be prepared/cancel === b1 :e2
PREPARED/cancel <-- e2 :e2
decide to cancel autonomously === e2 :z1
B1 :E2 <--------------------PREPARED/cancel
E2 :B1 XXX disruption III
B1 :D1 === decide to prepare
D1 :G1 === decide to cancel
G1 :Z XXX disruption I
Both cancel (-:-)
superior inferior
ENROL/no-rsp-req <-- i1 :b1
decide to be prepared/cancel === b1 :e2
I1 :B1 <-------------------ENROL/no-rsp-req
PREPARED/cancel <-- e2 :e2
B1 :B1 --> SUP_STATE/active/y
B1 :E2 <--------------------PREPARED/cancel
decide to cancel autonomously === e2 :z1
SUP_STATE/active/y-----------------> z1 :y3
E2 :J1 <---------------------------------CANCELLED <-- y3 :z1
J1 :Z XXX disruption I
superior never decided, inferior cancelled (:-)
superior inferior
ENROL/no-rsp-req <-- i1 :b1
decide to be prepared/cancel === b1 :e2
PREPARED/cancel <-- e2 :e2
I1 :B1 <-------------------ENROL/no-rsp-req
B1 :E2 <--------------------PREPARED/cancel
detect problem === e2 :m3
E2 :M0 <------------------------------------HAZARD <-- m3 :m3
M0 :M3 === record contradiction
M3 :Z --> CONTRADICTION-----------------------------> m3 :z
Inferior detected problem, contradiction reported (!:?)
superior inferior
I1 :B1 <--------------------------ENROL/no-rsp-req <-- i1 :b1
decide to be prepared/cancel === b1 :e2
B1 :E2 <---------------------------PREPARED/cancel <-- e2 :e2
E2 :E2 <---------------------------PREPARED/cancel <-- e2 :e2
E2 :Z === decide to cancel
decide to cancel autonomously === e2 :z1
Both cancel (-:-)
superior inferior
ENROL/no-rsp-req <-- i1 :b1
decide to be prepared/cancel === b1 :e2
I1 :B1 <-------------------ENROL/no-rsp-req
B1 :E2 <---------------------------PREPARED/cancel <-- e2 :e2
E2 :E2 --> PREPARE-----------------------------------> e2 :e2
E2 :Z === decide to cancel
decide to cancel autonomously === e2 :z1
Both cancel (-:-)
superior inferior
ENROL/no-rsp-req <-- i1 :b1
decide to be prepared/cancel === b1 :e2
PREPARED/cancel <-- e2 :e2
decide to cancel autonomously === e2 :z1
I1 :B1 <-------------------ENROL/no-rsp-req
B1 :E2 <--------------------PREPARED/cancel
E2 :N1 --> REQUEST_CONFIRM---------------------------> z1 :y1
N1 :Z <-------------------------INF_STATE/unknown <-- y1 :z
Superior requested confirm, inferior cancelled (=:-)
superior inferior
ENROL/no-rsp-req <-- i1 :b1
INF_STATE/active/y <-- b1 :b1
decide to be prepared/cancel === b1 :e2
I1 :B1 <-------------------ENROL/no-rsp-req
B1 :B1 <-----------------INF_STATE/active/y
B1 :E2 <---------------------------PREPARED/cancel <-- e2 :e2
E2 :E2 --> SUP_STATE/preparedreceived
E2 :Z === decide to cancel
SUP_STATE/preparedreceived---------> e2 :e2
decide to cancel autonomously === e2 :z1
Both cancel (-:-)
superior inferior
ENROL/no-rsp-req <-- i1 :b1
decide to be prepared/cancel === b1 :e2
I1 :B1 <-------------------ENROL/no-rsp-req
B1 :E2 <---------------------------PREPARED/cancel <-- e2 :e2
E2 :E2 --> SUP_STATE/preparedreceived/y--------------> e2 :e2
decide to cancel autonomously === e2 :z1
E2 :Z === decide to cancel
Both cancel (-:-)
superior inferior
ENROL/no-rsp-req <-- i1 :b1
decide to be prepared === b1 :e1
I1 :B1 <-------------------ENROL/no-rsp-req
PREPARED <-- e1 :e1
decide to confirm autonomously === e1 :h1
B1 :E1 <---------------------------PREPARED
E1 :F1 === decide to confirm
F1 :F1 XXX disruption 0
F1 :F1 --> CONFIRM-----------------------------------> h1 :h2
F1 :Z0 <------------------------CONFIRMED/response <-- h2 :z
Both confirm (+:#)
superior inferior
ENROL/no-rsp-req <-- i1 :b1
decide to be prepared === b1 :e1
PREPARED <-- e1 :e1
I1 :B1 <-------------------ENROL/no-rsp-req
B1 :E1 <---------------------------PREPARED
E1 :F1 === decide to confirm
decide to cancel autonomously === e1 :j1
F1 :K0 <---------------------------------CANCELLED <-- j1 :j2
K0 :K1 === record contradiction
K1 :Z --> CONTRADICTION-----------------------------> j2 :z
Superior confirms, inferior cancelled - contradiction reported (+!:-)
superior inferior
ENROL/no-rsp-req <-- i1 :b1
decide to be prepared === b1 :e1
decide to confirm autonomously === e1 :h1
CONFIRMED/auto <-- h1 :h1
I1 :B1 <-------------------ENROL/no-rsp-req
B1 :H1 <---------------------CONFIRMED/auto
H1 :F1 === decide to confirm
CONFIRMED/auto <-- h1 :h1
F1 :F1 --> CONFIRM-----------------------------------> h1 :h2
CONFIRMED/response <-- h2 :z
F1 :F1 <---------------------CONFIRMED/auto
F1 :Z0 <-----------------CONFIRMED/response
Both confirm (+:#)
superior inferior
I1 :B1 <--------------------------ENROL/no-rsp-req <-- i1 :b1
decide to be prepared === b1 :e1
B1 :E1 <----------------------------------PREPARED <-- e1 :e1
decide to confirm autonomously === e1 :h1
E1 :F1 === decide to confirm
F1 :F1 --> CONFIRM-----------------------------------> h1 :h2
F1 :Z0 <------------------------CONFIRMED/response <-- h2 :z
Both confirm (+:#)
superior inferior
ENROL/no-rsp-req <-- i1 :b1
decide to be prepared === b1 :e1
PREPARED <-- e1 :e1
I1 :B1 <-------------------ENROL/no-rsp-req
B1 :E1 <---------------------------PREPARED
E1 :F1 === decide to confirm
detect problem === e1 :m3
F1 :M1 <------------------------------------HAZARD <-- m3 :m3
M1 :M3 === record contradiction
M3 :Z --> CONTRADICTION-----------------------------> m3 :z
Superior confirms, inferior only detects mix - contradiction reported (+!:?)
superior inferior
ENROL/no-rsp-req <-- i1 :b1
decide to be prepared === b1 :e1
PREPARED <-- e1 :e1
PREPARED <-- e1 :e1
I1 :B1 <-------------------ENROL/no-rsp-req
B1 :E1 <---------------------------PREPARED
E1 :F1 === decide to confirm
F1 :F1 --> CONFIRM
F1 :F1 <---------------------------PREPARED
decide to confirm autonomously === e1 :h1
CONFIRM----------------------------> h1 :h2
F1 :Z0 <------------------------CONFIRMED/response <-- h2 :z
Both confirm (+:#)
superior inferior
ENROL/no-rsp-req <-- i1 :b1
decide to be prepared/cancel === b1 :e2
PREPARED/cancel <-- e2 :e2
I1 :B1 <-------------------ENROL/no-rsp-req
B1 :E2 <--------------------PREPARED/cancel
E2 :F1 === decide to confirm
F1 :F1 <---------------------------PREPARED/cancel <-- e2 :e2
F1 :F1 --> CONFIRM-----------------------------------> e2 :f1
apply ordered confirmation === f1 :f2
F1 :Z0 <------------------------CONFIRMED/response <-- f2 :z
Confirm ordered and applied (+:+)
superior inferior
ENROL/no-rsp-req <-- i1 :b1
decide to be prepared === b1 :e1
decide to confirm autonomously === e1 :h1
CONFIRMED/auto <-- h1 :h1
I1 :B1 <-------------------ENROL/no-rsp-req
B1 :H1 <---------------------CONFIRMED/auto
H1 :F1 === decide to confirm
F1 :F1 --> CONFIRM-----------------------------------> h1 :h2
F1 :Z0 <------------------------CONFIRMED/response <-- h2 :z
Both confirm (+:#)
superior inferior
I1 :B1 <--------------------------ENROL/no-rsp-req <-- i1 :b1
B1 :G1 === decide to cancel
RESIGN/no-rsp-req <-- b1 :z
G1 :G1 XXX disruption 0
G1 :Z <------------------RESIGN/no-rsp-req
Superior cancels, inferior never decided (-:)
superior inferior
ENROL/no-rsp-req <-- i1 :b1
RESIGN/no-rsp-req <-- b1 :z
I1 :B1 <-------------------ENROL/no-rsp-req
B1 :G1 === decide to cancel
G1 :Z XXX disruption I
X---RESIGN/no-rsp-req
Superior cancels, inferior never decided (-:)
superior inferior
I1 :B1 <--------------------------ENROL/no-rsp-req <-- i1 :b1
CANCELLED <-- b1 :z
B1 :G1 === decide to cancel
G1 :J2 <--------------------------CANCELLED
J2 :Z XXX disruption I
Superior cancels, inferior never decided (-:)
superior inferior
ENROL/no-rsp-req <-- i1 :b1
decide to be prepared === b1 :e1
decide to confirm autonomously === e1 :h1
I1 :B1 <-------------------ENROL/no-rsp-req
B1 :G1 === decide to cancel
G1 :L0 <----------------------------CONFIRMED/auto <-- h1 :h1
L0 :L1 === record contradiction
L1 :Z --> CONTRADICTION-----------------------------> h1 :z
Superior cancels, inferior confirmed - contradiction reported (-!:#)
superior inferior
I1 :B1 <--------------------------ENROL/no-rsp-req <-- i1 :b1
B1 :G1 === decide to cancel
detect problem === b1 :m2
G1 :M2 <------------------------------------HAZARD <-- m2 :m2
disruption I XXX m2 :z
M2 :Z XXX disruption I
Superior cancels, unreported hazard (-:?)
superior inferior
I1 :B1 <--------------------------ENROL/no-rsp-req <-- i1 :b1
B1 :B1 --> SUP_STATE/active/y------------------------> b1 :b1
INF_STATE/active <-- b1 :b1
RESIGN/no-rsp-req <-- b1 :z
B1 :G1 === decide to cancel
G1 :G1 <-------------------INF_STATE/active
G1 :Z <------------------RESIGN/no-rsp-req
Superior cancels, inferior never decided (-:)
superior inferior
ENROL/no-rsp-req <-- i1 :b1
INF_STATE/active/y <-- b1 :b1
I1 :B1 <-------------------ENROL/no-rsp-req
B1 :G1 === decide to cancel
G1 :G1 <-----------------INF_STATE/active/y
G1 :Z <-------------------------RESIGN/no-rsp-req <-- b1 :z
Superior cancels, inferior never decided (-:)
superior inferior
ENROL/no-rsp-req <-- i1 :b1
RESIGN/no-rsp-req <-- b1 :z
disruption 0 XXX z :z
X---RESIGN/no-rsp-req
I1 :B1 <-------------------ENROL/no-rsp-req
B1 :B1 --> SUP_STATE/active/y
B1 :G1 === decide to cancel
SUP_STATE/active/y-----------------> z :y1
G1 :Z <-------------------------INF_STATE/unknown <-- y1 :z
Superior cancels, inferior never decided (-:)
superior inferior
I1 :B1 <--------------------------ENROL/no-rsp-req <-- i1 :b1
B1 :G1 === decide to cancel
decide to be prepared === b1 :e1
PREPARED <-- e1 :e1
decide to cancel autonomously === e1 :j1
G1 :G1 <---------------------------PREPARED
CANCELLED <-- j1 :j2
G1 :G2 --> CANCEL
G2 :Z <--------------------------CANCELLED
CANCEL-----------------------------> j2 :z
Both cancel (-:-)
superior inferior
I1 :B1 <--------------------------ENROL/no-rsp-req <-- i1 :b1
decide to be prepared/cancel === b1 :e2
PREPARED/cancel <-- e2 :e2
decide to cancel autonomously === e2 :z1
B1 :G1 === decide to cancel
G1 :G1 <--------------------PREPARED/cancel
G1 :Z XXX disruption I
Both cancel (-:-)
superior inferior
I1 :B1 <--------------------------ENROL/no-rsp-req <-- i1 :b1
B1 :G1 === decide to cancel
G1 :Z <-------------------------RESIGN/no-rsp-req <-- b1 :z
Superior cancels, inferior never decided (-:)
superior inferior
ENROL/no-rsp-req <-- i1 :b1
RESIGN/rsp-req <-- b1 :c1
I1 :B1 <-------------------ENROL/no-rsp-req
B1 :G1 === decide to cancel
RESIGN/no-rsp-req <-- c1 :z
G1 :G3 <---------------------RESIGN/rsp-req
G3 :Z <------------------RESIGN/no-rsp-req
Superior cancels, inferior never decided (-:)
superior inferior
I1 :B1 <--------------------------ENROL/no-rsp-req <-- i1 :b1
B1 :G1 === decide to cancel
G1 :G2 --> CANCEL------------------------------------> b1 :g2
G2 :Z <---------------------------------CANCELLED <-- g2 :z
Superior cancels, inferior never decided (-:)
superior inferior
I1 :B1 <--------------------------ENROL/no-rsp-req <-- i1 :b1
B1 :G1 === decide to cancel
G1 :G2 --> CANCEL------------------------------------> b1 :g2
G2 :G2 XXX disruption 0
G2 :Z <---------------------------------CANCELLED <-- g2 :z
Superior cancels, inferior never decided (-:)
superior inferior
ENROL/no-rsp-req <-- i1 :b1
decide to be prepared/cancel === b1 :e2
I1 :B1 <-------------------ENROL/no-rsp-req
B1 :G1 === decide to cancel
G1 :G2 --> CANCEL
decide to cancel autonomously === e2 :z1
G2 :Z XXX disruption I
CANCEL---X
Both cancel (-:-)
superior inferior
I1 :B1 <--------------------------ENROL/no-rsp-req <-- i1 :b1
B1 :G1 === decide to cancel
G1 :G2 --> CANCEL------------------------------------> b1 :g2
G2 :Z <---------------------------------CANCELLED <-- g2 :z
Superior cancels, inferior never decided (-:)
superior inferior
ENROL/no-rsp-req <-- i1 :b1
decide to be prepared === b1 :e1
I1 :B1 <-------------------ENROL/no-rsp-req
B1 :G1 === decide to cancel
G1 :G2 --> CANCEL
decide to confirm autonomously === e1 :h1
G2 :L0 <----------------------------CONFIRMED/auto <-- h1 :h1
L0 :L1 === record contradiction
L1 :Z --> CONTRADICTION
CANCEL-----------------------------> h1 :l1
CONTRADICTION----------------------> l1 :z
Superior cancels, inferior confirmed - contradiction reported (-!:#)
superior inferior
I1 :B1 <--------------------------ENROL/no-rsp-req <-- i1 :b1
detect problem === b1 :m2
B1 :G1 === decide to cancel
G1 :G2 --> CANCEL------------------------------------> m2 :m2
G2 :M2 <------------------------------------HAZARD <-- m2 :m2
disruption I XXX m2 :z
M2 :Z XXX disruption I
Superior cancels, unreported hazard (-:?)
superior inferior
I1 :B1 <--------------------------ENROL/no-rsp-req <-- i1 :b1
B1 :B1 --> SUP_STATE/active/y
B1 :G1 === decide to cancel
SUP_STATE/active/y-----------------> b1 :b1
INF_STATE/active <-- b1 :b1
G1 :G2 --> CANCEL
RESIGN/rsp-req <-- b1 :c1
CANCEL-----------------------------> c1 :z
G2 :G2 <-------------------INF_STATE/active
G2 :Z <---------------------RESIGN/rsp-req
Superior cancels, inferior never decided (-:)
superior inferior
I1 :B1 <--------------------------ENROL/no-rsp-req <-- i1 :b1
B1 :G1 === decide to cancel
INF_STATE/active/y <-- b1 :b1
G1 :G2 --> CANCEL
G2 :G2 <-----------------INF_STATE/active/y
CANCEL-----------------------------> b1 :g2
G2 :Z <---------------------------------CANCELLED <-- g2 :z
Superior cancels, inferior never decided (-:)
superior inferior
I1 :B1 <--------------------------ENROL/no-rsp-req <-- i1 :b1
B1 :G1 === decide to cancel
decide to be prepared/cancel === b1 :e2
G1 :G2 --> CANCEL
decide to cancel autonomously === e2 :z1
CANCEL-----------------------------> z1 :y1
G2 :Z <-------------------------INF_STATE/unknown <-- y1 :z
Both cancel (-:-)
superior inferior
ENROL/no-rsp-req <-- i1 :b1
decide to be prepared === b1 :e1
I1 :B1 <-------------------ENROL/no-rsp-req
B1 :G1 === decide to cancel
G1 :G2 --> CANCEL
G2 :G2 <----------------------------------PREPARED <-- e1 :e1
CANCEL-----------------------------> e1 :g0
remove prepared information === g0 :g2
G2 :Z <---------------------------------CANCELLED <-- g2 :z
Superior cancels, inferior never decided (-:)
superior inferior
ENROL/no-rsp-req <-- i1 :b1
decide to be prepared/cancel === b1 :e2
I1 :B1 <-------------------ENROL/no-rsp-req
B1 :G1 === decide to cancel
G1 :G2 --> CANCEL
G2 :G2 <---------------------------PREPARED/cancel <-- e2 :e2
CANCEL-----------------------------> e2 :g1
remove prepared information === g1 :g2
G2 :Z <---------------------------------CANCELLED <-- g2 :z
Superior cancels, inferior never decided (-:)
superior inferior
ENROL/no-rsp-req <-- i1 :b1
RESIGN/no-rsp-req <-- b1 :z
I1 :B1 <-------------------ENROL/no-rsp-req
B1 :G1 === decide to cancel
G1 :G2 --> CANCEL
G2 :Z <------------------RESIGN/no-rsp-req
disruption 0 XXX z :z
CANCEL---X
Superior cancels, inferior never decided (-:)
superior inferior
I1 :B1 <--------------------------ENROL/no-rsp-req <-- i1 :b1
B1 :G1 === decide to cancel
G1 :G2 --> CANCEL
RESIGN/rsp-req <-- b1 :c1
CANCEL-----------------------------> c1 :z
G2 :Z <---------------------RESIGN/rsp-req
Superior cancels, inferior never decided (-:)
superior inferior
I1 :B1 <--------------------------ENROL/no-rsp-req <-- i1 :b1
B1 :G1 === decide to cancel
G1 :G2 --> CANCEL------------------------------------> b1 :g2
G2 :G2 --> CANCEL------------------------------------> g2 :g2
G2 :Z <---------------------------------CANCELLED <-- g2 :z
Superior cancels, inferior never decided (-:)
superior inferior
I1 :B1 <--------------------------ENROL/no-rsp-req <-- i1 :b1
RESIGN/rsp-req <-- b1 :c1
B1 :G1 === decide to cancel
G1 :G3 <---------------------RESIGN/rsp-req
G3 :G3 XXX disruption 0
G3 :Z <-------------------------RESIGN/no-rsp-req <-- c1 :z
Superior cancels, inferior never decided (-:)
superior inferior
ENROL/no-rsp-req <-- i1 :b1
RESIGN/rsp-req <-- b1 :c1
I1 :B1 <-------------------ENROL/no-rsp-req
B1 :G1 === decide to cancel
G1 :G3 <---------------------RESIGN/rsp-req
disruption I XXX c1 :z
G3 :Z XXX disruption I
Superior cancels, inferior never decided (-:)
superior inferior
ENROL/no-rsp-req <-- i1 :b1
RESIGN/rsp-req <-- b1 :c1
I1 :B1 <-------------------ENROL/no-rsp-req
B1 :G1 === decide to cancel
RESIGN/no-rsp-req <-- c1 :z
G1 :G3 <---------------------RESIGN/rsp-req
G3 :Z <------------------RESIGN/no-rsp-req
Superior cancels, inferior never decided (-:)
superior inferior
ENROL/no-rsp-req <-- i1 :b1
RESIGN/rsp-req <-- b1 :c1
I1 :B1 <-------------------ENROL/no-rsp-req
B1 :G1 === decide to cancel
G1 :G3 <---------------------RESIGN/rsp-req
G3 :G3 <----------------------------RESIGN/rsp-req <-- c1 :c1
G3 :Z <-------------------------RESIGN/no-rsp-req <-- c1 :z
Superior cancels, inferior never decided (-:)
superior inferior
ENROL/no-rsp-req <-- i1 :b1
RESIGN/rsp-req <-- b1 :c1
I1 :B1 <-------------------ENROL/no-rsp-req
B1 :G1 === decide to cancel
G1 :G3 <---------------------RESIGN/rsp-req
G3 :Z --> CANCEL------------------------------------> c1 :z
Superior cancels, inferior never decided (-:)
superior inferior
ENROL/no-rsp-req <-- i1 :b1
decide to be prepared === b1 :e1
decide to confirm autonomously === e1 :h1
I1 :B1 <-------------------ENROL/no-rsp-req
B1 :H1 <----------------------------CONFIRMED/auto <-- h1 :h1
H1 :L0 === decide to cancel
L0 :L1 === record contradiction
L1 :Z --> CONTRADICTION-----------------------------> h1 :z
Superior cancels, inferior confirmed - contradiction reported (-!:#)
superior inferior
ENROL/no-rsp-req <-- i1 :b1
decide to be prepared === b1 :e1
decide to confirm autonomously === e1 :h1
CONFIRMED/auto <-- h1 :h1
I1 :B1 <-------------------ENROL/no-rsp-req
B1 :H1 <---------------------CONFIRMED/auto
H1 :F1 === decide to confirm
F1 :F1 --> CONFIRM-----------------------------------> h1 :h2
F1 :Z0 <------------------------CONFIRMED/response <-- h2 :z
Both confirm (+:#)
superior inferior
ENROL/no-rsp-req <-- i1 :b1
decide to be prepared === b1 :e1
I1 :B1 <-------------------ENROL/no-rsp-req
decide to confirm autonomously === e1 :h1
B1 :H1 <----------------------------CONFIRMED/auto <-- h1 :h1
H1 :H1 XXX disruption 0
H1 :L0 === decide to cancel
L0 :L1 === record contradiction
L1 :Z --> CONTRADICTION-----------------------------> h1 :z
Superior cancels, inferior confirmed - contradiction reported (-!:#)
superior inferior
ENROL/no-rsp-req <-- i1 :b1
decide to be prepared === b1 :e1
decide to confirm autonomously === e1 :h1
I1 :B1 <-------------------ENROL/no-rsp-req
B1 :H1 <----------------------------CONFIRMED/auto <-- h1 :h1
H1 :Z XXX disruption I
Z :L2 <----------------------------CONFIRMED/auto <-- h1 :h1
L2 :L1 === record contradiction
L1 :Z --> CONTRADICTION-----------------------------> h1 :z
Superior never decided, inferior confirmed - contradiction reported (!:#)
superior inferior
ENROL/no-rsp-req <-- i1 :b1
decide to be prepared === b1 :e1
decide to confirm autonomously === e1 :h1
CONFIRMED/auto <-- h1 :h1
I1 :B1 <-------------------ENROL/no-rsp-req
B1 :H1 <---------------------CONFIRMED/auto
H1 :E1 XXX disruption II
E1 :N1 --> REQUEST_CONFIRM---------------------------> h1 :n2
N1 :Z <------------------------CONFIRMED/response <-- n2 :z
Superior requested confirm, inferior confirmed (=:#)
superior inferior
ENROL/no-rsp-req <-- i1 :b1
decide to be prepared === b1 :e1
decide to confirm autonomously === e1 :h1
I1 :B1 <-------------------ENROL/no-rsp-req
B1 :H1 <----------------------------CONFIRMED/auto <-- h1 :h1
H1 :D1 XXX disruption III
D1 :H1 <----------------------------CONFIRMED/auto <-- h1 :h1
H1 :F1 === decide to confirm
F1 :F1 --> CONFIRM-----------------------------------> h1 :h2
F1 :Z0 <------------------------CONFIRMED/response <-- h2 :z
Both confirm (+:#)
superior inferior
ENROL/no-rsp-req <-- i1 :b1
decide to be prepared === b1 :e1
decide to confirm autonomously === e1 :h1
I1 :B1 <-------------------ENROL/no-rsp-req
B1 :H1 <----------------------------CONFIRMED/auto <-- h1 :h1
H1 :B1 XXX disruption IV
B1 :N1 --> REQUEST_CONFIRM---------------------------> h1 :n2
N1 :Z <------------------------CONFIRMED/response <-- n2 :z
Superior requested confirm, inferior confirmed (=:#)
superior inferior
ENROL/no-rsp-req <-- i1 :b1
decide to be prepared === b1 :e1
I1 :B1 <-------------------ENROL/no-rsp-req
decide to confirm autonomously === e1 :h1
B1 :H1 <----------------------------CONFIRMED/auto <-- h1 :h1
H1 :H1 <----------------------------CONFIRMED/auto <-- h1 :h1
H1 :L0 === decide to cancel
L0 :L1 === record contradiction
L1 :Z --> CONTRADICTION-----------------------------> h1 :z
Superior cancels, inferior confirmed - contradiction reported (-!:#)
superior inferior
I1 :I1 XXX disruption 0
ENROL/rsp-req <-- i1 :a1
I1 :Z XXX disruption I
X---ENROL/rsp-req
disruption I XXX a1 :z
Nothing happens (:)
superior inferior
ENROL/no-rsp-req <-- i1 :b1
CANCELLED <-- b1 :z
I1 :Z XXX disruption I
X---ENROL/no-rsp-req
X---CANCELLED
Nothing happens (:)
superior inferior
ENROL/no-rsp-req <-- i1 :b1
I1 :I1 XXX disruption 0
X---ENROL/no-rsp-req
I1 :Y1 <---------------------------------CANCELLED <-- b1 :z
Y1 :Z --> SUP_STATE/unknown-------------------------> z :z
Nothing happens (:)
superior inferior
ENROL/no-rsp-req <-- i1 :b1
decide to be prepared === b1 :e1
PREPARED <-- e1 :e1
decide to confirm autonomously === e1 :h1
disruption 0 XXX h1 :h1
X---PREPARED
X---ENROL/no-rsp-req
I1 :L2 <----------------------------CONFIRMED/auto <-- h1 :h1
L2 :L1 === record contradiction
L1 :Z --> CONTRADICTION-----------------------------> h1 :z
Superior never decided, inferior confirmed - contradiction reported (!:#)
superior inferior
ENROL/no-rsp-req <-- i1 :b1
CANCELLED <-- b1 :z
I1 :B1 <-------------------ENROL/no-rsp-req
B1 :Z <--------------------------CANCELLED
Nothing happens (:)
superior inferior
I1 :A1 <-----------------------------ENROL/rsp-req <-- i1 :a1
disruption I XXX a1 :z
A1 :Z XXX disruption I
Nothing happens (:)
superior inferior
ENROL/rsp-req <-- i1 :a1
detect problem === a1 :m2
disruption 0 XXX m2 :m2
X---ENROL/rsp-req
I1 :M0 <------------------------------------HAZARD <-- m2 :m2
M0 :M3 === record contradiction
M3 :Z --> CONTRADICTION-----------------------------> m2 :z
Inferior detected problem, contradiction reported (!:?)
superior inferior
ENROL/rsp-req <-- i1 :a1
I1 :I1 XXX disruption 0
X---ENROL/rsp-req
I1 :Y1 <------------------------INF_STATE/active/y <-- a1 :a1
Y1 :Z --> SUP_STATE/unknown-------------------------> a1 :z
Nothing happens (:)
superior inferior
ENROL/no-rsp-req <-- i1 :b1
INF_STATE/active/y <-- b1 :b1
decide to be prepared === b1 :e1
I1 :I1 XXX disruption 0
X---ENROL/no-rsp-req
X---INF_STATE/active/y
PREPARED <-- e1 :e1
decide to cancel autonomously === e1 :j1
I1 :Y1 <---------------------------PREPARED
Y1 :Y1 <---------------------------------CANCELLED <-- j1 :j2
Y1 :Z --> SUP_STATE/unknown-------------------------> j2 :z
superior never decided, inferior cancelled (:-)
superior inferior
ENROL/no-rsp-req <-- i1 :b1
decide to be prepared/cancel === b1 :e2
disruption 0 XXX e2 :e2
X---ENROL/no-rsp-req
I1 :Y1 <---------------------------PREPARED/cancel <-- e2 :e2
Y1 :Z --> SUP_STATE/unknown-------------------------> e2 :y0
remove prepared information === y0 :z
Nothing happens (:)
superior inferior
ENROL/no-rsp-req <-- i1 :b1
RESIGN/no-rsp-req <-- b1 :z
I1 :I1 XXX disruption 0
X---ENROL/no-rsp-req
I1 :Z <------------------RESIGN/no-rsp-req
Nothing happens (:)
superior inferior
ENROL/no-rsp-req <-- i1 :b1
disruption 0 XXX b1 :b1
X---ENROL/no-rsp-req
RESIGN/rsp-req <-- b1 :c1
RESIGN/no-rsp-req <-- c1 :z
I1 :Y1 <---------------------RESIGN/rsp-req
Y1 :Z <------------------RESIGN/no-rsp-req
Nothing happens (:)
superior inferior
ENROL/no-rsp-req <-- i1 :b1
decide to be prepared === b1 :e1
PREPARED <-- e1 :e1
decide to cancel autonomously === e1 :j1
CANCELLED <-- j1 :j2
I1 :B1 <-------------------ENROL/no-rsp-req
B1 :E1 <---------------------------PREPARED
E1 :J1 <--------------------------CANCELLED
J1 :J2 === decide to cancel
J2 :Z --> CANCEL------------------------------------> j2 :z
Both cancel (-:-)
superior inferior
ENROL/no-rsp-req <-- i1 :b1
decide to be prepared === b1 :e1
PREPARED <-- e1 :e1
I1 :B1 <-------------------ENROL/no-rsp-req
decide to cancel autonomously === e1 :j1
B1 :E1 <---------------------------PREPARED
E1 :J1 <---------------------------------CANCELLED <-- j1 :j2
J1 :K0 === decide to confirm
K0 :K1 === record contradiction
K1 :Z --> CONTRADICTION-----------------------------> j2 :z
Superior confirms, inferior cancelled - contradiction reported (+!:-)
superior inferior
I1 :B1 <--------------------------ENROL/no-rsp-req <-- i1 :b1
decide to be prepared/cancel === b1 :e2
B1 :B1 --> SUP_STATE/active/y
PREPARED/cancel <-- e2 :e2
decide to cancel autonomously === e2 :z1
SUP_STATE/active/y-----------------> z1 :y3
CANCELLED <-- y3 :z1
B1 :E2 <--------------------PREPARED/cancel
E2 :J1 <--------------------------CANCELLED
J1 :J1 XXX disruption 0
J1 :J2 === decide to cancel
J2 :Z --> CANCEL------------------------------------> z1 :y1
Z :Z <-------------------------INF_STATE/unknown <-- y1 :z
Both cancel (-:-)
superior inferior
ENROL/no-rsp-req <-- i1 :b1
decide to be prepared/cancel === b1 :e2
I1 :B1 <-------------------ENROL/no-rsp-req
PREPARED/cancel <-- e2 :e2
B1 :B1 --> SUP_STATE/active/y
B1 :E2 <--------------------PREPARED/cancel
decide to cancel autonomously === e2 :z1
SUP_STATE/active/y-----------------> z1 :y3
E2 :J1 <---------------------------------CANCELLED <-- y3 :z1
J1 :Z XXX disruption I
superior never decided, inferior cancelled (:-)
superior inferior
ENROL/no-rsp-req <-- i1 :b1
decide to be prepared === b1 :e1
I1 :B1 <-------------------ENROL/no-rsp-req
PREPARED <-- e1 :e1
decide to cancel autonomously === e1 :j1
CANCELLED <-- j1 :j2
B1 :E1 <---------------------------PREPARED
E1 :J1 <--------------------------CANCELLED
J1 :E1 XXX disruption II
E1 :N1 --> REQUEST_CONFIRM---------------------------> j2 :n3
N1 :Z <---------------------------------CANCELLED <-- n3 :z
Superior requested confirm, inferior cancelled (=:-)
superior inferior
ENROL/no-rsp-req <-- i1 :b1
decide to be prepared === b1 :e1
PREPARED <-- e1 :e1
I1 :B1 <-------------------ENROL/no-rsp-req
B1 :E1 <---------------------------PREPARED
decide to cancel autonomously === e1 :j1
E1 :J1 <---------------------------------CANCELLED <-- j1 :j2
J1 :B1 XXX disruption III
B1 :D1 === decide to prepare
D1 :Z <---------------------------------CANCELLED <-- j2 :j2
Z :Y1 <---------------------------------CANCELLED <-- j2 :j2
Y1 :Z --> SUP_STATE/unknown-------------------------> j2 :z
superior never decided, inferior cancelled (:-)
superior inferior
ENROL/no-rsp-req <-- i1 :b1
decide to be prepared === b1 :e1
I1 :B1 <-------------------ENROL/no-rsp-req
PREPARED <-- e1 :e1
decide to cancel autonomously === e1 :j1
B1 :E1 <---------------------------PREPARED
E1 :E1 === decide to prepare
E1 :J1 <---------------------------------CANCELLED <-- j1 :j2
J1 :B1 XXX disruption IV
B1 :G1 === decide to cancel
G1 :G2 --> CANCEL
CANCELLED <-- j2 :j2
CANCEL-----------------------------> j2 :z
G2 :Z <--------------------------CANCELLED
Both cancel (-:-)
superior inferior
ENROL/no-rsp-req <-- i1 :b1
decide to be prepared === b1 :e1
I1 :B1 <-------------------ENROL/no-rsp-req
PREPARED <-- e1 :e1
decide to cancel autonomously === e1 :j1
CANCELLED <-- j1 :j2
B1 :E1 <---------------------------PREPARED
CANCELLED <-- j2 :j2
E1 :J1 <--------------------------CANCELLED
J1 :J1 <--------------------------CANCELLED
J1 :J2 === decide to cancel
J2 :Z --> CANCEL------------------------------------> j2 :z
Both cancel (-:-)
superior inferior
I1 :B1 <--------------------------ENROL/no-rsp-req <-- i1 :b1
CANCELLED <-- b1 :z
B1 :G1 === decide to cancel
G1 :J2 <--------------------------CANCELLED
J2 :J2 XXX disruption 0
J2 :Z XXX disruption III
Superior cancels, inferior never decided (-:)
superior inferior
ENROL/no-rsp-req <-- i1 :b1
CANCELLED <-- b1 :z
I1 :B1 <-------------------ENROL/no-rsp-req
B1 :G1 === decide to cancel
G1 :J2 <--------------------------CANCELLED
J2 :Z XXX disruption I
Superior cancels, inferior never decided (-:)
superior inferior
I1 :B1 <--------------------------ENROL/no-rsp-req <-- i1 :b1
B1 :G1 === decide to cancel
G1 :J2 <---------------------------------CANCELLED <-- b1 :z
J2 :G2 XXX disruption II
G2 :Z XXX disruption I
Superior cancels, inferior never decided (-:)
superior inferior
I1 :B1 <--------------------------ENROL/no-rsp-req <-- i1 :b1
CANCELLED <-- b1 :z
B1 :G1 === decide to cancel
G1 :J2 <--------------------------CANCELLED
J2 :Z XXX disruption III
Superior cancels, inferior never decided (-:)
superior inferior
ENROL/no-rsp-req <-- i1 :b1
decide to be prepared === b1 :e1
I1 :B1 <-------------------ENROL/no-rsp-req
decide to cancel autonomously === e1 :j1
B1 :G1 === decide to cancel
G1 :J2 <---------------------------------CANCELLED <-- j1 :j2
J2 :J2 <---------------------------------CANCELLED <-- j2 :j2
J2 :Z --> CANCEL------------------------------------> j2 :z
Both cancel (-:-)
superior inferior
ENROL/no-rsp-req <-- i1 :b1
CANCELLED <-- b1 :z
I1 :B1 <-------------------ENROL/no-rsp-req
B1 :B1 --> SUP_STATE/active/y
B1 :G1 === decide to cancel
SUP_STATE/active/y-----------------> z :y1
INF_STATE/unknown <-- y1 :z
G1 :J2 <--------------------------CANCELLED
J2 :Z <------------------INF_STATE/unknown
Superior cancels, inferior never decided (-:)
superior inferior
I1 :B1 <--------------------------ENROL/no-rsp-req <-- i1 :b1
CANCELLED <-- b1 :z
B1 :G1 === decide to cancel
G1 :J2 <--------------------------CANCELLED
J2 :Z --> CANCEL
disruption 0 XXX z :z
CANCEL---X
Superior cancels, inferior never decided (-:)
superior inferior
I1 :B1 <--------------------------ENROL/no-rsp-req <-- i1 :b1
B1 :D1 === decide to prepare
decide to be prepared === b1 :e1
D1 :E1 <----------------------------------PREPARED <-- e1 :e1
decide to cancel autonomously === e1 :j1
E1 :F1 === decide to confirm
F1 :K0 <---------------------------------CANCELLED <-- j1 :j2
K0 :K0 XXX disruption 0
K0 :K1 === record contradiction
K1 :Z --> CONTRADICTION-----------------------------> j2 :z
Superior confirms, inferior cancelled - contradiction reported (+!:-)
superior inferior
ENROL/no-rsp-req <-- i1 :b1
decide to be prepared === b1 :e1
I1 :B1 <-------------------ENROL/no-rsp-req
PREPARED <-- e1 :e1
decide to cancel autonomously === e1 :j1
B1 :E1 <---------------------------PREPARED
E1 :E1 --> SUP_STATE/preparedreceived/y
E1 :F1 === decide to confirm
SUP_STATE/preparedreceived/y-------> j1 :j1
F1 :K0 <---------------------------------CANCELLED <-- j1 :j2
K0 :F1 XXX disruption I
F1 :K0 <---------------------------------CANCELLED <-- j2 :j2
K0 :K1 === record contradiction
K1 :Z --> CONTRADICTION-----------------------------> j2 :z
Superior confirms, inferior cancelled - contradiction reported (+!:-)
superior inferior
ENROL/no-rsp-req <-- i1 :b1
decide to be prepared === b1 :e1
PREPARED <-- e1 :e1
I1 :B1 <-------------------ENROL/no-rsp-req
B1 :E1 <---------------------------PREPARED
E1 :F1 === decide to confirm
decide to cancel autonomously === e1 :j1
F1 :K0 <---------------------------------CANCELLED <-- j1 :j2
K0 :K0 <---------------------------------CANCELLED <-- j2 :j2
K0 :K1 === record contradiction
K1 :Z --> CONTRADICTION-----------------------------> j2 :z
Superior confirms, inferior cancelled - contradiction reported (+!:-)
superior inferior
ENROL/no-rsp-req <-- i1 :b1
decide to be prepared === b1 :e1
PREPARED <-- e1 :e1
I1 :B1 <-------------------ENROL/no-rsp-req
B1 :E1 <---------------------------PREPARED
E1 :F1 === decide to confirm
decide to cancel autonomously === e1 :j1
F1 :K0 <---------------------------------CANCELLED <-- j1 :j2
K0 :K1 === record contradiction
K1 :Z --> CONTRADICTION-----------------------------> j2 :z
Superior confirms, inferior cancelled - contradiction reported (+!:-)
superior inferior
I1 :B1 <--------------------------ENROL/no-rsp-req <-- i1 :b1
decide to be prepared === b1 :e1
B1 :E1 <----------------------------------PREPARED <-- e1 :e1
E1 :F1 === decide to confirm
decide to cancel autonomously === e1 :j1
F1 :K0 <---------------------------------CANCELLED <-- j1 :j2
K0 :K1 === record contradiction
K1 :K1 XXX disruption 0
K1 :Z --> CONTRADICTION-----------------------------> j2 :z
Superior confirms, inferior cancelled - contradiction reported (+!:-)
superior inferior
I1 :B1 <--------------------------ENROL/no-rsp-req <-- i1 :b1
decide to be prepared/cancel === b1 :e2
B1 :E2 <---------------------------PREPARED/cancel <-- e2 :e2
decide to cancel autonomously === e2 :z1
E2 :F1 === decide to confirm
F1 :F1 --> CONFIRM-----------------------------------> z1 :y3
F1 :K0 <---------------------------------CANCELLED <-- y3 :z1
K0 :K1 === record contradiction
K1 :Z XXX disruption I
Superior confirms, inferior cancelled - contradiction reported (+!:-)
superior inferior
ENROL/no-rsp-req <-- i1 :b1
decide to be prepared === b1 :e1
PREPARED <-- e1 :e1
I1 :B1 <-------------------ENROL/no-rsp-req
decide to cancel autonomously === e1 :j1
B1 :E1 <---------------------------PREPARED
E1 :F1 === decide to confirm
F1 :K0 <---------------------------------CANCELLED <-- j1 :j2
K0 :K1 === record contradiction
K1 :K1 <---------------------------------CANCELLED <-- j2 :j2
K1 :Z --> CONTRADICTION-----------------------------> j2 :z
Superior confirms, inferior cancelled - contradiction reported (+!:-)
superior inferior
ENROL/no-rsp-req <-- i1 :b1
decide to be prepared === b1 :e1
PREPARED <-- e1 :e1
I1 :B1 <-------------------ENROL/no-rsp-req
B1 :E1 <---------------------------PREPARED
E1 :F1 === decide to confirm
decide to cancel autonomously === e1 :j1
F1 :K0 <---------------------------------CANCELLED <-- j1 :j2
K0 :K1 === record contradiction
K1 :Z --> CONTRADICTION-----------------------------> j2 :z
Superior confirms, inferior cancelled - contradiction reported (+!:-)
superior inferior
I1 :B1 <--------------------------ENROL/no-rsp-req <-- i1 :b1
decide to be prepared === b1 :e1
B1 :G1 === decide to cancel
decide to confirm autonomously === e1 :h1
G1 :L0 <----------------------------CONFIRMED/auto <-- h1 :h1
L0 :L0 XXX disruption 0
L0 :L1 === record contradiction
L1 :Z --> CONTRADICTION-----------------------------> h1 :z
Superior cancels, inferior confirmed - contradiction reported (-!:#)
superior inferior
ENROL/no-rsp-req <-- i1 :b1
decide to be prepared === b1 :e1
I1 :B1 <-------------------ENROL/no-rsp-req
decide to confirm autonomously === e1 :h1
CONFIRMED/auto <-- h1 :h1
B1 :G1 === decide to cancel
G1 :L0 <---------------------CONFIRMED/auto
L0 :Z XXX disruption I
Z :L2 <----------------------------CONFIRMED/auto <-- h1 :h1
L2 :L1 === record contradiction
L1 :Z --> CONTRADICTION-----------------------------> h1 :z
Superior cancels, inferior confirmed - contradiction reported (-!:#)
superior inferior
ENROL/no-rsp-req <-- i1 :b1
decide to be prepared === b1 :e1
I1 :B1 <-------------------ENROL/no-rsp-req
decide to confirm autonomously === e1 :h1
B1 :G1 === decide to cancel
G1 :L0 <----------------------------CONFIRMED/auto <-- h1 :h1
L0 :G2 XXX disruption II
G2 :L0 <----------------------------CONFIRMED/auto <-- h1 :h1
L0 :L1 === record contradiction
L1 :Z --> CONTRADICTION-----------------------------> h1 :z
Superior cancels, inferior confirmed - contradiction reported (-!:#)
superior inferior
ENROL/no-rsp-req <-- i1 :b1
decide to be prepared === b1 :e1
I1 :B1 <-------------------ENROL/no-rsp-req
B1 :G1 === decide to cancel
decide to confirm autonomously === e1 :h1
CONFIRMED/auto <-- h1 :h1
CONFIRMED/auto <-- h1 :h1
G1 :L0 <---------------------CONFIRMED/auto
L0 :L0 <---------------------CONFIRMED/auto
L0 :L1 === record contradiction
L1 :Z --> CONTRADICTION-----------------------------> h1 :z
Superior cancels, inferior confirmed - contradiction reported (-!:#)
superior inferior
ENROL/no-rsp-req <-- i1 :b1
decide to be prepared === b1 :e1
decide to confirm autonomously === e1 :h1
I1 :B1 <-------------------ENROL/no-rsp-req
B1 :G1 === decide to cancel
G1 :L0 <----------------------------CONFIRMED/auto <-- h1 :h1
L0 :L1 === record contradiction
L1 :Z --> CONTRADICTION-----------------------------> h1 :z
Superior cancels, inferior confirmed - contradiction reported (-!:#)
superior inferior
ENROL/no-rsp-req <-- i1 :b1
decide to be prepared === b1 :e1
decide to confirm autonomously === e1 :h1
I1 :B1 <-------------------ENROL/no-rsp-req
B1 :H1 <----------------------------CONFIRMED/auto <-- h1 :h1
H1 :L0 === decide to cancel
L0 :L1 === record contradiction
L1 :L1 XXX disruption 0
L1 :Z --> CONTRADICTION-----------------------------> h1 :z
Superior cancels, inferior confirmed - contradiction reported (-!:#)
superior inferior
ENROL/no-rsp-req <-- i1 :b1
decide to be prepared === b1 :e1
decide to confirm autonomously === e1 :h1
I1 :B1 <-------------------ENROL/no-rsp-req
B1 :H1 <----------------------------CONFIRMED/auto <-- h1 :h1
H1 :L0 === decide to cancel
L0 :L1 === record contradiction
CONFIRMED/auto <-- h1 :h1
L1 :Z --> CONTRADICTION
Z :L2 <---------------------CONFIRMED/auto
CONTRADICTION----------------------> h1 :z
L2 :L1 === record contradiction
L1 :Z XXX disruption I
Superior cancels, inferior confirmed - contradiction reported (-!:#)
superior inferior
ENROL/no-rsp-req <-- i1 :b1
decide to be prepared === b1 :e1
decide to confirm autonomously === e1 :h1
CONFIRMED/auto <-- h1 :h1
I1 :B1 <-------------------ENROL/no-rsp-req
B1 :H1 <---------------------CONFIRMED/auto
H1 :L0 === decide to cancel
L0 :L1 === record contradiction
L1 :L1 <----------------------------CONFIRMED/auto <-- h1 :h1
L1 :Z --> CONTRADICTION-----------------------------> h1 :z
Superior cancels, inferior confirmed - contradiction reported (-!:#)
superior inferior
ENROL/no-rsp-req <-- i1 :b1
decide to be prepared === b1 :e1
decide to confirm autonomously === e1 :h1
I1 :B1 <-------------------ENROL/no-rsp-req
B1 :G1 === decide to cancel
G1 :L0 <----------------------------CONFIRMED/auto <-- h1 :h1
L0 :L1 === record contradiction
L1 :Z --> CONTRADICTION-----------------------------> h1 :z
Superior cancels, inferior confirmed - contradiction reported (-!:#)
superior inferior
I1 :Z XXX disruption I
Z :Z <--------------------------ENROL/no-rsp-req <-- i1 :b1
decide to be prepared === b1 :e1
decide to confirm autonomously === e1 :h1
Z :L2 <----------------------------CONFIRMED/auto <-- h1 :h1
L2 :L2 <----------------------------CONFIRMED/auto <-- h1 :h1
L2 :L2 XXX disruption 0
L2 :L1 === record contradiction
L1 :Z --> CONTRADICTION-----------------------------> h1 :z
Superior never decided, inferior confirmed - contradiction reported (!:#)
superior inferior
I1 :B1 <--------------------------ENROL/no-rsp-req <-- i1 :b1
decide to be prepared === b1 :e1
B1 :G1 === decide to cancel
decide to confirm autonomously === e1 :h1
G1 :L0 <----------------------------CONFIRMED/auto <-- h1 :h1
L0 :L1 === record contradiction
CONFIRMED/auto <-- h1 :h1
L1 :Z --> CONTRADICTION
Z :L2 <---------------------CONFIRMED/auto
CONTRADICTION----------------------> h1 :z
L2 :Z XXX disruption I
Superior cancels, inferior confirmed - contradiction reported (-!:#)
superior inferior
ENROL/no-rsp-req <-- i1 :b1
decide to be prepared === b1 :e1
decide to confirm autonomously === e1 :h1
I1 :Z XXX disruption I
X---ENROL/no-rsp-req
Z :L2 <----------------------------CONFIRMED/auto <-- h1 :h1
L2 :L2 <----------------------------CONFIRMED/auto <-- h1 :h1
L2 :L1 === record contradiction
L1 :Z --> CONTRADICTION-----------------------------> h1 :z
Superior never decided, inferior confirmed - contradiction reported (!:#)
superior inferior
I1 :Z XXX disruption I
ENROL/no-rsp-req <-- i1 :b1
decide to be prepared === b1 :e1
decide to confirm autonomously === e1 :h1
Z :Z <-------------------ENROL/no-rsp-req
Z :L2 <----------------------------CONFIRMED/auto <-- h1 :h1
L2 :L1 === record contradiction
L1 :Z --> CONTRADICTION-----------------------------> h1 :z
Superior never decided, inferior confirmed - contradiction reported (!:#)
superior inferior
I1 :A1 <-----------------------------ENROL/rsp-req <-- i1 :a1
detect problem === a1 :m2
A1 :M0 <------------------------------------HAZARD <-- m2 :m2
M0 :M0 XXX disruption 0
M0 :M3 === record contradiction
M3 :Z --> CONTRADICTION-----------------------------> m2 :z
Inferior detected problem, contradiction reported (!:?)
superior inferior
I1 :A1 <-----------------------------ENROL/rsp-req <-- i1 :a1
detect problem === a1 :m2
A1 :M0 <------------------------------------HAZARD <-- m2 :m2
M0 :Z XXX disruption I
disruption I XXX m2 :z
Superior nothing, unreported hazard (:?)
superior inferior
I1 :A1 <-----------------------------ENROL/rsp-req <-- i1 :a1
detect problem === a1 :m2
A1 :M0 <------------------------------------HAZARD <-- m2 :m2
M0 :M0 <------------------------------------HAZARD <-- m2 :m2
M0 :Z XXX disruption I
disruption I XXX m2 :z
Superior nothing, unreported hazard (:?)
superior inferior
ENROL/no-rsp-req <-- i1 :b1
detect problem === b1 :m2
HAZARD <-- m2 :m2
disruption I XXX m2 :z
I1 :B1 <-------------------ENROL/no-rsp-req
B1 :B1 --> SUP_STATE/active/y
B1 :M0 <-----------------------------HAZARD
SUP_STATE/active/y-----------------> z :y1
M0 :M0 <-------------------------INF_STATE/unknown <-- y1 :z
disruption 0 XXX z :z
M0 :M3 === record contradiction
M3 :Z XXX disruption I
Inferior detected problem, contradiction reported (!:?)
superior inferior
I1 :A1 <-----------------------------ENROL/rsp-req <-- i1 :a1
detect problem === a1 :m2
A1 :M0 <------------------------------------HAZARD <-- m2 :m2
M0 :M3 === record contradiction
M3 :Z --> CONTRADICTION-----------------------------> m2 :z
Inferior detected problem, contradiction reported (!:?)
superior inferior
ENROL/no-rsp-req <-- i1 :b1
decide to be prepared/cancel === b1 :e2
PREPARED/cancel <-- e2 :e2
detect problem === e2 :m3
I1 :B1 <-------------------ENROL/no-rsp-req
B1 :E2 <--------------------PREPARED/cancel
E2 :F1 === decide to confirm
detect and record problem === m3 :m1
F1 :M1 <------------------------------------HAZARD <-- m1 :m1
M1 :M1 XXX disruption 0
M1 :M3 === record contradiction
M3 :Z --> CONTRADICTION-----------------------------> m1 :z
Superior confirms, inferior detects mix - contradiction reported (+!:!)
superior inferior
ENROL/no-rsp-req <-- i1 :b1
decide to be prepared === b1 :e1
I1 :B1 <-------------------ENROL/no-rsp-req
B1 :E1 <----------------------------------PREPARED <-- e1 :e1
E1 :F1 === decide to confirm
detect problem === e1 :m3
HAZARD <-- m3 :m3
detect and record problem === m3 :m1
F1 :M1 <-----------------------------HAZARD
M1 :Z XXX disruption I
Z :M0 <------------------------------------HAZARD <-- m1 :m1
M0 :M3 === record contradiction
M3 :Z --> CONTRADICTION-----------------------------> m1 :z
Superior confirms, inferior detects mix - contradiction reported (+!:!)
superior inferior
ENROL/no-rsp-req <-- i1 :b1
decide to be prepared/cancel === b1 :e2
I1 :B1 <-------------------ENROL/no-rsp-req
PREPARED/cancel <-- e2 :e2
detect problem === e2 :m3
detect and record problem === m3 :m1
B1 :E2 <--------------------PREPARED/cancel
E2 :F1 === decide to confirm
F1 :M1 <------------------------------------HAZARD <-- m1 :m1
M1 :F1 XXX disruption II
F1 :F1 --> CONFIRM-----------------------------------> m1 :m1
F1 :M1 <------------------------------------HAZARD <-- m1 :m1
M1 :M3 === record contradiction
M3 :Z --> CONTRADICTION-----------------------------> m1 :z
Superior confirms, inferior detects mix - contradiction reported (+!:!)
superior inferior
ENROL/no-rsp-req <-- i1 :b1
decide to be prepared === b1 :e1
I1 :B1 <-------------------ENROL/no-rsp-req
PREPARED <-- e1 :e1
detect problem === e1 :m3
B1 :E1 <---------------------------PREPARED
E1 :F1 === decide to confirm
F1 :M1 <------------------------------------HAZARD <-- m3 :m3
M1 :M1 <------------------------------------HAZARD <-- m3 :m3
M1 :M3 === record contradiction
M3 :Z --> CONTRADICTION-----------------------------> m3 :z
Superior confirms, inferior only detects mix - contradiction reported (+!:?)
superior inferior
ENROL/no-rsp-req <-- i1 :b1
decide to be prepared/cancel === b1 :e2
PREPARED/cancel <-- e2 :e2
I1 :B1 <-------------------ENROL/no-rsp-req
B1 :E2 <--------------------PREPARED/cancel
detect problem === e2 :m3
E2 :F1 === decide to confirm
F1 :M1 <------------------------------------HAZARD <-- m3 :m3
M1 :M3 === record contradiction
M3 :Z --> CONTRADICTION-----------------------------> m3 :z
Superior confirms, inferior only detects mix - contradiction reported (+!:?)
superior inferior
ENROL/no-rsp-req <-- i1 :b1
detect problem === b1 :m2
I1 :B1 <-------------------ENROL/no-rsp-req
B1 :G1 === decide to cancel
G1 :M2 <------------------------------------HAZARD <-- m2 :m2
M2 :M2 XXX disruption 0
M2 :M3 === record contradiction
M3 :Z --> CONTRADICTION-----------------------------> m2 :z
Superior cancels, Inferior detected problem, contradiction reported (-!:?)
superior inferior
I1 :B1 <--------------------------ENROL/no-rsp-req <-- i1 :b1
B1 :G1 === decide to cancel
detect problem === b1 :m2
G1 :M2 <------------------------------------HAZARD <-- m2 :m2
disruption I XXX m2 :z
M2 :Z XXX disruption I
Superior cancels, unreported hazard (-:?)
superior inferior
I1 :B1 <--------------------------ENROL/no-rsp-req <-- i1 :b1
detect problem === b1 :m2
B1 :G1 === decide to cancel
G1 :M2 <------------------------------------HAZARD <-- m2 :m2
disruption I XXX m2 :z
M2 :G2 XXX disruption II
G2 :G2 --> CANCEL------------------------------------> z :y1
G2 :Z <-------------------------INF_STATE/unknown <-- y1 :z
Superior cancels, unreported hazard (-:?)
superior inferior
ENROL/no-rsp-req <-- i1 :b1
detect problem === b1 :m2
I1 :B1 <-------------------ENROL/no-rsp-req
B1 :G1 === decide to cancel
HAZARD <-- m2 :m2
HAZARD <-- m2 :m2
G1 :M2 <-----------------------------HAZARD
M2 :M2 <-----------------------------HAZARD
disruption I XXX m2 :z
M2 :Z XXX disruption I
Superior cancels, unreported hazard (-:?)
superior inferior
I1 :A1 <-----------------------------ENROL/rsp-req <-- i1 :a1
A1 :B1 --> ENROLLED----------------------------------> a1 :b1
B1 :G1 === decide to cancel
detect problem === b1 :m2
HAZARD <-- m2 :m2
G1 :G2 --> CANCEL
G2 :M2 <-----------------------------HAZARD
disruption I XXX m2 :z
CANCEL-----------------------------> z :y1
M2 :M2 <-------------------------INF_STATE/unknown <-- y1 :z
M2 :M3 === record contradiction
M3 :Z --> CONTRADICTION-----------------------------> z :z
Superior cancels, Inferior detected problem, contradiction reported (-!:?)
superior inferior
ENROL/no-rsp-req <-- i1 :b1
detect problem === b1 :m2
I1 :B1 <-------------------ENROL/no-rsp-req
B1 :G1 === decide to cancel
G1 :M2 <------------------------------------HAZARD <-- m2 :m2
M2 :M3 === record contradiction
M3 :Z --> CONTRADICTION-----------------------------> m2 :z
Superior cancels, Inferior detected problem, contradiction reported (-!:?)
superior inferior
ENROL/rsp-req <-- i1 :a1
detect problem === a1 :m2
HAZARD <-- m2 :m2
I1 :A1 <----------------------ENROL/rsp-req
A1 :M0 <-----------------------------HAZARD
M0 :M3 === record contradiction
M3 :M3 XXX disruption 0
M3 :Z --> CONTRADICTION-----------------------------> m2 :z
Inferior detected problem, contradiction reported (!:?)
superior inferior
ENROL/no-rsp-req <-- i1 :b1
detect problem === b1 :m2
I1 :B1 <-------------------ENROL/no-rsp-req
B1 :M0 <------------------------------------HAZARD <-- m2 :m2
M0 :M3 === record contradiction
disruption I XXX m2 :z
M3 :Z XXX disruption I
Inferior detected problem, contradiction reported (!:?)
superior inferior
ENROL/no-rsp-req <-- i1 :b1
detect problem === b1 :m2
I1 :B1 <-------------------ENROL/no-rsp-req
HAZARD <-- m2 :m2
HAZARD <-- m2 :m2
B1 :M0 <-----------------------------HAZARD
M0 :M3 === record contradiction
M3 :M3 <-----------------------------HAZARD
M3 :Z --> CONTRADICTION-----------------------------> m2 :z
Inferior detected problem, contradiction reported (!:?)
superior inferior
I1 :B1 <--------------------------ENROL/no-rsp-req <-- i1 :b1
detect problem === b1 :m2
B1 :N1 --> REQUEST_CONFIRM
HAZARD <-- m2 :m2
REQUEST_CONFIRM--------------------> m2 :n5
HAZARD <-- n5 :z
N1 :N1 --> REQUEST_CONFIRM---------------------------> z :y1
INF_STATE/unknown <-- y1 :z
N1 :Z <-----------------------------HAZARD
Z :M0 <-----------------------------HAZARD
M0 :M3 === record contradiction
M3 :M3 <------------------INF_STATE/unknown
M3 :Z XXX disruption I
Confirm requested, inferior detected problem, contradiction reported (=!:?)
superior inferior
I1 :A1 <-----------------------------ENROL/rsp-req <-- i1 :a1
detect problem === a1 :m2
A1 :M0 <------------------------------------HAZARD <-- m2 :m2
M0 :M3 === record contradiction
M3 :Z --> CONTRADICTION-----------------------------> m2 :z
Inferior detected problem, contradiction reported (!:?)
superior inferior
I1 :B1 <--------------------------ENROL/no-rsp-req <-- i1 :b1
INF_STATE/active/y <-- b1 :b1
RESIGN/no-rsp-req <-- b1 :z
B1 :N1 --> REQUEST_CONFIRM
N1 :N1 XXX disruption 0
REQUEST_CONFIRM---X
X---INF_STATE/active/y
N1 :Z <------------------RESIGN/no-rsp-req
Superior requested confirm, inferior never decided (=:)
superior inferior
I1 :B1 <--------------------------ENROL/no-rsp-req <-- i1 :b1
decide to be prepared/cancel === b1 :e2
decide to cancel autonomously === e2 :z1
B1 :N1 --> REQUEST_CONFIRM
N1 :Z XXX disruption I
REQUEST_CONFIRM---X
Superior requested confirm, inferior cancelled (=:-)
superior inferior
ENROL/no-rsp-req <-- i1 :b1
CANCELLED <-- b1 :z
I1 :B1 <-------------------ENROL/no-rsp-req
B1 :N1 --> REQUEST_CONFIRM
disruption 0 XXX z :z
REQUEST_CONFIRM---X
N1 :Z <--------------------------CANCELLED
Superior requested confirm, inferior never decided (=:)
superior inferior
ENROL/no-rsp-req <-- i1 :b1
decide to be prepared === b1 :e1
decide to confirm autonomously === e1 :h1
I1 :B1 <-------------------ENROL/no-rsp-req
CONFIRMED/auto <-- h1 :h1
B1 :N1 --> REQUEST_CONFIRM---------------------------> h1 :n2
N1 :N1 <---------------------CONFIRMED/auto
N1 :Z <------------------------CONFIRMED/response <-- n2 :z
Superior requested confirm, inferior confirmed (=:#)
superior inferior
I1 :B1 <--------------------------ENROL/no-rsp-req <-- i1 :b1
B1 :N1 --> REQUEST_CONFIRM---------------------------> b1 :n1
decide to confirm autonomously === n1 :n2
N1 :Z <------------------------CONFIRMED/response <-- n2 :z
Superior requested confirm, inferior confirmed (=:#)
superior inferior
ENROL/no-rsp-req <-- i1 :b1
detect problem === b1 :m2
I1 :B1 <-------------------ENROL/no-rsp-req
B1 :N1 --> REQUEST_CONFIRM---------------------------> m2 :n5
N1 :Z <------------------------------------HAZARD <-- n5 :z
Confirm requested, inferior detected problem, contradiction not reported (=:?)
superior inferior
I1 :B1 <--------------------------ENROL/no-rsp-req <-- i1 :b1
B1 :B1 --> SUP_STATE/active/y------------------------> b1 :b1
INF_STATE/active <-- b1 :b1
B1 :N1 --> REQUEST_CONFIRM
N1 :N1 <-------------------INF_STATE/active
REQUEST_CONFIRM--------------------> b1 :n1
detect and record problem === n1 :n4
N1 :Z <------------------------------------HAZARD <-- n4 :z
Superior requested confirm, inferior detects mix - contradiction NOT reported (=:!)
superior inferior
ENROL/no-rsp-req <-- i1 :b1
INF_STATE/active/y <-- b1 :b1
I1 :B1 <-------------------ENROL/no-rsp-req
RESIGN/no-rsp-req <-- b1 :z
B1 :N1 --> REQUEST_CONFIRM
N1 :N1 <-----------------INF_STATE/active/y
N1 :Z <------------------RESIGN/no-rsp-req
Z :Z XXX disruption 0
REQUEST_CONFIRM---X
Superior requested confirm, inferior never decided (=:)
superior inferior
ENROL/no-rsp-req <-- i1 :b1
disruption I XXX b1 :z
I1 :B1 <-------------------ENROL/no-rsp-req
B1 :N1 --> REQUEST_CONFIRM---------------------------> z :y1
N1 :Z <-------------------------INF_STATE/unknown <-- y1 :z
Superior requested confirm, inferior never decided (=:)
superior inferior
ENROL/no-rsp-req <-- i1 :b1
decide to be prepared === b1 :e1
I1 :B1 <-------------------ENROL/no-rsp-req
PREPARED <-- e1 :e1
B1 :N1 --> REQUEST_CONFIRM
decide to confirm autonomously === e1 :h1
REQUEST_CONFIRM--------------------> h1 :n2
N1 :N1 <---------------------------PREPARED
N1 :Z <------------------------CONFIRMED/response <-- n2 :z
Superior requested confirm, inferior confirmed (=:#)
superior inferior
ENROL/no-rsp-req <-- i1 :b1
decide to be prepared/cancel === b1 :e2
PREPARED/cancel <-- e2 :e2
decide to cancel autonomously === e2 :z1
I1 :B1 <-------------------ENROL/no-rsp-req
B1 :N1 --> REQUEST_CONFIRM
N1 :N1 <--------------------PREPARED/cancel
REQUEST_CONFIRM--------------------> z1 :y1
N1 :Z <-------------------------INF_STATE/unknown <-- y1 :z
Superior requested confirm, inferior cancelled (=:-)
superior inferior
I1 :B1 <--------------------------ENROL/no-rsp-req <-- i1 :b1
RESIGN/no-rsp-req <-- b1 :z
B1 :N1 --> REQUEST_CONFIRM
N1 :Z <------------------RESIGN/no-rsp-req
disruption 0 XXX z :z
REQUEST_CONFIRM---X
Superior requested confirm, inferior never decided (=:)
superior inferior
ENROL/no-rsp-req <-- i1 :b1
RESIGN/rsp-req <-- b1 :c1
I1 :B1 <-------------------ENROL/no-rsp-req
B1 :N1 --> REQUEST_CONFIRM---------------------------> c1 :c1
N1 :C1 <---------------------RESIGN/rsp-req
C1 :Z <-------------------------RESIGN/no-rsp-req <-- c1 :z
Superior requested confirm, inferior never decided (=:)
superior inferior
ENROL/rsp-req <-- i1 :a1
detect problem === a1 :m2
I1 :A1 <----------------------ENROL/rsp-req
disruption I XXX m2 :z
A1 :B1 --> ENROLLED
B1 :N1 --> REQUEST_CONFIRM
N1 :N1 --> REQUEST_CONFIRM
N1 :Z XXX disruption I
REQUEST_CONFIRM---X
REQUEST_CONFIRM---X
ENROLLED---X
Confirm requested, inferior detected problem, contradiction not reported (=:?)
superior inferior
I1 :Z XXX disruption I
Z :Y1 <-----------------------------ENROL/rsp-req <-- i1 :a1
Y1 :Y1 XXX disruption 0
Y1 :Z --> SUP_STATE/unknown-------------------------> a1 :z
Nothing happens (:)
superior inferior
ENROL/no-rsp-req <-- i1 :b1
INF_STATE/active/y <-- b1 :b1
CANCELLED <-- b1 :z
I1 :I1 XXX disruption 0
X---ENROL/no-rsp-req
I1 :Y1 <-----------------INF_STATE/active/y
Y1 :Y1 <--------------------------CANCELLED
Y1 :Z --> SUP_STATE/unknown-------------------------> z :z
Nothing happens (:)
superior inferior
I1 :Z XXX disruption I
ENROL/no-rsp-req <-- i1 :b1
decide to be prepared === b1 :e1
PREPARED <-- e1 :e1
Z :Z <-------------------ENROL/no-rsp-req
Z :Y1 <---------------------------PREPARED
decide to confirm autonomously === e1 :h1
Y1 :L2 <----------------------------CONFIRMED/auto <-- h1 :h1
L2 :L1 === record contradiction
L1 :Z --> CONTRADICTION-----------------------------> h1 :z
Superior never decided, inferior confirmed - contradiction reported (!:#)
superior inferior
I1 :Z XXX disruption I
ENROL/rsp-req <-- i1 :a1
detect problem === a1 :m2
HAZARD <-- m2 :m2
Z :Y1 <----------------------ENROL/rsp-req
Y1 :M0 <-----------------------------HAZARD
M0 :M3 === record contradiction
M3 :Z --> CONTRADICTION-----------------------------> m2 :z
Inferior detected problem, contradiction reported (!:?)
superior inferior
I1 :Z XXX disruption I
ENROL/rsp-req <-- i1 :a1
INF_STATE/active/y <-- a1 :a1
Z :Y1 <----------------------ENROL/rsp-req
Y1 :Y1 <-----------------INF_STATE/active/y
Y1 :Z --> SUP_STATE/unknown-------------------------> a1 :z
Nothing happens (:)
superior inferior
ENROL/no-rsp-req <-- i1 :b1
CANCELLED <-- b1 :z
I1 :B1 <-------------------ENROL/no-rsp-req
B1 :N1 --> REQUEST_CONFIRM---------------------------> z :y1
N1 :Z XXX disruption I
Z :Y1 <--------------------------CANCELLED
Y1 :Z <-------------------------INF_STATE/unknown <-- y1 :z
Superior requested confirm, inferior never decided (=:)
superior inferior
I1 :B1 <--------------------------ENROL/no-rsp-req <-- i1 :b1
B1 :Z XXX disruption I
Z :Y1 <------------------------INF_STATE/active/y <-- b1 :b1
decide to be prepared === b1 :e1
Y1 :Y1 <----------------------------------PREPARED <-- e1 :e1
Y1 :Z --> SUP_STATE/unknown
decide to cancel autonomously === e1 :j1
SUP_STATE/unknown------------------> j1 :z
superior never decided, inferior cancelled (:-)
superior inferior
ENROL/no-rsp-req <-- i1 :b1
decide to be prepared/cancel === b1 :e2
disruption 0 XXX e2 :e2
X---ENROL/no-rsp-req
I1 :Y1 <---------------------------PREPARED/cancel <-- e2 :e2
PREPARED/cancel <-- e2 :e2
decide to cancel autonomously === e2 :z1
Y1 :Y1 <--------------------PREPARED/cancel
Y1 :Z --> SUP_STATE/unknown-------------------------> z1 :z
superior never decided, inferior cancelled (:-)
superior inferior
ENROL/no-rsp-req <-- i1 :b1
disruption 0 XXX b1 :b1
X---ENROL/no-rsp-req
RESIGN/rsp-req <-- b1 :c1
RESIGN/no-rsp-req <-- c1 :z
I1 :Y1 <---------------------RESIGN/rsp-req
Y1 :Z <------------------RESIGN/no-rsp-req
Nothing happens (:)
superior inferior
ENROL/no-rsp-req <-- i1 :b1
RESIGN/rsp-req <-- b1 :c1
I1 :Z XXX disruption I
X---ENROL/no-rsp-req
RESIGN/rsp-req <-- c1 :c1
RESIGN/no-rsp-req <-- c1 :z
Z :Y1 <---------------------RESIGN/rsp-req
Y1 :Y1 <---------------------RESIGN/rsp-req
Y1 :Z <------------------RESIGN/no-rsp-req
Nothing happens (:)
superior inferior
I1 :Z XXX disruption I
Z :Y1 <-----------------------------ENROL/rsp-req <-- i1 :a1
Y1 :Z --> SUP_STATE/unknown-------------------------> a1 :z
Nothing happens (:)
superior inferior
ENROL/no-rsp-req <-- i1 :b1
decide to be prepared === b1 :e1
decide to confirm autonomously === e1 :h1
I1 :B1 <-------------------ENROL/no-rsp-req
B1 :D1 === decide to prepare
D1 :H1 <----------------------------CONFIRMED/auto <-- h1 :h1
H1 :F1 === decide to confirm
F1 :F1 --> CONFIRM-----------------------------------> h1 :h2
F1 :F1 --> CONFIRM-----------------------------------> h2 :h2
CONFIRMED/response <-- h2 :z
F1 :F1 --> CONFIRM
F1 :Z0 <-----------------CONFIRMED/response
CONFIRM----------------------------> z :y2
Z0 :Z0 XXX disruption 0
Z0 :Z0 <------------------------CONFIRMED/response <-- y2 :z
Both confirm (+:#)
superior inferior
ENROL/no-rsp-req <-- i1 :b1
decide to be prepared === b1 :e1
PREPARED <-- e1 :e1
I1 :B1 <-------------------ENROL/no-rsp-req
B1 :E1 <---------------------------PREPARED
E1 :F1 === decide to confirm
decide to confirm autonomously === e1 :h1
F1 :F1 --> CONFIRM-----------------------------------> h1 :h2
F1 :F1 --> CONFIRM
CONFIRMED/response <-- h2 :z
CONFIRM----------------------------> z :y2
F1 :Z0 <-----------------CONFIRMED/response
Z0 :Z0 <------------------------CONFIRMED/response <-- y2 :z
Both confirm (+:#)
superior inferior
ENROL/no-rsp-req <-- i1 :b1
decide to be prepared === b1 :e1
decide to confirm autonomously === e1 :h1
CONFIRMED/auto <-- h1 :h1
I1 :B1 <-------------------ENROL/no-rsp-req
B1 :H1 <---------------------CONFIRMED/auto
H1 :F1 === decide to confirm
F1 :F1 --> CONFIRM-----------------------------------> h1 :h2
F1 :F1 --> CONFIRM
CONFIRMED/response <-- h2 :z
CONFIRM----------------------------> z :y2
F1 :Z0 <-----------------CONFIRMED/response
CONFIRMED/response <-- y2 :z
Z0 :Z === remove confirm information
Z :Z <-----------------CONFIRMED/response
Both confirm (+:#)
superior inferior
I1 :Z XXX disruption I
ENROL/no-rsp-req <-- i1 :b1
CANCELLED <-- b1 :z
Z :Z <-------------------ENROL/no-rsp-req
Z :Z XXX disruption 0
X---CANCELLED
Nothing happens (:)
superior inferior
ENROL/no-rsp-req <-- i1 :b1
CANCELLED <-- b1 :z
I1 :Z XXX disruption I
X---ENROL/no-rsp-req
Z :Y1 <--------------------------CANCELLED
Y1 :Z --> SUP_STATE/unknown-------------------------> z :z
Nothing happens (:)
superior inferior
I1 :Z XXX disruption I
ENROL/no-rsp-req <-- i1 :b1
decide to be prepared === b1 :e1
Z :Z <-------------------ENROL/no-rsp-req
decide to confirm autonomously === e1 :h1
Z :L2 <----------------------------CONFIRMED/auto <-- h1 :h1
L2 :L1 === record contradiction
L1 :Z --> CONTRADICTION-----------------------------> h1 :z
Superior never decided, inferior confirmed - contradiction reported (!:#)
superior inferior
I1 :B1 <--------------------------ENROL/no-rsp-req <-- i1 :b1
B1 :N1 --> REQUEST_CONFIRM---------------------------> b1 :n1
decide to confirm autonomously === n1 :n2
N1 :Z XXX disruption I
Z :Z <------------------------CONFIRMED/response <-- n2 :z
Superior requested confirm, inferior confirmed (=:#)
superior inferior
I1 :Z XXX disruption I
Z :Z <--------------------------ENROL/no-rsp-req <-- i1 :b1
disruption I XXX b1 :z
Nothing happens (:)
superior inferior
I1 :Z XXX disruption I
Z :Y1 <-----------------------------ENROL/rsp-req <-- i1 :a1
Y1 :Z --> SUP_STATE/unknown-------------------------> a1 :z
Nothing happens (:)
superior inferior
ENROL/rsp-req <-- i1 :a1
I1 :Z XXX disruption I
X---ENROL/rsp-req
detect problem === a1 :m2
Z :M0 <------------------------------------HAZARD <-- m2 :m2
M0 :M3 === record contradiction
M3 :Z --> CONTRADICTION-----------------------------> m2 :z
Inferior detected problem, contradiction reported (!:?)
superior inferior
I1 :A1 <-----------------------------ENROL/rsp-req <-- i1 :a1
INF_STATE/active/y <-- a1 :a1
A1 :B1 --> ENROLLED
B1 :B1 --> SUP_STATE/active/y
ENROLLED---------------------------> a1 :b1
B1 :N1 --> REQUEST_CONFIRM
N1 :N1 <-----------------INF_STATE/active/y
SUP_STATE/active/y-----------------> b1 :b1
INF_STATE/active <-- b1 :b1
decide to be prepared === b1 :e1
REQUEST_CONFIRM--------------------> e1 :n0
N1 :Z XXX disruption I
Z :Z <-------------------INF_STATE/active
remove prepared information === n0 :n1
decide to cancel autonomously === n1 :n3
Z :Y1 <---------------------------------CANCELLED <-- n3 :z
Y1 :Z --> SUP_STATE/unknown-------------------------> z :z
Superior requested confirm, inferior cancelled (=:-)
superior inferior
ENROL/rsp-req <-- i1 :a1
INF_STATE/active/y <-- a1 :a1
I1 :Z XXX disruption I
X---ENROL/rsp-req
Z :Y1 <-----------------INF_STATE/active/y
Y1 :Z --> SUP_STATE/unknown-------------------------> a1 :z
Nothing happens (:)
superior inferior
ENROL/no-rsp-req <-- i1 :b1
CANCELLED <-- b1 :z
I1 :B1 <-------------------ENROL/no-rsp-req
B1 :N1 --> REQUEST_CONFIRM---------------------------> z :y1
N1 :Z <--------------------------CANCELLED
Z :Z <-------------------------INF_STATE/unknown <-- y1 :z
Superior requested confirm, inferior never decided (=:)
superior inferior
I1 :Z XXX disruption I
Z :Z <--------------------------ENROL/no-rsp-req <-- i1 :b1
decide to be prepared === b1 :e1
Z :Y1 <----------------------------------PREPARED <-- e1 :e1
Y1 :Z --> SUP_STATE/unknown-------------------------> e1 :y0
remove prepared information === y0 :z
Nothing happens (:)
superior inferior
ENROL/no-rsp-req <-- i1 :b1
decide to be prepared/cancel === b1 :e2
I1 :Z XXX disruption I
X---ENROL/no-rsp-req
Z :Y1 <---------------------------PREPARED/cancel <-- e2 :e2
decide to cancel autonomously === e2 :z1
Y1 :Z --> SUP_STATE/unknown-------------------------> z1 :z
superior never decided, inferior cancelled (:-)
superior inferior
ENROL/no-rsp-req <-- i1 :b1
I1 :Z XXX disruption I
X---ENROL/no-rsp-req
Z :Z <-------------------------RESIGN/no-rsp-req <-- b1 :z
Nothing happens (:)
superior inferior
ENROL/no-rsp-req <-- i1 :b1
RESIGN/rsp-req <-- b1 :c1
RESIGN/no-rsp-req <-- c1 :z
I1 :Z XXX disruption I
X---ENROL/no-rsp-req
Z :Y1 <---------------------RESIGN/rsp-req
Y1 :Z <------------------RESIGN/no-rsp-req
Nothing happens (:)
superior inferior
ENROL/rsp-req <-- i1 :a1
detect problem === a1 :m2
I1 :A1 <----------------------ENROL/rsp-req
disruption I XXX m2 :z
A1 :Z XXX disruption I
Superior nothing, unreported hazard (:?)
superior inferior
ENROL/rsp-req <-- i1 :a1
disruption 0 XXX a1 :a1
I1 :A1 <----------------------ENROL/rsp-req
disruption I XXX a1 :z
A1 :Z XXX disruption I
Nothing happens (:)
superior inferior
ENROL/rsp-req <-- i1 :a1
I1 :Z XXX disruption I
disruption I XXX a1 :z
X---ENROL/rsp-req
Nothing happens (:)
superior inferior
I1 :A1 <-----------------------------ENROL/rsp-req <-- i1 :a1
A1 :B1 --> ENROLLED
disruption 0 XXX a1 :a1
ENROLLED---X
B1 :G1 === decide to cancel
G1 :G2 --> CANCEL------------------------------------> a1 :g2
G2 :G2 --> CANCEL------------------------------------> g2 :g2
G2 :Z <---------------------------------CANCELLED <-- g2 :z
Superior cancels, inferior never decided (-:)
superior inferior
I1 :A1 <-----------------------------ENROL/rsp-req <-- i1 :a1
A1 :B1 --> ENROLLED----------------------------------> a1 :b1
B1 :Z <---------------------------------CANCELLED <-- b1 :z
Nothing happens (:)
superior inferior
I1 :A1 <-----------------------------ENROL/rsp-req <-- i1 :a1
A1 :B1 --> ENROLLED
B1 :D1 === decide to prepare
D1 :D1 XXX disruption 0
ENROLLED---X
D1 :D1 --> PREPARE-----------------------------------> a1 :d1
D1 :Z <---------------------------------CANCELLED <-- d1 :z
Nothing happens (:)
superior inferior
I1 :A1 <-----------------------------ENROL/rsp-req <-- i1 :a1
A1 :B1 --> ENROLLED
B1 :B1 XXX disruption 0
ENROLLED---X
B1 :N1 --> REQUEST_CONFIRM---------------------------> a1 :n1
N1 :N1 --> REQUEST_CONFIRM
detect and record problem === n1 :n4
N1 :Z <------------------------------------HAZARD <-- n4 :z
REQUEST_CONFIRM--------------------> z :y1
Z :Z <-------------------------INF_STATE/unknown <-- y1 :z
Superior requested confirm, inferior detects mix - contradiction NOT reported (=:!)
superior inferior
I1 :A1 <-----------------------------ENROL/rsp-req <-- i1 :a1
A1 :B1 --> ENROLLED
disruption 0 XXX a1 :a1
ENROLLED---X
B1 :B1 --> SUP_STATE/active/y------------------------> a1 :b1
CANCELLED <-- b1 :z
B1 :N1 --> REQUEST_CONFIRM---------------------------> z :y1
N1 :Z <--------------------------CANCELLED
Z :Z <-------------------------INF_STATE/unknown <-- y1 :z
Superior requested confirm, inferior never decided (=:)
superior inferior
I1 :Z XXX disruption I
Z :Y1 <-----------------------------ENROL/rsp-req <-- i1 :a1
Y1 :Z --> SUP_STATE/unknown-------------------------> a1 :z
Nothing happens (:)
superior inferior
I1 :A1 <-----------------------------ENROL/rsp-req <-- i1 :a1
INF_STATE/active/y <-- a1 :a1
disruption I XXX a1 :z
X---INF_STATE/active/y
A1 :Z XXX disruption I
Nothing happens (:)
superior inferior
ENROL/no-rsp-req <-- i1 :b1
decide to be prepared === b1 :e1
decide to confirm autonomously === e1 :h1
I1 :B1 <-------------------ENROL/no-rsp-req
B1 :N1 --> REQUEST_CONFIRM---------------------------> h1 :n2
N1 :Z <------------------------CONFIRMED/response <-- n2 :z
Superior requested confirm, inferior confirmed (=:#)
superior inferior
ENROL/no-rsp-req <-- i1 :b1
decide to be prepared/cancel === b1 :e2
decide to cancel autonomously === e2 :z1
I1 :Z XXX disruption I
X---ENROL/no-rsp-req
superior never decided, inferior cancelled (:-)
superior inferior
I1 :Z XXX disruption I
ENROL/no-rsp-req <-- i1 :b1
detect problem === b1 :m2
disruption I XXX m2 :z
X---ENROL/no-rsp-req
Superior nothing, unreported hazard (:?)
superior inferior
ENROL/no-rsp-req <-- i1 :b1
disruption 0 XXX b1 :b1
X---ENROL/no-rsp-req
I1 :Z <-------------------------RESIGN/no-rsp-req <-- b1 :z
Nothing happens (:)
superior inferior
I1 :Z XXX disruption I
Z :Z <--------------------------ENROL/no-rsp-req <-- i1 :b1
disruption I XXX b1 :z
Nothing happens (:)
superior inferior
I1 :B1 <--------------------------ENROL/no-rsp-req <-- i1 :b1
B1 :G1 === decide to cancel
G1 :G2 --> CANCEL------------------------------------> b1 :g2
G2 :Z <---------------------------------CANCELLED <-- g2 :z
Superior cancels, inferior never decided (-:)
superior inferior
I1 :B1 <--------------------------ENROL/no-rsp-req <-- i1 :b1
B1 :D1 === decide to prepare
D1 :D1 --> PREPARE-----------------------------------> b1 :d1
D1 :Z <-------------------------RESIGN/no-rsp-req <-- d1 :z
Nothing happens (:)
superior inferior
I1 :B1 <--------------------------ENROL/no-rsp-req <-- i1 :b1
B1 :N1 --> REQUEST_CONFIRM---------------------------> b1 :n1
disruption I XXX n1 :z
N1 :Z XXX disruption I
Superior requested confirm, inferior never decided (=:)
superior inferior
I1 :B1 <--------------------------ENROL/no-rsp-req <-- i1 :b1
B1 :B1 <------------------------INF_STATE/active/y <-- b1 :b1
B1 :B1 --> SUP_STATE/active--------------------------> b1 :b1
B1 :Z <---------------------------------CANCELLED <-- b1 :z
Nothing happens (:)
superior inferior
I1 :B1 <--------------------------ENROL/no-rsp-req <-- i1 :b1
B1 :B1 --> SUP_STATE/active/y------------------------> b1 :b1
B1 :Z <-------------------------RESIGN/no-rsp-req <-- b1 :z
Nothing happens (:)
superior inferior
I1 :Z XXX disruption I
Z :Z <--------------------------ENROL/no-rsp-req <-- i1 :b1
Z :Y1 <------------------------INF_STATE/active/y <-- b1 :b1
Y1 :Z --> SUP_STATE/unknown-------------------------> b1 :z
Nothing happens (:)
superior inferior
ENROL/no-rsp-req <-- i1 :b1
CANCELLED <-- b1 :z
I1 :Z XXX disruption I
X---ENROL/no-rsp-req
X---CANCELLED
Nothing happens (:)
superior inferior
I1 :B1 <--------------------------ENROL/no-rsp-req <-- i1 :b1
B1 :B1 --> SUP_STATE/active/y------------------------> b1 :b1
B1 :B1 <--------------------------INF_STATE/active <-- b1 :b1
B1 :Z <---------------------------------CANCELLED <-- b1 :z
Nothing happens (:)
superior inferior
ENROL/no-rsp-req <-- i1 :b1
INF_STATE/active/y <-- b1 :b1
RESIGN/no-rsp-req <-- b1 :z
I1 :Z XXX disruption I
X---ENROL/no-rsp-req
X---INF_STATE/active/y
X---RESIGN/no-rsp-req
Nothing happens (:)
superior inferior
ENROL/no-rsp-req <-- i1 :b1
RESIGN/no-rsp-req <-- b1 :z
I1 :Z XXX disruption I
X---ENROL/no-rsp-req
X---RESIGN/no-rsp-req
Nothing happens (:)
superior inferior
ENROL/no-rsp-req <-- i1 :b1
RESIGN/rsp-req <-- b1 :c1
RESIGN/no-rsp-req <-- c1 :z
I1 :Z XXX disruption I
X---ENROL/no-rsp-req
X---RESIGN/rsp-req
X---RESIGN/no-rsp-req
Nothing happens (:)
superior inferior
ENROL/no-rsp-req <-- i1 :b1
RESIGN/rsp-req <-- b1 :c1
disruption 0 XXX c1 :c1
X---RESIGN/rsp-req
X---ENROL/no-rsp-req
I1 :Z <-------------------------RESIGN/no-rsp-req <-- c1 :z
Nothing happens (:)
superior inferior
I1 :Z XXX disruption I
ENROL/no-rsp-req <-- i1 :b1
RESIGN/rsp-req <-- b1 :c1
Z :Z <-------------------ENROL/no-rsp-req
disruption I XXX c1 :z
X---RESIGN/rsp-req
Nothing happens (:)
superior inferior
I1 :B1 <--------------------------ENROL/no-rsp-req <-- i1 :b1
B1 :G1 === decide to cancel
G1 :G2 --> CANCEL
RESIGN/rsp-req <-- b1 :c1
CANCEL-----------------------------> c1 :z
G2 :Z <---------------------RESIGN/rsp-req
Superior cancels, inferior never decided (-:)
superior inferior
I1 :B1 <--------------------------ENROL/no-rsp-req <-- i1 :b1
RESIGN/rsp-req <-- b1 :c1
B1 :D1 === decide to prepare
D1 :D1 --> PREPARE-----------------------------------> c1 :c1
D1 :C1 <---------------------RESIGN/rsp-req
C1 :Z <-------------------------RESIGN/no-rsp-req <-- c1 :z
Nothing happens (:)
superior inferior
ENROL/no-rsp-req <-- i1 :b1
RESIGN/rsp-req <-- b1 :c1
I1 :B1 <-------------------ENROL/no-rsp-req
B1 :N1 --> REQUEST_CONFIRM---------------------------> c1 :c1
N1 :C1 <---------------------RESIGN/rsp-req
C1 :Z <-------------------------RESIGN/no-rsp-req <-- c1 :z
Superior requested confirm, inferior never decided (=:)
superior inferior
ENROL/no-rsp-req <-- i1 :b1
RESIGN/rsp-req <-- b1 :c1
I1 :B1 <-------------------ENROL/no-rsp-req
B1 :C1 <---------------------RESIGN/rsp-req
C1 :Z --> RESIGNED----------------------------------> c1 :z
Nothing happens (:)
superior inferior
I1 :B1 <--------------------------ENROL/no-rsp-req <-- i1 :b1
INF_STATE/active/y <-- b1 :b1
RESIGN/rsp-req <-- b1 :c1
B1 :B1 <-----------------INF_STATE/active/y
B1 :B1 --> SUP_STATE/active--------------------------> c1 :c1
B1 :C1 <---------------------RESIGN/rsp-req
C1 :Z <-------------------------RESIGN/no-rsp-req <-- c1 :z
Nothing happens (:)
superior inferior
ENROL/no-rsp-req <-- i1 :b1
RESIGN/rsp-req <-- b1 :c1
I1 :B1 <-------------------ENROL/no-rsp-req
B1 :B1 --> SUP_STATE/active/y
B1 :C1 <---------------------RESIGN/rsp-req
SUP_STATE/active/y-----------------> c1 :c1
C1 :Z <-------------------------RESIGN/no-rsp-req <-- c1 :z
Nothing happens (:)
superior inferior
ENROL/no-rsp-req <-- i1 :b1
disruption 0 XXX b1 :b1
X---ENROL/no-rsp-req
I1 :Y1 <----------------------------RESIGN/rsp-req <-- b1 :c1
Y1 :Z --> SUP_STATE/unknown-------------------------> c1 :z
Nothing happens (:)
superior inferior
ENROL/no-rsp-req <-- i1 :b1
RESIGN/rsp-req <-- b1 :c1
RESIGN/no-rsp-req <-- c1 :z
I1 :Z XXX disruption I
X---ENROL/no-rsp-req
X---RESIGN/rsp-req
X---RESIGN/no-rsp-req
Nothing happens (:)
superior inferior
ENROL/no-rsp-req <-- i1 :b1
RESIGN/rsp-req <-- b1 :c1
RESIGN/rsp-req <-- c1 :c1
I1 :Z XXX disruption I
X---ENROL/no-rsp-req
X---RESIGN/rsp-req
X---RESIGN/rsp-req
Z :Z <-------------------------RESIGN/no-rsp-req <-- c1 :z
Nothing happens (:)
superior inferior
I1 :B1 <--------------------------ENROL/no-rsp-req <-- i1 :b1
B1 :D1 === decide to prepare
D1 :D1 --> PREPARE-----------------------------------> b1 :d1
decide to be prepared === d1 :e1
decide to cancel autonomously === e1 :j1
D1 :G1 === decide to cancel
G1 :G2 --> CANCEL------------------------------------> j1 :j3
G2 :Z <---------------------------------CANCELLED <-- j3 :z
Both cancel (-:-)
superior inferior
I1 :B1 <--------------------------ENROL/no-rsp-req <-- i1 :b1
B1 :D1 === decide to prepare
D1 :D1 --> PREPARE-----------------------------------> b1 :d1
decide to be prepared/cancel === d1 :e2
D1 :G1 === decide to cancel
decide to cancel autonomously === e2 :z1
G1 :Z XXX disruption I
Both cancel (-:-)
superior inferior
I1 :B1 <--------------------------ENROL/no-rsp-req <-- i1 :b1
B1 :D1 === decide to prepare
D1 :D1 --> PREPARE-----------------------------------> b1 :d1
detect problem === d1 :m2
D1 :M0 <------------------------------------HAZARD <-- m2 :m2
M0 :M3 === record contradiction
M3 :Z --> CONTRADICTION-----------------------------> m2 :z
Inferior detected problem, contradiction reported (!:?)
superior inferior
I1 :A1 <-----------------------------ENROL/rsp-req <-- i1 :a1
A1 :B1 --> ENROLLED
B1 :D1 === decide to prepare
ENROLLED---------------------------> a1 :b1
D1 :D1 --> PREPARE-----------------------------------> b1 :d1
D1 :G1 === decide to cancel
disruption 0 XXX d1 :d1
G1 :G2 --> CANCEL
G2 :Z <----------------------------RESIGN/rsp-req <-- d1 :c1
CANCEL-----------------------------> c1 :z
Superior cancels, inferior never decided (-:)
superior inferior
I1 :I1 XXX disruption 0
I1 :B1 <--------------------------ENROL/no-rsp-req <-- i1 :b1
B1 :D1 === decide to prepare
D1 :D1 --> PREPARE-----------------------------------> b1 :d1
D1 :D1 --> PREPARE-----------------------------------> d1 :d1
D1 :G1 === decide to cancel
disruption I XXX d1 :z
G1 :G2 --> CANCEL------------------------------------> z :y1
disruption 0 XXX y1 :y1
disruption 0 XXX y1 :y1
G2 :Z <-------------------------INF_STATE/unknown <-- y1 :z
Superior cancels, inferior never decided (-:)
superior inferior
I1 :B1 <--------------------------ENROL/no-rsp-req <-- i1 :b1
B1 :D1 === decide to prepare
D1 :D1 --> PREPARE
D1 :G1 === decide to cancel
PREPARE----------------------------> b1 :d1
G1 :G2 --> CANCEL------------------------------------> d1 :g2
G2 :Z <---------------------------------CANCELLED <-- g2 :z
Superior cancels, inferior never decided (-:)
superior inferior
I1 :B1 <--------------------------ENROL/no-rsp-req <-- i1 :b1
B1 :D1 === decide to prepare
D1 :D1 --> PREPARE
D1 :D1 --> PREPARE
PREPARE----------------------------> b1 :d1
PREPARE----------------------------> d1 :d1
D1 :Z <-------------------------RESIGN/no-rsp-req <-- d1 :z
Nothing happens (:)
superior inferior
I1 :B1 <--------------------------ENROL/no-rsp-req <-- i1 :b1
B1 :D1 === decide to prepare
D1 :D1 --> PREPARE-----------------------------------> b1 :d1
D1 :Z <---------------------------------CANCELLED <-- d1 :z
Nothing happens (:)
superior inferior
I1 :A1 <-----------------------------ENROL/rsp-req <-- i1 :a1
A1 :B1 --> ENROLLED
B1 :B1 --> SUP_STATE/active/y
ENROLLED---------------------------> a1 :b1
SUP_STATE/active/y-----------------> b1 :b1
B1 :D1 === decide to prepare
D1 :D1 --> PREPARE-----------------------------------> b1 :d1
INF_STATE/active <-- d1 :d1
CANCELLED <-- d1 :z
D1 :D1 <-------------------INF_STATE/active
D1 :Z <--------------------------CANCELLED
Nothing happens (:)
superior inferior
I1 :B1 <--------------------------ENROL/no-rsp-req <-- i1 :b1
B1 :D1 === decide to prepare
D1 :D1 --> PREPARE-----------------------------------> b1 :d1
INF_STATE/active/y <-- d1 :d1
CANCELLED <-- d1 :z
D1 :D1 <-----------------INF_STATE/active/y
D1 :Z <--------------------------CANCELLED
Nothing happens (:)
superior inferior
I1 :B1 <--------------------------ENROL/no-rsp-req <-- i1 :b1
B1 :D1 === decide to prepare
D1 :D1 --> PREPARE-----------------------------------> b1 :d1
D1 :Z <-------------------------RESIGN/no-rsp-req <-- d1 :z
Nothing happens (:)
superior inferior
I1 :B1 <--------------------------ENROL/no-rsp-req <-- i1 :b1
B1 :D1 === decide to prepare
D1 :D1 --> PREPARE-----------------------------------> b1 :d1
D1 :C1 <----------------------------RESIGN/rsp-req <-- d1 :c1
C1 :Z <-------------------------RESIGN/no-rsp-req <-- c1 :z
Nothing happens (:)
superior inferior
ENROL/no-rsp-req <-- i1 :b1
decide to be prepared === b1 :e1
decide to cancel autonomously === e1 :j1
I1 :B1 <-------------------ENROL/no-rsp-req
B1 :N1 --> REQUEST_CONFIRM---------------------------> j1 :n3
N1 :Z <---------------------------------CANCELLED <-- n3 :z
Superior requested confirm, inferior cancelled (=:-)
superior inferior
ENROL/no-rsp-req <-- i1 :b1
decide to be prepared === b1 :e1
decide to confirm autonomously === e1 :h1
I1 :B1 <-------------------ENROL/no-rsp-req
B1 :N1 --> REQUEST_CONFIRM---------------------------> h1 :n2
N1 :Z <------------------------CONFIRMED/response <-- n2 :z
Superior requested confirm, inferior confirmed (=:#)
superior inferior
ENROL/no-rsp-req <-- i1 :b1
decide to be prepared === b1 :e1
I1 :B1 <-------------------ENROL/no-rsp-req
B1 :N1 --> REQUEST_CONFIRM
detect problem === e1 :m3
REQUEST_CONFIRM--------------------> m3 :n5
N1 :Z <------------------------------------HAZARD <-- n5 :z
Confirm requested, inferior detected problem, contradiction not reported (=:?)
superior inferior
ENROL/no-rsp-req <-- i1 :b1
decide to be prepared === b1 :e1
disruption 0 XXX e1 :e1
X---ENROL/no-rsp-req
decide to cancel autonomously === e1 :j1
I1 :Y1 <---------------------------------CANCELLED <-- j1 :j2
Y1 :Z --> SUP_STATE/unknown-------------------------> j2 :z
superior never decided, inferior cancelled (:-)
superior inferior
I1 :B1 <--------------------------ENROL/no-rsp-req <-- i1 :b1
decide to be prepared === b1 :e1
B1 :G1 === decide to cancel
G1 :G2 --> CANCEL------------------------------------> e1 :g0
remove prepared information === g0 :g2
G2 :Z <---------------------------------CANCELLED <-- g2 :z
Superior cancels, inferior never decided (-:)
superior inferior
I1 :B1 <--------------------------ENROL/no-rsp-req <-- i1 :b1
decide to be prepared === b1 :e1
B1 :E1 <----------------------------------PREPARED <-- e1 :e1
E1 :F1 === decide to confirm
F1 :F1 --> CONFIRM-----------------------------------> e1 :f0
apply ordered confirmation === f0 :f2
F1 :Z0 <------------------------CONFIRMED/response <-- f2 :z
Confirm ordered and applied (+:+)
superior inferior
ENROL/no-rsp-req <-- i1 :b1
decide to be prepared === b1 :e1
I1 :B1 <-------------------ENROL/no-rsp-req
B1 :D1 === decide to prepare
D1 :D1 --> PREPARE-----------------------------------> e1 :e1
decide to cancel autonomously === e1 :j1
D1 :G1 === decide to cancel
G1 :G2 --> CANCEL------------------------------------> j1 :j3
G2 :Z <---------------------------------CANCELLED <-- j3 :z
Both cancel (-:-)
superior inferior
I1 :B1 <--------------------------ENROL/no-rsp-req <-- i1 :b1
decide to be prepared === b1 :e1
B1 :N1 --> REQUEST_CONFIRM---------------------------> e1 :n0
remove prepared information === n0 :n1
decide to confirm autonomously === n1 :n2
N1 :Z <------------------------CONFIRMED/response <-- n2 :z
Superior requested confirm, inferior confirmed (=:#)
superior inferior
ENROL/no-rsp-req <-- i1 :b1
INF_STATE/active/y <-- b1 :b1
I1 :B1 <-------------------ENROL/no-rsp-req
B1 :B1 <-----------------INF_STATE/active/y
B1 :B1 --> SUP_STATE/active
decide to be prepared === b1 :e1
B1 :N1 --> REQUEST_CONFIRM
SUP_STATE/active-------------------> e1 :e1
decide to cancel autonomously === e1 :j1
REQUEST_CONFIRM--------------------> j1 :n3
N1 :Z <---------------------------------CANCELLED <-- n3 :z
Superior requested confirm, inferior cancelled (=:-)
superior inferior
ENROL/no-rsp-req <-- i1 :b1
decide to be prepared === b1 :e1
I1 :B1 <-------------------ENROL/no-rsp-req
B1 :B1 --> SUP_STATE/active/y------------------------> e1 :e1
decide to confirm autonomously === e1 :h1
B1 :N1 --> REQUEST_CONFIRM---------------------------> h1 :n2
N1 :Z <------------------------CONFIRMED/response <-- n2 :z
Superior requested confirm, inferior confirmed (=:#)
superior inferior
I1 :A1 <-----------------------------ENROL/rsp-req <-- i1 :a1
A1 :B1 --> ENROLLED
INF_STATE/active/y <-- a1 :a1
ENROLLED---------------------------> a1 :b1
decide to be prepared === b1 :e1
PREPARED <-- e1 :e1
B1 :B1 <-----------------INF_STATE/active/y
B1 :E1 <---------------------------PREPARED
E1 :E1 --> SUP_STATE/preparedreceived----------------> e1 :e1
decide to confirm autonomously === e1 :h1
E1 :N1 --> REQUEST_CONFIRM---------------------------> h1 :n2
N1 :Z <------------------------CONFIRMED/response <-- n2 :z
Superior requested confirm, inferior confirmed (=:#)
superior inferior
ENROL/no-rsp-req <-- i1 :b1
decide to be prepared === b1 :e1
PREPARED <-- e1 :e1
I1 :B1 <-------------------ENROL/no-rsp-req
B1 :E1 <---------------------------PREPARED
E1 :E1 --> SUP_STATE/preparedreceived/y--------------> e1 :e1
E1 :N1 --> REQUEST_CONFIRM
decide to confirm autonomously === e1 :h1
REQUEST_CONFIRM--------------------> h1 :n2
N1 :Z <------------------------CONFIRMED/response <-- n2 :z
Superior requested confirm, inferior confirmed (=:#)
superior inferior
I1 :Z XXX disruption I
Z :Z <--------------------------ENROL/no-rsp-req <-- i1 :b1
decide to be prepared === b1 :e1
Z :Y1 <----------------------------------PREPARED <-- e1 :e1
Y1 :Z --> SUP_STATE/unknown-------------------------> e1 :y0
remove prepared information === y0 :z
Nothing happens (:)
superior inferior
I1 :Z XXX disruption I
ENROL/no-rsp-req <-- i1 :b1
decide to be prepared === b1 :e1
PREPARED <-- e1 :e1
Z :Z <-------------------ENROL/no-rsp-req
Z :Y1 <---------------------------PREPARED
Y1 :Z --> SUP_STATE/unknown-------------------------> e1 :y0
remove prepared information === y0 :z
Nothing happens (:)
superior inferior
ENROL/no-rsp-req <-- i1 :b1
decide to be prepared/cancel === b1 :e2
decide to cancel autonomously === e2 :z1
I1 :Z XXX disruption I
X---ENROL/no-rsp-req
superior never decided, inferior cancelled (:-)
superior inferior
ENROL/no-rsp-req <-- i1 :b1
decide to be prepared/cancel === b1 :e2
detect problem === e2 :m3
I1 :B1 <-------------------ENROL/no-rsp-req
B1 :N1 --> REQUEST_CONFIRM---------------------------> m3 :n5
N1 :Z <------------------------------------HAZARD <-- n5 :z
Confirm requested, inferior detected problem, contradiction not reported (=:?)
superior inferior
I1 :Z XXX disruption I
ENROL/no-rsp-req <-- i1 :b1
decide to be prepared/cancel === b1 :e2
Z :Z <-------------------ENROL/no-rsp-req
disruption 0 XXX e2 :e2
decide to cancel autonomously === e2 :z1
superior never decided, inferior cancelled (:-)
superior inferior
ENROL/no-rsp-req <-- i1 :b1
decide to be prepared/cancel === b1 :e2
I1 :B1 <-------------------ENROL/no-rsp-req
B1 :G1 === decide to cancel
G1 :G2 --> CANCEL------------------------------------> e2 :g1
remove prepared information === g1 :g2
G2 :Z <---------------------------------CANCELLED <-- g2 :z
Superior cancels, inferior never decided (-:)
superior inferior
ENROL/no-rsp-req <-- i1 :b1
decide to be prepared/cancel === b1 :e2
PREPARED/cancel <-- e2 :e2
I1 :B1 <-------------------ENROL/no-rsp-req
B1 :E2 <--------------------PREPARED/cancel
E2 :F1 === decide to confirm
F1 :F1 --> CONFIRM-----------------------------------> e2 :f1
apply ordered confirmation === f1 :f2
F1 :Z0 <------------------------CONFIRMED/response <-- f2 :z
Confirm ordered and applied (+:+)
superior inferior
I1 :B1 <--------------------------ENROL/no-rsp-req <-- i1 :b1
decide to be prepared/cancel === b1 :e2
B1 :D1 === decide to prepare
D1 :D1 --> PREPARE-----------------------------------> e2 :e2
decide to cancel autonomously === e2 :z1
D1 :Z XXX disruption I
superior never decided, inferior cancelled (:-)
superior inferior
ENROL/no-rsp-req <-- i1 :b1
decide to be prepared/cancel === b1 :e2
I1 :B1 <-------------------ENROL/no-rsp-req
B1 :N1 --> REQUEST_CONFIRM---------------------------> e2 :n0
remove prepared information === n0 :n1
decide to cancel autonomously === n1 :n3
N1 :Z <---------------------------------CANCELLED <-- n3 :z
Superior requested confirm, inferior cancelled (=:-)
superior inferior
ENROL/no-rsp-req <-- i1 :b1
INF_STATE/active/y <-- b1 :b1
I1 :B1 <-------------------ENROL/no-rsp-req
decide to be prepared/cancel === b1 :e2
B1 :B1 <-----------------INF_STATE/active/y
B1 :B1 --> SUP_STATE/active--------------------------> e2 :e2
decide to cancel autonomously === e2 :z1
B1 :G1 === decide to cancel
G1 :Z XXX disruption I
Both cancel (-:-)
superior inferior
ENROL/no-rsp-req <-- i1 :b1
decide to be prepared/cancel === b1 :e2
I1 :B1 <-------------------ENROL/no-rsp-req
B1 :B1 --> SUP_STATE/active/y------------------------> e2 :e2
decide to cancel autonomously === e2 :z1
B1 :Z XXX disruption I
superior never decided, inferior cancelled (:-)
superior inferior
ENROL/no-rsp-req <-- i1 :b1
INF_STATE/active/y <-- b1 :b1
decide to be prepared/cancel === b1 :e2
I1 :B1 <-------------------ENROL/no-rsp-req
B1 :B1 <-----------------INF_STATE/active/y
B1 :E2 <---------------------------PREPARED/cancel <-- e2 :e2
E2 :E2 --> SUP_STATE/preparedreceived
E2 :Z === decide to cancel
SUP_STATE/preparedreceived---------> e2 :e2
decide to cancel autonomously === e2 :z1
Both cancel (-:-)
superior inferior
ENROL/no-rsp-req <-- i1 :b1
decide to be prepared/cancel === b1 :e2
I1 :B1 <-------------------ENROL/no-rsp-req
B1 :E2 <---------------------------PREPARED/cancel <-- e2 :e2
E2 :E2 --> SUP_STATE/preparedreceived/y--------------> e2 :e2
decide to cancel autonomously === e2 :z1
E2 :Z === decide to cancel
Both cancel (-:-)
superior inferior
ENROL/no-rsp-req <-- i1 :b1
decide to be prepared/cancel === b1 :e2
disruption 0 XXX e2 :e2
X---ENROL/no-rsp-req
I1 :Y1 <---------------------------PREPARED/cancel <-- e2 :e2
Y1 :Z --> SUP_STATE/unknown-------------------------> e2 :y0
remove prepared information === y0 :z
Nothing happens (:)
superior inferior
I1 :B1 <--------------------------ENROL/no-rsp-req <-- i1 :b1
decide to be prepared/cancel === b1 :e2
B1 :E2 <---------------------------PREPARED/cancel <-- e2 :e2
E2 :Z === decide to cancel
decide to cancel autonomously === e2 :z1
Both cancel (-:-)
superior inferior
ENROL/no-rsp-req <-- i1 :b1
decide to be prepared === b1 :e1
PREPARED <-- e1 :e1
I1 :B1 <-------------------ENROL/no-rsp-req
B1 :E1 <---------------------------PREPARED
E1 :F1 === decide to confirm
F1 :F1 --> CONFIRM-----------------------------------> e1 :f0
apply ordered confirmation === f0 :f2
F1 :Z0 <------------------------CONFIRMED/response <-- f2 :z
Confirm ordered and applied (+:+)
superior inferior
ENROL/no-rsp-req <-- i1 :b1
decide to be prepared === b1 :e1
I1 :B1 <-------------------ENROL/no-rsp-req
B1 :E1 <----------------------------------PREPARED <-- e1 :e1
E1 :F1 === decide to confirm
F1 :F1 --> CONFIRM-----------------------------------> e1 :f0
detect problem === f0 :m3
F1 :M1 <------------------------------------HAZARD <-- m3 :m3
detect and record problem === m3 :m1
M1 :M3 === record contradiction
M3 :Z --> CONTRADICTION-----------------------------> m1 :z
Superior confirms, inferior detects mix - contradiction reported (+!:!)
superior inferior
ENROL/no-rsp-req <-- i1 :b1
decide to be prepared === b1 :e1
PREPARED <-- e1 :e1
I1 :B1 <-------------------ENROL/no-rsp-req
B1 :E1 <---------------------------PREPARED
E1 :F1 === decide to confirm
F1 :F1 --> CONFIRM
PREPARED <-- e1 :e1
CONFIRM----------------------------> e1 :f0
F1 :F1 <---------------------------PREPARED
disruption 0 XXX f0 :f0
F1 :F1 --> CONFIRM-----------------------------------> f0 :f0
F1 :F1 --> CONFIRM-----------------------------------> f0 :f0
detect problem === f0 :m3
F1 :M1 <------------------------------------HAZARD <-- m3 :m3
M1 :M3 === record contradiction
M3 :Z --> CONTRADICTION-----------------------------> m3 :z
Superior confirms, inferior only detects mix - contradiction reported (+!:?)
superior inferior
ENROL/no-rsp-req <-- i1 :b1
decide to be prepared === b1 :e1
PREPARED <-- e1 :e1
I1 :B1 <-------------------ENROL/no-rsp-req
PREPARED <-- e1 :e1
B1 :E1 <---------------------------PREPARED
E1 :E1 <---------------------------PREPARED
E1 :E1 === decide to prepare
E1 :F1 === decide to confirm
PREPARED <-- e1 :e1
F1 :F1 --> CONFIRM
F1 :F1 <---------------------------PREPARED
CONFIRM----------------------------> e1 :f0
disruption I XXX f0 :e1
detect problem === e1 :m3
detect and record problem === m3 :m1
F1 :F1 --> CONFIRM-----------------------------------> m1 :m1
F1 :M1 <------------------------------------HAZARD <-- m1 :m1
M1 :M1 <------------------------------------HAZARD <-- m1 :m1
M1 :M3 === record contradiction
M3 :M3 <------------------------------------HAZARD <-- m1 :m1
M3 :Z --> CONTRADICTION-----------------------------> m1 :z
Superior confirms, inferior detects mix - contradiction reported (+!:!)
superior inferior
ENROL/no-rsp-req <-- i1 :b1
decide to be prepared === b1 :e1
PREPARED <-- e1 :e1
I1 :B1 <-------------------ENROL/no-rsp-req
B1 :E1 <---------------------------PREPARED
E1 :F1 === decide to confirm
F1 :F1 --> CONFIRM-----------------------------------> e1 :f0
F1 :F1 --> CONFIRM-----------------------------------> f0 :f0
apply ordered confirmation === f0 :f2
F1 :Z0 <------------------------CONFIRMED/response <-- f2 :z
Confirm ordered and applied (+:+)
superior inferior
ENROL/no-rsp-req <-- i1 :b1
decide to be prepared/cancel === b1 :e2
PREPARED/cancel <-- e2 :e2
I1 :B1 <-------------------ENROL/no-rsp-req
B1 :E2 <--------------------PREPARED/cancel
E2 :F1 === decide to confirm
F1 :F1 --> CONFIRM-----------------------------------> e2 :f1
apply ordered confirmation === f1 :f2
F1 :Z0 <------------------------CONFIRMED/response <-- f2 :z
Confirm ordered and applied (+:+)
superior inferior
I1 :B1 <--------------------------ENROL/no-rsp-req <-- i1 :b1
decide to be prepared/cancel === b1 :e2
B1 :E2 <---------------------------PREPARED/cancel <-- e2 :e2
E2 :F1 === decide to confirm
F1 :F1 --> CONFIRM-----------------------------------> e2 :f1
detect problem === f1 :m3
F1 :M1 <------------------------------------HAZARD <-- m3 :m3
M1 :M3 === record contradiction
M3 :Z --> CONTRADICTION-----------------------------> m3 :z
Superior confirms, inferior only detects mix - contradiction reported (+!:?)
superior inferior
I1 :B1 <--------------------------ENROL/no-rsp-req <-- i1 :b1
decide to be prepared/cancel === b1 :e2
B1 :D1 === decide to prepare
D1 :E2 <---------------------------PREPARED/cancel <-- e2 :e2
E2 :F1 === decide to confirm
F1 :F1 --> CONFIRM-----------------------------------> e2 :f1
F1 :F1 --> CONFIRM-----------------------------------> f1 :f1
F1 :F1 --> CONFIRM-----------------------------------> f1 :f1
disruption 0 XXX f1 :f1
detect problem === f1 :m3
detect and record problem === m3 :m1
F1 :M1 <------------------------------------HAZARD <-- m1 :m1
M1 :M3 === record contradiction
M3 :Z --> CONTRADICTION-----------------------------> m1 :z
Superior confirms, inferior detects mix - contradiction reported (+!:!)
superior inferior
ENROL/no-rsp-req <-- i1 :b1
decide to be prepared/cancel === b1 :e2
PREPARED/cancel <-- e2 :e2
I1 :B1 <-------------------ENROL/no-rsp-req
B1 :E2 <--------------------PREPARED/cancel
E2 :E2 === decide to prepare
E2 :F1 === decide to confirm
F1 :F1 --> CONFIRM-----------------------------------> e2 :f1
disruption I XXX f1 :e2
decide to cancel autonomously === e2 :z1
F1 :F1 --> CONFIRM
F1 :F1 --> CONFIRM
CONFIRM----------------------------> z1 :y3
CONFIRM----------------------------> y3 :y3
F1 :K0 <---------------------------------CANCELLED <-- y3 :z1
K0 :K1 === record contradiction
K1 :Z --> CONTRADICTION-----------------------------> z1 :z
Superior confirms, inferior cancelled - contradiction reported (+!:-)
superior inferior
ENROL/no-rsp-req <-- i1 :b1
decide to be prepared/cancel === b1 :e2
I1 :B1 <-------------------ENROL/no-rsp-req
B1 :E2 <---------------------------PREPARED/cancel <-- e2 :e2
E2 :F1 === decide to confirm
F1 :F1 --> CONFIRM-----------------------------------> e2 :f1
F1 :F1 --> CONFIRM-----------------------------------> f1 :f1
apply ordered confirmation === f1 :f2
F1 :Z0 <------------------------CONFIRMED/response <-- f2 :z
Confirm ordered and applied (+:+)
superior inferior
ENROL/no-rsp-req <-- i1 :b1
decide to be prepared/cancel === b1 :e2
PREPARED/cancel <-- e2 :e2
I1 :B1 <-------------------ENROL/no-rsp-req
B1 :E2 <--------------------PREPARED/cancel
E2 :F1 === decide to confirm
F1 :F1 --> CONFIRM-----------------------------------> e2 :f1
apply ordered confirmation === f1 :f2
disruption 0 XXX f2 :f2
F1 :F1 --> CONFIRM-----------------------------------> f2 :f2
F1 :Z0 <------------------------CONFIRMED/response <-- f2 :z
Confirm ordered and applied (+:+)
superior inferior
I1 :B1 <--------------------------ENROL/no-rsp-req <-- i1 :b1
B1 :D1 === decide to prepare
decide to be prepared/cancel === b1 :e2
D1 :E2 <---------------------------PREPARED/cancel <-- e2 :e2
E2 :F1 === decide to confirm
F1 :F1 --> CONFIRM-----------------------------------> e2 :f1
apply ordered confirmation === f1 :f2
disruption I XXX f2 :z
F1 :F1 --> CONFIRM-----------------------------------> z :y2
F1 :Z0 <------------------------CONFIRMED/response <-- y2 :z
Confirm ordered and applied (+:+)
superior inferior
ENROL/no-rsp-req <-- i1 :b1
decide to be prepared/cancel === b1 :e2
I1 :B1 <-------------------ENROL/no-rsp-req
B1 :E2 <---------------------------PREPARED/cancel <-- e2 :e2
E2 :F1 === decide to confirm
F1 :F1 --> CONFIRM-----------------------------------> e2 :f1
apply ordered confirmation === f1 :f2
F1 :F1 --> CONFIRM-----------------------------------> f2 :f2
F1 :Z0 <------------------------CONFIRMED/response <-- f2 :z
Confirm ordered and applied (+:+)
superior inferior
ENROL/no-rsp-req <-- i1 :b1
decide to be prepared/cancel === b1 :e2
PREPARED/cancel <-- e2 :e2
I1 :B1 <-------------------ENROL/no-rsp-req
B1 :E2 <--------------------PREPARED/cancel
E2 :F1 === decide to confirm
F1 :F1 --> CONFIRM-----------------------------------> e2 :f1
apply ordered confirmation === f1 :f2
F1 :Z0 <------------------------CONFIRMED/response <-- f2 :z
Confirm ordered and applied (+:+)
superior inferior
I1 :B1 <--------------------------ENROL/no-rsp-req <-- i1 :b1
decide to be prepared === b1 :e1
B1 :G1 === decide to cancel
G1 :G2 --> CANCEL------------------------------------> e1 :g0
detect problem === g0 :m3
G2 :M2 <------------------------------------HAZARD <-- m3 :m3
M2 :M3 === record contradiction
M3 :Z --> CONTRADICTION-----------------------------> m3 :z
Superior cancels, Inferior detected problem, contradiction reported (-!:?)
superior inferior
I1 :B1 <--------------------------ENROL/no-rsp-req <-- i1 :b1
B1 :G1 === decide to cancel
G1 :G2 --> CANCEL
decide to be prepared === b1 :e1
CANCEL-----------------------------> e1 :g0
disruption 0 XXX g0 :g0
remove prepared information === g0 :g2
G2 :Z <---------------------------------CANCELLED <-- g2 :z
Superior cancels, inferior never decided (-:)
superior inferior
I1 :B1 <--------------------------ENROL/no-rsp-req <-- i1 :b1
B1 :G1 === decide to cancel
decide to be prepared === b1 :e1
G1 :G2 --> CANCEL------------------------------------> e1 :g0
disruption I XXX g0 :e1
decide to cancel autonomously === e1 :j1
G2 :G2 --> CANCEL
G2 :Z <---------------------------------CANCELLED <-- j1 :j2
Z :Y1 <---------------------------------CANCELLED <-- j2 :j2
CANCEL-----------------------------> j2 :z
Y1 :Z --> SUP_STATE/unknown-------------------------> z :z
Both cancel (-:-)
superior inferior
ENROL/no-rsp-req <-- i1 :b1
decide to be prepared === b1 :e1
I1 :B1 <-------------------ENROL/no-rsp-req
B1 :G1 === decide to cancel
G1 :G2 --> CANCEL
G2 :G2 --> CANCEL
CANCEL-----------------------------> e1 :g0
CANCEL-----------------------------> g0 :g0
remove prepared information === g0 :g2
G2 :Z <---------------------------------CANCELLED <-- g2 :z
Superior cancels, inferior never decided (-:)
superior inferior
ENROL/no-rsp-req <-- i1 :b1
decide to be prepared === b1 :e1
I1 :B1 <-------------------ENROL/no-rsp-req
B1 :G1 === decide to cancel
G1 :G2 --> CANCEL------------------------------------> e1 :g0
remove prepared information === g0 :g2
G2 :Z <---------------------------------CANCELLED <-- g2 :z
Superior cancels, inferior never decided (-:)
superior inferior
I1 :B1 <--------------------------ENROL/no-rsp-req <-- i1 :b1
decide to be prepared/cancel === b1 :e2
B1 :G1 === decide to cancel
G1 :G2 --> CANCEL------------------------------------> e2 :g1
detect problem === g1 :m3
G2 :M2 <------------------------------------HAZARD <-- m3 :m3
M2 :M3 === record contradiction
M3 :Z --> CONTRADICTION-----------------------------> m3 :z
Superior cancels, Inferior detected problem, contradiction reported (-!:?)
superior inferior
ENROL/no-rsp-req <-- i1 :b1
decide to be prepared/cancel === b1 :e2
I1 :B1 <-------------------ENROL/no-rsp-req
B1 :G1 === decide to cancel
G1 :G2 --> CANCEL------------------------------------> e2 :g1
disruption 0 XXX g1 :g1
remove prepared information === g1 :g2
disruption 0 XXX g2 :g2
G2 :Z <---------------------------------CANCELLED <-- g2 :z
Superior cancels, inferior never decided (-:)
superior inferior
ENROL/no-rsp-req <-- i1 :b1
decide to be prepared/cancel === b1 :e2
I1 :B1 <-------------------ENROL/no-rsp-req
B1 :G1 === decide to cancel
G1 :G2 --> CANCEL------------------------------------> e2 :g1
G2 :G2 --> CANCEL------------------------------------> g1 :g1
G2 :Z XXX disruption I
disruption I XXX g1 :e2
decide to cancel autonomously === e2 :z1
Both cancel (-:-)
superior inferior
I1 :B1 <--------------------------ENROL/no-rsp-req <-- i1 :b1
B1 :G1 === decide to cancel
decide to be prepared/cancel === b1 :e2
G1 :G2 --> CANCEL------------------------------------> e2 :g1
G2 :G2 --> CANCEL------------------------------------> g1 :g1
remove prepared information === g1 :g2
G2 :Z <---------------------------------CANCELLED <-- g2 :z
Superior cancels, inferior never decided (-:)
superior inferior
ENROL/no-rsp-req <-- i1 :b1
decide to be prepared/cancel === b1 :e2
I1 :B1 <-------------------ENROL/no-rsp-req
B1 :G1 === decide to cancel
G1 :G2 --> CANCEL------------------------------------> e2 :g1
remove prepared information === g1 :g2
G2 :Z <---------------------------------CANCELLED <-- g2 :z
Superior cancels, inferior never decided (-:)
superior inferior
I1 :B1 <--------------------------ENROL/no-rsp-req <-- i1 :b1
B1 :G1 === decide to cancel
G1 :G2 --> CANCEL------------------------------------> b1 :g2
disruption 0 XXX g2 :g2
G2 :Z <---------------------------------CANCELLED <-- g2 :z
Superior cancels, inferior never decided (-:)
superior inferior
I1 :B1 <--------------------------ENROL/no-rsp-req <-- i1 :b1
B1 :G1 === decide to cancel
G1 :G2 --> CANCEL------------------------------------> b1 :g2
disruption I XXX g2 :z
G2 :Z XXX disruption I
Superior cancels, inferior never decided (-:)
superior inferior
I1 :B1 <--------------------------ENROL/no-rsp-req <-- i1 :b1
B1 :G1 === decide to cancel
G1 :G2 --> CANCEL------------------------------------> b1 :g2
G2 :G2 --> CANCEL------------------------------------> g2 :g2
G2 :Z <---------------------------------CANCELLED <-- g2 :z
Superior cancels, inferior never decided (-:)
superior inferior
I1 :B1 <--------------------------ENROL/no-rsp-req <-- i1 :b1
B1 :G1 === decide to cancel
G1 :G2 --> CANCEL------------------------------------> b1 :g2
G2 :Z <---------------------------------CANCELLED <-- g2 :z
Superior cancels, inferior never decided (-:)
superior inferior
ENROL/no-rsp-req <-- i1 :b1
decide to be prepared === b1 :e1
PREPARED <-- e1 :e1
decide to confirm autonomously === e1 :h1
disruption 0 XXX h1 :h1
X---PREPARED
X---ENROL/no-rsp-req
I1 :L2 <----------------------------CONFIRMED/auto <-- h1 :h1
L2 :L1 === record contradiction
L1 :Z --> CONTRADICTION-----------------------------> h1 :z
Superior never decided, inferior confirmed - contradiction reported (!:#)
superior inferior
ENROL/no-rsp-req <-- i1 :b1
decide to be prepared === b1 :e1
I1 :B1 <-------------------ENROL/no-rsp-req
B1 :G1 === decide to cancel
G1 :G2 --> CANCEL
decide to confirm autonomously === e1 :h1
G2 :L0 <----------------------------CONFIRMED/auto <-- h1 :h1
L0 :L1 === record contradiction
L1 :Z --> CONTRADICTION
CANCEL-----------------------------> h1 :l1
CONTRADICTION----------------------> l1 :z
Superior cancels, inferior confirmed - contradiction reported (-!:#)
superior inferior
I1 :B1 <--------------------------ENROL/no-rsp-req <-- i1 :b1
decide to be prepared === b1 :e1
B1 :E1 <----------------------------------PREPARED <-- e1 :e1
decide to confirm autonomously === e1 :h1
E1 :F1 === decide to confirm
F1 :F1 --> CONFIRM-----------------------------------> h1 :h2
F1 :Z0 <------------------------CONFIRMED/response <-- h2 :z
Both confirm (+:#)
superior inferior
ENROL/no-rsp-req <-- i1 :b1
decide to be prepared === b1 :e1
decide to confirm autonomously === e1 :h1
I1 :B1 <-------------------ENROL/no-rsp-req
B1 :G1 === decide to cancel
G1 :L0 <----------------------------CONFIRMED/auto <-- h1 :h1
L0 :L1 === record contradiction
L1 :Z --> CONTRADICTION-----------------------------> h1 :z
Superior cancels, inferior confirmed - contradiction reported (-!:#)
superior inferior
ENROL/no-rsp-req <-- i1 :b1
decide to be prepared === b1 :e1
I1 :B1 <-------------------ENROL/no-rsp-req
B1 :E1 <----------------------------------PREPARED <-- e1 :e1
E1 :E1 --> PREPARE
E1 :N1 --> REQUEST_CONFIRM
decide to confirm autonomously === e1 :h1
PREPARE----------------------------> h1 :h1
REQUEST_CONFIRM--------------------> h1 :n2
N1 :Z <------------------------CONFIRMED/response <-- n2 :z
Superior requested confirm, inferior confirmed (=:#)
superior inferior
ENROL/no-rsp-req <-- i1 :b1
decide to be prepared === b1 :e1
I1 :B1 <-------------------ENROL/no-rsp-req
B1 :N1 --> REQUEST_CONFIRM
decide to confirm autonomously === e1 :h1
REQUEST_CONFIRM--------------------> h1 :n2
N1 :Z <------------------------CONFIRMED/response <-- n2 :z
Superior requested confirm, inferior confirmed (=:#)
superior inferior
ENROL/no-rsp-req <-- i1 :b1
INF_STATE/active/y <-- b1 :b1
I1 :B1 <-------------------ENROL/no-rsp-req
decide to be prepared === b1 :e1
B1 :B1 <-----------------INF_STATE/active/y
B1 :B1 --> SUP_STATE/active
decide to confirm autonomously === e1 :h1
SUP_STATE/active-------------------> h1 :h1
B1 :N1 --> REQUEST_CONFIRM---------------------------> h1 :n2
N1 :Z <------------------------CONFIRMED/response <-- n2 :z
Superior requested confirm, inferior confirmed (=:#)
superior inferior
ENROL/no-rsp-req <-- i1 :b1
decide to be prepared === b1 :e1
decide to confirm autonomously === e1 :h1
I1 :B1 <-------------------ENROL/no-rsp-req
B1 :B1 --> SUP_STATE/active/y------------------------> h1 :h1
B1 :N1 --> REQUEST_CONFIRM---------------------------> h1 :n2
N1 :Z <------------------------CONFIRMED/response <-- n2 :z
Superior requested confirm, inferior confirmed (=:#)
superior inferior
I1 :B1 <--------------------------ENROL/no-rsp-req <-- i1 :b1
INF_STATE/active/y <-- b1 :b1
decide to be prepared === b1 :e1
B1 :B1 <-----------------INF_STATE/active/y
PREPARED <-- e1 :e1
decide to confirm autonomously === e1 :h1
B1 :E1 <---------------------------PREPARED
E1 :E1 --> SUP_STATE/preparedreceived
E1 :E1 === decide to prepare
SUP_STATE/preparedreceived---------> h1 :h1
E1 :N1 --> REQUEST_CONFIRM---------------------------> h1 :n2
N1 :Z <------------------------CONFIRMED/response <-- n2 :z
Superior requested confirm, inferior confirmed (=:#)
superior inferior
ENROL/no-rsp-req <-- i1 :b1
decide to be prepared === b1 :e1
PREPARED <-- e1 :e1
I1 :B1 <-------------------ENROL/no-rsp-req
B1 :E1 <---------------------------PREPARED
decide to confirm autonomously === e1 :h1
E1 :E1 --> SUP_STATE/preparedreceived/y
E1 :N1 --> REQUEST_CONFIRM
SUP_STATE/preparedreceived/y-------> h1 :h1
REQUEST_CONFIRM--------------------> h1 :n2
N1 :Z <------------------------CONFIRMED/response <-- n2 :z
Superior requested confirm, inferior confirmed (=:#)
superior inferior
I1 :Z XXX disruption I
Z :Z <--------------------------ENROL/no-rsp-req <-- i1 :b1
decide to be prepared === b1 :e1
PREPARED <-- e1 :e1
decide to confirm autonomously === e1 :h1
Z :Y1 <---------------------------PREPARED
Y1 :Z --> SUP_STATE/unknown-------------------------> h1 :l1
Z :L2 <----------------------------CONFIRMED/auto <-- l1 :l1
L2 :L1 === record contradiction
L1 :Z --> CONTRADICTION-----------------------------> l1 :z
Superior never decided, inferior confirmed - contradiction reported (!:#)
superior inferior
ENROL/no-rsp-req <-- i1 :b1
decide to be prepared === b1 :e1
decide to confirm autonomously === e1 :h1
I1 :B1 <-------------------ENROL/no-rsp-req
B1 :G1 === decide to cancel
G1 :L0 <----------------------------CONFIRMED/auto <-- h1 :h1
L0 :L1 === record contradiction
L1 :Z --> CONTRADICTION-----------------------------> h1 :z
Superior cancels, inferior confirmed - contradiction reported (-!:#)
superior inferior
ENROL/no-rsp-req <-- i1 :b1
decide to be prepared === b1 :e1
decide to confirm autonomously === e1 :h1
CONFIRMED/auto <-- h1 :h1
I1 :B1 <-------------------ENROL/no-rsp-req
B1 :H1 <---------------------CONFIRMED/auto
H1 :F1 === decide to confirm
F1 :F1 --> CONFIRM-----------------------------------> h1 :h2
disruption 0 XXX h2 :h2
F1 :Z0 <------------------------CONFIRMED/response <-- h2 :z
Both confirm (+:#)
superior inferior
I1 :B1 <--------------------------ENROL/no-rsp-req <-- i1 :b1
decide to be prepared === b1 :e1
decide to confirm autonomously === e1 :h1
B1 :H1 <----------------------------CONFIRMED/auto <-- h1 :h1
H1 :H1 <----------------------------CONFIRMED/auto <-- h1 :h1
H1 :F1 === decide to confirm
F1 :F1 --> CONFIRM-----------------------------------> h1 :h2
disruption I XXX h2 :h1
F1 :F1 --> CONFIRM-----------------------------------> h1 :h2
F1 :Z0 <------------------------CONFIRMED/response <-- h2 :z
Both confirm (+:#)
superior inferior
I1 :B1 <--------------------------ENROL/no-rsp-req <-- i1 :b1
decide to be prepared === b1 :e1
B1 :E1 <----------------------------------PREPARED <-- e1 :e1
E1 :F1 === decide to confirm
decide to confirm autonomously === e1 :h1
F1 :F1 --> CONFIRM-----------------------------------> h1 :h2
F1 :F1 --> CONFIRM-----------------------------------> h2 :h2
F1 :Z0 <------------------------CONFIRMED/response <-- h2 :z
Both confirm (+:#)
superior inferior
ENROL/no-rsp-req <-- i1 :b1
decide to be prepared === b1 :e1
decide to confirm autonomously === e1 :h1
CONFIRMED/auto <-- h1 :h1
I1 :B1 <-------------------ENROL/no-rsp-req
B1 :H1 <---------------------CONFIRMED/auto
H1 :F1 === decide to confirm
F1 :F1 --> CONFIRM-----------------------------------> h1 :h2
F1 :Z0 <------------------------CONFIRMED/response <-- h2 :z
Both confirm (+:#)
superior inferior
disruption 0 XXX i1 :i1
ENROL/no-rsp-req <-- i1 :b1
RESIGN/no-rsp-req <-- b1 :z
I1 :B1 <-------------------ENROL/no-rsp-req
B1 :Z <------------------RESIGN/no-rsp-req
Nothing happens (:)
superior inferior
ENROL/no-rsp-req <-- i1 :b1
CANCELLED <-- b1 :z
I1 :Z XXX disruption I
X---ENROL/no-rsp-req
X---CANCELLED
Nothing happens (:)
superior inferior
ENROL/rsp-req <-- i1 :a1
I1 :Z XXX disruption I
disruption I XXX a1 :z
X---ENROL/rsp-req
Nothing happens (:)
superior inferior
ENROL/no-rsp-req <-- i1 :b1
decide to be prepared === b1 :e1
decide to cancel autonomously === e1 :j1
disruption 0 XXX j1 :j1
X---ENROL/no-rsp-req
I1 :Y1 <---------------------------------CANCELLED <-- j1 :j2
Y1 :Z --> SUP_STATE/unknown-------------------------> j2 :z
superior never decided, inferior cancelled (:-)
superior inferior
ENROL/no-rsp-req <-- i1 :b1
decide to be prepared === b1 :e1
decide to cancel autonomously === e1 :j1
disruption I XXX j1 :j2
X---ENROL/no-rsp-req
I1 :Y1 <---------------------------------CANCELLED <-- j2 :j2
Y1 :Z --> SUP_STATE/unknown-------------------------> j2 :z
superior never decided, inferior cancelled (:-)
superior inferior
ENROL/no-rsp-req <-- i1 :b1
decide to be prepared === b1 :e1
decide to cancel autonomously === e1 :j1
I1 :B1 <-------------------ENROL/no-rsp-req
B1 :G1 === decide to cancel
G1 :G2 --> CANCEL------------------------------------> j1 :j3
G2 :Z <---------------------------------CANCELLED <-- j3 :z
Both cancel (-:-)
superior inferior
I1 :B1 <--------------------------ENROL/no-rsp-req <-- i1 :b1
decide to be prepared === b1 :e1
B1 :E1 <----------------------------------PREPARED <-- e1 :e1
E1 :F1 === decide to confirm
decide to cancel autonomously === e1 :j1
F1 :F1 --> CONFIRM-----------------------------------> j1 :k1
F1 :K0 <---------------------------------CANCELLED <-- k1 :k1
K0 :K1 === record contradiction
K1 :Z --> CONTRADICTION-----------------------------> k1 :z
Superior confirms, inferior cancelled - contradiction reported (+!:-)
superior inferior
I1 :B1 <--------------------------ENROL/no-rsp-req <-- i1 :b1
B1 :D1 === decide to prepare
decide to be prepared === b1 :e1
decide to cancel autonomously === e1 :j1
D1 :D1 --> PREPARE-----------------------------------> j1 :j1
CANCELLED <-- j1 :j2
D1 :G1 === decide to cancel
G1 :J2 <--------------------------CANCELLED
J2 :Z --> CANCEL------------------------------------> j2 :z
Both cancel (-:-)
superior inferior
ENROL/no-rsp-req <-- i1 :b1
decide to be prepared === b1 :e1
decide to cancel autonomously === e1 :j1
I1 :B1 <-------------------ENROL/no-rsp-req
B1 :N1 --> REQUEST_CONFIRM---------------------------> j1 :n3
N1 :Z <---------------------------------CANCELLED <-- n3 :z
Superior requested confirm, inferior cancelled (=:-)
superior inferior
ENROL/no-rsp-req <-- i1 :b1
INF_STATE/active/y <-- b1 :b1
I1 :B1 <-------------------ENROL/no-rsp-req
decide to be prepared === b1 :e1
B1 :B1 <-----------------INF_STATE/active/y
decide to cancel autonomously === e1 :j1
B1 :B1 --> SUP_STATE/active--------------------------> j1 :j1
B1 :N1 --> REQUEST_CONFIRM---------------------------> j1 :n3
N1 :Z <---------------------------------CANCELLED <-- n3 :z
Superior requested confirm, inferior cancelled (=:-)
superior inferior
ENROL/no-rsp-req <-- i1 :b1
decide to be prepared === b1 :e1
I1 :B1 <-------------------ENROL/no-rsp-req
decide to cancel autonomously === e1 :j1
B1 :B1 --> SUP_STATE/active/y
B1 :N1 --> REQUEST_CONFIRM
SUP_STATE/active/y-----------------> j1 :j1
REQUEST_CONFIRM--------------------> j1 :n3
N1 :Z <---------------------------------CANCELLED <-- n3 :z
Superior requested confirm, inferior cancelled (=:-)
superior inferior
ENROL/no-rsp-req <-- i1 :b1
INF_STATE/active/y <-- b1 :b1
I1 :B1 <-------------------ENROL/no-rsp-req
B1 :B1 <-----------------INF_STATE/active/y
decide to be prepared === b1 :e1
B1 :E1 <----------------------------------PREPARED <-- e1 :e1
decide to cancel autonomously === e1 :j1
E1 :E1 --> SUP_STATE/preparedreceived
E1 :G1 === decide to cancel
SUP_STATE/preparedreceived---------> j1 :j1
G1 :J2 <---------------------------------CANCELLED <-- j1 :j2
J2 :Z --> CANCEL------------------------------------> j2 :z
Both cancel (-:-)
superior inferior
ENROL/no-rsp-req <-- i1 :b1
decide to be prepared === b1 :e1
PREPARED <-- e1 :e1
I1 :B1 <-------------------ENROL/no-rsp-req
B1 :E1 <---------------------------PREPARED
decide to cancel autonomously === e1 :j1
E1 :E1 --> SUP_STATE/preparedreceived/y
E1 :N1 --> REQUEST_CONFIRM
SUP_STATE/preparedreceived/y-------> j1 :j1
REQUEST_CONFIRM--------------------> j1 :n3
N1 :Z <---------------------------------CANCELLED <-- n3 :z
Superior requested confirm, inferior cancelled (=:-)
superior inferior
I1 :Z XXX disruption I
Z :Z <--------------------------ENROL/no-rsp-req <-- i1 :b1
Z :Y1 <------------------------INF_STATE/active/y <-- b1 :b1
decide to be prepared === b1 :e1
decide to cancel autonomously === e1 :j1
Y1 :Z --> SUP_STATE/unknown-------------------------> j1 :z
superior never decided, inferior cancelled (:-)
superior inferior
ENROL/no-rsp-req <-- i1 :b1
decide to be prepared === b1 :e1
disruption 0 XXX e1 :e1
X---ENROL/no-rsp-req
decide to cancel autonomously === e1 :j1
I1 :Y1 <---------------------------------CANCELLED <-- j1 :j2
Y1 :Z --> SUP_STATE/unknown-------------------------> j2 :z
superior never decided, inferior cancelled (:-)
superior inferior
ENROL/no-rsp-req <-- i1 :b1
decide to be prepared === b1 :e1
I1 :B1 <-------------------ENROL/no-rsp-req
B1 :G1 === decide to cancel
decide to cancel autonomously === e1 :j1
G1 :J2 <---------------------------------CANCELLED <-- j1 :j2
disruption 0 XXX j2 :j2
J2 :Z --> CANCEL------------------------------------> j2 :z
Both cancel (-:-)
superior inferior
ENROL/no-rsp-req <-- i1 :b1
decide to be prepared === b1 :e1
decide to cancel autonomously === e1 :j1
I1 :B1 <-------------------ENROL/no-rsp-req
CANCELLED <-- j1 :j2
B1 :G1 === decide to cancel
G1 :G2 --> CANCEL
G2 :Z <--------------------------CANCELLED
CANCEL-----------------------------> j2 :z
Both cancel (-:-)
superior inferior
ENROL/no-rsp-req <-- i1 :b1
decide to be prepared === b1 :e1
PREPARED <-- e1 :e1
I1 :B1 <-------------------ENROL/no-rsp-req
B1 :E1 <---------------------------PREPARED
decide to cancel autonomously === e1 :j1
E1 :F1 === decide to confirm
F1 :F1 --> CONFIRM
F1 :K0 <---------------------------------CANCELLED <-- j1 :j2
CONFIRM----------------------------> j2 :k1
K0 :K1 === record contradiction
K1 :Z --> CONTRADICTION-----------------------------> k1 :z
Superior confirms, inferior cancelled - contradiction reported (+!:-)
superior inferior
ENROL/no-rsp-req <-- i1 :b1
decide to be prepared === b1 :e1
PREPARED <-- e1 :e1
I1 :B1 <-------------------ENROL/no-rsp-req
B1 :E1 <---------------------------PREPARED
E1 :F1 === decide to confirm
decide to cancel autonomously === e1 :j1
F1 :K0 <---------------------------------CANCELLED <-- j1 :j2
K0 :K1 === record contradiction
K1 :Z --> CONTRADICTION-----------------------------> j2 :z
Superior confirms, inferior cancelled - contradiction reported (+!:-)
superior inferior
I1 :B1 <--------------------------ENROL/no-rsp-req <-- i1 :b1
decide to be prepared === b1 :e1
decide to cancel autonomously === e1 :j1
B1 :D1 === decide to prepare
CANCELLED <-- j1 :j2
D1 :D1 --> PREPARE
D1 :G1 === decide to cancel
G1 :J2 <--------------------------CANCELLED
PREPARE----------------------------> j2 :j2
J2 :Z --> CANCEL------------------------------------> j2 :z
Both cancel (-:-)
superior inferior
ENROL/no-rsp-req <-- i1 :b1
decide to be prepared === b1 :e1
decide to cancel autonomously === e1 :j1
disruption I XXX j1 :j2
I1 :B1 <-------------------ENROL/no-rsp-req
B1 :N1 --> REQUEST_CONFIRM---------------------------> j2 :n3
N1 :Z <---------------------------------CANCELLED <-- n3 :z
Superior requested confirm, inferior cancelled (=:-)
superior inferior
ENROL/no-rsp-req <-- i1 :b1
INF_STATE/active/y <-- b1 :b1
decide to be prepared === b1 :e1
I1 :B1 <-------------------ENROL/no-rsp-req
decide to cancel autonomously === e1 :j1
B1 :B1 <-----------------INF_STATE/active/y
B1 :B1 --> SUP_STATE/active
CANCELLED <-- j1 :j2
B1 :G1 === decide to cancel
G1 :J2 <--------------------------CANCELLED
SUP_STATE/active-------------------> j2 :j2
J2 :Z --> CANCEL------------------------------------> j2 :z
Both cancel (-:-)
superior inferior
ENROL/no-rsp-req <-- i1 :b1
decide to be prepared === b1 :e1
decide to cancel autonomously === e1 :j1
I1 :B1 <-------------------ENROL/no-rsp-req
B1 :B1 --> SUP_STATE/active/y
B1 :G1 === decide to cancel
CANCELLED <-- j1 :j2
SUP_STATE/active/y-----------------> j2 :j2
G1 :J2 <--------------------------CANCELLED
J2 :Z --> CANCEL------------------------------------> j2 :z
Both cancel (-:-)
superior inferior
I1 :B1 <--------------------------ENROL/no-rsp-req <-- i1 :b1
B1 :B1 <------------------------INF_STATE/active/y <-- b1 :b1
decide to be prepared === b1 :e1
PREPARED <-- e1 :e1
decide to cancel autonomously === e1 :j1
B1 :E1 <---------------------------PREPARED
E1 :E1 --> SUP_STATE/preparedreceived
E1 :J1 <---------------------------------CANCELLED <-- j1 :j2
SUP_STATE/preparedreceived---------> j2 :j2
J1 :J2 === decide to cancel
J2 :Z --> CANCEL------------------------------------> j2 :z
Both cancel (-:-)
superior inferior
ENROL/no-rsp-req <-- i1 :b1
decide to be prepared === b1 :e1
I1 :B1 <-------------------ENROL/no-rsp-req
B1 :E1 <----------------------------------PREPARED <-- e1 :e1
decide to cancel autonomously === e1 :j1
E1 :E1 --> SUP_STATE/preparedreceived/y
E1 :G1 === decide to cancel
CANCELLED <-- j1 :j2
G1 :G2 --> CANCEL
SUP_STATE/preparedreceived/y-------> j2 :j2
CANCEL-----------------------------> j2 :z
G2 :Z <--------------------------CANCELLED
Both cancel (-:-)
superior inferior
ENROL/no-rsp-req <-- i1 :b1
decide to be prepared === b1 :e1
disruption 0 XXX e1 :e1
X---ENROL/no-rsp-req
decide to cancel autonomously === e1 :j1
I1 :Y1 <---------------------------------CANCELLED <-- j1 :j2
Y1 :Z --> SUP_STATE/unknown-------------------------> j2 :z
superior never decided, inferior cancelled (:-)
superior inferior
ENROL/no-rsp-req <-- i1 :b1
decide to be prepared === b1 :e1
decide to cancel autonomously === e1 :j1
disruption I XXX j1 :j2
X---ENROL/no-rsp-req
I1 :Y1 <---------------------------------CANCELLED <-- j2 :j2
Y1 :Z --> SUP_STATE/unknown-------------------------> j2 :z
superior never decided, inferior cancelled (:-)
superior inferior
ENROL/no-rsp-req <-- i1 :b1
decide to be prepared === b1 :e1
I1 :B1 <-------------------ENROL/no-rsp-req
B1 :G1 === decide to cancel
decide to cancel autonomously === e1 :j1
G1 :G2 --> CANCEL------------------------------------> j1 :j3
disruption 0 XXX j3 :j3
G2 :Z <---------------------------------CANCELLED <-- j3 :z
Both cancel (-:-)
superior inferior
I1 :B1 <--------------------------ENROL/no-rsp-req <-- i1 :b1
B1 :G1 === decide to cancel
decide to be prepared === b1 :e1
decide to cancel autonomously === e1 :j1
G1 :G2 --> CANCEL------------------------------------> j1 :j3
G2 :Z XXX disruption I
disruption I XXX j3 :z
Both cancel (-:-)
superior inferior
ENROL/no-rsp-req <-- i1 :b1
decide to be prepared === b1 :e1
I1 :B1 <-------------------ENROL/no-rsp-req
B1 :G1 === decide to cancel
decide to cancel autonomously === e1 :j1
G1 :G2 --> CANCEL------------------------------------> j1 :j3
G2 :G2 --> CANCEL------------------------------------> j3 :j3
G2 :Z <---------------------------------CANCELLED <-- j3 :z
Both cancel (-:-)
superior inferior
ENROL/no-rsp-req <-- i1 :b1
decide to be prepared === b1 :e1
I1 :B1 <-------------------ENROL/no-rsp-req
decide to cancel autonomously === e1 :j1
B1 :G1 === decide to cancel
G1 :G2 --> CANCEL------------------------------------> j1 :j3
G2 :Z <---------------------------------CANCELLED <-- j3 :z
Both cancel (-:-)
superior inferior
ENROL/no-rsp-req <-- i1 :b1
decide to be prepared === b1 :e1
PREPARED <-- e1 :e1
decide to cancel autonomously === e1 :j1
I1 :B1 <-------------------ENROL/no-rsp-req
B1 :E1 <---------------------------PREPARED
E1 :F1 === decide to confirm
F1 :F1 --> CONFIRM
F1 :K0 <---------------------------------CANCELLED <-- j1 :j2
CONFIRM----------------------------> j2 :k1
disruption 0 XXX k1 :k1
CANCELLED <-- k1 :k1
K0 :K1 === record contradiction
K1 :K1 <--------------------------CANCELLED
K1 :Z --> CONTRADICTION-----------------------------> k1 :z
Superior confirms, inferior cancelled - contradiction reported (+!:-)
superior inferior
I1 :B1 <--------------------------ENROL/no-rsp-req <-- i1 :b1
decide to be prepared === b1 :e1
PREPARED <-- e1 :e1
decide to cancel autonomously === e1 :j1
B1 :E1 <---------------------------PREPARED
E1 :F1 === decide to confirm
CANCELLED <-- j1 :j2
F1 :F1 --> CONFIRM
F1 :F1 --> CONFIRM
CONFIRM----------------------------> j2 :k1
CONFIRM----------------------------> k1 :k1
F1 :K0 <--------------------------CANCELLED
K0 :K1 === record contradiction
K1 :Z --> CONTRADICTION-----------------------------> k1 :z
Superior confirms, inferior cancelled - contradiction reported (+!:-)
superior inferior
I1 :B1 <--------------------------ENROL/no-rsp-req <-- i1 :b1
decide to be prepared === b1 :e1
B1 :E1 <----------------------------------PREPARED <-- e1 :e1
E1 :F1 === decide to confirm
decide to cancel autonomously === e1 :j1
F1 :F1 --> CONFIRM-----------------------------------> j1 :k1
F1 :K0 <---------------------------------CANCELLED <-- k1 :k1
K0 :K1 === record contradiction
K1 :Z --> CONTRADICTION-----------------------------> k1 :z
Superior confirms, inferior cancelled - contradiction reported (+!:-)
superior inferior
ENROL/no-rsp-req <-- i1 :b1
decide to be prepared === b1 :e1
PREPARED <-- e1 :e1
decide to cancel autonomously === e1 :j1
I1 :B1 <-------------------ENROL/no-rsp-req
B1 :E1 <---------------------------PREPARED
E1 :F1 === decide to confirm
F1 :F1 --> CONFIRM-----------------------------------> j1 :k1
F1 :K0 <---------------------------------CANCELLED <-- k1 :k1
K0 :K1 === record contradiction
K1 :Z XXX disruption I
Z :Y1 <---------------------------------CANCELLED <-- k1 :k1
Y1 :Z --> SUP_STATE/unknown-------------------------> k1 :z
Superior confirms, inferior cancelled - contradiction reported (+!:-)
superior inferior
I1 :B1 <--------------------------ENROL/no-rsp-req <-- i1 :b1
decide to be prepared === b1 :e1
B1 :E1 <----------------------------------PREPARED <-- e1 :e1
E1 :F1 === decide to confirm
decide to cancel autonomously === e1 :j1
F1 :F1 --> CONFIRM-----------------------------------> j1 :k1
F1 :K0 <---------------------------------CANCELLED <-- k1 :k1
K0 :K1 === record contradiction
K1 :Z --> CONTRADICTION-----------------------------> k1 :z
Superior confirms, inferior cancelled - contradiction reported (+!:-)
superior inferior
I1 :B1 <--------------------------ENROL/no-rsp-req <-- i1 :b1
B1 :G1 === decide to cancel
decide to be prepared === b1 :e1
G1 :G2 --> CANCEL
decide to confirm autonomously === e1 :h1
G2 :L0 <----------------------------CONFIRMED/auto <-- h1 :h1
L0 :L1 === record contradiction
CANCEL-----------------------------> h1 :l1
disruption 0 XXX l1 :l1
L1 :Z --> CONTRADICTION-----------------------------> l1 :z
Superior cancels, inferior confirmed - contradiction reported (-!:#)
superior inferior
I1 :B1 <--------------------------ENROL/no-rsp-req <-- i1 :b1
decide to be prepared === b1 :e1
B1 :G1 === decide to cancel
G1 :G2 --> CANCEL
decide to confirm autonomously === e1 :h1
CANCEL-----------------------------> h1 :l1
G2 :G2 --> CANCEL
G2 :L0 <----------------------------CONFIRMED/auto <-- l1 :l1
L0 :L1 === record contradiction
CANCEL-----------------------------> l1 :l1
L1 :Z --> CONTRADICTION-----------------------------> l1 :z
Superior cancels, inferior confirmed - contradiction reported (-!:#)
superior inferior
ENROL/no-rsp-req <-- i1 :b1
decide to be prepared === b1 :e1
I1 :B1 <-------------------ENROL/no-rsp-req
B1 :G1 === decide to cancel
G1 :G2 --> CANCEL
decide to confirm autonomously === e1 :h1
G2 :L0 <----------------------------CONFIRMED/auto <-- h1 :h1
L0 :L1 === record contradiction
L1 :Z --> CONTRADICTION
CANCEL-----------------------------> h1 :l1
CONTRADICTION----------------------> l1 :z
Superior cancels, inferior confirmed - contradiction reported (-!:#)
superior inferior
I1 :Z XXX disruption I
ENROL/no-rsp-req <-- i1 :b1
decide to be prepared === b1 :e1
PREPARED <-- e1 :e1
Z :Z <-------------------ENROL/no-rsp-req
Z :Y1 <---------------------------PREPARED
PREPARED <-- e1 :e1
Y1 :Z --> SUP_STATE/unknown
decide to confirm autonomously === e1 :h1
Z :Y1 <---------------------------PREPARED
SUP_STATE/unknown------------------> h1 :l1
Y1 :Z --> SUP_STATE/unknown-------------------------> l1 :l1
Z :L2 <----------------------------CONFIRMED/auto <-- l1 :l1
L2 :L1 === record contradiction
L1 :Z --> CONTRADICTION-----------------------------> l1 :z
Superior never decided, inferior confirmed - contradiction reported (!:#)
superior inferior
I1 :B1 <--------------------------ENROL/no-rsp-req <-- i1 :b1
B1 :G1 === decide to cancel
decide to be prepared === b1 :e1
decide to confirm autonomously === e1 :h1
G1 :G2 --> CANCEL------------------------------------> h1 :l1
G2 :L0 <----------------------------CONFIRMED/auto <-- l1 :l1
L0 :L1 === record contradiction
L1 :Z --> CONTRADICTION-----------------------------> l1 :z
Superior cancels, inferior confirmed - contradiction reported (-!:#)
superior inferior
ENROL/rsp-req <-- i1 :a1
detect problem === a1 :m2
detect and record problem === m2 :m1
disruption 0 XXX m1 :m1
X---ENROL/rsp-req
I1 :M0 <------------------------------------HAZARD <-- m1 :m1
M0 :M3 === record contradiction
M3 :Z --> CONTRADICTION-----------------------------> m1 :z
Superior never decided, inferior detects mix - contradiction reported (!:!)
superior inferior
I1 :B1 <--------------------------ENROL/no-rsp-req <-- i1 :b1
detect problem === b1 :m2
B1 :G1 === decide to cancel
detect and record problem === m2 :m1
G1 :G2 --> CANCEL------------------------------------> m1 :m1
G2 :M2 <------------------------------------HAZARD <-- m1 :m1
M2 :M3 === record contradiction
M3 :Z --> CONTRADICTION-----------------------------> m1 :z
Superior cancels, inferior detects mix - contradiction reported (-!:!)
superior inferior
ENROL/no-rsp-req <-- i1 :b1
decide to be prepared/cancel === b1 :e2
PREPARED/cancel <-- e2 :e2
I1 :B1 <-------------------ENROL/no-rsp-req
detect problem === e2 :m3
B1 :E2 <--------------------PREPARED/cancel
E2 :F1 === decide to confirm
detect and record problem === m3 :m1
F1 :F1 --> CONFIRM
F1 :M1 <------------------------------------HAZARD <-- m1 :m1
M1 :M3 === record contradiction
M3 :Z --> CONTRADICTION
CONFIRM----------------------------> m1 :m1
CONTRADICTION----------------------> m1 :z
Superior confirms, inferior detects mix - contradiction reported (+!:!)
superior inferior
I1 :A1 <-----------------------------ENROL/rsp-req <-- i1 :a1
detect problem === a1 :m2
A1 :M0 <------------------------------------HAZARD <-- m2 :m2
detect and record problem === m2 :m1
M0 :M3 === record contradiction
M3 :Z --> CONTRADICTION-----------------------------> m1 :z
Superior never decided, inferior detects mix - contradiction reported (!:!)
superior inferior
I1 :A1 <-----------------------------ENROL/rsp-req <-- i1 :a1
detect problem === a1 :m2
detect and record problem === m2 :m1
A1 :B1 --> ENROLLED
B1 :N1 --> REQUEST_CONFIRM
ENROLLED---------------------------> m1 :m1
REQUEST_CONFIRM--------------------> m1 :n4
N1 :Z <------------------------------------HAZARD <-- n4 :z
Superior requested confirm, inferior detects mix - contradiction NOT reported (=:!)
superior inferior
I1 :B1 <--------------------------ENROL/no-rsp-req <-- i1 :b1
B1 :D1 === decide to prepare
detect problem === b1 :m2
detect and record problem === m2 :m1
D1 :D1 --> PREPARE
D1 :M0 <------------------------------------HAZARD <-- m1 :m1
PREPARE----------------------------> m1 :m1
M0 :M3 === record contradiction
M3 :Z --> CONTRADICTION-----------------------------> m1 :z
Superior never decided, inferior detects mix - contradiction reported (!:!)
superior inferior
ENROL/no-rsp-req <-- i1 :b1
detect problem === b1 :m2
detect and record problem === m2 :m1
I1 :B1 <-------------------ENROL/no-rsp-req
B1 :N1 --> REQUEST_CONFIRM---------------------------> m1 :n4
N1 :Z <------------------------------------HAZARD <-- n4 :z
Superior requested confirm, inferior detects mix - contradiction NOT reported (=:!)
superior inferior
ENROL/no-rsp-req <-- i1 :b1
INF_STATE/active/y <-- b1 :b1
detect problem === b1 :m2
detect and record problem === m2 :m1
I1 :B1 <-------------------ENROL/no-rsp-req
B1 :B1 <-----------------INF_STATE/active/y
B1 :B1 --> SUP_STATE/active
B1 :N1 --> REQUEST_CONFIRM
SUP_STATE/active-------------------> m1 :m1
REQUEST_CONFIRM--------------------> m1 :n4
N1 :Z <------------------------------------HAZARD <-- n4 :z
Superior requested confirm, inferior detects mix - contradiction NOT reported (=:!)
superior inferior
ENROL/no-rsp-req <-- i1 :b1
detect problem === b1 :m2
I1 :B1 <-------------------ENROL/no-rsp-req
detect and record problem === m2 :m1
B1 :B1 --> SUP_STATE/active/y
B1 :N1 --> REQUEST_CONFIRM
SUP_STATE/active/y-----------------> m1 :m1
REQUEST_CONFIRM--------------------> m1 :n4
N1 :Z <------------------------------------HAZARD <-- n4 :z
Superior requested confirm, inferior detects mix - contradiction NOT reported (=:!)
superior inferior
I1 :B1 <--------------------------ENROL/no-rsp-req <-- i1 :b1
INF_STATE/active/y <-- b1 :b1
decide to be prepared === b1 :e1
PREPARED <-- e1 :e1
detect problem === e1 :m3
B1 :B1 <-----------------INF_STATE/active/y
B1 :E1 <---------------------------PREPARED
detect and record problem === m3 :m1
E1 :E1 --> SUP_STATE/preparedreceived
E1 :N1 --> REQUEST_CONFIRM
SUP_STATE/preparedreceived---------> m1 :m1
REQUEST_CONFIRM--------------------> m1 :n4
N1 :Z <------------------------------------HAZARD <-- n4 :z
Superior requested confirm, inferior detects mix - contradiction NOT reported (=:!)
superior inferior
ENROL/no-rsp-req <-- i1 :b1
decide to be prepared/cancel === b1 :e2
PREPARED/cancel <-- e2 :e2
detect problem === e2 :m3
I1 :B1 <-------------------ENROL/no-rsp-req
B1 :E2 <--------------------PREPARED/cancel
E2 :E2 --> SUP_STATE/preparedreceived/y
detect and record problem === m3 :m1
SUP_STATE/preparedreceived/y-------> m1 :m1
E2 :N1 --> REQUEST_CONFIRM---------------------------> m1 :n4
N1 :Z <------------------------------------HAZARD <-- n4 :z
Superior requested confirm, inferior detects mix - contradiction NOT reported (=:!)
superior inferior
I1 :Z XXX disruption I
ENROL/rsp-req <-- i1 :a1
detect problem === a1 :m2
Z :Y1 <----------------------ENROL/rsp-req
detect and record problem === m2 :m1
Y1 :Z --> SUP_STATE/unknown
HAZARD <-- m1 :m1
SUP_STATE/unknown------------------> m1 :m1
Z :M0 <-----------------------------HAZARD
M0 :M3 === record contradiction
M3 :Z --> CONTRADICTION-----------------------------> m1 :z
Superior never decided, inferior detects mix - contradiction reported (!:!)
superior inferior
I1 :A1 <-----------------------------ENROL/rsp-req <-- i1 :a1
detect problem === a1 :m2
detect and record problem === m2 :m1
A1 :M0 <------------------------------------HAZARD <-- m1 :m1
M0 :M3 === record contradiction
M3 :Z --> CONTRADICTION-----------------------------> m1 :z
Superior never decided, inferior detects mix - contradiction reported (!:!)
superior inferior
ENROL/no-rsp-req <-- i1 :b1
detect problem === b1 :m2
I1 :B1 <-------------------ENROL/no-rsp-req
detect and record problem === m2 :m1
B1 :N1 --> REQUEST_CONFIRM---------------------------> m1 :n4
N1 :Z <------------------------------------HAZARD <-- n4 :z
Superior requested confirm, inferior detects mix - contradiction NOT reported (=:!)
superior inferior
ENROL/rsp-req <-- i1 :a1
detect problem === a1 :m2
I1 :A1 <----------------------ENROL/rsp-req
disruption 0 XXX m2 :m2
disruption I XXX m2 :z
A1 :Z XXX disruption I
Superior nothing, unreported hazard (:?)
superior inferior
I1 :Z XXX disruption I
ENROL/no-rsp-req <-- i1 :b1
detect problem === b1 :m2
disruption I XXX m2 :z
X---ENROL/no-rsp-req
Superior nothing, unreported hazard (:?)
superior inferior
I1 :B1 <--------------------------ENROL/no-rsp-req <-- i1 :b1
B1 :G1 === decide to cancel
detect problem === b1 :m2
G1 :G2 --> CANCEL------------------------------------> m2 :m2
disruption I XXX m2 :z
G2 :Z XXX disruption I
Superior cancels, unreported hazard (-:?)
superior inferior
ENROL/rsp-req <-- i1 :a1
detect problem === a1 :m2
HAZARD <-- m2 :m2
I1 :A1 <----------------------ENROL/rsp-req
A1 :M0 <-----------------------------HAZARD
M0 :M3 === record contradiction
M3 :Z --> CONTRADICTION-----------------------------> m2 :z
Inferior detected problem, contradiction reported (!:?)
superior inferior
I1 :A1 <-----------------------------ENROL/rsp-req <-- i1 :a1
detect problem === a1 :m2
A1 :B1 --> ENROLLED----------------------------------> m2 :m2
B1 :G1 === decide to cancel
disruption I XXX m2 :z
G1 :Z XXX disruption I
Superior cancels, unreported hazard (-:?)
superior inferior
I1 :B1 <--------------------------ENROL/no-rsp-req <-- i1 :b1
detect problem === b1 :m2
B1 :D1 === decide to prepare
D1 :D1 --> PREPARE
D1 :M0 <------------------------------------HAZARD <-- m2 :m2
PREPARE----------------------------> m2 :m2
M0 :M3 === record contradiction
M3 :Z --> CONTRADICTION-----------------------------> m2 :z
Inferior detected problem, contradiction reported (!:?)
superior inferior
ENROL/no-rsp-req <-- i1 :b1
detect problem === b1 :m2
I1 :B1 <-------------------ENROL/no-rsp-req
B1 :N1 --> REQUEST_CONFIRM---------------------------> m2 :n5
N1 :Z <------------------------------------HAZARD <-- n5 :z
Confirm requested, inferior detected problem, contradiction not reported (=:?)
superior inferior
I1 :B1 <--------------------------ENROL/no-rsp-req <-- i1 :b1
B1 :B1 <------------------------INF_STATE/active/y <-- b1 :b1
B1 :B1 --> SUP_STATE/active
B1 :N1 --> REQUEST_CONFIRM
detect problem === b1 :m2
SUP_STATE/active-------------------> m2 :m2
REQUEST_CONFIRM--------------------> m2 :n5
N1 :Z <------------------------------------HAZARD <-- n5 :z
Confirm requested, inferior detected problem, contradiction not reported (=:?)
superior inferior
ENROL/no-rsp-req <-- i1 :b1
detect problem === b1 :m2
I1 :B1 <-------------------ENROL/no-rsp-req
B1 :B1 --> SUP_STATE/active/y------------------------> m2 :m2
B1 :N1 --> REQUEST_CONFIRM---------------------------> m2 :n5
N1 :Z <------------------------------------HAZARD <-- n5 :z
Confirm requested, inferior detected problem, contradiction not reported (=:?)
superior inferior
I1 :Z XXX disruption I
Z :Y1 <-----------------------------ENROL/rsp-req <-- i1 :a1
detect problem === a1 :m2
Y1 :Z --> SUP_STATE/unknown-------------------------> m2 :m2
disruption I XXX m2 :z
Superior nothing, unreported hazard (:?)
superior inferior
ENROL/rsp-req <-- i1 :a1
detect problem === a1 :m2
HAZARD <-- m2 :m2
disruption I XXX m2 :z
X---HAZARD
I1 :A1 <----------------------ENROL/rsp-req
A1 :Z XXX disruption I
Superior nothing, unreported hazard (:?)
superior inferior
ENROL/no-rsp-req <-- i1 :b1
decide to be prepared/cancel === b1 :e2
I1 :B1 <-------------------ENROL/no-rsp-req
B1 :N1 --> REQUEST_CONFIRM
detect problem === e2 :m3
detect and record problem === m3 :m1
REQUEST_CONFIRM--------------------> m1 :n4
N1 :Z <------------------------------------HAZARD <-- n4 :z
Superior requested confirm, inferior detects mix - contradiction NOT reported (=:!)
superior inferior
ENROL/no-rsp-req <-- i1 :b1
decide to be prepared/cancel === b1 :e2
detect problem === e2 :m3
disruption 0 XXX m3 :m3
X---ENROL/no-rsp-req
detect and record problem === m3 :m1
I1 :M0 <------------------------------------HAZARD <-- m1 :m1
M0 :M3 === record contradiction
M3 :Z --> CONTRADICTION-----------------------------> m1 :z
Superior never decided, inferior detects mix - contradiction reported (!:!)
superior inferior
ENROL/no-rsp-req <-- i1 :b1
decide to be prepared/cancel === b1 :e2
I1 :B1 <-------------------ENROL/no-rsp-req
detect problem === e2 :m3
B1 :G1 === decide to cancel
G1 :G2 --> CANCEL
HAZARD <-- m3 :m3
CANCEL-----------------------------> m3 :m3
G2 :M2 <-----------------------------HAZARD
M2 :M3 === record contradiction
M3 :Z --> CONTRADICTION-----------------------------> m3 :z
Superior cancels, Inferior detected problem, contradiction reported (-!:?)
superior inferior
ENROL/no-rsp-req <-- i1 :b1
decide to be prepared/cancel === b1 :e2
PREPARED/cancel <-- e2 :e2
I1 :B1 <-------------------ENROL/no-rsp-req
B1 :E2 <--------------------PREPARED/cancel
E2 :F1 === decide to confirm
detect problem === e2 :m3
F1 :F1 --> CONFIRM-----------------------------------> m3 :m3
F1 :M1 <------------------------------------HAZARD <-- m3 :m3
M1 :M3 === record contradiction
M3 :Z --> CONTRADICTION-----------------------------> m3 :z
Superior confirms, inferior only detects mix - contradiction reported (+!:?)
superior inferior
ENROL/no-rsp-req <-- i1 :b1
decide to be prepared/cancel === b1 :e2
detect problem === e2 :m3
I1 :B1 <-------------------ENROL/no-rsp-req
B1 :M0 <------------------------------------HAZARD <-- m3 :m3
M0 :M3 === record contradiction
M3 :Z --> CONTRADICTION-----------------------------> m3 :z
Inferior detected problem, contradiction reported (!:?)
superior inferior
ENROL/no-rsp-req <-- i1 :b1
decide to be prepared/cancel === b1 :e2
I1 :B1 <-------------------ENROL/no-rsp-req
B1 :D1 === decide to prepare
detect problem === e2 :m3
HAZARD <-- m3 :m3
D1 :D1 --> PREPARE
D1 :M0 <-----------------------------HAZARD
PREPARE----------------------------> m3 :m3
M0 :M3 === record contradiction
M3 :Z --> CONTRADICTION-----------------------------> m3 :z
Inferior detected problem, contradiction reported (!:?)
superior inferior
I1 :B1 <--------------------------ENROL/no-rsp-req <-- i1 :b1
decide to be prepared === b1 :e1
detect problem === e1 :m3
B1 :N1 --> REQUEST_CONFIRM---------------------------> m3 :n5
N1 :Z <------------------------------------HAZARD <-- n5 :z
Confirm requested, inferior detected problem, contradiction not reported (=:?)
superior inferior
ENROL/no-rsp-req <-- i1 :b1
INF_STATE/active/y <-- b1 :b1
decide to be prepared/cancel === b1 :e2
I1 :B1 <-------------------ENROL/no-rsp-req
B1 :B1 <-----------------INF_STATE/active/y
detect problem === e2 :m3
B1 :B1 --> SUP_STATE/active
B1 :N1 --> REQUEST_CONFIRM
SUP_STATE/active-------------------> m3 :m3
REQUEST_CONFIRM--------------------> m3 :n5
N1 :Z <------------------------------------HAZARD <-- n5 :z
Confirm requested, inferior detected problem, contradiction not reported (=:?)
superior inferior
ENROL/no-rsp-req <-- i1 :b1
decide to be prepared === b1 :e1
detect problem === e1 :m3
I1 :B1 <-------------------ENROL/no-rsp-req
B1 :B1 --> SUP_STATE/active/y------------------------> m3 :m3
B1 :N1 --> REQUEST_CONFIRM---------------------------> m3 :n5
N1 :Z <------------------------------------HAZARD <-- n5 :z
Confirm requested, inferior detected problem, contradiction not reported (=:?)
superior inferior
ENROL/no-rsp-req <-- i1 :b1
INF_STATE/active/y <-- b1 :b1
decide to be prepared/cancel === b1 :e2
PREPARED/cancel <-- e2 :e2
detect problem === e2 :m3
I1 :B1 <-------------------ENROL/no-rsp-req
B1 :D1 === decide to prepare
D1 :D1 <-----------------INF_STATE/active/y
D1 :E2 <--------------------PREPARED/cancel
E2 :E2 --> SUP_STATE/preparedreceived
E2 :N1 --> REQUEST_CONFIRM
SUP_STATE/preparedreceived---------> m3 :m3
REQUEST_CONFIRM--------------------> m3 :n5
N1 :Z <------------------------------------HAZARD <-- n5 :z
Confirm requested, inferior detected problem, contradiction not reported (=:?)
superior inferior
ENROL/no-rsp-req <-- i1 :b1
decide to be prepared === b1 :e1
I1 :B1 <-------------------ENROL/no-rsp-req
PREPARED <-- e1 :e1
detect problem === e1 :m3
B1 :E1 <---------------------------PREPARED
E1 :E1 --> SUP_STATE/preparedreceived/y
E1 :N1 --> REQUEST_CONFIRM
SUP_STATE/preparedreceived/y-------> m3 :m3
REQUEST_CONFIRM--------------------> m3 :n5
N1 :Z <------------------------------------HAZARD <-- n5 :z
Confirm requested, inferior detected problem, contradiction not reported (=:?)
superior inferior
I1 :Z XXX disruption I
ENROL/no-rsp-req <-- i1 :b1
INF_STATE/active/y <-- b1 :b1
decide to be prepared/cancel === b1 :e2
Z :Z <-------------------ENROL/no-rsp-req
Z :Y1 <-----------------INF_STATE/active/y
detect problem === e2 :m3
Y1 :Z --> SUP_STATE/unknown-------------------------> m3 :m3
Z :M0 <------------------------------------HAZARD <-- m3 :m3
M0 :M3 === record contradiction
M3 :Z --> CONTRADICTION-----------------------------> m3 :z
Inferior detected problem, contradiction reported (!:?)
superior inferior
ENROL/no-rsp-req <-- i1 :b1
decide to be prepared/cancel === b1 :e2
I1 :B1 <-------------------ENROL/no-rsp-req
detect problem === e2 :m3
B1 :M0 <------------------------------------HAZARD <-- m3 :m3
M0 :M3 === record contradiction
M3 :Z --> CONTRADICTION-----------------------------> m3 :z
Inferior detected problem, contradiction reported (!:?)
superior inferior
I1 :B1 <--------------------------ENROL/no-rsp-req <-- i1 :b1
B1 :N1 --> REQUEST_CONFIRM
decide to be prepared === b1 :e1
REQUEST_CONFIRM--------------------> e1 :n0
disruption 0 XXX n0 :n0
remove prepared information === n0 :n1
decide to confirm autonomously === n1 :n2
N1 :Z <------------------------CONFIRMED/response <-- n2 :z
Superior requested confirm, inferior confirmed (=:#)
superior inferior
I1 :B1 <--------------------------ENROL/no-rsp-req <-- i1 :b1
decide to be prepared/cancel === b1 :e2
B1 :N1 --> REQUEST_CONFIRM---------------------------> e2 :n0
disruption I XXX n0 :e1
N1 :N1 --> REQUEST_CONFIRM
decide to cancel autonomously === e1 :j1
REQUEST_CONFIRM--------------------> j1 :n3
N1 :Z <---------------------------------CANCELLED <-- n3 :z
Superior requested confirm, inferior cancelled (=:-)
superior inferior
ENROL/no-rsp-req <-- i1 :b1
decide to be prepared/cancel === b1 :e2
I1 :B1 <-------------------ENROL/no-rsp-req
B1 :N1 --> REQUEST_CONFIRM---------------------------> e2 :n0
N1 :N1 --> REQUEST_CONFIRM---------------------------> n0 :n0
remove prepared information === n0 :n1
decide to cancel autonomously === n1 :n3
N1 :Z <---------------------------------CANCELLED <-- n3 :z
Superior requested confirm, inferior cancelled (=:-)
superior inferior
I1 :B1 <--------------------------ENROL/no-rsp-req <-- i1 :b1
decide to be prepared === b1 :e1
PREPARED <-- e1 :e1
B1 :N1 --> REQUEST_CONFIRM---------------------------> e1 :n0
N1 :Z XXX disruption I
Z :Y1 <---------------------------PREPARED
Y1 :Z --> SUP_STATE/unknown-------------------------> n0 :z
Superior requested confirm, inferior never decided (=:)
superior inferior
I1 :B1 <--------------------------ENROL/no-rsp-req <-- i1 :b1
decide to be prepared/cancel === b1 :e2
B1 :N1 --> REQUEST_CONFIRM---------------------------> e2 :n0
remove prepared information === n0 :n1
decide to confirm autonomously === n1 :n2
N1 :Z <------------------------CONFIRMED/response <-- n2 :z
Superior requested confirm, inferior confirmed (=:#)
superior inferior
I1 :B1 <--------------------------ENROL/no-rsp-req <-- i1 :b1
B1 :N1 --> REQUEST_CONFIRM---------------------------> b1 :n1
decide to cancel autonomously === n1 :n3
N1 :Z <---------------------------------CANCELLED <-- n3 :z
Superior requested confirm, inferior cancelled (=:-)
superior inferior
I1 :B1 <--------------------------ENROL/no-rsp-req <-- i1 :b1
B1 :N1 --> REQUEST_CONFIRM---------------------------> b1 :n1
decide to confirm autonomously === n1 :n2
N1 :Z <------------------------CONFIRMED/response <-- n2 :z
Superior requested confirm, inferior confirmed (=:#)
superior inferior
I1 :B1 <--------------------------ENROL/no-rsp-req <-- i1 :b1
B1 :N1 --> REQUEST_CONFIRM---------------------------> b1 :n1
detect and record problem === n1 :n4
N1 :Z <------------------------------------HAZARD <-- n4 :z
Superior requested confirm, inferior detects mix - contradiction NOT reported (=:!)
superior inferior
I1 :B1 <--------------------------ENROL/no-rsp-req <-- i1 :b1
B1 :N1 --> REQUEST_CONFIRM---------------------------> b1 :n1
disruption 0 XXX n1 :n1
decide to cancel autonomously === n1 :n3
N1 :Z <---------------------------------CANCELLED <-- n3 :z
Superior requested confirm, inferior cancelled (=:-)
superior inferior
I1 :B1 <--------------------------ENROL/no-rsp-req <-- i1 :b1
B1 :N1 --> REQUEST_CONFIRM---------------------------> b1 :n1
disruption I XXX n1 :z
N1 :Z XXX disruption I
Superior requested confirm, inferior never decided (=:)
superior inferior
I1 :B1 <--------------------------ENROL/no-rsp-req <-- i1 :b1
B1 :N1 --> REQUEST_CONFIRM---------------------------> b1 :n1
N1 :N1 --> REQUEST_CONFIRM---------------------------> n1 :n1
detect and record problem === n1 :n4
N1 :Z <------------------------------------HAZARD <-- n4 :z
Superior requested confirm, inferior detects mix - contradiction NOT reported (=:!)
superior inferior
I1 :B1 <--------------------------ENROL/no-rsp-req <-- i1 :b1
B1 :N1 --> REQUEST_CONFIRM---------------------------> b1 :n1
decide to confirm autonomously === n1 :n2
disruption 0 XXX n2 :n2
N1 :Z <------------------------CONFIRMED/response <-- n2 :z
Superior requested confirm, inferior confirmed (=:#)
superior inferior
I1 :B1 <--------------------------ENROL/no-rsp-req <-- i1 :b1
B1 :N1 --> REQUEST_CONFIRM---------------------------> b1 :n1
decide to confirm autonomously === n1 :n2
N1 :N1 --> REQUEST_CONFIRM---------------------------> n2 :n2
N1 :Z <------------------------CONFIRMED/response <-- n2 :z
Superior requested confirm, inferior confirmed (=:#)
superior inferior
I1 :B1 <--------------------------ENROL/no-rsp-req <-- i1 :b1
B1 :N1 --> REQUEST_CONFIRM---------------------------> b1 :n1
decide to confirm autonomously === n1 :n2
N1 :Z <------------------------CONFIRMED/response <-- n2 :z
Superior requested confirm, inferior confirmed (=:#)
superior inferior
I1 :B1 <--------------------------ENROL/no-rsp-req <-- i1 :b1
B1 :N1 --> REQUEST_CONFIRM---------------------------> b1 :n1
decide to cancel autonomously === n1 :n3
disruption 0 XXX n3 :n3
N1 :Z <---------------------------------CANCELLED <-- n3 :z
Superior requested confirm, inferior cancelled (=:-)
superior inferior
I1 :B1 <--------------------------ENROL/no-rsp-req <-- i1 :b1
B1 :N1 --> REQUEST_CONFIRM---------------------------> b1 :n1
decide to cancel autonomously === n1 :n3
N1 :N1 --> REQUEST_CONFIRM---------------------------> n3 :n3
N1 :Z <---------------------------------CANCELLED <-- n3 :z
Superior requested confirm, inferior cancelled (=:-)
superior inferior
ENROL/no-rsp-req <-- i1 :b1
decide to be prepared === b1 :e1
decide to cancel autonomously === e1 :j1
CANCELLED <-- j1 :j2
CANCELLED <-- j2 :j2
I1 :B1 <-------------------ENROL/no-rsp-req
B1 :N1 --> REQUEST_CONFIRM
N1 :Z <--------------------------CANCELLED
Z :Y1 <--------------------------CANCELLED
REQUEST_CONFIRM--------------------> j2 :n3
Y1 :Z --> SUP_STATE/unknown-------------------------> n3 :z
Superior requested confirm, inferior cancelled (=:-)
superior inferior
I1 :B1 <--------------------------ENROL/no-rsp-req <-- i1 :b1
B1 :N1 --> REQUEST_CONFIRM---------------------------> b1 :n1
decide to cancel autonomously === n1 :n3
N1 :Z <---------------------------------CANCELLED <-- n3 :z
Superior requested confirm, inferior cancelled (=:-)
superior inferior
I1 :B1 <--------------------------ENROL/no-rsp-req <-- i1 :b1
B1 :N1 --> REQUEST_CONFIRM---------------------------> b1 :n1
detect and record problem === n1 :n4
disruption 0 XXX n4 :n4
N1 :Z <------------------------------------HAZARD <-- n4 :z
Superior requested confirm, inferior detects mix - contradiction NOT reported (=:!)
superior inferior
ENROL/no-rsp-req <-- i1 :b1
detect problem === b1 :m2
detect and record problem === m2 :m1
I1 :B1 <-------------------ENROL/no-rsp-req
HAZARD <-- m1 :m1
B1 :N1 --> REQUEST_CONFIRM
HAZARD <-- m1 :m1
N1 :Z <-----------------------------HAZARD
REQUEST_CONFIRM--------------------> m1 :n4
Z :M0 <-----------------------------HAZARD
M0 :M3 === record contradiction
M3 :Z --> CONTRADICTION-----------------------------> n4 :n4
Z :M0 <------------------------------------HAZARD <-- n4 :z
M0 :Z XXX disruption I
Superior requested confirm, inferior detects mix - contradiction reported (=!:!)
superior inferior
I1 :B1 <--------------------------ENROL/no-rsp-req <-- i1 :b1
B1 :N1 --> REQUEST_CONFIRM---------------------------> b1 :n1
detect and record problem === n1 :n4
N1 :N1 --> REQUEST_CONFIRM---------------------------> n4 :n4
N1 :Z <------------------------------------HAZARD <-- n4 :z
Superior requested confirm, inferior detects mix - contradiction NOT reported (=:!)
superior inferior
I1 :A1 <-----------------------------ENROL/rsp-req <-- i1 :a1
A1 :B1 --> ENROLLED
B1 :N1 --> REQUEST_CONFIRM
N1 :Z XXX disruption I
INF_STATE/active/y <-- a1 :a1
detect problem === a1 :m2
detect and record problem === m2 :m1
Z :Y1 <-----------------INF_STATE/active/y
ENROLLED---------------------------> m1 :m1
Y1 :Z --> SUP_STATE/unknown
REQUEST_CONFIRM--------------------> m1 :n4
SUP_STATE/unknown------------------> n4 :z
Superior requested confirm, inferior detects mix - contradiction NOT reported (=:!)
superior inferior
I1 :B1 <--------------------------ENROL/no-rsp-req <-- i1 :b1
B1 :N1 --> REQUEST_CONFIRM---------------------------> b1 :n1
detect and record problem === n1 :n4
N1 :Z <------------------------------------HAZARD <-- n4 :z
Superior requested confirm, inferior detects mix - contradiction NOT reported (=:!)
superior inferior
ENROL/no-rsp-req <-- i1 :b1
detect problem === b1 :m2
I1 :B1 <-------------------ENROL/no-rsp-req
B1 :N1 --> REQUEST_CONFIRM---------------------------> m2 :n5
disruption 0 XXX n5 :n5
N1 :Z <------------------------------------HAZARD <-- n5 :z
Confirm requested, inferior detected problem, contradiction not reported (=:?)
superior inferior
ENROL/no-rsp-req <-- i1 :b1
detect problem === b1 :m2
I1 :B1 <-------------------ENROL/no-rsp-req
B1 :N1 --> REQUEST_CONFIRM
N1 :Z <------------------------------------HAZARD <-- m2 :m2
Z :M0 <------------------------------------HAZARD <-- m2 :m2
M0 :M3 === record contradiction
M3 :Z --> CONTRADICTION
REQUEST_CONFIRM--------------------> m2 :n5
CONTRADICTION----------------------> n5 :z
Confirm requested, inferior detected problem, contradiction reported (=!:?)
superior inferior
ENROL/no-rsp-req <-- i1 :b1
detect problem === b1 :m2
I1 :B1 <-------------------ENROL/no-rsp-req
B1 :N1 --> REQUEST_CONFIRM---------------------------> m2 :n5
N1 :N1 --> REQUEST_CONFIRM---------------------------> n5 :n5
N1 :Z <------------------------------------HAZARD <-- n5 :z
Confirm requested, inferior detected problem, contradiction not reported (=:?)
superior inferior
ENROL/no-rsp-req <-- i1 :b1
detect problem === b1 :m2
I1 :B1 <-------------------ENROL/no-rsp-req
B1 :N1 --> REQUEST_CONFIRM---------------------------> m2 :n5
N1 :Z <------------------------------------HAZARD <-- n5 :z
Confirm requested, inferior detected problem, contradiction not reported (=:?)
superior inferior
I1 :Z XXX disruption I
Z :Z <--------------------------ENROL/no-rsp-req <-- i1 :b1
INF_STATE/active/y <-- b1 :b1
decide to be prepared === b1 :e1
Z :Y1 <-----------------INF_STATE/active/y
Y1 :Z --> SUP_STATE/unknown-------------------------> e1 :y0
disruption 0 XXX y0 :y0
remove prepared information === y0 :z
Nothing happens (:)
superior inferior
I1 :Z XXX disruption I
ENROL/no-rsp-req <-- i1 :b1
decide to be prepared/cancel === b1 :e2
PREPARED/cancel <-- e2 :e2
Z :Z <-------------------ENROL/no-rsp-req
Z :Y1 <--------------------PREPARED/cancel
Y1 :Z --> SUP_STATE/unknown-------------------------> e2 :y0
disruption 0 XXX y0 :y0
disruption I XXX y0 :e1
detect problem === e1 :m3
Z :M0 <------------------------------------HAZARD <-- m3 :m3
M0 :M3 === record contradiction
M3 :M3 <------------------------------------HAZARD <-- m3 :m3
M3 :M3 <------------------------------------HAZARD <-- m3 :m3
M3 :Z --> CONTRADICTION-----------------------------> m3 :z
Inferior detected problem, contradiction reported (!:?)
superior inferior
I1 :Z XXX disruption I
Z :Z <--------------------------ENROL/no-rsp-req <-- i1 :b1
Z :Y1 <------------------------INF_STATE/active/y <-- b1 :b1
decide to be prepared/cancel === b1 :e2
PREPARED/cancel <-- e2 :e2
Y1 :Z --> SUP_STATE/unknown-------------------------> e2 :y0
Z :Y1 <--------------------PREPARED/cancel
Y1 :Z --> SUP_STATE/unknown-------------------------> y0 :y0
remove prepared information === y0 :z
Nothing happens (:)
superior inferior
ENROL/no-rsp-req <-- i1 :b1
decide to be prepared/cancel === b1 :e2
disruption 0 XXX e2 :e2
X---ENROL/no-rsp-req
I1 :Y1 <---------------------------PREPARED/cancel <-- e2 :e2
Y1 :Z --> SUP_STATE/unknown-------------------------> e2 :y0
remove prepared information === y0 :z
Nothing happens (:)
superior inferior
I1 :B1 <--------------------------ENROL/no-rsp-req <-- i1 :b1
B1 :N1 --> REQUEST_CONFIRM
RESIGN/no-rsp-req <-- b1 :z
REQUEST_CONFIRM--------------------> z :y1
disruption 0 XXX y1 :y1
X---RESIGN/no-rsp-req
N1 :Z <-------------------------INF_STATE/unknown <-- y1 :z
Superior requested confirm, inferior never decided (=:)
superior inferior
ENROL/no-rsp-req <-- i1 :b1
disruption I XXX b1 :z
I1 :B1 <-------------------ENROL/no-rsp-req
B1 :G1 === decide to cancel
G1 :G2 --> CANCEL------------------------------------> z :y1
G2 :G2 --> CANCEL------------------------------------> y1 :y1
G2 :Z <-------------------------INF_STATE/unknown <-- y1 :z
Superior cancels, inferior never decided (-:)
superior inferior
ENROL/no-rsp-req <-- i1 :b1
detect problem === b1 :m2
I1 :B1 <-------------------ENROL/no-rsp-req
B1 :N1 --> REQUEST_CONFIRM
HAZARD <-- m2 :m2
REQUEST_CONFIRM--------------------> m2 :n5
N1 :N1 --> REQUEST_CONFIRM
N1 :Z <-----------------------------HAZARD
HAZARD <-- n5 :z
REQUEST_CONFIRM--------------------> z :y1
Z :M0 <-----------------------------HAZARD
M0 :M3 === record contradiction
M3 :Z --> CONTRADICTION-----------------------------> y1 :z
Confirm requested, inferior detected problem, contradiction reported (=!:?)
superior inferior
ENROL/no-rsp-req <-- i1 :b1
RESIGN/no-rsp-req <-- b1 :z
I1 :B1 <-------------------ENROL/no-rsp-req
B1 :B1 --> SUP_STATE/active/y
B1 :D1 === decide to prepare
SUP_STATE/active/y-----------------> z :y1
D1 :D1 --> PREPARE
D1 :Z <------------------RESIGN/no-rsp-req
PREPARE----------------------------> y1 :y1
Z :Z <-------------------------INF_STATE/unknown <-- y1 :z
Nothing happens (:)
superior inferior
ENROL/no-rsp-req <-- i1 :b1
CANCELLED <-- b1 :z
I1 :B1 <-------------------ENROL/no-rsp-req
B1 :N1 --> REQUEST_CONFIRM---------------------------> z :y1
N1 :N1 --> REQUEST_CONFIRM---------------------------> y1 :y1
INF_STATE/unknown <-- y1 :z
N1 :Z XXX disruption I
X---CANCELLED
X---INF_STATE/unknown
Superior requested confirm, inferior never decided (=:)
superior inferior
ENROL/no-rsp-req <-- i1 :b1
RESIGN/rsp-req <-- b1 :c1
disruption I XXX c1 :z
I1 :B1 <-------------------ENROL/no-rsp-req
B1 :B1 --> SUP_STATE/active/y
B1 :C1 <---------------------RESIGN/rsp-req
SUP_STATE/active/y-----------------> z :y1
C1 :Z --> RESIGNED----------------------------------> y1 :y1
Z :Z <-------------------------INF_STATE/unknown <-- y1 :z
Nothing happens (:)
superior inferior
I1 :B1 <--------------------------ENROL/no-rsp-req <-- i1 :b1
INF_STATE/active/y <-- b1 :b1
CANCELLED <-- b1 :z
B1 :B1 --> SUP_STATE/active/y
B1 :B1 <-----------------INF_STATE/active/y
B1 :B1 --> SUP_STATE/active
B1 :Z <--------------------------CANCELLED
SUP_STATE/active/y-----------------> z :y1
SUP_STATE/active-------------------> y1 :y1
Z :Z <-------------------------INF_STATE/unknown <-- y1 :z
Nothing happens (:)
superior inferior
ENROL/no-rsp-req <-- i1 :b1
CANCELLED <-- b1 :z
I1 :B1 <-------------------ENROL/no-rsp-req
B1 :B1 --> SUP_STATE/active/y
B1 :B1 --> SUP_STATE/active/y
SUP_STATE/active/y-----------------> z :y1
B1 :Z <--------------------------CANCELLED
SUP_STATE/active/y-----------------> y1 :y1
Z :Z <-------------------------INF_STATE/unknown <-- y1 :z
Nothing happens (:)
superior inferior
I1 :B1 <--------------------------ENROL/no-rsp-req <-- i1 :b1
B1 :G1 === decide to cancel
G1 :G2 --> CANCEL
G2 :G2 --> CANCEL
CANCEL-----------------------------> b1 :g2
G2 :Z XXX disruption I
CANCELLED <-- g2 :z
CANCEL-----------------------------> z :y1
Z :Y1 <--------------------------CANCELLED
Y1 :Z --> SUP_STATE/unknown-------------------------> y1 :y1
Z :Z <-------------------------INF_STATE/unknown <-- y1 :z
Superior cancels, inferior never decided (-:)
superior inferior
ENROL/no-rsp-req <-- i1 :b1
disruption I XXX b1 :z
I1 :B1 <-------------------ENROL/no-rsp-req
B1 :N1 --> REQUEST_CONFIRM---------------------------> z :y1
N1 :Z <-------------------------INF_STATE/unknown <-- y1 :z
Superior requested confirm, inferior never decided (=:)
superior inferior
ENROL/no-rsp-req <-- i1 :b1
decide to be prepared === b1 :e1
decide to confirm autonomously === e1 :h1
CONFIRMED/auto <-- h1 :h1
I1 :B1 <-------------------ENROL/no-rsp-req
B1 :H1 <---------------------CONFIRMED/auto
H1 :F1 === decide to confirm
F1 :F1 --> CONFIRM-----------------------------------> h1 :h2
F1 :F1 --> CONFIRM
CONFIRMED/response <-- h2 :z
CONFIRM----------------------------> z :y2
F1 :Z0 <-----------------CONFIRMED/response
Z0 :Z === remove confirm information
disruption 0 XXX y2 :y2
Z :Z <------------------------CONFIRMED/response <-- y2 :z
Both confirm (+:#)
superior inferior
ENROL/no-rsp-req <-- i1 :b1
decide to be prepared === b1 :e1
I1 :B1 <-------------------ENROL/no-rsp-req
B1 :E1 <----------------------------------PREPARED <-- e1 :e1
decide to confirm autonomously === e1 :h1
E1 :F1 === decide to confirm
F1 :F1 --> CONFIRM-----------------------------------> h1 :h2
F1 :F1 --> CONFIRM
F1 :F1 --> CONFIRM
F1 :Z0 <------------------------CONFIRMED/response <-- h2 :z
CONFIRM----------------------------> z :y2
CONFIRM----------------------------> y2 :y2
Z0 :Z0 <------------------------CONFIRMED/response <-- y2 :z
Both confirm (+:#)
superior inferior
ENROL/no-rsp-req <-- i1 :b1
decide to be prepared === b1 :e1
decide to confirm autonomously === e1 :h1
CONFIRMED/auto <-- h1 :h1
I1 :B1 <-------------------ENROL/no-rsp-req
B1 :H1 <---------------------CONFIRMED/auto
H1 :F1 === decide to confirm
F1 :F1 --> CONFIRM
F1 :F1 --> CONFIRM
CONFIRM----------------------------> h1 :h2
CONFIRMED/response <-- h2 :z
CONFIRM----------------------------> z :y2
F1 :Z0 <-----------------CONFIRMED/response
Z0 :Z0 <------------------------CONFIRMED/response <-- y2 :z
Both confirm (+:#)
superior inferior
ENROL/no-rsp-req <-- i1 :b1
decide to be prepared/cancel === b1 :e2
I1 :B1 <-------------------ENROL/no-rsp-req
B1 :B1 --> SUP_STATE/active/y
B1 :N1 --> REQUEST_CONFIRM
decide to cancel autonomously === e2 :z1
SUP_STATE/active/y-----------------> z1 :y3
REQUEST_CONFIRM--------------------> y3 :y3
disruption 0 XXX y3 :y3
N1 :Z <---------------------------------CANCELLED <-- y3 :z1
Superior requested confirm, inferior cancelled (=:-)
superior inferior
I1 :B1 <--------------------------ENROL/no-rsp-req <-- i1 :b1
decide to be prepared/cancel === b1 :e2
B1 :B1 --> SUP_STATE/active/y
B1 :G1 === decide to cancel
decide to cancel autonomously === e2 :z1
G1 :G2 --> CANCEL
SUP_STATE/active/y-----------------> z1 :y3
CANCEL-----------------------------> y3 :z
G2 :Z XXX disruption I
Both cancel (-:-)
superior inferior
ENROL/no-rsp-req <-- i1 :b1
decide to be prepared/cancel === b1 :e2
PREPARED/cancel <-- e2 :e2
I1 :B1 <-------------------ENROL/no-rsp-req
B1 :E2 <--------------------PREPARED/cancel
E2 :F1 === decide to confirm
decide to cancel autonomously === e2 :z1
F1 :F1 --> CONFIRM-----------------------------------> z1 :y3
F1 :F1 --> CONFIRM-----------------------------------> y3 :y3
F1 :K0 <---------------------------------CANCELLED <-- y3 :z1
K0 :K1 === record contradiction
K1 :Z XXX disruption I
Superior confirms, inferior cancelled - contradiction reported (+!:-)
superior inferior
I1 :B1 <--------------------------ENROL/no-rsp-req <-- i1 :b1
decide to be prepared/cancel === b1 :e2
PREPARED/cancel <-- e2 :e2
decide to cancel autonomously === e2 :z1
B1 :E2 <--------------------PREPARED/cancel
E2 :F1 === decide to confirm
F1 :F1 --> CONFIRM-----------------------------------> z1 :y3
CANCELLED <-- y3 :z1
F1 :F1 --> CONFIRM
F1 :K0 <--------------------------CANCELLED
CONFIRM----------------------------> z1 :y3
K0 :K1 === record contradiction
K1 :Z --> CONTRADICTION-----------------------------> y3 :z
Superior confirms, inferior cancelled - contradiction reported (+!:-)
superior inferior
ENROL/no-rsp-req <-- i1 :b1
decide to be prepared/cancel === b1 :e2
I1 :B1 <-------------------ENROL/no-rsp-req
decide to cancel autonomously === e2 :z1
B1 :B1 --> SUP_STATE/active/y
B1 :D1 === decide to prepare
SUP_STATE/active/y-----------------> z1 :y3
D1 :D1 --> PREPARE-----------------------------------> y3 :y3
D1 :Z <---------------------------------CANCELLED <-- y3 :z1
superior never decided, inferior cancelled (:-)
superior inferior
I1 :B1 <--------------------------ENROL/no-rsp-req <-- i1 :b1
decide to be prepared/cancel === b1 :e2
decide to cancel autonomously === e2 :z1
B1 :B1 --> SUP_STATE/active/y------------------------> z1 :y3
B1 :N1 --> REQUEST_CONFIRM---------------------------> y3 :y3
N1 :Z <---------------------------------CANCELLED <-- y3 :z1
Superior requested confirm, inferior cancelled (=:-)
superior inferior
ENROL/no-rsp-req <-- i1 :b1
INF_STATE/active/y <-- b1 :b1
I1 :B1 <-------------------ENROL/no-rsp-req
decide to be prepared/cancel === b1 :e2
B1 :B1 --> SUP_STATE/active/y
B1 :B1 <-----------------INF_STATE/active/y
B1 :B1 --> SUP_STATE/active
decide to cancel autonomously === e2 :z1
SUP_STATE/active/y-----------------> z1 :y3
SUP_STATE/active-------------------> y3 :y3
B1 :Z <---------------------------------CANCELLED <-- y3 :z1
superior never decided, inferior cancelled (:-)
superior inferior
ENROL/no-rsp-req <-- i1 :b1
decide to be prepared/cancel === b1 :e2
decide to cancel autonomously === e2 :z1
I1 :B1 <-------------------ENROL/no-rsp-req
B1 :B1 --> SUP_STATE/active/y------------------------> z1 :y3
B1 :B1 --> SUP_STATE/active/y------------------------> y3 :y3
B1 :Z <---------------------------------CANCELLED <-- y3 :z1
superior never decided, inferior cancelled (:-)
superior inferior
I1 :I1 XXX disruption 0
ENROL/no-rsp-req <-- i1 :b1
INF_STATE/active/y <-- b1 :b1
decide to be prepared/cancel === b1 :e2
PREPARED/cancel <-- e2 :e2
PREPARED/cancel <-- e2 :e2
decide to cancel autonomously === e2 :z1
I1 :B1 <-------------------ENROL/no-rsp-req
B1 :B1 --> SUP_STATE/active/y
B1 :B1 <-----------------INF_STATE/active/y
B1 :E2 <--------------------PREPARED/cancel
E2 :E2 --> SUP_STATE/preparedreceived
E2 :E2 <--------------------PREPARED/cancel
E2 :Z === decide to cancel
SUP_STATE/active/y-----------------> z1 :y3
SUP_STATE/preparedreceived---------> y3 :y3
Z :Y1 <---------------------------------CANCELLED <-- y3 :z1
Y1 :Z --> SUP_STATE/unknown-------------------------> z1 :z
Both cancel (-:-)
superior inferior
ENROL/no-rsp-req <-- i1 :b1
decide to be prepared/cancel === b1 :e2
I1 :B1 <-------------------ENROL/no-rsp-req
PREPARED/cancel <-- e2 :e2
decide to cancel autonomously === e2 :z1
B1 :B1 --> SUP_STATE/active/y------------------------> z1 :y3
B1 :E2 <--------------------PREPARED/cancel
E2 :E2 --> SUP_STATE/preparedreceived/y--------------> y3 :y3
E2 :N1 --> REQUEST_CONFIRM---------------------------> y3 :y3
N1 :Z <---------------------------------CANCELLED <-- y3 :z1
Superior requested confirm, inferior cancelled (=:-)
superior inferior
ENROL/no-rsp-req <-- i1 :b1
decide to be prepared/cancel === b1 :e2
I1 :B1 <-------------------ENROL/no-rsp-req
B1 :E2 <---------------------------PREPARED/cancel <-- e2 :e2
E2 :E2 --> SUP_STATE/preparedreceived/y
E2 :Z === decide to cancel
PREPARED/cancel <-- e2 :e2
decide to cancel autonomously === e2 :z1
Z :Y1 <--------------------PREPARED/cancel
SUP_STATE/preparedreceived/y-------> z1 :y3
Y1 :Z --> SUP_STATE/unknown-------------------------> y3 :y3
Z :Y1 <---------------------------------CANCELLED <-- y3 :z1
Y1 :Z --> SUP_STATE/unknown-------------------------> z1 :z
Both cancel (-:-)
superior inferior
I1 :B1 <--------------------------ENROL/no-rsp-req <-- i1 :b1
B1 :B1 --> SUP_STATE/active/y
decide to be prepared/cancel === b1 :e2
decide to cancel autonomously === e2 :z1
SUP_STATE/active/y-----------------> z1 :y3
B1 :Z <---------------------------------CANCELLED <-- y3 :z1
superior never decided, inferior cancelled (:-)
superior inferior
ENROL/no-rsp-req <-- i1 :b1
decide to be prepared/cancel === b1 :e2
decide to cancel autonomously === e2 :z1
I1 :B1 <-------------------ENROL/no-rsp-req
B1 :G1 === decide to cancel
disruption 0 XXX z1 :z1
G1 :Z XXX disruption I
Both cancel (-:-)
superior inferior
I1 :B1 <--------------------------ENROL/no-rsp-req <-- i1 :b1
B1 :G1 === decide to cancel
decide to be prepared/cancel === b1 :e2
G1 :G2 --> CANCEL
decide to cancel autonomously === e2 :z1
CANCEL-----------------------------> z1 :y1
G2 :Z <-------------------------INF_STATE/unknown <-- y1 :z
Both cancel (-:-)
superior inferior
ENROL/no-rsp-req <-- i1 :b1
decide to be prepared/cancel === b1 :e2
PREPARED/cancel <-- e2 :e2
decide to cancel autonomously === e2 :z1
I1 :B1 <-------------------ENROL/no-rsp-req
B1 :E2 <--------------------PREPARED/cancel
E2 :F1 === decide to confirm
F1 :F1 --> CONFIRM-----------------------------------> z1 :y3
F1 :K0 <---------------------------------CANCELLED <-- y3 :z1
K0 :K1 === record contradiction
K1 :Z XXX disruption I
Superior confirms, inferior cancelled - contradiction reported (+!:-)
superior inferior
ENROL/no-rsp-req <-- i1 :b1
decide to be prepared/cancel === b1 :e2
PREPARED/cancel <-- e2 :e2
decide to cancel autonomously === e2 :z1
I1 :B1 <-------------------ENROL/no-rsp-req
B1 :E2 <--------------------PREPARED/cancel
E2 :F1 === decide to confirm
F1 :F1 --> CONFIRM-----------------------------------> z1 :y3
F1 :K0 <---------------------------------CANCELLED <-- y3 :z1
K0 :K1 === record contradiction
K1 :Z --> CONTRADICTION-----------------------------> z1 :z
Superior confirms, inferior cancelled - contradiction reported (+!:-)
superior inferior
ENROL/no-rsp-req <-- i1 :b1
decide to be prepared/cancel === b1 :e2
decide to cancel autonomously === e2 :z1
I1 :B1 <-------------------ENROL/no-rsp-req
B1 :D1 === decide to prepare
D1 :D1 --> PREPARE
D1 :Z XXX disruption I
PREPARE----------------------------> z1 :z1
superior never decided, inferior cancelled (:-)
superior inferior
ENROL/no-rsp-req <-- i1 :b1
decide to be prepared/cancel === b1 :e2
I1 :B1 <-------------------ENROL/no-rsp-req
B1 :N1 --> REQUEST_CONFIRM
decide to cancel autonomously === e2 :z1
REQUEST_CONFIRM--------------------> z1 :y1
N1 :Z <-------------------------INF_STATE/unknown <-- y1 :z
Superior requested confirm, inferior cancelled (=:-)
superior inferior
I1 :B1 <--------------------------ENROL/no-rsp-req <-- i1 :b1
INF_STATE/active/y <-- b1 :b1
decide to be prepared/cancel === b1 :e2
B1 :B1 <-----------------INF_STATE/active/y
B1 :B1 --> SUP_STATE/active
decide to cancel autonomously === e2 :z1
SUP_STATE/active-------------------> z1 :z1
B1 :G1 === decide to cancel
G1 :Z XXX disruption I
Both cancel (-:-)
superior inferior
ENROL/no-rsp-req <-- i1 :b1
decide to be prepared/cancel === b1 :e2
decide to cancel autonomously === e2 :z1
I1 :B1 <-------------------ENROL/no-rsp-req
B1 :B1 --> SUP_STATE/active/y------------------------> z1 :y3
B1 :Z <---------------------------------CANCELLED <-- y3 :z1
superior never decided, inferior cancelled (:-)
superior inferior
ENROL/no-rsp-req <-- i1 :b1
INF_STATE/active/y <-- b1 :b1
decide to be prepared/cancel === b1 :e2
I1 :B1 <-------------------ENROL/no-rsp-req
PREPARED/cancel <-- e2 :e2
B1 :B1 <-----------------INF_STATE/active/y
B1 :E2 <--------------------PREPARED/cancel
decide to cancel autonomously === e2 :z1
E2 :E2 --> SUP_STATE/preparedreceived----------------> z1 :y3
E2 :Z === decide to cancel
Z :Y1 <---------------------------------CANCELLED <-- y3 :z1
Y1 :Z --> SUP_STATE/unknown-------------------------> z1 :z
Both cancel (-:-)
superior inferior
ENROL/no-rsp-req <-- i1 :b1
decide to be prepared/cancel === b1 :e2
PREPARED/cancel <-- e2 :e2
I1 :B1 <-------------------ENROL/no-rsp-req
decide to cancel autonomously === e2 :z1
B1 :E2 <--------------------PREPARED/cancel
E2 :E2 --> SUP_STATE/preparedreceived/y
E2 :N1 --> REQUEST_CONFIRM
SUP_STATE/preparedreceived/y-------> z1 :y3
REQUEST_CONFIRM--------------------> y3 :y3
N1 :Z <---------------------------------CANCELLED <-- y3 :z1
Superior requested confirm, inferior cancelled (=:-)
superior inferior
ENROL/no-rsp-req <-- i1 :b1
decide to be prepared/cancel === b1 :e2
I1 :Z XXX disruption I
X---ENROL/no-rsp-req
Z :Y1 <---------------------------PREPARED/cancel <-- e2 :e2
decide to cancel autonomously === e2 :z1
Y1 :Z --> SUP_STATE/unknown-------------------------> z1 :z
superior never decided, inferior cancelled (:-)
superior inferior
ENROL/no-rsp-req <-- i1 :b1
CANCELLED <-- b1 :z
disruption 0 XXX z :z
I1 :B1 <-------------------ENROL/no-rsp-req
B1 :Z <--------------------------CANCELLED
Nothing happens (:)
superior inferior
ENROL/no-rsp-req <-- i1 :b1
CANCELLED <-- b1 :z
I1 :B1 <-------------------ENROL/no-rsp-req
B1 :G1 === decide to cancel
G1 :J2 <--------------------------CANCELLED
J2 :Z --> CANCEL------------------------------------> z :y1
Z :Z <-------------------------INF_STATE/unknown <-- y1 :z
Superior cancels, inferior never decided (-:)
superior inferior
ENROL/no-rsp-req <-- i1 :b1
decide to be prepared === b1 :e1
PREPARED <-- e1 :e1
I1 :B1 <-------------------ENROL/no-rsp-req
B1 :E1 <---------------------------PREPARED
E1 :F1 === decide to confirm
decide to confirm autonomously === e1 :h1
F1 :F1 --> CONFIRM-----------------------------------> h1 :h2
F1 :F1 --> CONFIRM
CONFIRMED/response <-- h2 :z
CONFIRM----------------------------> z :y2
F1 :Z0 <-----------------CONFIRMED/response
Z0 :Z0 <------------------------CONFIRMED/response <-- y2 :z
Both confirm (+:#)
superior inferior
I1 :A1 <-----------------------------ENROL/rsp-req <-- i1 :a1
detect problem === a1 :m2
A1 :M0 <------------------------------------HAZARD <-- m2 :m2
M0 :M3 === record contradiction
disruption I XXX m2 :z
M3 :Z --> CONTRADICTION-----------------------------> z :z
Inferior detected problem, contradiction reported (!:?)
superior inferior
I1 :A1 <-----------------------------ENROL/rsp-req <-- i1 :a1
disruption I XXX a1 :z
A1 :B1 --> ENROLLED----------------------------------> z :z
B1 :Z XXX disruption I
Nothing happens (:)
superior inferior
ENROL/no-rsp-req <-- i1 :b1
RESIGN/no-rsp-req <-- b1 :z
I1 :B1 <-------------------ENROL/no-rsp-req
B1 :D1 === decide to prepare
D1 :D1 --> PREPARE
D1 :Z <------------------RESIGN/no-rsp-req
PREPARE----------------------------> z :y1
Z :Z <-------------------------INF_STATE/unknown <-- y1 :z
Nothing happens (:)
superior inferior
ENROL/no-rsp-req <-- i1 :b1
disruption I XXX b1 :z
I1 :B1 <-------------------ENROL/no-rsp-req
B1 :N1 --> REQUEST_CONFIRM---------------------------> z :y1
N1 :Z <-------------------------INF_STATE/unknown <-- y1 :z
Superior requested confirm, inferior never decided (=:)
superior inferior
I1 :B1 <--------------------------ENROL/no-rsp-req <-- i1 :b1
B1 :C1 <----------------------------RESIGN/rsp-req <-- b1 :c1
disruption I XXX c1 :z
C1 :Z --> RESIGNED----------------------------------> z :z
Nothing happens (:)
superior inferior
ENROL/no-rsp-req <-- i1 :b1
INF_STATE/active/y <-- b1 :b1
CANCELLED <-- b1 :z
I1 :B1 <-------------------ENROL/no-rsp-req
B1 :B1 <-----------------INF_STATE/active/y
B1 :B1 --> SUP_STATE/active--------------------------> z :z
B1 :Z <--------------------------CANCELLED
Nothing happens (:)
superior inferior
ENROL/no-rsp-req <-- i1 :b1
CANCELLED <-- b1 :z
I1 :B1 <-------------------ENROL/no-rsp-req
B1 :B1 --> SUP_STATE/active/y
B1 :Z <--------------------------CANCELLED
SUP_STATE/active/y-----------------> z :y1
Z :Z <-------------------------INF_STATE/unknown <-- y1 :z
Nothing happens (:)
superior inferior
ENROL/no-rsp-req <-- i1 :b1
CANCELLED <-- b1 :z
I1 :Z XXX disruption I
X---ENROL/no-rsp-req
Z :Y1 <--------------------------CANCELLED
Y1 :Z --> SUP_STATE/unknown-------------------------> z :z
Nothing happens (:)