Philips Protocol

 These verification conditions arise from a main invariant used in verifying a safety property of the Philips protocol. The invariant is taken from Havelund and Shankar: Experiments in Theorem Proving and Model Checking for Protocol Verification, FME96 .

The system consists of 8 transitions (atomic actions). Each transition is written as a guarded assignment guard --> x' := e. For each transition STeP generates the verification condition 

guard /\ I --> I[e/x]
These are the verification conditions listed below.

Below we summarize sample formulas and running times for a lemma in a safety proof for the Philips protocol.

Clicking on this button will run our procedure on each of these formulas.
Philips 1 
type     Data
value    null_data : Data
in       Last : [1..]
in       max : [1..]
type     Counter = [0..max]
type     Position = [0..Last + 1]
type     File = array [0..Last + 1] of Data
type     Msg = bool*bool*bool*Data
macro    first(m: bool*bool*bool*Data) : bool = 
    #1 m
macro    last(m: bool*bool*bool*Data) : bool = 
    #2 m
macro    toggle(m: bool*bool*bool*Data) : bool = 
    #3 m
macro    data(m: bool*bool*bool*Data) : Data = 
    #4 m
type     Msg_first = bool
type     Msg_last = bool
type     Msg_toggle = bool
type     Msg_data = Data
type     Spc == WR | SF | WA | SC | WT2
type     Rpc == WF | SI | SA | RTS | NOK
type     Conf == OK | NOT_OK | DONT_KNOW
type     IndT == FIRST | INCOMPLETE | LAST
macro    nil : int = 
    Last + 1
macro    incr_rn(r: [0..max]) : [0..max] = 
    if r < max then r + 1 else r
macro    incr_head(h: [0..Last + 1]) : [0..Last + 1] = 
    if h < nil then h + 1 else h
local    aerror : bool
local    afirst : bool
local    ahead : [0..Last + 1]
local    afile : array [0..Last + 1] of Data
local    abusy : bool
local    rtimer_enabled : bool
local    rtimer_on : bool
local    msg : bool*bool*bool*Data
local    ctoggle : bool
local    rtoggle : bool
local    rfirst : bool
local    rpc : Rpc
local    ind_error : bool
local    ind_full : bool
local    ind_indication : IndT
local    ind_data : Data
local    stimer2_enabled : bool
local    stimer2_on : bool
local    stimer1_enabled : bool
local    stimer1_on : bool
local    rn : [0..max]
local    head : [0..Last + 1]
local    file : array [0..Last + 1] of Data
local    stoggle : bool
local    sfirst : bool
local    spc : Spc
local    conf_full : bool
local    conf : Conf
local    req_full : bool
local    req : array [0..Last + 1] of Data
local    L : bool
local    K_full : bool
local    K : bool*bool*bool*Data
local    SAFE : bool
macro    ref_abusy : bool = 
    abusy = (spc = SF \/ spc = WA \/ spc = SC)
macro    ref_afirst : bool = 
    afirst = rfirst
macro    ref_aerror : bool = 
    aerror = (rpc = NOK \/ 
             spc = WT2 /\ rtimer_on /\ ~rfirst)
macro    ref_afile : bool = 
    Forall i : [0..Last + 1] . afile[i] = file[i]
macro    ref_ahead : bool = 
    ahead = (if spc = WT2 \/ (ctoggle --> stoggle = rtoggle)
                then head
                else head + 1)
macro    spc_1 : bool = 
    spc = WR \/ spc = SF \/ spc = SC --> rpc = WF
macro    spc_2 : bool = 
    spc = SF /\ rn = 0 --> ctoggle --> stoggle = rtoggle
macro    spc_3 : bool = 
    spc = WA --> ~(rn = 0)
macro    spc_4 : bool = 
    spc = WT2 /\ ~rtimer_enabled --> ~ctoggle
macro    spc_5 : bool = 
    spc = SC /\ head = nil --> ctoggle /\ stoggle = rtoggle
macro    spc_6 : bool = 
    spc = SC /\ head = nil --> rfirst
macro    spc_7 : bool = 
    spc = WR --> ctoggle --> stoggle = rtoggle
macro    spc_8 : bool = 
    spc = WT2 --> rn = 0
macro    spc_9 : bool = 
    spc = SC /\ rn = 0 --> ctoggle --> stoggle = rtoggle
macro    spc_10 : bool = 
    spc = SF --> 
    (ctoggle --> stoggle = rtoggle) --> sfirst = rfirst
macro    spc_11 : bool = 
    spc = WR --> 
    (ctoggle --> stoggle = rtoggle) --> sfirst = rfirst
macro    spc_12 : bool = 
    spc = WA --> 
    (ctoggle --> stoggle = rtoggle) --> sfirst = rfirst
macro    spc_13 : bool = 
    spc = SC --> 
    (ctoggle --> stoggle = rtoggle) --> sfirst = rfirst
macro    spc_14 : bool = 
    spc = WT2 --> sfirst
macro    spc_15 : bool = 
    spc = WA --> ~(head = nil)
macro    spc_16 : bool = 
    spc = SF --> ~(head = nil)
macro    rpc_1 : bool = 
    rpc = SI \/ rpc = SA \/ rpc = RTS --> spc = WA
macro    rpc_2 : bool = 
    rpc = NOK --> spc = WT2
macro    rpc_3 : bool = 
    rpc = SI --> last(msg) = (head = Last)
macro    rpc_4 : bool = 
    rpc = NOK --> ~ctoggle
macro    rpc_5 : bool = 
    rpc = SI --> stoggle = toggle(msg)
macro    rpc_6 : bool = 
    rpc = SA \/ rpc = RTS --> stoggle = toggle(msg)
macro    rpc_7 : bool = 
    rpc = SA \/ rpc = RTS --> 
    ctoggle /\ ~(toggle(msg) = rtoggle)
macro    rpc_8 : bool = 
    rpc = WF \/ rpc = RTS --> rtimer_on
macro    rpc_9 : bool = 
    rpc = SI --> ctoggle --> toggle(msg) = rtoggle
macro    rpc_10 : bool = 
    rpc = SI --> data(msg) = file[head]
macro    rpc_11 : bool = 
    rpc = SI --> rfirst = first(msg)
macro    K_1 : bool = 
    K_full --> spc = WA /\ rpc = WF /\ ~L
macro    K_2 : bool = 
    K_full --> last(K) = (head = Last)
macro    K_3 : bool = 
    K_full --> toggle(K) = stoggle
macro    K_4 : bool = 
    K_full --> data(K) = file[head]
macro    K_5 : bool = 
    K_full --> 
    (ctoggle --> toggle(K) = rtoggle) --> first(K) = rfirst
macro    L_1 : bool = 
    L --> spc = WA /\ rpc = WF /\ ~K_full
macro    L_2 : bool = 
    L --> ctoggle /\ ~rtoggle = stoggle
macro    stimer1_1 : bool = 
    stimer1_enabled --> 
    spc = WA /\ rpc = WF /\ ~K_full /\ ~L
macro    stimer2_1 : bool = 
    stimer2_enabled --> 
    spc = WT2 /\ rpc = WF /\ ~K_full /\ ~L
macro    stimer2_2 : bool = 
    stimer2_enabled --> rfirst
macro    stimer2_3 : bool = 
    stimer2_enabled --> rfirst
macro    rtimer_1 : bool = 
    rtimer_enabled --> 
    spc = WT2 /\ 
    rpc = WF /\ ~K_full /\ ~L /\ ~stimer2_enabled
macro    rn_1 : bool = 
    ~(rn = 0) --> ~(spc = WR)
macro    rn_2 : bool = 
    ~(rn = 0) /\ ctoggle /\ ~(stoggle = rtoggle) --> 
    rfirst = (head = Last)
macro    head_1 : bool = 
    head = nil --> spc = WR \/ spc = WT2 \/ spc = SC
macro    safe_1 : bool = 
    spc = WR --> ~abusy
macro    safe_2 : bool = 
    spc = SC --> abusy
macro    safe_3 : bool = 
    spc = SC --> ~aerror
macro    safe_4 : bool = 
    spc = SC --> 
    (head = nil --> ahead = nil) /\ 
    (head = Last /\ ~(rn = 0) --> 
    ahead = nil \/ ahead = Last) /\ 
    (head = Last /\ rn = 0 --> ~(ahead = nil)) /\ 
    (head < Last --> ~(ahead = nil))
macro    safe_5 : bool = 
    rpc = SI --> abusy
macro    safe_6 : bool = 
    rpc = SI --> ~aerror
macro    safe_7 : bool = 
    rpc = SI --> ~(ahead = nil)
macro    safe_8 : bool = 
    rpc = SI --> data(msg) = afile[ahead]
macro    safe_9 : bool = 
    rpc = SI --> 
    last(msg) = (ahead = Last) /\ first(msg) = afirst
macro    safe_10 : bool = 
    rpc = NOK --> aerror
macro    safe : bool = 
    SAFE
macro    all : bool = 
    ref_abusy /\ 
    ref_afirst /\ 
    ref_aerror /\ 
    ref_afile /\ 
    ref_ahead /\ 
    spc_1 /\ 
    spc_2 /\ 
    spc_3 /\ 
    spc_4 /\ 
    spc_5 /\ 
    spc_6 /\ 
    spc_7 /\ 
    spc_8 /\ 
    spc_9 /\ 
    spc_10 /\ 
    spc_11 /\ 
    spc_12 /\ 
    spc_13 /\ 
    spc_14 /\ 
    spc_15 /\ 
    spc_16 /\ 
    rpc_1 /\ 
    rpc_2 /\ 
    rpc_3 /\ 
    rpc_4 /\ 
    rpc_5 /\ 
    rpc_6 /\ 
    rpc_7 /\ 
    rpc_8 /\ 
    rpc_9 /\ 
    rpc_10 /\ 
    rpc_11 /\ 
    K_1 /\ 
    K_2 /\ 
    K_3 /\ 
    K_4 /\ 
    K_5 /\ 
    L_1 /\ 
    L_2 /\ 
    stimer1_1 /\ 
    stimer2_1 /\ 
    stimer2_2 /\ 
    stimer2_3 /\ rtimer_1 /\ rn_1 /\ rn_2 /\ head_1
;
aerror = false /\ 
afirst = true /\ 
ahead = Last + 1 /\ 
(Forall i : [0..Last + 1] . afile[i] = null_data) /\ 
abusy = false /\ 
rtimer_enabled = false /\ 
rtimer_on = true /\ 
msg = (false,false,false,null_data) /\ 
ctoggle = false /\ 
rtoggle = false /\ 
rfirst = true /\ 
rpc = WF /\ 
ind_error = false /\ 
ind_full = false /\ 
ind_indication = FIRST /\ 
ind_data = null_data /\ 
stimer2_enabled = false /\ 
stimer2_on = false /\ 
stimer1_enabled = false /\ 
stimer1_on = false /\ 
rn = 0 /\ 
head = Last + 1 /\ 
(Forall i : [0..Last + 1] . file[i] = null_data) /\ 
stoggle = false /\ 
sfirst = true /\ 
spc = WR /\ 
conf_full = false /\ 
conf = OK /\ 
req_full = false /\ 
(Forall i : [0..Last + 1] . req[i] = null_data) /\ 
L = false /\ 
K_full = false /\ 
K = (false,false,false,null_data) /\ SAFE = true --> 
abusy = (spc = SF \/ spc = WA \/ spc = SC) /\ 
afirst = rfirst /\ 
aerror = (rpc = NOK \/ 
         spc = WT2 /\ rtimer_on /\ ~rfirst) /\ 
(Forall i : [0..Last + 1] . afile[i] = file[i]) /\ 
ahead = (if spc = WT2 \/ (ctoggle --> stoggle = rtoggle)
            then head
            else head + 1) /\ 
(spc = WR \/ spc = SF \/ spc = SC --> rpc = WF) /\ 
(spc = SF /\ rn = 0 --> ctoggle --> stoggle = rtoggle) /\ 
(spc = WA --> ~(rn = 0)) /\ 
(spc = WT2 /\ ~rtimer_enabled --> ~ctoggle) /\ 
(spc = SC /\ head = Last + 1 --> 
ctoggle /\ stoggle = rtoggle) /\ 
(spc = SC /\ head = Last + 1 --> rfirst) /\ 
(spc = WR --> ctoggle --> stoggle = rtoggle) /\ 
(spc = WT2 --> rn = 0) /\ 
(spc = SC /\ rn = 0 --> ctoggle --> stoggle = rtoggle) /\ 
(spc = SF --> 
(ctoggle --> stoggle = rtoggle) --> sfirst = rfirst) /\ 
(spc = WR --> 
(ctoggle --> stoggle = rtoggle) --> sfirst = rfirst) /\ 
(spc = WA --> 
(ctoggle --> stoggle = rtoggle) --> sfirst = rfirst) /\ 
(spc = SC --> 
(ctoggle --> stoggle = rtoggle) --> sfirst = rfirst) /\ 
(spc = WT2 --> sfirst) /\ 
(spc = WA --> ~(head = Last + 1)) /\ 
(spc = SF --> ~(head = Last + 1)) /\ 
(rpc = SI \/ rpc = SA \/ rpc = RTS --> spc = WA) /\ 
(rpc = NOK --> spc = WT2) /\ 
(rpc = SI --> #2 msg = (head = Last)) /\ 
(rpc = NOK --> ~ctoggle) /\ 
(rpc = SI --> stoggle = #3 msg) /\ 
(rpc = SA \/ rpc = RTS --> stoggle = #3 msg) /\ 
(rpc = SA \/ rpc = RTS --> 
ctoggle /\ ~(#3 msg = rtoggle)) /\ 
(rpc = WF \/ rpc = RTS --> rtimer_on) /\ 
(rpc = SI --> ctoggle --> #3 msg = rtoggle) /\ 
(rpc = SI --> #4 msg = file[head]) /\ 
(rpc = SI --> rfirst = #1 msg) /\ 
(K_full --> spc = WA /\ rpc = WF /\ ~L) /\ 
(K_full --> #2 K = (head = Last)) /\ 
(K_full --> #3 K = stoggle) /\ 
(K_full --> #4 K = file[head]) /\ 
(K_full --> 
(ctoggle --> #3 K = rtoggle) --> #1 K = rfirst) /\ 
(L --> spc = WA /\ rpc = WF /\ ~K_full) /\ 
(L --> ctoggle /\ ~rtoggle = stoggle) /\ 
(stimer1_enabled --> 
spc = WA /\ rpc = WF /\ ~K_full /\ ~L) /\ 
(stimer2_enabled --> 
spc = WT2 /\ rpc = WF /\ ~K_full /\ ~L) /\ 
(stimer2_enabled --> rfirst) /\ 
(stimer2_enabled --> rfirst) /\ 
(rtimer_enabled --> 
spc = WT2 /\ 
rpc = WF /\ ~K_full /\ ~L /\ ~stimer2_enabled) /\ 
(~(rn = 0) --> ~(spc = WR)) /\ 
(~(rn = 0) /\ ctoggle /\ ~(stoggle = rtoggle) --> 
rfirst = (head = Last)) /\ 
(head = Last + 1 --> spc = WR \/ spc = WT2 \/ spc = SC)
Philips 2 
(abusy = (spc = SF \/ spc = WA \/ spc = SC) /\ 
afirst = rfirst /\ 
aerror = (rpc = NOK \/ 
         spc = WT2 /\ rtimer_on /\ ~rfirst) /\ 
(Forall i : [0..Last + 1] . afile[i] = file[i]) /\ 
ahead = (if spc = WT2 \/ (ctoggle --> stoggle = rtoggle)
            then head
            else head + 1) /\ 
(spc = WR \/ spc = SF \/ spc = SC --> rpc = WF) /\ 
(spc = SF /\ rn = 0 --> ctoggle --> stoggle = rtoggle) /\ 
(spc = WA --> ~(rn = 0)) /\ 
(spc = WT2 /\ ~rtimer_enabled --> ~ctoggle) /\ 
(spc = SC /\ head = Last + 1 --> 
ctoggle /\ stoggle = rtoggle) /\ 
(spc = SC /\ head = Last + 1 --> rfirst) /\ 
(spc = WR --> ctoggle --> stoggle = rtoggle) /\ 
(spc = WT2 --> rn = 0) /\ 
(spc = SC /\ rn = 0 --> ctoggle --> stoggle = rtoggle) /\ 
(spc = SF --> 
(ctoggle --> stoggle = rtoggle) --> sfirst = rfirst) /\ 
(spc = WR --> 
(ctoggle --> stoggle = rtoggle) --> sfirst = rfirst) /\ 
(spc = WA --> 
(ctoggle --> stoggle = rtoggle) --> sfirst = rfirst) /\ 
(spc = SC --> 
(ctoggle --> stoggle = rtoggle) --> sfirst = rfirst) /\ 
(spc = WT2 --> sfirst) /\ 
(spc = WA --> ~(head = Last + 1)) /\ 
(spc = SF --> ~(head = Last + 1)) /\ 
(rpc = SI \/ rpc = SA \/ rpc = RTS --> spc = WA) /\ 
(rpc = NOK --> spc = WT2) /\ 
(rpc = SI --> #2 msg = (head = Last)) /\ 
(rpc = NOK --> ~ctoggle) /\ 
(rpc = SI --> stoggle = #3 msg) /\ 
(rpc = SA \/ rpc = RTS --> stoggle = #3 msg) /\ 
(rpc = SA \/ rpc = RTS --> 
ctoggle /\ ~(#3 msg = rtoggle)) /\ 
(rpc = WF \/ rpc = RTS --> rtimer_on) /\ 
(rpc = SI --> ctoggle --> #3 msg = rtoggle) /\ 
(rpc = SI --> #4 msg = file[head]) /\ 
(rpc = SI --> rfirst = #1 msg) /\ 
(K_full --> spc = WA /\ rpc = WF /\ ~L) /\ 
(K_full --> #2 K = (head = Last)) /\ 
(K_full --> #3 K = stoggle) /\ 
(K_full --> #4 K = file[head]) /\ 
(K_full --> 
(ctoggle --> #3 K = rtoggle) --> #1 K = rfirst) /\ 
(L --> spc = WA /\ rpc = WF /\ ~K_full) /\ 
(L --> ctoggle /\ ~rtoggle = stoggle) /\ 
(stimer1_enabled --> 
spc = WA /\ rpc = WF /\ ~K_full /\ ~L) /\ 
(stimer2_enabled --> 
spc = WT2 /\ rpc = WF /\ ~K_full /\ ~L) /\ 
(stimer2_enabled --> rfirst) /\ 
(stimer2_enabled --> rfirst) /\ 
(rtimer_enabled --> 
spc = WT2 /\ 
rpc = WF /\ ~K_full /\ ~L /\ ~stimer2_enabled) /\ 
(~(rn = 0) --> ~(spc = WR)) /\ 
(~(rn = 0) /\ ctoggle /\ ~(stoggle = rtoggle) --> 
rfirst = (head = Last)) /\ 
(head = Last + 1 --> spc = WR \/ spc = WT2 \/ spc = SC)) /\ 
K_full --> 
abusy = (spc = SF \/ spc = WA \/ spc = SC) /\ 
afirst = rfirst /\ 
aerror = (rpc = NOK \/ 
         spc = WT2 /\ rtimer_on /\ ~rfirst) /\ 
(Forall i : [0..Last + 1] . afile[i] = file[i]) /\ 
ahead = (if spc = WT2 \/ (ctoggle --> stoggle = rtoggle)
            then head
            else head + 1) /\ 
(spc = WR \/ spc = SF \/ spc = SC --> rpc = WF) /\ 
(spc = SF /\ rn = 0 --> ctoggle --> stoggle = rtoggle) /\ 
(spc = WA --> ~(rn = 0)) /\ 
(spc = WT2 /\ ~rtimer_enabled --> ~ctoggle) /\ 
(spc = SC /\ head = Last + 1 --> 
ctoggle /\ stoggle = rtoggle) /\ 
(spc = SC /\ head = Last + 1 --> rfirst) /\ 
(spc = WR --> ctoggle --> stoggle = rtoggle) /\ 
(spc = WT2 --> rn = 0) /\ 
(spc = SC /\ rn = 0 --> ctoggle --> stoggle = rtoggle) /\ 
(spc = SF --> 
(ctoggle --> stoggle = rtoggle) --> sfirst = rfirst) /\ 
(spc = WR --> 
(ctoggle --> stoggle = rtoggle) --> sfirst = rfirst) /\ 
(spc = WA --> 
(ctoggle --> stoggle = rtoggle) --> sfirst = rfirst) /\ 
(spc = SC --> 
(ctoggle --> stoggle = rtoggle) --> sfirst = rfirst) /\ 
(spc = WT2 --> sfirst) /\ 
(spc = WA --> ~(head = Last + 1)) /\ 
(spc = SF --> ~(head = Last + 1)) /\ 
(rpc = SI \/ rpc = SA \/ rpc = RTS --> spc = WA) /\ 
(rpc = NOK --> spc = WT2) /\ 
(rpc = SI --> #2 msg = (head = Last)) /\ 
(rpc = NOK --> ~ctoggle) /\ 
(rpc = SI --> stoggle = #3 msg) /\ 
(rpc = SA \/ rpc = RTS --> stoggle = #3 msg) /\ 
(rpc = SA \/ rpc = RTS --> 
ctoggle /\ ~(#3 msg = rtoggle)) /\ 
(rpc = WF \/ rpc = RTS --> rtimer_on) /\ 
(rpc = SI --> ctoggle --> #3 msg = rtoggle) /\ 
(rpc = SI --> #4 msg = file[head]) /\ 
(rpc = SI --> rfirst = #1 msg) /\ 
(false --> spc = WA /\ rpc = WF /\ ~L) /\ 
(false --> #2 K = (head = Last)) /\ 
(false --> #3 K = stoggle) /\ 
(false --> #4 K = file[head]) /\ 
(false --> 
(ctoggle --> #3 K = rtoggle) --> #1 K = rfirst) /\ 
(L --> spc = WA /\ rpc = WF /\ ~false) /\ 
(L --> ctoggle /\ ~rtoggle = stoggle) /\ 
(true --> spc = WA /\ rpc = WF /\ ~false /\ ~L) /\ 
(stimer2_enabled --> 
spc = WT2 /\ rpc = WF /\ ~false /\ ~L) /\ 
(stimer2_enabled --> rfirst) /\ 
(stimer2_enabled --> rfirst) /\ 
(rtimer_enabled --> 
spc = WT2 /\ 
rpc = WF /\ ~false /\ ~L /\ ~stimer2_enabled) /\ 
(~(rn = 0) --> ~(spc = WR)) /\ 
(~(rn = 0) /\ ctoggle /\ ~(stoggle = rtoggle) --> 
rfirst = (head = Last)) /\ 
(head = Last + 1 --> spc = WR \/ spc = WT2 \/ spc = SC)
Philips 3 

(abusy = (spc = SF \/ spc = WA \/ spc = SC) /\ 
afirst = rfirst /\ 
aerror = (rpc = NOK \/ 
         spc = WT2 /\ rtimer_on /\ ~rfirst) /\ 
(Forall i : [0..Last + 1] . afile[i] = file[i]) /\ 
ahead = (if spc = WT2 \/ (ctoggle --> stoggle = rtoggle)
            then head
            else head + 1) /\ 
(spc = WR \/ spc = SF \/ spc = SC --> rpc = WF) /\ 
(spc = SF /\ rn = 0 --> ctoggle --> stoggle = rtoggle) /\ 
(spc = WA --> ~(rn = 0)) /\ 
(spc = WT2 /\ ~rtimer_enabled --> ~ctoggle) /\ 
(spc = SC /\ head = Last + 1 --> 
ctoggle /\ stoggle = rtoggle) /\ 
(spc = SC /\ head = Last + 1 --> rfirst) /\ 
(spc = WR --> ctoggle --> stoggle = rtoggle) /\ 
(spc = WT2 --> rn = 0) /\ 
(spc = SC /\ rn = 0 --> ctoggle --> stoggle = rtoggle) /\ 
(spc = SF --> 
(ctoggle --> stoggle = rtoggle) --> sfirst = rfirst) /\ 
(spc = WR --> 
(ctoggle --> stoggle = rtoggle) --> sfirst = rfirst) /\ 
(spc = WA --> 
(ctoggle --> stoggle = rtoggle) --> sfirst = rfirst) /\ 
(spc = SC --> 
(ctoggle --> stoggle = rtoggle) --> sfirst = rfirst) /\ 
(spc = WT2 --> sfirst) /\ 
(spc = WA --> ~(head = Last + 1)) /\ 
(spc = SF --> ~(head = Last + 1)) /\ 
(rpc = SI \/ rpc = SA \/ rpc = RTS --> spc = WA) /\ 
(rpc = NOK --> spc = WT2) /\ 
(rpc = SI --> #2 msg = (head = Last)) /\ 
(rpc = NOK --> ~ctoggle) /\ 
(rpc = SI --> stoggle = #3 msg) /\ 
(rpc = SA \/ rpc = RTS --> stoggle = #3 msg) /\ 
(rpc = SA \/ rpc = RTS --> 
ctoggle /\ ~(#3 msg = rtoggle)) /\ 
(rpc = WF \/ rpc = RTS --> rtimer_on) /\ 
(rpc = SI --> ctoggle --> #3 msg = rtoggle) /\ 
(rpc = SI --> #4 msg = file[head]) /\ 
(rpc = SI --> rfirst = #1 msg) /\ 
(K_full --> spc = WA /\ rpc = WF /\ ~L) /\ 
(K_full --> #2 K = (head = Last)) /\ 
(K_full --> #3 K = stoggle) /\ 
(K_full --> #4 K = file[head]) /\ 
(K_full --> 
(ctoggle --> #3 K = rtoggle) --> #1 K = rfirst) /\ 
(L --> spc = WA /\ rpc = WF /\ ~K_full) /\ 
(L --> ctoggle /\ ~rtoggle = stoggle) /\ 
(stimer1_enabled --> 
spc = WA /\ rpc = WF /\ ~K_full /\ ~L) /\ 
(stimer2_enabled --> 
spc = WT2 /\ rpc = WF /\ ~K_full /\ ~L) /\ 
(stimer2_enabled --> rfirst) /\ 
(stimer2_enabled --> rfirst) /\ 
(rtimer_enabled --> 
spc = WT2 /\ 
rpc = WF /\ ~K_full /\ ~L /\ ~stimer2_enabled) /\ 
(~(rn = 0) --> ~(spc = WR)) /\ 
(~(rn = 0) /\ ctoggle /\ ~(stoggle = rtoggle) --> 
rfirst = (head = Last)) /\ 
(head = Last + 1 --> spc = WR \/ spc = WT2 \/ spc = SC)) /\ 
L --> 
abusy = (spc = SF \/ spc = WA \/ spc = SC) /\ 
afirst = rfirst /\ 
aerror = (rpc = NOK \/ 
         spc = WT2 /\ rtimer_on /\ ~rfirst) /\ 
(Forall i : [0..Last + 1] . afile[i] = file[i]) /\ 
ahead = (if spc = WT2 \/ (ctoggle --> stoggle = rtoggle)
            then head
            else head + 1) /\ 
(spc = WR \/ spc = SF \/ spc = SC --> rpc = WF) /\ 
(spc = SF /\ rn = 0 --> ctoggle --> stoggle = rtoggle) /\ 
(spc = WA --> ~(rn = 0)) /\ 
(spc = WT2 /\ ~rtimer_enabled --> ~ctoggle) /\ 
(spc = SC /\ head = Last + 1 --> 
ctoggle /\ stoggle = rtoggle) /\ 
(spc = SC /\ head = Last + 1 --> rfirst) /\ 
(spc = WR --> ctoggle --> stoggle = rtoggle) /\ 
(spc = WT2 --> rn = 0) /\ 
(spc = SC /\ rn = 0 --> ctoggle --> stoggle = rtoggle) /\ 
(spc = SF --> 
(ctoggle --> stoggle = rtoggle) --> sfirst = rfirst) /\ 
(spc = WR --> 
(ctoggle --> stoggle = rtoggle) --> sfirst = rfirst) /\ 
(spc = WA --> 
(ctoggle --> stoggle = rtoggle) --> sfirst = rfirst) /\ 
(spc = SC --> 
(ctoggle --> stoggle = rtoggle) --> sfirst = rfirst) /\ 
(spc = WT2 --> sfirst) /\ 
(spc = WA --> ~(head = Last + 1)) /\ 
(spc = SF --> ~(head = Last + 1)) /\ 
(rpc = SI \/ rpc = SA \/ rpc = RTS --> spc = WA) /\ 
(rpc = NOK --> spc = WT2) /\ 
(rpc = SI --> #2 msg = (head = Last)) /\ 
(rpc = NOK --> ~ctoggle) /\ 
(rpc = SI --> stoggle = #3 msg) /\ 
(rpc = SA \/ rpc = RTS --> stoggle = #3 msg) /\ 
(rpc = SA \/ rpc = RTS --> 
ctoggle /\ ~(#3 msg = rtoggle)) /\ 
(rpc = WF \/ rpc = RTS --> rtimer_on) /\ 
(rpc = SI --> ctoggle --> #3 msg = rtoggle) /\ 
(rpc = SI --> #4 msg = file[head]) /\ 
(rpc = SI --> rfirst = #1 msg) /\ 
(K_full --> spc = WA /\ rpc = WF /\ ~false) /\ 
(K_full --> #2 K = (head = Last)) /\ 
(K_full --> #3 K = stoggle) /\ 
(K_full --> #4 K = file[head]) /\ 
(K_full --> 
(ctoggle --> #3 K = rtoggle) --> #1 K = rfirst) /\ 
(false --> spc = WA /\ rpc = WF /\ ~K_full) /\ 
(false --> ctoggle /\ ~rtoggle = stoggle) /\ 
(true --> spc = WA /\ rpc = WF /\ ~K_full /\ ~false) /\ 
(stimer2_enabled --> 
spc = WT2 /\ rpc = WF /\ ~K_full /\ ~false) /\ 
(stimer2_enabled --> rfirst) /\ 
(stimer2_enabled --> rfirst) /\ 
(rtimer_enabled --> 
spc = WT2 /\ 
rpc = WF /\ ~K_full /\ ~false /\ ~stimer2_enabled) /\ 
(~(rn = 0) --> ~(spc = WR)) /\ 
(~(rn = 0) /\ ctoggle /\ ~(stoggle = rtoggle) --> 
rfirst = (head = Last)) /\ 
(head = Last + 1 --> spc = WR \/ spc = WT2 \/ spc = SC)
Philips 4 
(abusy = (spc = SF \/ spc = WA \/ spc = SC) /\ 
afirst = rfirst /\ 
aerror = (rpc = NOK \/ 
         spc = WT2 /\ rtimer_on /\ ~rfirst) /\ 
(Forall i : [0..Last + 1] . afile[i] = file[i]) /\ 
ahead = (if spc = WT2 \/ (ctoggle --> stoggle = rtoggle)
            then head
            else head + 1) /\ 
(spc = WR \/ spc = SF \/ spc = SC --> rpc = WF) /\ 
(spc = SF /\ rn = 0 --> ctoggle --> stoggle = rtoggle) /\ 
(spc = WA --> ~(rn = 0)) /\ 
(spc = WT2 /\ ~rtimer_enabled --> ~ctoggle) /\ 
(spc = SC /\ head = Last + 1 --> 
ctoggle /\ stoggle = rtoggle) /\ 
(spc = SC /\ head = Last + 1 --> rfirst) /\ 
(spc = WR --> ctoggle --> stoggle = rtoggle) /\ 
(spc = WT2 --> rn = 0) /\ 
(spc = SC /\ rn = 0 --> ctoggle --> stoggle = rtoggle) /\ 
(spc = SF --> 
(ctoggle --> stoggle = rtoggle) --> sfirst = rfirst) /\ 
(spc = WR --> 
(ctoggle --> stoggle = rtoggle) --> sfirst = rfirst) /\ 
(spc = WA --> 
(ctoggle --> stoggle = rtoggle) --> sfirst = rfirst) /\ 
(spc = SC --> 
(ctoggle --> stoggle = rtoggle) --> sfirst = rfirst) /\ 
(spc = WT2 --> sfirst) /\ 
(spc = WA --> ~(head = Last + 1)) /\ 
(spc = SF --> ~(head = Last + 1)) /\ 
(rpc = SI \/ rpc = SA \/ rpc = RTS --> spc = WA) /\ 
(rpc = NOK --> spc = WT2) /\ 
(rpc = SI --> #2 msg = (head = Last)) /\ 
(rpc = NOK --> ~ctoggle) /\ 
(rpc = SI --> stoggle = #3 msg) /\ 
(rpc = SA \/ rpc = RTS --> stoggle = #3 msg) /\ 
(rpc = SA \/ rpc = RTS --> 
ctoggle /\ ~(#3 msg = rtoggle)) /\ 
(rpc = WF \/ rpc = RTS --> rtimer_on) /\ 
(rpc = SI --> ctoggle --> #3 msg = rtoggle) /\ 
(rpc = SI --> #4 msg = file[head]) /\ 
(rpc = SI --> rfirst = #1 msg) /\ 
(K_full --> spc = WA /\ rpc = WF /\ ~L) /\ 
(K_full --> #2 K = (head = Last)) /\ 
(K_full --> #3 K = stoggle) /\ 
(K_full --> #4 K = file[head]) /\ 
(K_full --> 
(ctoggle --> #3 K = rtoggle) --> #1 K = rfirst) /\ 
(L --> spc = WA /\ rpc = WF /\ ~K_full) /\ 
(L --> ctoggle /\ ~rtoggle = stoggle) /\ 
(stimer1_enabled --> 
spc = WA /\ rpc = WF /\ ~K_full /\ ~L) /\ 
(stimer2_enabled --> 
spc = WT2 /\ rpc = WF /\ ~K_full /\ ~L) /\ 
(stimer2_enabled --> rfirst) /\ 
(stimer2_enabled --> rfirst) /\ 
(rtimer_enabled --> 
spc = WT2 /\ 
rpc = WF /\ ~K_full /\ ~L /\ ~stimer2_enabled) /\ 
(~(rn = 0) --> ~(spc = WR)) /\ 
(~(rn = 0) /\ ctoggle /\ ~(stoggle = rtoggle) --> 
rfirst = (head = Last)) /\ 
(head = Last + 1 --> spc = WR \/ spc = WT2 \/ spc = SC)) /\ 
spc = WR /\ req_full --> 
true = (SF = SF \/ SF = WA \/ SF = SC) /\ 
afirst = rfirst /\ 
aerror = (rpc = NOK \/ SF = WT2 /\ rtimer_on /\ ~rfirst) /\ 
(Forall i : [0..Last + 1] . req[i] = req[i]) /\ 
1 = (if SF = WT2 \/ (ctoggle --> stoggle = rtoggle)
        then 1
        else 1 + 1) /\ 
(SF = WR \/ SF = SF \/ SF = SC --> rpc = WF) /\ 
(SF = SF /\ rn = 0 --> ctoggle --> stoggle = rtoggle) /\ 
(SF = WA --> ~(rn = 0)) /\ 
(SF = WT2 /\ ~rtimer_enabled --> ~ctoggle) /\ 
(SF = SC /\ 1 = Last + 1 --> 
ctoggle /\ stoggle = rtoggle) /\ 
(SF = SC /\ 1 = Last + 1 --> rfirst) /\ 
(SF = WR --> ctoggle --> stoggle = rtoggle) /\ 
(SF = WT2 --> rn = 0) /\ 
(SF = SC /\ rn = 0 --> ctoggle --> stoggle = rtoggle) /\ 
(SF = SF --> 
(ctoggle --> stoggle = rtoggle) --> sfirst = rfirst) /\ 
(SF = WR --> 
(ctoggle --> stoggle = rtoggle) --> sfirst = rfirst) /\ 
(SF = WA --> 
(ctoggle --> stoggle = rtoggle) --> sfirst = rfirst) /\ 
(SF = SC --> 
(ctoggle --> stoggle = rtoggle) --> sfirst = rfirst) /\ 
(SF = WT2 --> sfirst) /\ 
(SF = WA --> ~(1 = Last + 1)) /\ 
(SF = SF --> ~(1 = Last + 1)) /\ 
(rpc = SI \/ rpc = SA \/ rpc = RTS --> SF = WA) /\ 
(rpc = NOK --> SF = WT2) /\ 
(rpc = SI --> #2 msg = (1 = Last)) /\ 
(rpc = NOK --> ~ctoggle) /\ 
(rpc = SI --> stoggle = #3 msg) /\ 
(rpc = SA \/ rpc = RTS --> stoggle = #3 msg) /\ 
(rpc = SA \/ rpc = RTS --> 
ctoggle /\ ~(#3 msg = rtoggle)) /\ 
(rpc = WF \/ rpc = RTS --> rtimer_on) /\ 
(rpc = SI --> ctoggle --> #3 msg = rtoggle) /\ 
(rpc = SI --> #4 msg = req[1]) /\ 
(rpc = SI --> rfirst = #1 msg) /\ 
(K_full --> SF = WA /\ rpc = WF /\ ~L) /\ 
(K_full --> #2 K = (1 = Last)) /\ 
(K_full --> #3 K = stoggle) /\ 
(K_full --> #4 K = req[1]) /\ 
(K_full --> 
(ctoggle --> #3 K = rtoggle) --> #1 K = rfirst) /\ 
(L --> SF = WA /\ rpc = WF /\ ~K_full) /\ 
(L --> ctoggle /\ ~rtoggle = stoggle) /\ 
(stimer1_enabled --> 
SF = WA /\ rpc = WF /\ ~K_full /\ ~L) /\ 
(stimer2_enabled --> 
SF = WT2 /\ rpc = WF /\ ~K_full /\ ~L) /\ 
(stimer2_enabled --> rfirst) /\ 
(stimer2_enabled --> rfirst) /\ 
(rtimer_enabled --> 
SF = WT2 /\ 
rpc = WF /\ ~K_full /\ ~L /\ ~stimer2_enabled) /\ 
(~(rn = 0) --> ~(SF = WR)) /\ 
(~(rn = 0) /\ ctoggle /\ ~(stoggle = rtoggle) --> 
rfirst = (1 = Last)) /\ 
(1 = Last + 1 --> SF = WR \/ SF = WT2 \/ SF = SC)
Philips 5 
(abusy = (spc = SF \/ spc = WA \/ spc = SC) /\ 
afirst = rfirst /\ 
aerror = (rpc = NOK \/ 
         spc = WT2 /\ rtimer_on /\ ~rfirst) /\ 
(Forall i : [0..Last + 1] . afile[i] = file[i]) /\ 
ahead = (if spc = WT2 \/ (ctoggle --> stoggle = rtoggle)
            then head
            else head + 1) /\ 
(spc = WR \/ spc = SF \/ spc = SC --> rpc = WF) /\ 
(spc = SF /\ rn = 0 --> ctoggle --> stoggle = rtoggle) /\ 
(spc = WA --> ~(rn = 0)) /\ 
(spc = WT2 /\ ~rtimer_enabled --> ~ctoggle) /\ 
(spc = SC /\ head = Last + 1 --> 
ctoggle /\ stoggle = rtoggle) /\ 
(spc = SC /\ head = Last + 1 --> rfirst) /\ 
(spc = WR --> ctoggle --> stoggle = rtoggle) /\ 
(spc = WT2 --> rn = 0) /\ 
(spc = SC /\ rn = 0 --> ctoggle --> stoggle = rtoggle) /\ 
(spc = SF --> 
(ctoggle --> stoggle = rtoggle) --> sfirst = rfirst) /\ 
(spc = WR --> 
(ctoggle --> stoggle = rtoggle) --> sfirst = rfirst) /\ 
(spc = WA --> 
(ctoggle --> stoggle = rtoggle) --> sfirst = rfirst) /\ 
(spc = SC --> 
(ctoggle --> stoggle = rtoggle) --> sfirst = rfirst) /\ 
(spc = WT2 --> sfirst) /\ 
(spc = WA --> ~(head = Last + 1)) /\ 
(spc = SF --> ~(head = Last + 1)) /\ 
(rpc = SI \/ rpc = SA \/ rpc = RTS --> spc = WA) /\ 
(rpc = NOK --> spc = WT2) /\ 
(rpc = SI --> #2 msg = (head = Last)) /\ 
(rpc = NOK --> ~ctoggle) /\ 
(rpc = SI --> stoggle = #3 msg) /\ 
(rpc = SA \/ rpc = RTS --> stoggle = #3 msg) /\ 
(rpc = SA \/ rpc = RTS --> 
ctoggle /\ ~(#3 msg = rtoggle)) /\ 
(rpc = WF \/ rpc = RTS --> rtimer_on) /\ 
(rpc = SI --> ctoggle --> #3 msg = rtoggle) /\ 
(rpc = SI --> #4 msg = file[head]) /\ 
(rpc = SI --> rfirst = #1 msg) /\ 
(K_full --> spc = WA /\ rpc = WF /\ ~L) /\ 
(K_full --> #2 K = (head = Last)) /\ 
(K_full --> #3 K = stoggle) /\ 
(K_full --> #4 K = file[head]) /\ 
(K_full --> 
(ctoggle --> #3 K = rtoggle) --> #1 K = rfirst) /\ 
(L --> spc = WA /\ rpc = WF /\ ~K_full) /\ 
(L --> ctoggle /\ ~rtoggle = stoggle) /\ 
(stimer1_enabled --> 
spc = WA /\ rpc = WF /\ ~K_full /\ ~L) /\ 
(stimer2_enabled --> 
spc = WT2 /\ rpc = WF /\ ~K_full /\ ~L) /\ 
(stimer2_enabled --> rfirst) /\ 
(stimer2_enabled --> rfirst) /\ 
(rtimer_enabled --> 
spc = WT2 /\ 
rpc = WF /\ ~K_full /\ ~L /\ ~stimer2_enabled) /\ 
(~(rn = 0) --> ~(spc = WR)) /\ 
(~(rn = 0) /\ ctoggle /\ ~(stoggle = rtoggle) --> 
rfirst = (head = Last)) /\ 
(head = Last + 1 --> spc = WR \/ spc = WT2 \/ spc = SC)) /\ 
spc = SF /\ ~K_full --> 
abusy = (WA = SF \/ WA = WA \/ WA = SC) /\ 
afirst = rfirst /\ 
aerror = (rpc = NOK \/ WA = WT2 /\ rtimer_on /\ ~rfirst) /\ 
(Forall i : [0..Last + 1] . afile[i] = file[i]) /\ 
ahead = (if WA = WT2 \/ (ctoggle --> stoggle = rtoggle)
            then head
            else head + 1) /\ 
(WA = WR \/ WA = SF \/ WA = SC --> rpc = WF) /\ 
(WA = SF /\ (if rn < max then rn + 1 else rn) = 0 --> 
ctoggle --> stoggle = rtoggle) /\ 
(WA = WA --> ~((if rn < max then rn + 1 else rn) = 0)) /\ 
(WA = WT2 /\ ~rtimer_enabled --> ~ctoggle) /\ 
(WA = SC /\ head = Last + 1 --> 
ctoggle /\ stoggle = rtoggle) /\ 
(WA = SC /\ head = Last + 1 --> rfirst) /\ 
(WA = WR --> ctoggle --> stoggle = rtoggle) /\ 
(WA = WT2 --> (if rn < max then rn + 1 else rn) = 0) /\ 
(WA = SC /\ (if rn < max then rn + 1 else rn) = 0 --> 
ctoggle --> stoggle = rtoggle) /\ 
(WA = SF --> 
(ctoggle --> stoggle = rtoggle) --> sfirst = rfirst) /\ 
(WA = WR --> 
(ctoggle --> stoggle = rtoggle) --> sfirst = rfirst) /\ 
(WA = WA --> 
(ctoggle --> stoggle = rtoggle) --> sfirst = rfirst) /\ 
(WA = SC --> 
(ctoggle --> stoggle = rtoggle) --> sfirst = rfirst) /\ 
(WA = WT2 --> sfirst) /\ 
(WA = WA --> ~(head = Last + 1)) /\ 
(WA = SF --> ~(head = Last + 1)) /\ 
(rpc = SI \/ rpc = SA \/ rpc = RTS --> WA = WA) /\ 
(rpc = NOK --> WA = WT2) /\ 
(rpc = SI --> #2 msg = (head = Last)) /\ 
(rpc = NOK --> ~ctoggle) /\ 
(rpc = SI --> stoggle = #3 msg) /\ 
(rpc = SA \/ rpc = RTS --> stoggle = #3 msg) /\ 
(rpc = SA \/ rpc = RTS --> 
ctoggle /\ ~(#3 msg = rtoggle)) /\ 
(rpc = WF \/ rpc = RTS --> rtimer_on) /\ 
(rpc = SI --> ctoggle --> #3 msg = rtoggle) /\ 
(rpc = SI --> #4 msg = file[head]) /\ 
(rpc = SI --> rfirst = #1 msg) /\ 
(true --> WA = WA /\ rpc = WF /\ ~L) /\ 
(true --> 
#2 (sfirst,head = Last,stoggle,
    file[head]) = (head = Last)) /\ 
(true --> 
#3 (sfirst,head = Last,stoggle,file[head]) = stoggle) /\ 
(true --> 
#4 (sfirst,head = Last,stoggle,file[head]) = file[head]) /\ 
(true --> 
(ctoggle --> 
#3 (sfirst,head = Last,stoggle,file[head]) = rtoggle) --> 
#1 (sfirst,head = Last,stoggle,file[head]) = rfirst) /\ 
(L --> WA = WA /\ rpc = WF /\ ~true) /\ 
(L --> ctoggle /\ ~rtoggle = stoggle) /\ 
(stimer1_enabled --> WA = WA /\ rpc = WF /\ ~true /\ ~L) /\ 
(stimer2_enabled --> 
WA = WT2 /\ rpc = WF /\ ~true /\ ~L) /\ 
(stimer2_enabled --> rfirst) /\ 
(stimer2_enabled --> rfirst) /\ 
(rtimer_enabled --> 
WA = WT2 /\ rpc = WF /\ ~true /\ ~L /\ ~stimer2_enabled) /\ 
(~((if rn < max then rn + 1 else rn) = 0) --> 
~(WA = WR)) /\ 
(~((if rn < max then rn + 1 else rn) = 0) /\ 
 ctoggle /\ ~(stoggle = rtoggle) --> 
rfirst = (head = Last)) /\ 
(head = Last + 1 --> WA = WR \/ WA = WT2 \/ WA = SC)
Philips 6 

(abusy = (spc = SF \/ spc = WA \/ spc = SC) /\ 
afirst = rfirst /\ 
aerror = (rpc = NOK \/ 
         spc = WT2 /\ rtimer_on /\ ~rfirst) /\ 
(Forall i : [0..Last + 1] . afile[i] = file[i]) /\ 
ahead = (if spc = WT2 \/ (ctoggle --> stoggle = rtoggle)
            then head
            else head + 1) /\ 
(spc = WR \/ spc = SF \/ spc = SC --> rpc = WF) /\ 
(spc = SF /\ rn = 0 --> ctoggle --> stoggle = rtoggle) /\ 
(spc = WA --> ~(rn = 0)) /\ 
(spc = WT2 /\ ~rtimer_enabled --> ~ctoggle) /\ 
(spc = SC /\ head = Last + 1 --> 
ctoggle /\ stoggle = rtoggle) /\ 
(spc = SC /\ head = Last + 1 --> rfirst) /\ 
(spc = WR --> ctoggle --> stoggle = rtoggle) /\ 
(spc = WT2 --> rn = 0) /\ 
(spc = SC /\ rn = 0 --> ctoggle --> stoggle = rtoggle) /\ 
(spc = SF --> 
(ctoggle --> stoggle = rtoggle) --> sfirst = rfirst) /\ 
(spc = WR --> 
(ctoggle --> stoggle = rtoggle) --> sfirst = rfirst) /\ 
(spc = WA --> 
(ctoggle --> stoggle = rtoggle) --> sfirst = rfirst) /\ 
(spc = SC --> 
(ctoggle --> stoggle = rtoggle) --> sfirst = rfirst) /\ 
(spc = WT2 --> sfirst) /\ 
(spc = WA --> ~(head = Last + 1)) /\ 
(spc = SF --> ~(head = Last + 1)) /\ 
(rpc = SI \/ rpc = SA \/ rpc = RTS --> spc = WA) /\ 
(rpc = NOK --> spc = WT2) /\ 
(rpc = SI --> #2 msg = (head = Last)) /\ 
(rpc = NOK --> ~ctoggle) /\ 
(rpc = SI --> stoggle = #3 msg) /\ 
(rpc = SA \/ rpc = RTS --> stoggle = #3 msg) /\ 
(rpc = SA \/ rpc = RTS --> 
ctoggle /\ ~(#3 msg = rtoggle)) /\ 
(rpc = WF \/ rpc = RTS --> rtimer_on) /\ 
(rpc = SI --> ctoggle --> #3 msg = rtoggle) /\ 
(rpc = SI --> #4 msg = file[head]) /\ 
(rpc = SI --> rfirst = #1 msg) /\ 
(K_full --> spc = WA /\ rpc = WF /\ ~L) /\ 
(K_full --> #2 K = (head = Last)) /\ 
(K_full --> #3 K = stoggle) /\ 
(K_full --> #4 K = file[head]) /\ 
(K_full --> 
(ctoggle --> #3 K = rtoggle) --> #1 K = rfirst) /\ 
(L --> spc = WA /\ rpc = WF /\ ~K_full) /\ 
(L --> ctoggle /\ ~rtoggle = stoggle) /\ 
(stimer1_enabled --> 
spc = WA /\ rpc = WF /\ ~K_full /\ ~L) /\ 
(stimer2_enabled --> 
spc = WT2 /\ rpc = WF /\ ~K_full /\ ~L) /\ 
(stimer2_enabled --> rfirst) /\ 
(stimer2_enabled --> rfirst) /\ 
(rtimer_enabled --> 
spc = WT2 /\ 
rpc = WF /\ ~K_full /\ ~L /\ ~stimer2_enabled) /\ 
(~(rn = 0) --> ~(spc = WR)) /\ 
(~(rn = 0) /\ ctoggle /\ ~(stoggle = rtoggle) --> 
rfirst = (head = Last)) /\ 
(head = Last + 1 --> spc = WR \/ spc = WT2 \/ spc = SC)) /\ 
spc = WA /\ L --> 
abusy = ((if head = Last then SC else SF) = SF \/ 
        (if head = Last then SC else SF) = WA \/ 
        (if head = Last then SC else SF) = SC) /\ 
afirst = rfirst /\ 
aerror = (rpc = NOK \/ 
         (if head = Last then SC else SF) = WT2 /\ 
         rtimer_on /\ ~rfirst) /\ 
(Forall i : [0..Last + 1] . afile[i] = file[i]) /\ 
ahead = (if (if head = Last then SC else SF) = WT2 \/ 
            (ctoggle --> ~stoggle = rtoggle)
            then if head < Last + 1 then head + 1 else head
            else (if head < Last + 1
                     then head + 1
                     else head) + 1) /\ 
((if head = Last then SC else SF) = WR \/ 
 (if head = Last then SC else SF) = SF \/ 
 (if head = Last then SC else SF) = SC --> rpc = WF) /\ 
((if head = Last then SC else SF) = SF /\ 
 (if ~(head = Last) then 0 else rn) = 0 --> 
ctoggle --> ~stoggle = rtoggle) /\ 
((if head = Last then SC else SF) = WA --> 
~((if ~(head = Last) then 0 else rn) = 0)) /\ 
((if head = Last then SC else SF) = WT2 /\ 
 ~rtimer_enabled --> ~ctoggle) /\ 
((if head = Last then SC else SF) = SC /\ 
 (if head < Last + 1
     then head + 1
     else head) = Last + 1 --> 
ctoggle /\ ~stoggle = rtoggle) /\ 
((if head = Last then SC else SF) = SC /\ 
 (if head < Last + 1
     then head + 1
     else head) = Last + 1 --> rfirst) /\ 
((if head = Last then SC else SF) = WR --> 
ctoggle --> ~stoggle = rtoggle) /\ 
((if head = Last then SC else SF) = WT2 --> 
(if ~(head = Last) then 0 else rn) = 0) /\ 
((if head = Last then SC else SF) = SC /\ 
 (if ~(head = Last) then 0 else rn) = 0 --> 
ctoggle --> ~stoggle = rtoggle) /\ 
((if head = Last then SC else SF) = SF --> 
(ctoggle --> ~stoggle = rtoggle) --> 
head = Last = rfirst) /\ 
((if head = Last then SC else SF) = WR --> 
(ctoggle --> ~stoggle = rtoggle) --> 
head = Last = rfirst) /\ 
((if head = Last then SC else SF) = WA --> 
(ctoggle --> ~stoggle = rtoggle) --> 
head = Last = rfirst) /\ 
((if head = Last then SC else SF) = SC --> 
(ctoggle --> ~stoggle = rtoggle) --> 
head = Last = rfirst) /\ 
((if head = Last then SC else SF) = WT2 --> head = Last) /\ 
((if head = Last then SC else SF) = WA --> 
~((if head < Last + 1
      then head + 1
      else head) = Last + 1)) /\ 
((if head = Last then SC else SF) = SF --> 
~((if head < Last + 1
      then head + 1
      else head) = Last + 1)) /\ 
(rpc = SI \/ rpc = SA \/ rpc = RTS --> 
(if head = Last then SC else SF) = WA) /\ 
(rpc = NOK --> (if head = Last then SC else SF) = WT2) /\ 
(rpc = SI --> 
#2 msg = ((if head < Last + 1
              then head + 1
              else head) = Last)) /\ 
(rpc = NOK --> ~ctoggle) /\ 
(rpc = SI --> ~stoggle = #3 msg) /\ 
(rpc = SA \/ rpc = RTS --> ~stoggle = #3 msg) /\ 
(rpc = SA \/ rpc = RTS --> 
ctoggle /\ ~(#3 msg = rtoggle)) /\ 
(rpc = WF \/ rpc = RTS --> rtimer_on) /\ 
(rpc = SI --> ctoggle --> #3 msg = rtoggle) /\ 
(rpc = SI --> 
#4 msg = file[if head < Last + 1
                  then head + 1
                  else head]) /\ 
(rpc = SI --> rfirst = #1 msg) /\ 
(K_full --> 
(if head = Last then SC else SF) = WA /\ 
rpc = WF /\ ~false) /\ 
(K_full --> 
#2 K = ((if head < Last + 1
            then head + 1
            else head) = Last)) /\ 
(K_full --> #3 K = ~stoggle) /\ 
(K_full --> 
#4 K = file[if head < Last + 1 then head + 1 else head]) /\ 
(K_full --> 
(ctoggle --> #3 K = rtoggle) --> #1 K = rfirst) /\ 
(false --> 
(if head = Last then SC else SF) = WA /\ 
rpc = WF /\ ~K_full) /\ 
(false --> ctoggle /\ ~rtoggle = ~stoggle) /\ 
(false --> 
(if head = Last then SC else SF) = WA /\ 
rpc = WF /\ ~K_full /\ ~false) /\ 
(stimer2_enabled --> 
(if head = Last then SC else SF) = WT2 /\ 
rpc = WF /\ ~K_full /\ ~false) /\ 
(stimer2_enabled --> rfirst) /\ 
(stimer2_enabled --> rfirst) /\ 
(rtimer_enabled --> 
(if head = Last then SC else SF) = WT2 /\ 
rpc = WF /\ ~K_full /\ ~false /\ ~stimer2_enabled) /\ 
(~((if ~(head = Last) then 0 else rn) = 0) --> 
~((if head = Last then SC else SF) = WR)) /\ 
(~((if ~(head = Last) then 0 else rn) = 0) /\ 
 ctoggle /\ ~(~stoggle = rtoggle) --> 
rfirst = ((if head < Last + 1
              then head + 1
              else head) = Last)) /\ 
((if head < Last + 1
     then head + 1
     else head) = Last + 1 --> 
(if head = Last then SC else SF) = WR \/ 
(if head = Last then SC else SF) = WT2 \/ 
(if head = Last then SC else SF) = SC)
Philips 7 

(abusy = (spc = SF \/ spc = WA \/ spc = SC) /\ 
afirst = rfirst /\ 
aerror = (rpc = NOK \/ 
         spc = WT2 /\ rtimer_on /\ ~rfirst) /\ 
(Forall i : [0..Last + 1] . afile[i] = file[i]) /\ 
ahead = (if spc = WT2 \/ (ctoggle --> stoggle = rtoggle)
            then head
            else head + 1) /\ 
(spc = WR \/ spc = SF \/ spc = SC --> rpc = WF) /\ 
(spc = SF /\ rn = 0 --> ctoggle --> stoggle = rtoggle) /\ 
(spc = WA --> ~(rn = 0)) /\ 
(spc = WT2 /\ ~rtimer_enabled --> ~ctoggle) /\ 
(spc = SC /\ head = Last + 1 --> 
ctoggle /\ stoggle = rtoggle) /\ 
(spc = SC /\ head = Last + 1 --> rfirst) /\ 
(spc = WR --> ctoggle --> stoggle = rtoggle) /\ 
(spc = WT2 --> rn = 0) /\ 
(spc = SC /\ rn = 0 --> ctoggle --> stoggle = rtoggle) /\ 
(spc = SF --> 
(ctoggle --> stoggle = rtoggle) --> sfirst = rfirst) /\ 
(spc = WR --> 
(ctoggle --> stoggle = rtoggle) --> sfirst = rfirst) /\ 
(spc = WA --> 
(ctoggle --> stoggle = rtoggle) --> sfirst = rfirst) /\ 
(spc = SC --> 
(ctoggle --> stoggle = rtoggle) --> sfirst = rfirst) /\ 
(spc = WT2 --> sfirst) /\ 
(spc = WA --> ~(head = Last + 1)) /\ 
(spc = SF --> ~(head = Last + 1)) /\ 
(rpc = SI \/ rpc = SA \/ rpc = RTS --> spc = WA) /\ 
(rpc = NOK --> spc = WT2) /\ 
(rpc = SI --> #2 msg = (head = Last)) /\ 
(rpc = NOK --> ~ctoggle) /\ 
(rpc = SI --> stoggle = #3 msg) /\ 
(rpc = SA \/ rpc = RTS --> stoggle = #3 msg) /\ 
(rpc = SA \/ rpc = RTS --> 
ctoggle /\ ~(#3 msg = rtoggle)) /\ 
(rpc = WF \/ rpc = RTS --> rtimer_on) /\ 
(rpc = SI --> ctoggle --> #3 msg = rtoggle) /\ 
(rpc = SI --> #4 msg = file[head]) /\ 
(rpc = SI --> rfirst = #1 msg) /\ 
(K_full --> spc = WA /\ rpc = WF /\ ~L) /\ 
(K_full --> #2 K = (head = Last)) /\ 
(K_full --> #3 K = stoggle) /\ 
(K_full --> #4 K = file[head]) /\ 
(K_full --> 
(ctoggle --> #3 K = rtoggle) --> #1 K = rfirst) /\ 
(L --> spc = WA /\ rpc = WF /\ ~K_full) /\ 
(L --> ctoggle /\ ~rtoggle = stoggle) /\ 
(stimer1_enabled --> 
spc = WA /\ rpc = WF /\ ~K_full /\ ~L) /\ 
(stimer2_enabled --> 
spc = WT2 /\ rpc = WF /\ ~K_full /\ ~L) /\ 
(stimer2_enabled --> rfirst) /\ 
(stimer2_enabled --> rfirst) /\ 
(rtimer_enabled --> 
spc = WT2 /\ 
rpc = WF /\ ~K_full /\ ~L /\ ~stimer2_enabled) /\ 
(~(rn = 0) --> ~(spc = WR)) /\ 
(~(rn = 0) /\ ctoggle /\ ~(stoggle = rtoggle) --> 
rfirst = (head = Last)) /\ 
(head = Last + 1 --> spc = WR \/ spc = WT2 \/ spc = SC)) /\ 
spc = SC /\ ~conf_full /\ head = Last + 1 --> 
false = (WR = SF \/ WR = WA \/ WR = SC) /\ 
afirst = rfirst /\ 
~afirst = (rpc = NOK \/ 
          WR = WT2 /\ rtimer_on /\ ~rfirst) /\ 
(Forall i : [0..Last + 1] . afile[i] = file[i]) /\ 
Last + 
1 = (if WR = WT2 \/ (ctoggle --> stoggle = rtoggle)
        then Last + 1
        else Last + 1 + 1) /\ 
(WR = WR \/ WR = SF \/ WR = SC --> rpc = WF) /\ 
(WR = SF /\ 0 = 0 --> ctoggle --> stoggle = rtoggle) /\ 
(WR = WA --> ~(0 = 0)) /\ 
(WR = WT2 /\ ~rtimer_enabled --> ~ctoggle) /\ 
(WR = SC /\ Last + 1 = Last + 1 --> 
ctoggle /\ stoggle = rtoggle) /\ 
(WR = SC /\ Last + 1 = Last + 1 --> rfirst) /\ 
(WR = WR --> ctoggle --> stoggle = rtoggle) /\ 
(WR = WT2 --> 0 = 0) /\ 
(WR = SC /\ 0 = 0 --> ctoggle --> stoggle = rtoggle) /\ 
(WR = SF --> 
(ctoggle --> stoggle = rtoggle) --> sfirst = rfirst) /\ 
(WR = WR --> 
(ctoggle --> stoggle = rtoggle) --> sfirst = rfirst) /\ 
(WR = WA --> 
(ctoggle --> stoggle = rtoggle) --> sfirst = rfirst) /\ 
(WR = SC --> 
(ctoggle --> stoggle = rtoggle) --> sfirst = rfirst) /\ 
(WR = WT2 --> sfirst) /\ 
(WR = WA --> ~(Last + 1 = Last + 1)) /\ 
(WR = SF --> ~(Last + 1 = Last + 1)) /\ 
(rpc = SI \/ rpc = SA \/ rpc = RTS --> WR = WA) /\ 
(rpc = NOK --> WR = WT2) /\ 
(rpc = SI --> #2 msg = (Last + 1 = Last)) /\ 
(rpc = NOK --> ~ctoggle) /\ 
(rpc = SI --> stoggle = #3 msg) /\ 
(rpc = SA \/ rpc = RTS --> stoggle = #3 msg) /\ 
(rpc = SA \/ rpc = RTS --> 
ctoggle /\ ~(#3 msg = rtoggle)) /\ 
(rpc = WF \/ rpc = RTS --> rtimer_on) /\ 
(rpc = SI --> ctoggle --> #3 msg = rtoggle) /\ 
(rpc = SI --> #4 msg = file[Last + 1]) /\ 
(rpc = SI --> rfirst = #1 msg) /\ 
(K_full --> WR = WA /\ rpc = WF /\ ~L) /\ 
(K_full --> #2 K = (Last + 1 = Last)) /\ 
(K_full --> #3 K = stoggle) /\ 
(K_full --> #4 K = file[Last + 1]) /\ 
(K_full --> 
(ctoggle --> #3 K = rtoggle) --> #1 K = rfirst) /\ 
(L --> WR = WA /\ rpc = WF /\ ~K_full) /\ 
(L --> ctoggle /\ ~rtoggle = stoggle) /\ 
(stimer1_enabled --> 
WR = WA /\ rpc = WF /\ ~K_full /\ ~L) /\ 
(stimer2_enabled --> 
WR = WT2 /\ rpc = WF /\ ~K_full /\ ~L) /\ 
(stimer2_enabled --> rfirst) /\ 
(stimer2_enabled --> rfirst) /\ 
(rtimer_enabled --> 
WR = WT2 /\ 
rpc = WF /\ ~K_full /\ ~L /\ ~stimer2_enabled) /\ 
(~(0 = 0) --> ~(WR = WR)) /\ 
(~(0 = 0) /\ ctoggle /\ ~(stoggle = rtoggle) --> 
rfirst = (Last + 1 = Last)) /\ 
(Last + 1 = Last + 1 --> WR = WR \/ WR = WT2 \/ WR = SC)
Philips 8 

(abusy = (spc = SF \/ spc = WA \/ spc = SC) /\ 
afirst = rfirst /\ 
aerror = (rpc = NOK \/ 
         spc = WT2 /\ rtimer_on /\ ~rfirst) /\ 
(Forall i : [0..Last + 1] . afile[i] = file[i]) /\ 
ahead = (if spc = WT2 \/ (ctoggle --> stoggle = rtoggle)
            then head
            else head + 1) /\ 
(spc = WR \/ spc = SF \/ spc = SC --> rpc = WF) /\ 
(spc = SF /\ rn = 0 --> ctoggle --> stoggle = rtoggle) /\ 
(spc = WA --> ~(rn = 0)) /\ 
(spc = WT2 /\ ~rtimer_enabled --> ~ctoggle) /\ 
(spc = SC /\ head = Last + 1 --> 
ctoggle /\ stoggle = rtoggle) /\ 
(spc = SC /\ head = Last + 1 --> rfirst) /\ 
(spc = WR --> ctoggle --> stoggle = rtoggle) /\ 
(spc = WT2 --> rn = 0) /\ 
(spc = SC /\ rn = 0 --> ctoggle --> stoggle = rtoggle) /\ 
(spc = SF --> 
(ctoggle --> stoggle = rtoggle) --> sfirst = rfirst) /\ 
(spc = WR --> 
(ctoggle --> stoggle = rtoggle) --> sfirst = rfirst) /\ 
(spc = WA --> 
(ctoggle --> stoggle = rtoggle) --> sfirst = rfirst) /\ 
(spc = SC --> 
(ctoggle --> stoggle = rtoggle) --> sfirst = rfirst) /\ 
(spc = WT2 --> sfirst) /\ 
(spc = WA --> ~(head = Last + 1)) /\ 
(spc = SF --> ~(head = Last + 1)) /\ 
(rpc = SI \/ rpc = SA \/ rpc = RTS --> spc = WA) /\ 
(rpc = NOK --> spc = WT2) /\ 
(rpc = SI --> #2 msg = (head = Last)) /\ 
(rpc = NOK --> ~ctoggle) /\ 
(rpc = SI --> stoggle = #3 msg) /\ 
(rpc = SA \/ rpc = RTS --> stoggle = #3 msg) /\ 
(rpc = SA \/ rpc = RTS --> 
ctoggle /\ ~(#3 msg = rtoggle)) /\ 
(rpc = WF \/ rpc = RTS --> rtimer_on) /\ 
(rpc = SI --> ctoggle --> #3 msg = rtoggle) /\ 
(rpc = SI --> #4 msg = file[head]) /\ 
(rpc = SI --> rfirst = #1 msg) /\ 
(K_full --> spc = WA /\ rpc = WF /\ ~L) /\ 
(K_full --> #2 K = (head = Last)) /\ 
(K_full --> #3 K = stoggle) /\ 
(K_full --> #4 K = file[head]) /\ 
(K_full --> 
(ctoggle --> #3 K = rtoggle) --> #1 K = rfirst) /\ 
(L --> spc = WA /\ rpc = WF /\ ~K_full) /\ 
(L --> ctoggle /\ ~rtoggle = stoggle) /\ 
(stimer1_enabled --> 
spc = WA /\ rpc = WF /\ ~K_full /\ ~L) /\ 
(stimer2_enabled --> 
spc = WT2 /\ rpc = WF /\ ~K_full /\ ~L) /\ 
(stimer2_enabled --> rfirst) /\ 
(stimer2_enabled --> rfirst) /\ 
(rtimer_enabled --> 
spc = WT2 /\ 
rpc = WF /\ ~K_full /\ ~L /\ ~stimer2_enabled) /\ 
(~(rn = 0) --> ~(spc = WR)) /\ 
(~(rn = 0) /\ ctoggle /\ ~(stoggle = rtoggle) --> 
rfirst = (head = Last)) /\ 
(head = Last + 1 --> spc = WR \/ spc = WT2 \/ spc = SC)) /\ 
spc = SC /\ ~conf_full /\ ~(head = Last + 1) --> 
false = (WT2 = SF \/ WT2 = WA \/ WT2 = SC) /\ 
afirst = rfirst /\ 
~afirst = (rpc = NOK \/ 
          WT2 = WT2 /\ rtimer_on /\ ~rfirst) /\ 
(Forall i : [0..Last + 1] . afile[i] = file[i]) /\ 
Last + 
1 = (if WT2 = WT2 \/ (ctoggle --> ~stoggle = rtoggle)
        then Last + 1
        else Last + 1 + 1) /\ 
(WT2 = WR \/ WT2 = SF \/ WT2 = SC --> rpc = WF) /\ 
(WT2 = SF /\ 0 = 0 --> ctoggle --> ~stoggle = rtoggle) /\ 
(WT2 = WA --> ~(0 = 0)) /\ 
(WT2 = WT2 /\ ~true --> ~ctoggle) /\ 
(WT2 = SC /\ Last + 1 = Last + 1 --> 
ctoggle /\ ~stoggle = rtoggle) /\ 
(WT2 = SC /\ Last + 1 = Last + 1 --> rfirst) /\ 
(WT2 = WR --> ctoggle --> ~stoggle = rtoggle) /\ 
(WT2 = WT2 --> 0 = 0) /\ 
(WT2 = SC /\ 0 = 0 --> ctoggle --> ~stoggle = rtoggle) /\ 
(WT2 = SF --> 
(ctoggle --> ~stoggle = rtoggle) --> true = rfirst) /\ 
(WT2 = WR --> 
(ctoggle --> ~stoggle = rtoggle) --> true = rfirst) /\ 
(WT2 = WA --> 
(ctoggle --> ~stoggle = rtoggle) --> true = rfirst) /\ 
(WT2 = SC --> 
(ctoggle --> ~stoggle = rtoggle) --> true = rfirst) /\ 
(WT2 = WT2 --> true) /\ 
(WT2 = WA --> ~(Last + 1 = Last + 1)) /\ 
(WT2 = SF --> ~(Last + 1 = Last + 1)) /\ 
(rpc = SI \/ rpc = SA \/ rpc = RTS --> WT2 = WA) /\ 
(rpc = NOK --> WT2 = WT2) /\ 
(rpc = SI --> #2 msg = (Last + 1 = Last)) /\ 
(rpc = NOK --> ~ctoggle) /\ 
(rpc = SI --> ~stoggle = #3 msg) /\ 
(rpc = SA \/ rpc = RTS --> ~stoggle = #3 msg) /\ 
(rpc = SA \/ rpc = RTS --> 
ctoggle /\ ~(#3 msg = rtoggle)) /\ 
(rpc = WF \/ rpc = RTS --> rtimer_on) /\ 
(rpc = SI --> ctoggle --> #3 msg = rtoggle) /\ 
(rpc = SI --> #4 msg = file[Last + 1]) /\ 
(rpc = SI --> rfirst = #1 msg) /\ 
(K_full --> WT2 = WA /\ rpc = WF /\ ~L) /\ 
(K_full --> #2 K = (Last + 1 = Last)) /\ 
(K_full --> #3 K = ~stoggle) /\ 
(K_full --> #4 K = file[Last + 1]) /\ 
(K_full --> 
(ctoggle --> #3 K = rtoggle) --> #1 K = rfirst) /\ 
(L --> WT2 = WA /\ rpc = WF /\ ~K_full) /\ 
(L --> ctoggle /\ ~rtoggle = ~stoggle) /\ 
(stimer1_enabled --> 
WT2 = WA /\ rpc = WF /\ ~K_full /\ ~L) /\ 
(stimer2_enabled --> 
WT2 = WT2 /\ rpc = WF /\ ~K_full /\ ~L) /\ 
(stimer2_enabled --> rfirst) /\ 
(stimer2_enabled --> rfirst) /\ 
(true --> 
WT2 = WT2 /\ 
rpc = WF /\ ~K_full /\ ~L /\ ~stimer2_enabled) /\ 
(~(0 = 0) --> ~(WT2 = WR)) /\ 
(~(0 = 0) /\ ctoggle /\ ~(~stoggle = rtoggle) --> 
rfirst = (Last + 1 = Last)) /\ 
(Last + 1 = Last + 1 --> WT2 = WR \/ WT2 = WT2 \/ WT2 = SC)

Running Times:


   Philips 1: (94 lines, 57 leaves)
        usr  :  2.7300
        sys  :  0.0400
        gc   :  0.1400

   Philips 2: (123 lines, 89 leaves)
        usr  :  1.4000
        sys  :  0.0900
        gc   :  0.0700

   Philips 3: (123 lines, 24 leaves)
        usr  :  0.5500
        sys  :  0.0100
        gc   :  0.0100

   Philips 4: (123 lines, 58 leaves)
        usr  :  0.7900
        sys  :  0.0500
        gc   :  0.0500

   Philips 5: (141 lines, 601 leaves)
        usr  :  4.6500
        sys  :  0.4000
        gc   :  0.1400

   Philips 6: (188 lines, 143 leaves)
        usr  :  1.7500
        sys  :  0.0400
        gc   :  0.1700

   Philips 7: (125 lines, 33 leaves)
        usr  :  0.7200
        sys  :  0.0300
        gc   :  0.0500

   Philips 8:	(125 lines, 218 leaves)
        usr  :  2.4200
        sys  :  0.0500
        gc   :  0.0800
Each verification condition instantiates 1 existentially quantified variable.

Verification of the conjunction of the eight formulas at one time takes 100 seconds and examines 5636 branches.

Go back to the top of this page.