:comment  DARPI  (Master Thesis by Andrea Di Pasquale)
:comment  Elena Pagani -- Last update: June 29, 2017
  
:comment  Modelization with no malicious host; no cache aging
:comment  All packets are sent broadcast, but processed just by the target
:comment  Victim is node 1
: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  GA indicates whether a Probe (1), Announcement (2), basic request (3), or an unsolicited Reply from the malicious (4) is generated
:global GA nat

: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  flag for host yet to send a Probe (0), or having to send Announce (1), or configured (2)
:local st 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 -------
:comment  none


: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) (= GA 0) (= TS[x] 0) (= sh 0) (= sp 0) (= tp 0) (= sm[x] 0) (= CM[x] 0) (= CP[x] 0) (= cu[x] 0) (= st[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
:cnj (not (= CM[z1] 1)) (= CP[z1] 1)


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

:comment  T1
:comment  exists node in state 0 --> it sends a Probe
:comment  it also initializes its DARPI_cache to empty --> Clean()
:comment  lines 8-10 Algorithm 3 -- go to T6 and successive
:transition
:var x
:var j
:guard (= phi 0) (= st[x] 0)
:numcases 2
:case (= x j)
:val 2
:val 1
:val 1
:val 0
:val 0
:val 0
:val 0
:val 1
:val 1
:val x
:val x
:val 0
:val 0
:val 0
:val 0
:val 0
:case (not (= x j))
:val 2
:val 1
:val 1
:val (+ TS[j] 1)
:val sm[j]
:val CM[j]
:val CP[j]
:val 0
:val st[j]
:val x
:val x
:val 0
:val fv[j]
:val tD[j]
:val cD[j]
:val tg[j]


:comment  T2
:comment  exists node in state 1 --> it sends a HONEST Gratuitous Request
:comment  lines 8-10 Algorithm 3 -- go to T6 and successive
:transition
:var x
:var j
:guard (= phi 0) (= st[x] 1) (not (= TS[x] 100))
:numcases 2
:case (= x j)
:val 2
:val 1
:val 2
:val (+ TS[j] 1)
:val sm[j]
:val CM[j]
:val CP[j]
:val 1
:val 2
:val x
: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 2
:val (+ TS[j] 1)
:val sm[j]
:val CM[j]
:val CP[j]
:val 0
:val st[j]
:val x
:val x
:val x
:val fv[j]
:val tD[j]
:val cD[j]
:val tg[j]


:comment  T3
:comment  exists node in state 2 --> it sends a HONEST base Request
:comment  go to T4
:transition
:var x
:var j
:guard (= phi 0) (= st[x] 2) (not (= TS[x] 100))
:numcases 2
:case (= x j)
:val 1
:val 1
:val 3
:val TS[j]
:val 1
:val CM[j]
:val CP[j]
:val 1
:val st[j]
:val tp
:val x
:val x
:val fv[j]
:val tD[j]
:val cD[j]
:val tg[j]
:case (not (= x j))
:val 1
:val 1
:val 3
:val TS[j]
:val sm[j]
:val CM[j]
:val CP[j]
:val 0
:val st[j]
:val tp
:val x
:val x
:val fv[j]
:val tD[j]
:val cD[j]
:val tg[j]


:comment  T4
:comment  generated honest base Request to victim
:comment  set of message fields depending on the sender, choosing random target
:comment  update of DARPI_cache -- lines 11-13 Algorithm 3
:comment  go to T6 and successive
:transition
:var x
:var y
:var j
:guard (= phi 1) (= sm[x] 1) (= sm[y] 0) (= y 1)
:numcases 2
:case (= x j)
:val 2
:val 1
:val GA
:val (+ TS[j] 1)
:val 0
:val CM[j]
:val CP[j]
:val 1
:val st[j]
:val y
:val x
:val x
:val fv[j]
:val y
:val TS[j]
:val tg[j]
:case (not (= x j))
:val 2
:val 1
:val GA
:val (+ TS[j] 1)
:val sm[j]
:val CM[j]
:val CP[j]
:val 0
:val st[j]
:val y
:val x
:val x
:val fv[j]
:val tD[j]
:val cD[j]
:val tg[j]


:comment  T5
:comment  generated honest base Request to target != victim
:comment  set of message fields depending on the sender, choosing random target
:comment  go to T6 and successive
:transition
:var x
:var y
:var j
:guard (= phi 1) (= sm[x] 1) (= sm[y] 0) (not (= y 1))
:numcases 2
:case (= x j)
:val 2
:val 1
:val GA
:val (+ TS[j] 1)
:val 0
:val CM[j]
:val CP[j]
:val 1
:val st[j]
: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 GA
:val (+ TS[j] 1)
:val sm[j]
:val CM[j]
:val CP[j]
:val 0
:val st[j]
:val y
:val x
:val x
: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 still unconfigured --> skip
:transition
:var x
:var j
:guard (= phi 2) (= cu[x] 0) (< I N) (= st[x] 0)
:numcases 2
:case (= x j)
:val phi
:val (+ I 1)
:val GA
:val TS[j]
:val sm[j]
:val CM[j]
:val CP[j]
:val 1
:val st[j]
: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 GA
:val TS[j]
:val sm[j]
:val CM[j]
:val CP[j]
:val cu[j]
:val st[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 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) (> st[x] 0) (not (= sh x)) (not (= x tp)) (not (= sp tp)) (not (= TS[x] 100))
:numcases 2
:case (= x j)
:val phi
:val (+ I 1)
:val GA
:val TS[j]
:val sm[j]
:val CM[j]
:val CP[j]
:val 1
:val st[j]
: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 GA
:val TS[j]
:val sm[j]
:val CM[j]
:val CP[j]
:val cu[j]
:val st[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 --> 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) (> st[x] 0) (= sp tp) (not (= sp x)) (not (= sp 1)) (not (= TS[x] 100))
:numcases 2
:case (= x j)
:val phi
:val (+ I 1)
:val GA
:val TS[j]
:val sm[j]
:val CM[j]
:val CP[j]
:val 1
:val st[j]
: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 GA
:val TS[j]
:val sm[j]
:val CM[j]
:val CP[j]
:val cu[j]
:val st[j]
:val tp
:val sh
:val sp
:val fv[j]
:val tD[j]
:val cD[j]
:val tg[j]


:comment  T9
:comment  Request processing when announce and source=myMAC --> skip
:comment  lines 8-10 Algorithm 3 -- just for configured nodes
:transition
:var x
:var j
:guard (= phi 2) (= cu[x] 0) (< I N) (> st[x] 0) (= sp tp) (= sh x) (not (= TS[x] 100))
:numcases 2
:case (= x j)
:val phi
:val (+ I 1)
:val GA
:val TS[j]
:val sm[j]
:val CM[j]
:val CP[j]
:val 1
:val st[j]
: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 GA
:val TS[j]
:val sm[j]
:val CM[j]
:val CP[j]
:val cu[j]
:val st[j]
:val tp
:val sh
:val sp
:val fv[j]
:val tD[j]
:val cD[j]
:val tg[j]


:comment  T10
:comment  Request processing when Probe and source=myIP --> skip
:comment  lines 8-10 Algorithm 3 -- just for configured nodes
:transition
:var x
:var j
:guard (= phi 2) (= cu[x] 0) (< I N) (> st[x] 0) (= sp 0) (= sh x) (not (= TS[x] 100))
:numcases 2
:case (= x j)
:val phi
:val (+ I 1)
:val GA
:val TS[j]
:val sm[j]
:val CM[j]
:val CP[j]
:val 1
:val st[j]
: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 GA
:val TS[j]
:val sm[j]
:val CM[j]
:val CP[j]
:val cu[j]
:val st[j]
:val tp
:val sh
:val sp
:val fv[j]
:val tD[j]
:val cD[j]
:val tg[j]


:comment  T11
:comment  Request processing when base and source=myIP --> update DARPI_cache
:comment  lines 11-13 Algorithm 3 -- just for configured nodes
:transition
:var x
:var j
:guard (= phi 2) (= cu[x] 0) (< I N) (> st[x] 0) (not (= sp tp)) (not (= sp 0)) (= sh x) (= sp x) (not (= TS[x] 100))
:numcases 2
:case (= x j)
:val phi
:val (+ I 1)
:val GA
:val TS[j]
:val sm[j]
:val CM[j]
:val CP[j]
:val 1
:val st[j]
:val tp
:val sh
:val sp
:val fv[j]
:val tp
:val TS[j]
:val tg[j]
:case (not (= x j))
:val phi
:val (+ I 1)
:val GA
:val TS[j]
:val sm[j]
:val CM[j]
:val CP[j]
:val cu[j]
:val st[j]
:val tp
:val sh
:val sp
:val fv[j]
:val tD[j]
:val cD[j]
:val tg[j]


:comment  T12
: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) (> st[x] 0) (= sp tp) (not (= sp x)) (= sp 1) (not (= TS[x] 100))
:numcases 2
:case (= x j)
:val phi
:val (+ I 1)
:val GA
:val TS[j]
:val sm[j]
:val 0
:val 0
:val 1
:val st[j]
: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 GA
:val TS[j]
:val sm[j]
:val CM[j]
:val CP[j]
:val cu[j]
:val st[j]
:val tp
:val sh
:val sp
:val fv[j]
:val tD[j]
:val cD[j]
:val tg[j]


:comment  T13
: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) (> st[x] 0) (not (= sp tp)) (not (= sp 0)) (= tp x) (not (= sp x)) (not (= sp 1)) (not (= TS[x] 100))
:numcases 2
:case (= x j)
:val phi
:val (+ I 1)
:val GA
:val TS[j]
:val 1
:val CM[j]
:val CP[j]
:val 1
:val st[j]
: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 GA
:val TS[j]
:val sm[j]
:val CM[j]
:val CP[j]
:val cu[j]
:val st[j]
:val tp
:val sh
:val sp
:val fv[j]
:val tD[j]
:val cD[j]
:val tg[j]


:comment  T14
: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) (> st[x] 0) (not (= sp tp)) (not (= sp 0)) (= tp x) (not (= sp x)) (= sp 1) (not (= tD[x] sp)) (not (= TS[x] 100))
:numcases 2
:case (= x j)
:val phi
:val (+ I 1)
:val GA
:val TS[j]
:val 1
:val 0
:val 0
:val 1
:val st[j]
: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 GA
:val TS[j]
:val sm[j]
:val CM[j]
:val CP[j]
:val cu[j]
:val st[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 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) (> st[x] 0) (not (= sp tp)) (not (= sp 0)) (= tp x) (not (= sp x)) (= sp 1) (= tD[x] sp) (not (= TS[x] 100))
:numcases 2
:case (= x j)
:val phi
:val (+ I 1)
:val GA
:val TS[j]
:val 1
:val 0
:val 0
:val 1
:val st[j]
: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 GA
:val TS[j]
:val sm[j]
:val CM[j]
:val CP[j]
:val cu[j]
:val st[j]
:val tp
:val sh
:val sp
:val fv[j]
:val tD[j]
:val cD[j]
:val tg[j]


:comment  T16
:comment  Probe Request processing when target
:comment  lines 26-30 Algorithm 3 -- just for configured nodes
:comment  generates Probe Reply (conflict detected)
:transition
:var x
:var j
:guard (= phi 2) (= cu[x] 0) (< I N) (> st[x] 0) (= sp 0) (= tp x) (not (= TS[x] 100))
:numcases 2
:case (= x j)
:val phi
:val (+ I 1)
:val GA
:val TS[j]
:val 2
:val CM[j]
:val CP[j]
:val 1
:val st[j]
: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 GA
:val TS[j]
:val sm[j]
:val CM[j]
:val CP[j]
:val cu[j]
:val st[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  T17
:comment  host performs Verify() --> 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 GA
:val (+ TS[j] 1)
:val sm[j]
:val CM[j]
:val CP[j]
:val 1
:val st[j]
:val sp
:val x
:val x
:val 0
:val sp
:val TS[j]
:val tg[j]
:case (not (= x j))
:val 3
:val 1
:val GA
:val (+ TS[j] 1)
:val sm[j]
:val CM[j]
:val CP[j]
:val 0
:val st[j]
:val sp
:val x
:val x
:val fv[j]
:val tD[j]
:val cD[j]
:val tg[j]


:comment  T18
: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 GA
:val TS[j]
:val sm[j]
:val CM[j]
:val CP[j]
:val cu[j]
:val st[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 GA
:val TS[j]
:val sm[j]
:val CM[j]
:val CP[j]
:val cu[j]
:val st[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  T19
:comment  Request processing when still unconfigured --> skip
:transition
:var x
:var j
:guard (= phi 3) (= cu[x] 0) (< I N) (= st[x] 0)
:numcases 2
:case (= x j)
:val phi
:val (+ I 1)
:val GA
:val TS[j]
:val sm[j]
:val CM[j]
:val CP[j]
:val 1
:val st[j]
: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 GA
:val TS[j]
:val sm[j]
:val CM[j]
:val CP[j]
:val cu[j]
:val st[j]
:val tp
:val sh
:val sp
:val fv[j]
:val tD[j]
:val cD[j]
:val tg[j]


:comment  T20
: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) (> st[x] 0) (not (= sh x)) (not (= x tp)) (not (= sp tp)) (not (= TS[x] 100))
:numcases 2
:case (= x j)
:val phi
:val (+ I 1)
:val GA
:val TS[j]
:val sm[j]
:val CM[j]
:val CP[j]
:val 1
:val st[j]
: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 GA
:val TS[j]
:val sm[j]
:val CM[j]
:val CP[j]
:val cu[j]
:val st[j]
:val tp
:val sh
:val sp
:val fv[j]
:val tD[j]
:val cD[j]
:val tg[j]


:comment  T21
: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) (> st[x] 0) (not (= sp tp)) (not (= sp 0)) (= tp x) (not (= sp x)) (not (= sp 1)) (not (= TS[x] 100))
:numcases 2
:case (= x j)
:val phi
:val (+ I 1)
:val GA
:val TS[j]
:val 1
:val CM[j]
:val CP[j]
:val 1
:val st[j]
: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 GA
:val TS[j]
:val sm[j]
:val CM[j]
:val CP[j]
:val cu[j]
:val st[j]
:val tp
:val sh
:val sp
:val fv[j]
:val tD[j]
:val cD[j]
:val tg[j]


:comment  T22
: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) (> st[x] 0) (not (= sp tp)) (not (= sp 0)) (= tp x) (not (= sp x)) (= sp 1) (= tD[x] sp) (not (= TS[x] 100))
:numcases 2
:case (= x j)
:val phi
:val (+ I 1)
:val GA
:val TS[j]
:val 1
:val 0
:val 0
:val 1
:val st[j]
: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 GA
:val TS[j]
:val sm[j]
:val CM[j]
:val CP[j]
:val cu[j]
:val st[j]
:val tp
:val sh
:val sp
:val fv[j]
:val tD[j]
:val cD[j]
:val tg[j]


:comment  T23
: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 (= st[x] 0)) (not (= sp tp)) (not (= sp 0)) (= tp x) (not (= sp x)) (= sp 1) (not (= tD[x] sp)) (not (= TS[x] 100))
:numcases 2
:case (= x j)
:val phi
:val (+ I 1)
:val GA
:val TS[j]
:val 1
:val 0
:val 0
:val 1
:val st[j]
: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 GA
:val TS[j]
:val sm[j]
:val CM[j]
:val CP[j]
:val cu[j]
:val st[j]
:val tp
:val sh
:val sp
:val fv[j]
:val tD[j]
:val cD[j]
:val tg[j]


:comment  T24
: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 GA
:val TS[j]
:val sm[j]
:val CM[j]
:val CP[j]
:val cu[j]
:val st[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 GA
:val TS[j]
:val sm[j]
:val CM[j]
:val CP[j]
:val cu[j]
:val st[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  T25
:comment  target generates 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 GA
:val (+ TS[j] 1)
:val 0
:val CM[j]
:val CP[j]
:val 1
:val st[j]
: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 GA
:val (+ TS[j] 1)
:val sm[j]
:val CM[j]
:val CP[j]
:val 0
:val st[j]
:val tg[x]
:val x
:val x
:val fv[j]
:val tD[j]
:val cD[j]
:val tg[j]


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


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


:comment  T27
:comment  Reply processing when node not configured --> skip
:comment  also applies to Probe Reply
:transition
:var x
:var j
:guard (= phi 5) (= cu[x] 0) (< I N) (= st[x] 0) 
:numcases 2
:case (= x j)
:val phi
:val (+ I 1)
:val GA
:val TS[j]
:val sm[j]
:val CM[j]
:val CP[j]
:val 1
:val st[j]
: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 GA
:val TS[j]
:val sm[j]
:val CM[j]
:val CP[j]
:val cu[j]
:val st[j]
:val tp
:val sh
:val sp
:val fv[j]
:val tD[j]
:val cD[j]
:val tg[j]


:comment  T28
:comment  Probe Reply processing when configuring node and replay raises conflict
:comment  goes back to configuration
:transition
:var x
:var j
:guard (= phi 5) (= cu[x] 0) (< I N) (= st[x] 1) (= tp 0) (not (= sh x)) (= sp x) (not (= TS[x] 100))
:numcases 2
:case (= x j)
:val phi
:val (+ I 1)
:val GA
:val 0
:val 0
:val 0
:val 0
:val 1
:val 0
:val tp
:val sh
:val sp
:val 0
:val 0
:val 0
:val 0
:case (not (= x j))
:val phi
:val (+ I 1)
:val GA
:val TS[j]
:val sm[j]
:val CM[j]
:val CP[j]
:val cu[j]
:val st[j]
:val tp
:val sh
:val sp
:val fv[j]
:val tD[j]
:val cD[j]
:val tg[j]


:comment  T29
:comment  Probe Reply processing when configuring node and replay for other node --> skip
:transition
:var x
:var j
:guard (= phi 5) (= cu[x] 0) (< I N) (= st[x] 1) (= tp 0) (not (= sp x)) (not (= TS[x] 100))
:numcases 2
:case (= x j)
:val phi
:val (+ I 1)
:val GA
:val TS[j]
:val sm[j]
:val CM[j]
:val CP[j]
:val 1
:val st[j]
: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 GA
:val TS[j]
:val sm[j]
:val CM[j]
:val CP[j]
:val cu[j]
:val st[j]
:val tp
:val sh
:val sp
:val fv[j]
:val tD[j]
:val cD[j]
:val tg[j]


:comment  T30
:comment  Probe Reply processing when configured node --> skip
:transition
:var x
:var j
:guard (= phi 5) (= cu[x] 0) (< I N) (= st[x] 2) (= tp 0) (not (= TS[x] 100))
:numcases 2
:case (= x j)
:val phi
:val (+ I 1)
:val GA
:val TS[j]
:val sm[j]
:val CM[j]
:val CP[j]
:val 1
:val st[j]
: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 GA
:val TS[j]
:val sm[j]
:val CM[j]
:val CP[j]
:val cu[j]
:val st[j]
:val tp
:val sh
:val sp
:val fv[j]
:val tD[j]
:val cD[j]
:val tg[j]


:comment  T31
: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) (> st[x] 0) (not (= tp 0)) (not (= x tp)) (not (= TS[x] 100))
:numcases 2
:case (= x j)
:val phi
:val (+ I 1)
:val GA
:val TS[j]
:val sm[j]
:val CM[j]
:val CP[j]
:val 1
:val st[j]
: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 GA
:val TS[j]
:val sm[j]
:val CM[j]
:val CP[j]
:val cu[j]
:val st[j]
:val tp
:val sh
:val sp
:val fv[j]
:val tD[j]
:val cD[j]
:val tg[j]


:comment  T32
: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) (> st[x] 0) (not (= tp 0)) (= x tp) (not (= sp x)) (not (= sp 1)) (not (= TS[x] 100))
:numcases 2
:case (= x j)
:val phi
:val (+ I 1)
:val GA
:val TS[j]
:val sm[j]
:val CM[j]
:val CP[j]
:val 1
:val st[j]
: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 GA
:val TS[j]
:val sm[j]
:val CM[j]
:val CP[j]
:val cu[j]
:val st[j]
:val tp
:val sh
:val sp
:val fv[j]
:val tD[j]
:val cD[j]
:val tg[j]


:comment  T33
: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) (> st[x] 0) (= sp x) (not (= TS[x] 100))
:numcases 2
:case (= x j)
:val phi
:val (+ I 1)
:val GA
:val TS[j]
:val sm[j]
:val CM[j]
:val CP[j]
:val 1
:val st[j]
: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 GA
:val TS[j]
:val sm[j]
:val CM[j]
:val CP[j]
:val cu[j]
:val st[j]
:val tp
:val sh
:val sp
:val fv[j]
:val tD[j]
:val cD[j]
:val tg[j]


:comment  T34
: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) (> st[x] 0) (not (= tp 0)) (= x tp) (not (= sp x)) (= sp 1) (= tD[x] sp) (not (= TS[x] 100))
:numcases 2
:case (= x j)
:val phi
:val (+ I 1)
:val GA
:val TS[j]
:val sm[j]
:val sh
:val sp
:val 1
:val st[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 1)
:val GA
:val TS[j]
:val sm[j]
:val CM[j]
:val CP[j]
:val cu[j]
:val st[j]
:val tp
:val sh
:val sp
:val fv[j]
:val tD[j]
:val cD[j]
:val tg[j]


:comment  T35
: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 (= st[x] 0)) (not (= tp 0)) (= x tp) (not (= sp x)) (= sp 1) (not (= tD[x] sp)) (not (= TS[x] 100))
:numcases 2
:case (= x j)
:val phi
:val (+ I 1)
:val GA
:val TS[j]
:val sm[j]
:val 0
:val 0
:val 1
:val st[j]
: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 GA
:val TS[j]
:val sm[j]
:val CM[j]
:val CP[j]
:val cu[j]
:val st[j]
:val tp
:val sh
:val sp
:val fv[j]
:val tD[j]
:val cD[j]
:val tg[j]


:comment  T36
: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 GA
:val TS[j]
:val sm[j]
:val CM[j]
:val CP[j]
:val cu[j]
:val st[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 GA
:val TS[j]
:val sm[j]
:val CM[j]
:val CP[j]
:val cu[j]
:val st[j]
:val tp
:val sh
:val sp
:val fv[j]
:val tD[j]
:val cD[j]
:val tg[j]


:comment  T37
: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 GA
:val TS[j]
:val sm[j]
:val CM[j]
:val CP[j]
:val cu[j]
:val st[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 GA
:val TS[j]
:val sm[j]
:val CM[j]
:val CP[j]
:val cu[j]
:val st[j]
:val tp
:val sh
:val sp
:val fv[j]
:val tD[j]
:val cD[j]
:val tg[j]


:comment  T38
: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 0
:val (+ TS[j] 1)
:val 0
:val CM[j]
:val CP[j]
:val 0
:val st[j]
: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 0
:val (+ TS[j] 1)
:val 0
:val CM[j]
:val CP[j]
:val 0
:val st[j]
: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  T39
: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) (not (= st[x] 0))
:numcases 2
:case (= x j)
:val phi
:val I
:val GA
:val 0
:val sm[j]
:val CM[j]
:val CP[j]
:val cu[j]
:val st[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 GA
:val TS[j]
:val sm[j]
:val CM[j]
:val CP[j]
:val cu[j]
:val st[j]
:val tp
:val sh
:val sp
:val fv[j]
:val tD[j]
:val cD[j]
:val tg[j]