Example of A1:disruption 0

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 (:)

Example of A1:disruption I

superior                                              inferior
I1 :A1  <-----------------------------ENROL/rsp-req <-- i1 :a1 
                                       disruption I XXX a1 :z  
A1 :Z   XXX disruption I           

Nothing happens (:)

Example of A1:receive HAZARD

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 (:?)

Example of A1:receive INF_STATE/active/y

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 (:)

Example of A1:send ENROLLED

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 (:)

Example of B1:decide to cancel

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 (-:)

Example of B1:decide to prepare

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 (:)

Example of B1:disruption 0

superior                                              inferior
I1 :B1  <--------------------------ENROL/no-rsp-req <-- i1 :b1 
                                          CANCELLED <-- b1 :z  
B1 :B1  XXX disruption 0           
B1 :Z   <--------------------------CANCELLED

Nothing happens (:)

Example of B1:disruption I

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 (:)

Example of B1:receive CANCELLED

superior                                              inferior
                                   ENROL/no-rsp-req <-- i1 :b1 
                                          CANCELLED <-- b1 :z  
I1 :B1  <-------------------ENROL/no-rsp-req
B1 :Z   <--------------------------CANCELLED

Nothing happens (:)

Example of B1:receive CONFIRMED/auto

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 (-!:#)

Example of B1:receive HAZARD

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 (:?)

Example of B1:receive INF_STATE/active

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 (:)

Example of B1:receive INF_STATE/active/y

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 (:)

Example of B1:receive INF_STATE/unknown

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 (:)

Example of B1:receive PREPARED

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 (=:-)

Example of B1:receive PREPARED/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   === decide to cancel           

Both cancel (-:-)

Example of B1:receive RESIGN/no-rsp-req

superior                                              inferior
I1 :B1  <--------------------------ENROL/no-rsp-req <-- i1 :b1 
B1 :Z   <-------------------------RESIGN/no-rsp-req <-- b1 :z  

Nothing happens (:)

Example of B1:receive RESIGN/rsp-req

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 (:)

Example of B1:send REQUEST_CONFIRM

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 (=:)

Example of B1:send SUP_STATE/active

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 (:)

Example of B1:send SUP_STATE/active/y

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 (:)

Example of C1:disruption 0

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 (:)

Example of C1:disruption I

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 (:)

Example of C1:receive INF_STATE/unknown

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 (=:)

Example of C1:receive RESIGN/no-rsp-req

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 (:)

Example of C1:receive RESIGN/rsp-req

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 (:)

Example of C1:send RESIGNED

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 (:)

Example of D1:decide to cancel

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 (-:)

Example of D1:disruption 0

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 (:)

Example of D1:disruption I

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 (:)

Example of D1:receive CANCELLED

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 (:)

Example of D1:receive CONFIRMED/auto

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 (-!:#)

Example of D1:receive HAZARD

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 (:?)

Example of D1:receive INF_STATE/active

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 (:)

Example of D1:receive INF_STATE/active/y

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 (:)

Example of D1:receive INF_STATE/unknown

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 (:?)

Example of D1:receive PREPARED

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 (=:#)

Example of D1:receive PREPARED/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 :D1  === decide to prepare           
D1 :E2  <--------------------PREPARED/cancel
E2 :Z   === decide to cancel           

Both cancel (-:-)

Example of D1:receive RESIGN/no-rsp-req

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 (:)

Example of D1:receive RESIGN/rsp-req

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 (:)

Example of D1:send PREPARE

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 (:)

Example of E1:decide to 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 :G1  === decide to cancel           
G1 :G2  --> CANCEL                                             
G2 :Z   <---------------------------------CANCELLED <-- j1 :j2 
                   CANCEL-----------------------------> j2 :z  

Both cancel (-:-)

Example of E1:decide to 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 :Z0  <------------------------CONFIRMED/response <-- h2 :z  

Both confirm (+:#)

Example of E1:decide to prepare

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 (=:-)

Example of E1:disruption 0

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 (-:-)

Example of E1:disruption I

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 (:-)

Example of E1:disruption II

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 (-:-)

Example of E1:disruption III

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 (=:-)

Example of E1:receive 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 (-:-)

Example of E1:receive CONFIRMED/auto

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 (-!:#)

Example of E1:receive HAZARD

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 (!:?)

Example of E1:receive PREPARED

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 (=:#)

Example of E1:send PREPARE

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 (=:?)

Example of E1:send REQUEST_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 
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 (=:?)

Example of E1:send SUP_STATE/preparedreceived

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 (=:#)

Example of E1:send SUP_STATE/preparedreceived/y

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 (=:-)

Example of E2:decide to cancel

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 (-:-)

Example of E2:decide to 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  --> CONFIRM-----------------------------------> e2 :f1 
                         apply ordered confirmation === f1 :f2 
F1 :Z0  <------------------------CONFIRMED/response <-- f2 :z  

Confirm ordered and applied (+:+)

Example of E2:decide to prepare

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 (-:-)

Example of E2:disruption 0

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 (-:-)

Example of E2:disruption I

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 (:-)

Example of E2:disruption II

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 (-:-)

Example of E2:disruption III

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 (-:-)

Example of E2:receive CANCELLED

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 (:-)

Example of E2:receive HAZARD

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 (!:?)

Example of E2:receive PREPARED/cancel

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 (-:-)

Example of E2:send PREPARE

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 (-:-)

Example of E2:send REQUEST_CONFIRM

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 (=:-)

Example of E2:send SUP_STATE/preparedreceived

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 (-:-)

Example of E2:send SUP_STATE/preparedreceived/y

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 (-:-)

Example of F1:disruption 0

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 (+:#)

Example of F1:receive 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
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 (+!:-)

Example of F1:receive CONFIRMED/auto

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 (+:#)

Example of F1:receive CONFIRMED/response

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 (+:#)

Example of F1:receive HAZARD

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 (+!:?)

Example of F1:receive PREPARED

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 (+:#)

Example of F1:receive PREPARED/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  <---------------------------PREPARED/cancel <-- e2 :e2 
F1 :F1  --> CONFIRM-----------------------------------> e2 :f1 
                         apply ordered confirmation === f1 :f2 
F1 :Z0  <------------------------CONFIRMED/response <-- f2 :z  

Confirm ordered and applied (+:+)

Example of F1:send 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 (+:#)

Example of G1:disruption 0

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 (-:)

Example of G1:disruption I

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 (-:)

Example of G1:receive CANCELLED

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 (-:)

Example of G1:receive CONFIRMED/auto

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 (-!:#)

Example of G1:receive HAZARD

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 (-:?)

Example of G1:receive INF_STATE/active

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 (-:)

Example of G1:receive INF_STATE/active/y

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 (-:)

Example of G1:receive INF_STATE/unknown

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 (-:)

Example of G1:receive PREPARED

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 (-:-)

Example of G1:receive PREPARED/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 (-:-)

Example of G1:receive RESIGN/no-rsp-req

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 (-:)

Example of G1:receive RESIGN/rsp-req

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 (-:)

Example of G1:send 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 (-:)

Example of G2:disruption 0

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 (-:)

Example of G2:disruption I

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 (-:-)

Example of G2:receive CANCELLED

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 (-:)

Example of G2:receive CONFIRMED/auto

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 (-!:#)

Example of G2:receive HAZARD

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 (-:?)

Example of G2:receive INF_STATE/active

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 (-:)

Example of G2:receive INF_STATE/active/y

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 (-:)

Example of G2:receive INF_STATE/unknown

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 (-:-)

Example of G2:receive PREPARED

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 (-:)

Example of G2:receive PREPARED/cancel

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 (-:)

Example of G2:receive RESIGN/no-rsp-req

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 (-:)

Example of G2:receive RESIGN/rsp-req

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 (-:)

Example of G2:send CANCEL

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 (-:)

Example of G3:disruption 0

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 (-:)

Example of G3:disruption I

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 (-:)

Example of G3:receive RESIGN/no-rsp-req

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 (-:)

Example of G3:receive RESIGN/rsp-req

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 (-:)

Example of G3:send CANCEL

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 (-:)

Example of H1:decide to cancel

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 (-!:#)

Example of H1:decide to 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 (+:#)

Example of H1:disruption 0

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 (-!:#)

Example of H1:disruption I

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 (!:#)

Example of H1:disruption II

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 (=:#)

Example of H1:disruption III

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 (+:#)

Example of H1:disruption IV

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 (=:#)

Example of H1:receive CONFIRMED/auto

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 (-!:#)

Example of I1:disruption 0

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 (:)

Example of I1:disruption I

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 (:)

Example of I1:receive CANCELLED

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 (:)

Example of I1:receive CONFIRMED/auto

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 (!:#)

Example of I1:receive ENROL/no-rsp-req

superior                                              inferior
                                   ENROL/no-rsp-req <-- i1 :b1 
                                          CANCELLED <-- b1 :z  
I1 :B1  <-------------------ENROL/no-rsp-req
B1 :Z   <--------------------------CANCELLED

Nothing happens (:)

Example of I1:receive ENROL/rsp-req

superior                                              inferior
I1 :A1  <-----------------------------ENROL/rsp-req <-- i1 :a1 
                                       disruption I XXX a1 :z  
A1 :Z   XXX disruption I           

Nothing happens (:)

Example of I1:receive HAZARD

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 (!:?)

Example of I1:receive INF_STATE/active/y

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 (:)

Example of I1:receive PREPARED

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 (:-)

Example of I1:receive PREPARED/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 (:)

Example of I1:receive RESIGN/no-rsp-req

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 (:)

Example of I1:receive RESIGN/rsp-req

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 (:)

Example of J1:decide to cancel

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 (-:-)

Example of J1:decide to confirm

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 (+!:-)

Example of J1:disruption 0

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 (-:-)

Example of J1:disruption I

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 (:-)

Example of J1:disruption II

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 (=:-)

Example of J1:disruption III

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 (:-)

Example of J1:disruption IV

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 (-:-)

Example of J1:receive 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
                                          CANCELLED <-- j2 :j2 
E1 :J1  <--------------------------CANCELLED
J1 :J1  <--------------------------CANCELLED
J1 :J2  === decide to cancel           
J2 :Z   --> CANCEL------------------------------------> j2 :z  

Both cancel (-:-)

Example of J2:disruption 0

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 (-:)

Example of J2:disruption I

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 (-:)

Example of J2:disruption II

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 (-:)

Example of J2:disruption III

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 (-:)

Example of J2:receive 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 :G1  === decide to cancel           
G1 :J2  <---------------------------------CANCELLED <-- j1 :j2 
J2 :J2  <---------------------------------CANCELLED <-- j2 :j2 
J2 :Z   --> CANCEL------------------------------------> j2 :z  

Both cancel (-:-)

Example of J2:receive INF_STATE/unknown

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 (-:)

Example of J2:send CANCEL

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 (-:)

Example of K0:disruption 0

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 (+!:-)

Example of K0:disruption I

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 (+!:-)

Example of K0:receive 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
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 (+!:-)

Example of K0:record contradiction

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 (+!:-)

Example of K1:disruption 0

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 (+!:-)

Example of K1:disruption I

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 (+!:-)

Example of K1:receive CANCELLED

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 (+!:-)

Example of K1:send CONTRADICTION

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 (+!:-)

Example of L0:disruption 0

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 (-!:#)

Example of L0:disruption I

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 (-!:#)

Example of L0:disruption II

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 (-!:#)

Example of L0:receive CONFIRMED/auto

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 (-!:#)

Example of L0:record contradiction

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 (-!:#)

Example of L1:disruption 0

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 (-!:#)

Example of L1:disruption I

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 (-!:#)

Example of L1:receive CONFIRMED/auto

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 (-!:#)

Example of L1:send CONTRADICTION

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 (-!:#)

Example of L2:disruption 0

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 (!:#)

Example of L2:disruption I

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 (-!:#)

Example of L2:receive CONFIRMED/auto

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 (!:#)

Example of L2:record contradiction

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 (!:#)

Example of M0:disruption 0

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 (!:?)

Example of M0:disruption I

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 (:?)

Example of M0:receive 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 (:?)

Example of M0:receive INF_STATE/unknown

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 (!:?)

Example of M0:record contradiction

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 (!:?)

Example of M1:disruption 0

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 (+!:!)

Example of M1:disruption I

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 (+!:!)

Example of M1:disruption II

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 (+!:!)

Example of M1:receive HAZARD

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 (+!:?)

Example of M1:record contradiction

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 (+!:?)

Example of M2:disruption 0

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 (-!:?)

Example of M2:disruption I

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 (-:?)

Example of M2:disruption II

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 (-:?)

Example of M2:receive 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 (-:?)

Example of M2:receive INF_STATE/unknown

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 (-!:?)

Example of M2:record contradiction

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 (-!:?)

Example of M3:disruption 0

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 (!:?)

Example of M3:disruption I

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 (!:?)

Example of M3:receive HAZARD

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 (!:?)

Example of M3:receive INF_STATE/unknown

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 (=!:?)

Example of M3:send CONTRADICTION

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 (!:?)

Example of N1:disruption 0

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 (=:)

Example of N1:disruption I

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 (=:-)

Example of N1:receive 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 (=:)

Example of N1:receive CONFIRMED/auto

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 (=:#)

Example of N1:receive CONFIRMED/response

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 (=:#)

Example of N1:receive HAZARD

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 (=:?)

Example of N1:receive INF_STATE/active

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 (=:!)

Example of N1:receive INF_STATE/active/y

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 (=:)

Example of N1:receive INF_STATE/unknown

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 (=:)

Example of N1:receive PREPARED

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 (=:#)

Example of N1:receive PREPARED/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 :N1  --> REQUEST_CONFIRM                                    
N1 :N1  <--------------------PREPARED/cancel
                   REQUEST_CONFIRM--------------------> z1 :y1 
N1 :Z   <-------------------------INF_STATE/unknown <-- y1 :z  

Superior requested confirm, inferior cancelled (=:-)

Example of N1:receive RESIGN/no-rsp-req

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 (=:)

Example of N1:receive RESIGN/rsp-req

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 (=:)

Example of N1:send REQUEST_CONFIRM

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 (=:?)

Example of Y1:disruption 0

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 (:)

Example of Y1:receive CANCELLED

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 (:)

Example of Y1:receive CONFIRMED/auto

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 (!:#)

Example of Y1:receive HAZARD

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 (!:?)

Example of Y1:receive INF_STATE/active/y

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 (:)

Example of Y1:receive INF_STATE/unknown

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 (=:)

Example of Y1:receive PREPARED

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 (:-)

Example of Y1:receive PREPARED/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 
                                    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 (:-)

Example of Y1:receive RESIGN/no-rsp-req

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 (:)

Example of Y1:receive RESIGN/rsp-req

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 (:)

Example of Y1:send SUP_STATE/unknown

superior                                              inferior
I1 :Z   XXX disruption I           
Z  :Y1  <-----------------------------ENROL/rsp-req <-- i1 :a1 
Y1 :Z   --> SUP_STATE/unknown-------------------------> a1 :z  

Nothing happens (:)

Example of Z0:disruption 0

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 (+:#)

Example of Z0:receive CONFIRMED/response

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 (+:#)

Example of Z0:remove confirm information

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 (+:#)

Example of Z:disruption 0

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 (:)

Example of Z:receive CANCELLED

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 (:)

Example of Z:receive CONFIRMED/auto

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 (!:#)

Example of Z:receive CONFIRMED/response

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 (=:#)

Example of Z:receive ENROL/no-rsp-req

superior                                              inferior
I1 :Z   XXX disruption I           
Z  :Z   <--------------------------ENROL/no-rsp-req <-- i1 :b1 
                                       disruption I XXX b1 :z  

Nothing happens (:)

Example of Z:receive ENROL/rsp-req

superior                                              inferior
I1 :Z   XXX disruption I           
Z  :Y1  <-----------------------------ENROL/rsp-req <-- i1 :a1 
Y1 :Z   --> SUP_STATE/unknown-------------------------> a1 :z  

Nothing happens (:)

Example of Z:receive HAZARD

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 (!:?)

Example of Z:receive INF_STATE/active

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 (=:-)

Example of Z:receive INF_STATE/active/y

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 (:)

Example of Z:receive INF_STATE/unknown

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 (=:)

Example of Z:receive PREPARED

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 (:)

Example of Z:receive PREPARED/cancel

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 (:-)

Example of Z:receive RESIGN/no-rsp-req

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 (:)

Example of Z:receive RESIGN/rsp-req

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 (:)

Example of a1:detect problem

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 (:?)

Example of a1:disruption 0

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 (:)

Example of a1:disruption I

superior                                              inferior
                                      ENROL/rsp-req <-- i1 :a1 
I1 :Z   XXX disruption I           
                                       disruption I XXX a1 :z  
                               X---ENROL/rsp-req

Nothing happens (:)

Example of a1:receive CANCEL

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 (-:)

Example of a1:receive ENROLLED

superior                                              inferior
I1 :A1  <-----------------------------ENROL/rsp-req <-- i1 :a1 
A1 :B1  --> ENROLLED----------------------------------> a1 :b1 
B1 :Z   <---------------------------------CANCELLED <-- b1 :z  

Nothing happens (:)

Example of a1:receive PREPARE

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 (:)

Example of a1:receive REQUEST_CONFIRM

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 (=:!)

Example of a1:receive SUP_STATE/active/y

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 (=:)

Example of a1:receive SUP_STATE/unknown

superior                                              inferior
I1 :Z   XXX disruption I           
Z  :Y1  <-----------------------------ENROL/rsp-req <-- i1 :a1 
Y1 :Z   --> SUP_STATE/unknown-------------------------> a1 :z  

Nothing happens (:)

Example of a1:send INF_STATE/active/y

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 (:)

Example of b1:decide to be prepared

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 (=:#)

Example of b1:decide to be prepared/cancel

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 (:-)

Example of b1:detect problem

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 (:?)

Example of b1:disruption 0

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 (:)

Example of b1:disruption I

superior                                              inferior
I1 :Z   XXX disruption I           
Z  :Z   <--------------------------ENROL/no-rsp-req <-- i1 :b1 
                                       disruption I XXX b1 :z  

Nothing happens (:)

Example of b1:receive 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 (-:)

Example of b1:receive PREPARE

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 (:)

Example of b1:receive REQUEST_CONFIRM

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 (=:)

Example of b1:receive SUP_STATE/active

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 (:)

Example of b1:receive SUP_STATE/active/y

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 (:)

Example of b1:receive SUP_STATE/unknown

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 (:)

Example of b1:send CANCELLED

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 (:)

Example of b1:send INF_STATE/active

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 (:)

Example of b1:send INF_STATE/active/y

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 (:)

Example of b1:send RESIGN/no-rsp-req

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 (:)

Example of b1:send RESIGN/rsp-req

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 (:)

Example of c1:disruption 0

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 (:)

Example of c1:disruption I

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 (:)

Example of c1:receive CANCEL

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 (-:)

Example of c1:receive PREPARE

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 (:)

Example of c1:receive REQUEST_CONFIRM

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 (=:)

Example of c1:receive RESIGNED

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 (:)

Example of c1:receive SUP_STATE/active

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 (:)

Example of c1:receive SUP_STATE/active/y

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 (:)

Example of c1:receive SUP_STATE/unknown

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 (:)

Example of c1:send RESIGN/no-rsp-req

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 (:)

Example of c1:send RESIGN/rsp-req

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 (:)

Example of d1:decide to be prepared

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 (-:-)

Example of d1:decide to be prepared/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 (-:-)

Example of d1:detect problem

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 (!:?)

Example of d1:disruption 0

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 (-:)

Example of d1:disruption I

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 (-:)

Example of d1:receive CANCEL

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 (-:)

Example of d1:receive PREPARE

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 (:)

Example of d1:send CANCELLED

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 (:)

Example of d1:send INF_STATE/active

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 (:)

Example of d1:send INF_STATE/active/y

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 (:)

Example of d1:send RESIGN/no-rsp-req

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 (:)

Example of d1:send RESIGN/rsp-req

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 (:)

Example of e1:decide to cancel autonomously

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 (=:-)

Example of e1:decide to confirm autonomously

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 (=:#)

Example of e1:detect problem

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 (=:?)

Example of e1:disruption 0

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 (:-)

Example of e1:receive CANCEL

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 (-:)

Example of e1:receive 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           
F1 :F1  --> CONFIRM-----------------------------------> e1 :f0 
                         apply ordered confirmation === f0 :f2 
F1 :Z0  <------------------------CONFIRMED/response <-- f2 :z  

Confirm ordered and applied (+:+)

Example of e1:receive PREPARE

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 (-:-)

Example of e1:receive REQUEST_CONFIRM

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 (=:#)

Example of e1:receive SUP_STATE/active

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 (=:-)

Example of e1:receive SUP_STATE/active/y

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 (=:#)

Example of e1:receive SUP_STATE/preparedreceived

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 (=:#)

Example of e1:receive SUP_STATE/preparedreceived/y

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 (=:#)

Example of e1:receive SUP_STATE/unknown

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 (:)

Example of e1:send PREPARED

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 (:)

Example of e2:decide to cancel autonomously

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 (:-)

Example of e2:detect problem

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 (=:?)

Example of e2:disruption 0

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 (:-)

Example of e2:receive CANCEL

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 (-:)

Example of e2:receive 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  --> CONFIRM-----------------------------------> e2 :f1 
                         apply ordered confirmation === f1 :f2 
F1 :Z0  <------------------------CONFIRMED/response <-- f2 :z  

Confirm ordered and applied (+:+)

Example of e2:receive PREPARE

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 (:-)

Example of e2:receive REQUEST_CONFIRM

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 (=:-)

Example of e2:receive SUP_STATE/active

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 (-:-)

Example of e2:receive SUP_STATE/active/y

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 (:-)

Example of e2:receive SUP_STATE/preparedreceived

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 (-:-)

Example of e2:receive SUP_STATE/preparedreceived/y

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 (-:-)

Example of e2:receive SUP_STATE/unknown

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 (:)

Example of e2:send PREPARED/cancel

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 (-:-)

Example of f0:apply ordered confirmation

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 (+:+)

Example of f0:detect problem

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 (+!:!)

Example of f0:disruption 0

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 (+!:?)

Example of f0:disruption I

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 (+!:!)

Example of f0:receive 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           
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 (+:+)

Example of f1:apply ordered confirmation

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 (+:+)

Example of f1:detect problem

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 (+!:?)

Example of f1:disruption 0

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 (+!:!)

Example of f1:disruption I

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 (+!:-)

Example of f1:receive CONFIRM

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 (+:+)

Example of f2:disruption 0

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 (+:+)

Example of f2:disruption I

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 (+:+)

Example of f2:receive CONFIRM

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 (+:+)

Example of f2:send CONFIRMED/response

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 (+:+)

Example of g0:detect problem

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 (-!:?)

Example of g0:disruption 0

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 (-:)

Example of g0:disruption I

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 (-:-)

Example of g0:receive 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 (-:)

Example of g0:remove prepared information

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 (-:)

Example of g1:detect problem

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 (-!:?)

Example of g1:disruption 0

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 (-:)

Example of g1:disruption I

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 (-:-)

Example of g1:receive 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 (-:)

Example of g1:remove prepared information

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 (-:)

Example of g2:disruption 0

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 (-:)

Example of g2:disruption I

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 (-:)

Example of g2:receive CANCEL

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 (-:)

Example of g2:send CANCELLED

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 (-:)

Example of h1:disruption 0

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 (!:#)

Example of h1:receive 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                                             
                     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 (-!:#)

Example of h1:receive 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 (+:#)

Example of h1:receive CONTRADICTION

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 (-!:#)

Example of h1:receive PREPARE

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 (=:#)

Example of h1:receive REQUEST_CONFIRM

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 (=:#)

Example of h1:receive SUP_STATE/active

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 (=:#)

Example of h1:receive SUP_STATE/active/y

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 (=:#)

Example of h1:receive SUP_STATE/preparedreceived

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 (=:#)

Example of h1:receive SUP_STATE/preparedreceived/y

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 (=:#)

Example of h1:receive SUP_STATE/unknown

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 (!:#)

Example of h1:send CONFIRMED/auto

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 (-!:#)

Example of h2:disruption 0

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 (+:#)

Example of h2:disruption I

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 (+:#)

Example of h2:receive 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 (+:#)

Example of h2:send CONFIRMED/response

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 (+:#)

Example of i1:disruption 0

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 (:)

Example of i1:send ENROL/no-rsp-req

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 (:)

Example of i1:send ENROL/rsp-req

superior                                              inferior
                                      ENROL/rsp-req <-- i1 :a1 
I1 :Z   XXX disruption I           
                                       disruption I XXX a1 :z  
                               X---ENROL/rsp-req

Nothing happens (:)

Example of j1:disruption 0

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 (:-)

Example of j1:disruption I

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 (:-)

Example of j1:receive 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 :G1  === decide to cancel           
G1 :G2  --> CANCEL------------------------------------> j1 :j3 
G2 :Z   <---------------------------------CANCELLED <-- j3 :z  

Both cancel (-:-)

Example of j1:receive 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 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 (+!:-)

Example of j1:receive PREPARE

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 (-:-)

Example of j1:receive REQUEST_CONFIRM

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 (=:-)

Example of j1:receive SUP_STATE/active

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 (=:-)

Example of j1:receive SUP_STATE/active/y

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 (=:-)

Example of j1:receive SUP_STATE/preparedreceived

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 (-:-)

Example of j1:receive SUP_STATE/preparedreceived/y

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 (=:-)

Example of j1:receive SUP_STATE/unknown

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 (:-)

Example of j1:send 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 (:-)

Example of j2:disruption 0

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 (-:-)

Example of j2:receive 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 (-:-)

Example of j2:receive 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
                      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 (+!:-)

Example of j2:receive CONTRADICTION

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 (+!:-)

Example of j2:receive PREPARE

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 (-:-)

Example of j2:receive REQUEST_CONFIRM

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 (=:-)

Example of j2:receive SUP_STATE/active

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 (-:-)

Example of j2:receive SUP_STATE/active/y

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 (-:-)

Example of j2:receive SUP_STATE/preparedreceived

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 (-:-)

Example of j2:receive SUP_STATE/preparedreceived/y

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 (-:-)

Example of j2:receive SUP_STATE/unknown

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 (:-)

Example of j2:send 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 (:-)

Example of j3:disruption 0

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 (-:-)

Example of j3:disruption I

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 (-:-)

Example of j3:receive 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 (-:-)

Example of j3:send 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 :G1  === decide to cancel           
G1 :G2  --> CANCEL------------------------------------> j1 :j3 
G2 :Z   <---------------------------------CANCELLED <-- j3 :z  

Both cancel (-:-)

Example of k1:disruption 0

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 (+!:-)

Example of k1:receive CONFIRM

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 (+!:-)

Example of k1:receive CONTRADICTION

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 (+!:-)

Example of k1:receive SUP_STATE/unknown

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 (+!:-)

Example of k1:send CANCELLED

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 (+!:-)

Example of l1:disruption 0

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 (-!:#)

Example of l1:receive CANCEL

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 (-!:#)

Example of l1:receive CONTRADICTION

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 (-!:#)

Example of l1:receive SUP_STATE/unknown

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 (!:#)

Example of l1:send CONFIRMED/auto

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 (-!:#)

Example of m1:disruption 0

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 (!:!)

Example of m1:receive CANCEL

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 (-!:!)

Example of m1:receive 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
                                     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 (+!:!)

Example of m1:receive CONTRADICTION

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 (!:!)

Example of m1:receive ENROLLED

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 (=:!)

Example of m1:receive PREPARE

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 (!:!)

Example of m1:receive REQUEST_CONFIRM

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 (=:!)

Example of m1:receive SUP_STATE/active

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 (=:!)

Example of m1:receive SUP_STATE/active/y

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 (=:!)

Example of m1:receive SUP_STATE/preparedreceived

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 (=:!)

Example of m1:receive SUP_STATE/preparedreceived/y

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 (=:!)

Example of m1:receive SUP_STATE/unknown

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 (!:!)

Example of m1:send HAZARD

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 (!:!)

Example of m2:detect and record problem

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 (=:!)

Example of m2:disruption 0

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 (:?)

Example of m2:disruption I

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 (:?)

Example of m2:receive CANCEL

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 (-:?)

Example of m2:receive CONTRADICTION

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 (!:?)

Example of m2:receive ENROLLED

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 (-:?)

Example of m2:receive PREPARE

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 (!:?)

Example of m2:receive REQUEST_CONFIRM

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 (=:?)

Example of m2:receive SUP_STATE/active

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 (=:?)

Example of m2:receive SUP_STATE/active/y

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 (=:?)

Example of m2:receive SUP_STATE/unknown

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 (:?)

Example of m2:send 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 (:?)

Example of m3:detect and record problem

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 (=:!)

Example of m3:disruption 0

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 (!:!)

Example of m3:receive CANCEL

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 (-!:?)

Example of m3:receive 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           
                                     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 (+!:?)

Example of m3:receive CONTRADICTION

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 (!:?)

Example of m3:receive PREPARE

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 (!:?)

Example of m3:receive REQUEST_CONFIRM

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 (=:?)

Example of m3:receive SUP_STATE/active

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 (=:?)

Example of m3:receive SUP_STATE/active/y

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 (=:?)

Example of m3:receive SUP_STATE/preparedreceived

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 (=:?)

Example of m3:receive SUP_STATE/preparedreceived/y

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 (=:?)

Example of m3:receive SUP_STATE/unknown

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 (!:?)

Example of m3:send HAZARD

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 (!:?)

Example of n0:disruption 0

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 (=:#)

Example of n0:disruption I

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 (=:-)

Example of n0:receive REQUEST_CONFIRM

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 (=:-)

Example of n0:receive SUP_STATE/unknown

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 (=:)

Example of n0:remove prepared information

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 (=:#)

Example of n1:decide to cancel autonomously

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 (=:-)

Example of n1:decide to confirm autonomously

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 (=:#)

Example of n1:detect and record problem

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 (=:!)

Example of n1:disruption 0

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 (=:-)

Example of n1:disruption I

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 (=:)

Example of n1:receive REQUEST_CONFIRM

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 (=:!)

Example of n2:disruption 0

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 (=:#)

Example of n2:receive REQUEST_CONFIRM

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 (=:#)

Example of n2:send CONFIRMED/response

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 (=:#)

Example of n3:disruption 0

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 (=:-)

Example of n3:receive REQUEST_CONFIRM

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 (=:-)

Example of n3:receive SUP_STATE/unknown

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 (=:-)

Example of n3:send 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 (=:-)

Example of n4:disruption 0

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 (=:!)

Example of n4:receive CONTRADICTION

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 (=!:!)

Example of n4:receive REQUEST_CONFIRM

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 (=:!)

Example of n4:receive SUP_STATE/unknown

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 (=:!)

Example of n4:send HAZARD

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 (=:!)

Example of n5:disruption 0

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 (=:?)

Example of n5:receive CONTRADICTION

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 (=!:?)

Example of n5:receive REQUEST_CONFIRM

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 (=:?)

Example of n5:send HAZARD

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 (=:?)

Example of y0:disruption 0

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 (:)

Example of y0:disruption I

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 (!:?)

Example of y0:receive SUP_STATE/unknown

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 (:)

Example of y0:remove prepared information

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 (:)

Example of y1:disruption 0

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 (=:)

Example of y1:receive CANCEL

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 (-:)

Example of y1:receive CONTRADICTION

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 (=!:?)

Example of y1:receive PREPARE

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 (:)

Example of y1:receive REQUEST_CONFIRM

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 (=:)

Example of y1:receive RESIGNED

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 (:)

Example of y1:receive SUP_STATE/active

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 (:)

Example of y1:receive SUP_STATE/active/y

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 (:)

Example of y1:receive SUP_STATE/unknown

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 (-:)

Example of y1:send INF_STATE/unknown

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 (=:)

Example of y2:disruption 0

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 (+:#)

Example of y2:receive 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 (+:#)

Example of y2:send CONFIRMED/response

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 (+:#)

Example of y3:disruption 0

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 (=:-)

Example of y3:receive CANCEL

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 (-:-)

Example of y3:receive 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           
                      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 (+!:-)

Example of y3:receive CONTRADICTION

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 (+!:-)

Example of y3:receive PREPARE

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 (:-)

Example of y3:receive REQUEST_CONFIRM

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 (=:-)

Example of y3:receive SUP_STATE/active

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 (:-)

Example of y3:receive SUP_STATE/active/y

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 (:-)

Example of y3:receive SUP_STATE/preparedreceived

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 (-:-)

Example of y3:receive SUP_STATE/preparedreceived/y

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 (=:-)

Example of y3:receive SUP_STATE/unknown

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 (-:-)

Example of y3:send CANCELLED

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 (:-)

Example of z1:disruption 0

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 (-:-)

Example of z1:receive 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 (-:-)

Example of z1:receive CONFIRM

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 (+!:-)

Example of z1:receive CONTRADICTION

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 (+!:-)

Example of z1:receive PREPARE

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 (:-)

Example of z1:receive REQUEST_CONFIRM

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 (=:-)

Example of z1:receive SUP_STATE/active

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 (-:-)

Example of z1:receive SUP_STATE/active/y

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 (:-)

Example of z1:receive SUP_STATE/preparedreceived

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 (-:-)

Example of z1:receive SUP_STATE/preparedreceived/y

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 (=:-)

Example of z1:receive SUP_STATE/unknown

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 (:-)

Example of z:disruption 0

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 (:)

Example of z:receive CANCEL

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 (-:)

Example of z:receive 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 (+:#)

Example of z:receive CONTRADICTION

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 (!:?)

Example of z:receive ENROLLED

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 (:)

Example of z:receive PREPARE

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 (:)

Example of z:receive REQUEST_CONFIRM

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 (=:)

Example of z:receive RESIGNED

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 (:)

Example of z:receive SUP_STATE/active

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 (:)

Example of z:receive SUP_STATE/active/y

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 (:)

Example of z:receive SUP_STATE/unknown

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 (:)