:comment  DARPI  (Master Thesis by Andrea Di Pasquale)
:comment  Elena Pagani -- Last update: June 29, 2017

:comment  SIMULO SOLO LE TRANSIZIONI CON 2 COME OGGETTO
  
:comment  Modelization with malicious hosts; no cache aging
:comment  All packets are sent broadcast, but processed just by the target
:comment  Any node (but victim) may behave maliciously against the victim.
:comment  Victim is node 2
:comment  "Honest" is any node behaving properly but different from victim

:comment  probe replay signals IP address conflict
:comment  unconfigured nodes can just send Probe and do not process any message

:comment  PROPERTY: safety (no MitM)


:index nat
:smt (define N::nat)

:comment  phi counts the phase of the computation
:global phi nat
:comment  I indicates whether at this phase all hosts performed their actions
:global I int

:comment  LOCAL CLOCK: new call when TS = 100 (= 1s.)  --> T24
:comment  TS indicates the time elapsed from the last timeout
:local TS nat
:comment  flag for host sending message
:local sm nat
:comment  MAC of victim in caches
:local CM nat
:comment  IP of victim in caches
:local CP nat
:comment  flag for host updating cache
:local cu nat

:comment  all addresses (both MAC and IP) equal the node ID
:comment  target ip address
:global tp nat
:comment  source hardware address
:global sh nat
:comment  source ip address
:global sp nat

:comment  variables to manage the DARPI_cache
:comment  flag remembering execution of Verify on behalf of every node
:local fv nat
:comment  target address in DARPI_cache
:local tD nat
:comment  time (clock) in DARPI_cache
:local cD nat
:comment  target of a (Probe) Reply
:local tg nat


:comment  ------- SYSTEM AXIOMS -------
:comment  none


:comment  ------- SUGGESTED INVARIANTS -------
:suggested_negated_invariants
:var z1
:cnj (not (= CP[z1] 0)) (not (= CP[z1] 2))
:cnj (not (= tD[z1] 0)) (not (= tD[z1] 2))
:end_of_suggested_negated_invariants


:comment  ------- INITIAL & UNSAFE -------

:initial
:var x
:comment  no process has done anything; this includes Clean() policy
:comment  lines 4-5 Algorithm 1
:cnj (= phi 0) (= I 0) (>= TS[x] 0) (< TS[x] 100) (= sh 0) (= sp 0) (= tp 0) (= sm[x] 0) (= CM[x] 0) (= CP[x] 0) (= cu[x] 0) (= fv[x] 0) (= tD[x] 0) (= cD[x] 0) (= tg[x] 0)


:unsafe
:var z1
:comment  MITM VERIFICATION - uncomment subsequent conjunct
:comment  >=1 process remembers MAC(v)!= v for IP(v)=v
:comment  cnj (not (= CM[z1] 2)) (= CP[z1] 2)
:cnj (not (= CM[z1] CP[z1]))

:u_cnj (> phi 5) (> I N) (> sm[z1] 2) (> cu[z1] 1) (> fv[z1] 1)

:comment  max_domain_cardinality 3



:comment  ------- TRANSITIONS -------

:comment  T1
:comment  node V sends a HONEST base Request
:comment  go to T4
:transition
:var x
:var y
:var j
:guard (= phi 0) (= x 2) (not (= TS[x] 100))
:numcases 2
:case (= x j)
:val 2
:val 1
:val (+ TS[j] 1)
:val sm[j]
:val CM[j]
:val CP[j]
:val 1
:val y
:val x
:val x
:val fv[j]
:val tD[j]
:val cD[j]
:val tg[j]
:case (not (= x j))
:val 2
:val 1
:val (+ TS[j] 1)
:val sm[j]
:val CM[j]
:val CP[j]
:val 0
:val y
:val x
:val x
:val fv[j]
:val tD[j]
:val cD[j]
:val tg[j]


:comment  T2
:comment  node sends a HONEST base Request to V
:comment  update DARPI_cache -- go to T4
:transition
:var x
:var j
:guard (= phi 0) (not (= x 2)) (not (= TS[x] 100))
:numcases 2
:case (= x j)
:val 2
:val 1
:val (+ TS[j] 1)
:val sm[j]
:val CM[j]
:val CP[j]
:val 1
:val 2
:val x
:val x
:val fv[j]
:val 2
:val TS[j]
:val tg[j]
:case (not (= x j))
:val 2
:val 1
:val (+ TS[j] 1)
:val sm[j]
:val CM[j]
:val CP[j]
:val 0
:val 2
:val x
:val x
:val fv[j]
:val tD[j]
:val cD[j]
:val tg[j]


:comment  T3
:comment  host sends a MALICIOUS Gratuitous Request (broadcast)
:comment  source != victim and configured; go to T8 and successive
:transition
:var x
:var j
:guard (= phi 0) (not (= x 2)) (not (= TS[x] 100))
:numcases 2
:case (= x j)
:val 2
:val 1
:val (+ TS[j] 1)
:val sm[j]
:val CM[j]
:val CP[j]
:val 1
:val 2
:val x
:val 2
:val fv[j]
:val tD[j]
:val cD[j]
:val tg[j]
:case (not (= x j))
:val 2
:val 1
:val (+ TS[j] 1)
:val sm[j]
:val CM[j]
:val CP[j]
:val 0
:val 2
:val x
:val 2
:val fv[j]
:val tD[j]
:val cD[j]
:val tg[j]


:comment  T4
:comment  host sends a MALICIOUS base Request (broadcast)
:comment  source != victim and configured; target chosen different from victim
:comment  goto T8 and successive
:transition
:var x
:var y
:var j
:guard (= phi 0) (not (= x 2)) (not (= y 2)) (= sm[y] 0) (not (= TS[x] 100))
:numcases 2
:case (= x j)
:val 2
:val 1
:val (+ TS[j] 1)
:val sm[j]
:val CM[j]
:val CP[j]
:val 1
:val y
:val x
:val 2
:val fv[j]
:val tD[j]
:val cD[j]
:val tg[j]
:case (not (= x j))
:val 2
:val 1
:val (+ TS[j] 1)
:val sm[j]
:val CM[j]
:val CP[j]
:val 0
:val y
:val x
:val 2
:val fv[j]
:val tD[j]
:val cD[j]
:val tg[j]


:comment  T5
:comment  host sends a MALICIOUS unsolicited Reply (broadcast)
:comment  source != victim and configured; target chosen different from victim
:comment  go to T27 and successive
:transition
:var x
:var y
:var j
:guard (= phi 0) (not (= x 2)) (not (= y 2)) (not (= TS[x] 100))
:numcases 2
:case (= x j)
:val 5
:val 1
:val (+ TS[j] 1)
:val sm[j]
:val CM[j]
:val CP[j]
:val 1
:val y
:val x
:val 2
:val fv[j]
:val tD[j]
:val cD[j]
:val tg[j]
:case (not (= x j))
:val 5
:val 1
:val (+ TS[j] 1)
:val sm[j]
:val CM[j]
:val CP[j]
:val 0
:val y
:val x
:val 2
:val fv[j]
:val tD[j]
:val cD[j]
:val tg[j]


:comment ============ END OF REQUEST GENERATION ============
:comment ============ REQUEST PROCESSING ============


:comment  T6
:comment  Request processing when not announce and node != target --> skip
:comment  just for configured nodes -- lines 44-46 Algorithm 3
:transition
:var x
:var j
:guard (= phi 2) (= cu[x] 0) (< I N) (not (= sh x)) (not (= x tp)) (not (= sp tp)) (not (= TS[x] 100))
:numcases 2
:case (= x j)
:val phi
:val (+ I 1)
:val TS[j]
:val sm[j]
:val CM[j]
:val CP[j]
:val 1
:val tp
:val sh
:val sp
:val fv[j]
:val tD[j]
:val cD[j]
:val tg[j]
:case (not (= x j))
:val phi
:val (+ I 1)
:val TS[j]
:val sm[j]
:val CM[j]
:val CP[j]
:val cu[j]
:val tp
:val sh
:val sp
:val fv[j]
:val tD[j]
:val cD[j]
:val tg[j]


:comment  T7
:comment  Request processing when announce and source!=victim and source!=myIP --> skip
:comment  lines 44-46 Algorithm 3 -- just for configured nodes
:comment  it would call SARPI
:transition
:var x
:var j
:guard (= phi 2) (= cu[x] 0) (< I N) (= sp tp) (not (= sp x)) (not (= sp 2)) (not (= TS[x] 100))
:numcases 2
:case (= x j)
:val phi
:val (+ I 1)
:val TS[j]
:val sm[j]
:val CM[j]
:val CP[j]
:val 1
:val tp
:val sh
:val sp
:val fv[j]
:val tD[j]
:val cD[j]
:val tg[j]
:case (not (= x j))
:val phi
:val (+ I 1)
:val TS[j]
:val sm[j]
:val CM[j]
:val CP[j]
:val cu[j]
:val tp
:val sh
:val sp
:val fv[j]
:val tD[j]
:val cD[j]
:val tg[j]


:comment  T8
:comment  Request processing when announce and source=victim and source!=myIP
:comment  lines 14-16 Algorithm 3 -- just for configured nodes
:comment  it calls Verify() + Deny(); DARPI_cache updated upon Req generation
:transition
:var x
:var j
:guard (= phi 2) (= cu[x] 0) (< I N) (= sp tp) (not (= sp x)) (= sp 2) (not (= TS[x] 100))
:numcases 2
:case (= x j)
:val phi
:val (+ I 1)
:val TS[j]
:val sm[j]
:val 0
:val 0
:val 1
:val tp
:val sh
:val sp
:val 1
:val tD[j]
:val cD[j]
:val tg[j]
:case (not (= x j))
:val phi
:val (+ I 1)
:val TS[j]
:val sm[j]
:val CM[j]
:val CP[j]
:val cu[j]
:val tp
:val sh
:val sp
:val fv[j]
:val tD[j]
:val cD[j]
:val tg[j]


:comment  T9
:comment  Base Request processing when target and source!=myIP and source!=victim
:comment  lines 44-46 Algorithm 3 -- just for configured nodes
:comment  it would generate a Reply and call SARPI
:transition
:var x
:var j
:guard (= phi 2) (= cu[x] 0) (< I N) (not (= sp tp)) (= tp x) (not (= sp x)) (not (= sp 2)) (not (= TS[x] 100))
:numcases 2
:case (= x j)
:val phi
:val (+ I 1)
:val TS[j]
:val 1
:val CM[j]
:val CP[j]
:val 1
:val tp
:val sh
:val sp
:val fv[j]
:val tD[j]
:val cD[j]
:val sp
:case (not (= x j))
:val phi
:val (+ I 1)
:val TS[j]
:val sm[j]
:val CM[j]
:val CP[j]
:val cu[j]
:val tp
:val sh
:val sp
:val fv[j]
:val tD[j]
:val cD[j]
:val tg[j]


:comment  T10
:comment  Base Request processing when target and source!=myIP and source=victim and source not in DARPI_cache
:comment  lines 17-25 Algorithm 3 -- just for configured nodes
:comment  it generates a Reply and calls Verify() + Deny(); DARPI_cache updated upon Req generation
:transition
:var x
:var j
:guard (= phi 2) (= cu[x] 0) (< I N) (not (= sp tp)) (= tp x) (not (= sp x)) (= sp 2) (not (= tD[x] sp)) (not (= TS[x] 100))
:numcases 2
:case (= x j)
:val phi
:val (+ I 1)
:val TS[j]
:val 1
:val 0
:val 0
:val 1
:val tp
:val sh
:val sp
:val 1
:val tD[j]
:val cD[j]
:val sp
:case (not (= x j))
:val phi
:val (+ I 1)
:val TS[j]
:val sm[j]
:val CM[j]
:val CP[j]
:val cu[j]
:val tp
:val sh
:val sp
:val fv[j]
:val tD[j]
:val cD[j]
:val tg[j]


:comment  T11
:comment  Base Request processing when target and source!=myIP and source=victim and source in DARPI_cache
:comment  lines 17-25 Algorithm 3 -- just for configured nodes
:comment  it generates a Reply and calls Deny()
:transition
:var x
:var j
:guard (= phi 2) (= cu[x] 0) (< I N) (not (= sp tp)) (= tp x) (not (= sp x)) (= sp 2) (= tD[x] sp) (not (= TS[x] 100))
:numcases 2
:case (= x j)
:val phi
:val (+ I 1)
:val TS[j]
:val 1
:val 0
:val 0
:val 1
:val tp
:val sh
:val sp
:val fv[j]
:val tD[j]
:val cD[j]
:val sp
:case (not (= x j))
:val phi
:val (+ I 1)
:val TS[j]
:val sm[j]
:val CM[j]
:val CP[j]
:val cu[j]
:val tp
:val sh
:val sp
:val fv[j]
:val tD[j]
:val cD[j]
:val tg[j]


:comment ============ END OF REQUEST PROCESSING ============
:comment ============ GENERATION OF VERIFICATIONS ============


:comment  T12
:comment  host performs Verify() --> HONEST Request generation
:comment  DARPI_cache updated -- lines 11-13 Algorithm 3
:comment  TS incremented of 1 tick for Request processing and verification generation 
:transition
:var x
:var j
:guard (= phi 2) (>= I N) (= cu[x] 1) (= fv[x] 1) (not (= TS[x] 100))
:numcases 2
:case (= x j)
:val 3
:val 1
:val (+ TS[j] 1)
:val sm[j]
:val CM[j]
:val CP[j]
:val 1
:val 2
:val x
:val x
:val 0
:val 2
:val TS[j]
:val tg[j]
:case (not (= x j))
:val 3
:val 1
:val (+ TS[j] 1)
:val sm[j]
:val CM[j]
:val CP[j]
:val 0
:val 2
:val x
:val x
:val fv[j]
:val tD[j]
:val cD[j]
:val tg[j]


:comment  T13
:comment  no host has verifications to send --> goto Reply generation
:transition
:var x
:var j
:guard (= phi 2) (>= I N) (= cu[x] 1) (= fv[x] 0) (not (= TS[x] 100))
:uguard (= fv[j] 0)
:numcases 2
:case (= x j)
:val 4
:val I
:val TS[j]
:val sm[j]
:val CM[j]
:val CP[j]
:val cu[j]
:val tp
:val sh
:val sp
:val fv[j]
:val tD[j]
:val cD[j]
:val tg[j]
:case (not (= x j))
:val 4
:val I
:val TS[j]
:val sm[j]
:val CM[j]
:val CP[j]
:val cu[j]
:val tp
:val sh
:val sp
:val fv[j]
:val tD[j]
:val cD[j]
:val tg[j]


:comment ============ END OF VERIFICATION GENERATION ============
:comment ============ VERIFICATION PROCESSING ============


:comment  T14
:comment  Request processing when not announce and node != target --> skip
:comment  just for configured nodes -- lines 44-46 Algorithm 3
:transition
:var x
:var j
:guard (= phi 3) (= cu[x] 0) (< I N) (not (= sh x)) (not (= x tp)) (not (= sp tp)) (not (= TS[x] 100))
:numcases 2
:case (= x j)
:val phi
:val (+ I 1)
:val TS[j]
:val sm[j]
:val CM[j]
:val CP[j]
:val 1
:val tp
:val sh
:val sp
:val fv[j]
:val tD[j]
:val cD[j]
:val tg[j]
:case (not (= x j))
:val phi
:val (+ I 1)
:val TS[j]
:val sm[j]
:val CM[j]
:val CP[j]
:val cu[j]
:val tp
:val sh
:val sp
:val fv[j]
:val tD[j]
:val cD[j]
:val tg[j]


:comment  T15
:comment  Base Request processing when target and source!=myIP and source!=victim
:comment  lines 44-46 Algorithm 3 -- just for configured nodes
:comment  it would generate a Reply and call SARPI
:transition
:var x
:var j
:guard (= phi 3) (= cu[x] 0) (< I N) (not (= sp tp)) (= tp x) (not (= sp x)) (not (= sp 2)) (not (= TS[x] 100))
:numcases 2
:case (= x j)
:val phi
:val (+ I 1)
:val TS[j]
:val 1
:val CM[j]
:val CP[j]
:val 1
:val tp
:val sh
:val sp
:val fv[j]
:val tD[j]
:val cD[j]
:val sp
:case (not (= x j))
:val phi
:val (+ I 1)
:val TS[j]
:val sm[j]
:val CM[j]
:val CP[j]
:val cu[j]
:val tp
:val sh
:val sp
:val fv[j]
:val tD[j]
:val cD[j]
:val tg[j]


:comment  T16
:comment  Base Request processing when target and source!=myIP and source=victim and source in DARPI_cache
:comment  lines 17-25 Algorithm 3 -- just for configured nodes
:comment  it generates a Reply and calls Deny()
:transition
:var x
:var j
:guard (= phi 3) (= cu[x] 0) (< I N) (not (= sp tp)) (= tp x) (not (= sp x)) (= sp 2) (= tD[x] sp) (not (= TS[x] 100))
:numcases 2
:case (= x j)
:val phi
:val (+ I 1)
:val TS[j]
:val 1
:val 0
:val 0
:val 1
:val tp
:val sh
:val sp
:val fv[j]
:val tD[j]
:val cD[j]
:val sp
:case (not (= x j))
:val phi
:val (+ I 1)
:val TS[j]
:val sm[j]
:val CM[j]
:val CP[j]
:val cu[j]
:val tp
:val sh
:val sp
:val fv[j]
:val tD[j]
:val cD[j]
:val tg[j]


:comment  T17
:comment  Base Request processing when target and source!=myIP and source=victim and source not in DARPI_cache
:comment  lines 17-25 Algorithm 3 -- just for configured nodes
:comment  it generates a Reply and calls Verify()+Deny()
:transition
:var x
:var j
:guard (= phi 3) (= cu[x] 0) (< I N) (not (= sp tp)) (= tp x) (not (= sp x)) (= sp 2) (not (= tD[x] sp)) (not (= TS[x] 100))
:numcases 2
:case (= x j)
:val phi
:val (+ I 1)
:val TS[j]
:val 1
:val 0
:val 0
:val 1
:val tp
:val sh
:val sp
:val 1
:val tD[j]
:val cD[j]
:val sp
:case (not (= x j))
:val phi
:val (+ I 1)
:val TS[j]
:val sm[j]
:val CM[j]
:val CP[j]
:val cu[j]
:val tp
:val sh
:val sp
:val fv[j]
:val tD[j]
:val cD[j]
:val tg[j]


:comment  T18
:comment  all hosts processed (verification) Request --> go back to loop
:transition
:var x
:var j
:guard (= phi 3) (= cu[x] 1) (>= I N)
:numcases 2
:case (= x j)
:val 2
:val I
:val TS[j]
:val sm[j]
:val CM[j]
:val CP[j]
:val cu[j]
:val tp
:val sh
:val sp
:val fv[j]
:val tD[j]
:val cD[j]
:val tg[j]
:case (not (= x j))
:val 2
:val I
:val TS[j]
:val sm[j]
:val CM[j]
:val CP[j]
:val cu[j]
:val tp
:val sh
:val sp
:val fv[j]
:val tD[j]
:val cD[j]
:val tg[j]


:comment ============ END OF VERIFICATION PROCESSING ============
:comment ============ REPLY GENERATION ============


:comment  T19
:comment  target generates HONEST Reply (broadcast)
:comment  TS incremented of 1 tick for Request processing and Reply generation 
:transition
:var x
:var j
:guard (= phi 4) (= sm[x] 1) (not (= TS[x] 100))
:numcases 2
:case (= x j)
:val 5
:val 1
:val (+ TS[j] 1)
:val 0
:val CM[j]
:val CP[j]
:val 1
:val tg[x]
:val x
:val x
:val fv[j]
:val tD[j]
:val cD[j]
:val 0
:case (not (= x j))
:val 5
:val 1
:val (+ TS[j] 1)
:val sm[j]
:val CM[j]
:val CP[j]
:val 0
:val tg[x]
:val x
:val x
:val fv[j]
:val tD[j]
:val cD[j]
:val tg[j]


:comment  T20
:comment  target generates MALICIOUS Reply (broadcast)
:comment  neither target nor Request source are the victim
:comment  TS incremented of 1 tick for Request processing and Reply generation 
:transition
:var x
:var j
:guard (= phi 4) (= sm[x] 1) (not (= x 2)) (not (= tg[x] 2)) (not (= TS[x] 100))
:numcases 2
:case (= x j)
:val 5
:val 1
:val (+ TS[j] 1)
:val 0
:val CM[j]
:val CP[j]
:val 1
:val tg[x]
:val x
:val 2
:val fv[j]
:val tD[j]
:val cD[j]
:val 0
:case (not (= x j))
:val 5
:val 1
:val (+ TS[j] 1)
:val sm[j]
:val CM[j]
:val CP[j]
:val 0
:val tg[x]
:val x
:val 2
:val fv[j]
:val tD[j]
:val cD[j]
:val tg[j]


:comment ============ END OF REPLY GENERATION ============
:comment ============ REPLY PROCESSING ============


:comment  T21
:comment  Reply processing when node != target --> skip
:comment  just for configured nodes
:transition
:var x
:var j
:guard (= phi 5) (= cu[x] 0) (< I N) (not (= tp 0)) (not (= x tp)) (not (= TS[x] 100))
:numcases 2
:case (= x j)
:val phi
:val (+ I 1)
:val TS[j]
:val sm[j]
:val CM[j]
:val CP[j]
:val 1
:val tp
:val sh
:val sp
:val fv[j]
:val tD[j]
:val cD[j]
:val tg[j]
:case (not (= x j))
:val phi
:val (+ I 1)
:val TS[j]
:val sm[j]
:val CM[j]
:val CP[j]
:val cu[j]
:val tp
:val sh
:val sp
:val fv[j]
:val tD[j]
:val cD[j]
:val tg[j]


:comment  T22
:comment  Reply processing when node=target and source!=myIP and source!=victim --> skip
:comment  lines 36-43 Algorithm 3 -- just for configured nodes
:comment  it would call SARPI for a host not looked at
:transition
:var x
:var j
:guard (= phi 5) (= cu[x] 0) (< I N) (not (= tp 0)) (= x tp) (not (= sp x)) (not (= sp 2)) (not (= TS[x] 100))
:numcases 2
:case (= x j)
:val phi
:val (+ I 1)
:val TS[j]
:val sm[j]
:val CM[j]
:val CP[j]
:val 1
:val tp
:val sh
:val sp
:val fv[j]
:val tD[j]
:val cD[j]
:val tg[j]
:case (not (= x j))
:val phi
:val (+ I 1)
:val TS[j]
:val sm[j]
:val CM[j]
:val CP[j]
:val cu[j]
:val tp
:val sh
:val sp
:val fv[j]
:val tD[j]
:val cD[j]
:val tg[j]


:comment  T23
:comment  Reply processing when source=myIP --> skip
:comment  lines 31-32 Algorithm 3 -- just for configured nodes
:transition
:var x
:var j
:guard (= phi 5) (= cu[x] 0) (< I N) (= sp x) (not (= TS[x] 100))
:numcases 2
:case (= x j)
:val phi
:val (+ I 1)
:val TS[j]
:val sm[j]
:val CM[j]
:val CP[j]
:val 1
:val tp
:val sh
:val sp
:val fv[j]
:val tD[j]
:val cD[j]
:val tg[j]
:case (not (= x j))
:val phi
:val (+ I 1)
:val TS[j]
:val sm[j]
:val CM[j]
:val CP[j]
:val cu[j]
:val tp
:val sh
:val sp
:val fv[j]
:val tD[j]
:val cD[j]
:val tg[j]


:comment  T24
:comment  Reply processing when node=target and source!=myIP and source=victim and source in DARPI_cache
:comment  lines 36-39 Algorithm 3 -- just for configured nodes
:comment  it calls Allow() and resets DARPI_cache
:transition
:var x
:var j
:guard (= phi 5) (= cu[x] 0) (< I N) (not (= tp 0)) (= x tp) (not (= sp x)) (= sp 2) (= tD[x] sp) (not (= TS[x] 100))
:numcases 2
:case (= x j)
:val phi
:val (+ I 1)
:val TS[j]
:val sm[j]
:val sh
:val sp
:val 1
:val tp
:val sh
:val sp
:val fv[j]
:val 0
:val 0
:val tg[j]
:case (not (= x j))
:val phi
:val (+ I 1)
:val TS[j]
:val sm[j]
:val CM[j]
:val CP[j]
:val cu[j]
:val tp
:val sh
:val sp
:val fv[j]
:val tD[j]
:val cD[j]
:val tg[j]


:comment  T25
:comment  Reply processing when node=target and source!=myIP and source=victim and source not in DARPI_cache
:comment  lines 40-43 Algorithm 3 -- just for configured nodes
:comment  it calls Verify()+Deny() and resets DARPI_cache
:transition
:var x
:var j
:guard (= phi 5) (= cu[x] 0) (< I N) (not (= tp 0)) (= x tp) (not (= sp x)) (= sp 2) (not (= tD[x] sp)) (not (= TS[x] 100))
:numcases 2
:case (= x j)
:val phi
:val (+ I 1)
:val TS[j]
:val sm[j]
:val 0
:val 0
:val 1
:val tp
:val sh
:val sp
:val 1
:val tD[j]
:val cD[j]
:val tg[j]
:case (not (= x j))
:val phi
:val (+ I 1)
:val TS[j]
:val sm[j]
:val CM[j]
:val CP[j]
:val cu[j]
:val tp
:val sh
:val sp
:val fv[j]
:val tD[j]
:val cD[j]
:val tg[j]


:comment  T26
:comment  all hosts processed (Probe) Reply and someone must Verify() --> go back to Verify() loop
:transition
:var x
:var j
:guard (= phi 5) (= cu[x] 1) (>= I N) (= fv[x] 1)
:numcases 2
:case (= x j)
:val 2
:val I
:val TS[j]
:val sm[j]
:val CM[j]
:val CP[j]
:val cu[j]
:val tp
:val sh
:val sp
:val fv[j]
:val tD[j]
:val cD[j]
:val tg[j]
:case (not (= x j))
:val 2
:val I
:val TS[j]
:val sm[j]
:val CM[j]
:val CP[j]
:val cu[j]
:val tp
:val sh
:val sp
:val fv[j]
:val tD[j]
:val cD[j]
:val tg[j]


:comment  T27
:comment  all hosts processed (Probe) Reply and someone must Reply but none needs to Verify() --> go back to Reply loop
:transition
:var x
:var j
:guard (= phi 5) (= cu[x] 1) (>= I N) (= fv[x] 0) (> sm[x] 0)
:uguard (= fv[j] 0)
:numcases 2
:case (= x j)
:val 4
:val I
:val TS[j]
:val sm[j]
:val CM[j]
:val CP[j]
:val cu[j]
:val tp
:val sh
:val sp
:val fv[j]
:val tD[j]
:val cD[j]
:val tg[j]
:case (not (= x j))
:val 4
:val I
:val TS[j]
:val sm[j]
:val CM[j]
:val CP[j]
:val cu[j]
:val tp
:val sh
:val sp
:val fv[j]
:val tD[j]
:val cD[j]
:val tg[j]


:comment  T28
:comment  all hosts processed (Probe) Reply and none must Verify() --> restart
:comment  re-set everything but caches before new iteration
:transition
:var x
:var j
:guard (= phi 5) (= cu[x] 1) (>= I N) (= fv[x] 0) (= sm[x] 0)
:uguard (= fv[j] 0) (= sm[j] 0)
:numcases 2
:case (= x j)
:val 0
:val 0
:val (+ TS[j] 1)
:val 0
:val CM[j]
:val CP[j]
:val 0
:val 0
:val 0
:val 0
:val 0
:val tD[j]
:val cD[j]
:val 0
:case (not (= x j))
:val 0
:val 0
:val (+ TS[j] 1)
:val 0
:val CM[j]
:val CP[j]
:val 0
:val 0
:val 0
:val 0
:val 0
:val tD[j]
:val cD[j]
:val 0


:comment ============ END OF REPLY PROCESSING ============
:comment ============ TIMEOUT: CLEANING OF DARPI_CACHE ============


:comment  T29
:comment  lines 5-7 Algorithm 3 -- cleaning of DARPI_cache
:comment  performed just for configured nodes; the other nodes can only execute T1
:transition
:var x
:var j
:guard (= TS[x] 100)
:numcases 2
:case (= x j)
:val phi
:val I
:val 0
:val sm[j]
:val CM[j]
:val CP[j]
:val cu[j]
:val tp
:val sh
:val sp
:val fv[j]
:val 0
:val 0
:val tg[j]
:case (not (= x j))
:val phi
:val I
:val TS[j]
:val sm[j]
:val CM[j]
:val CP[j]
:val cu[j]
:val tp
:val sh
:val sp
:val fv[j]
:val tD[j]
:val cD[j]
:val tg[j]