:comment  SARPI  (Master Thesis by Andrea Di Pasquale)
:comment  Elena Pagani -- Last update: June 26, 2017
  
:comment  Modelization with malicious hosts; no cache aging
:comment  All honest packets are broadcast, but processed just by the target
:comment  Any node (but the victim) may behave maliciously against the victim; it may send UNICAST packets.  
:comment  Victim is node 2. 
:comment  "Honest" is any node behaving properly but different from victim
:comment  The config_file includes info for just the victim, i.e. the couple <1,1>

: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 honest Probe (1), Announcement (2), basic request (3); or unsolicited Reply from the malicious (4) is generated.
:global GA nat

:comment  LOCAL CLOCK: new call when TS = 600 (s.)  --> T32
:comment  TS indicates the time elapsed from the last call to Update()
: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  eth_dest (used just for fake announces); -1 means broadcast
:global ed int

:comment  These variables take their values from the (abstracted) config_file in the initialization; the values are never changed afterwards
:comment  ScM indicates the value of the MAC address of the victim in the config_file
:global ScM nat
:comment  ScP indicates the value of the IP address of the victim in the config_file
:global ScP nat


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


:comment  ------- SUGGESTED INVARIANTS -------
:suggested_negated_invariants
:var z1
:cnj (not (= ScM 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) (= 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) (= ScM 2) (= ScP 2) (= ed -1)


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


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

:comment  T1
:comment  exists node in state 0 --> it sends a Probe
:comment  it also initializes its ARP_cache to its SARPI_cache --> Update()
:comment  go to T8 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 sm[j]
:val ScM
:val ScP
:val 1
:val 1
:val x
:val x
:val 0
:val -1
:val ScM
:val ScP
: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 -1
:val ScM
:val ScP


:comment  T2
:comment  exists node in state 1 --> it sends a HONEST Gratuitous Request
:comment  go to T8 and successive
:transition
:var x
:var j
:guard (= phi 0) (= st[x] 1) (not (= TS[x] 600))
: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 -1
:val ScM
:val ScP
: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 -1
:val ScM
:val ScP


:comment  T3
:comment  exists node in state 2 --> it sends a HONEST base Request
:comment  go to T7
:transition
:var x
:var j
:guard (= phi 0) (= st[x] 2) (not (= TS[x] 600))
: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 -1
:val ScM
:val ScP
: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 -1
:val ScM
:val ScP


:comment  T4
:comment  host sends a MALICIOUS Gratuitous Request (unicast)
:comment  source != victim; unicast destination chosen different from the victim
:comment  go to T8 and successive
:transition
:var x
:var y
:var j
:guard (= phi 0) (not (= x 2)) (not (= y 2)) (not (= TS[x] 600))
: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 st[j]
:val 2
:val x
:val 2
:val y
:val ScM
:val ScP
: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 2
:val x
:val 2
:val y
:val ScM
:val ScP


:comment  T5
:comment  host sends a MALICIOUS base Request (unicast)
:comment  source != victim; 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] 600))
:numcases 2
:case (= x j)
:val 2
:val 1
:val 3
:val (+ TS[j] 1)
:val sm[j]
:val CM[j]
:val CP[j]
:val 1
:val st[j]
:val y
:val x
:val 2
:val y
:val ScM
:val ScP
:case (not (= x j))
:val 2
:val 1
:val 3
:val (+ TS[j] 1)
:val sm[j]
:val CM[j]
:val CP[j]
:val 0
:val st[j]
:val y
:val x
:val 2
:val y
:val ScM
:val ScP


:comment  T6
:comment  host sends an MALICIOUS unsolicited Reply
:comment  source!= victim; target chosen different from victim
:comment  go to T19 and successive
:transition
:var x
:var y
:var j
:guard (= phi 0) (not (= x 2)) (not (= y 2)) (not (= TS[x] 600))
:numcases 2
:case (= x j)
:val 3
:val 1
:val 4
:val (+ TS[j] 1)
:val sm[j]
:val CM[j]
:val CP[j]
:val 1
:val st[j]
:val y
:val x
:val 2
:val y
:val ScM
:val ScP
:case (not (= x j))
:val 3
:val 1
:val 4
:val (+ TS[j] 1)
:val sm[j]
:val CM[j]
:val CP[j]
:val 0
:val st[j]
:val y
:val x
:val 2
:val y
:val ScM
:val ScP


:comment  T7
:comment  generated honest base Request
:comment  set message fields depending on the sender, choosing random target
:comment  go to T8 and successive
:transition
:var x
:var y
:var j
:guard (= phi 1) (= sm[x] 1) (= sm[y] 0)
: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 -1
:val ScM
:val ScP
: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 -1
:val ScM
:val ScP


:comment  T8
: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 ed
:val ScM
:val ScP
: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 ed
:val ScM
:val ScP


:comment  T9
:comment  Request processing when not announce and node != target --> skip
:comment  just for configured nodes
:transition
:var x
:var j
:guard (= phi 2) (= cu[x] 0) (< I N) (not (= st[x] 0)) (not (= x tp)) (not (= sp tp)) (not (= TS[x] 600))
: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 ed
:val ScM
:val ScP
: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 ed
:val ScM
:val ScP


:comment  T10
:comment  Request processing when broadcast announce and source!=victim and source!=myIP --> skip
:comment  lines 25-30 Algorithm 1  --  just for configured nodes
:comment  it would call Allow() for a cache entry we don't look at
:transition
:var x
:var j
:guard (= phi 2) (= cu[x] 0) (< I N) (not (= st[x] 0)) (= sp tp) (< ed 0) (not (= sp x)) (not (= sp 2)) (not (= TS[x] 600))
: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 ed
:val ScM
:val ScP
: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 ed
:val ScM
:val ScP


:comment  T11
:comment  Request processing when broadcast announce and source=myIP --> skip
:comment  lines 25-30 and 47 Algorithm 1  --  just for configured nodes
:transition
:var x
:var j
:guard (= phi 2) (= cu[x] 0) (< I N) (not (= st[x] 0)) (= sp tp) (< ed 0) (= sp x) (not (= TS[x] 600))
: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 ed
:val ScM
:val ScP
: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 ed
:val ScM
:val ScP


:comment  T12
:comment  Request processing when broadcast announce and source=victim and source!=myIP
:comment  lines 25-30 Algorithm 1  --  just for configured nodes
:comment  it calls Refresh()
:transition
:var x
:var j
:guard (= phi 2) (= cu[x] 0) (< I N) (not (= st[x] 0)) (= sp tp) (< ed 0) (not (= sp x)) (= sp 2) (not (= TS[x] 600))
:numcases 2
:case (= x j)
:val phi
:val (+ I 1)
:val GA
:val TS[j]
:val sm[j]
:val ScM
:val ScP
:val 1
:val st[j]
:val tp
:val sh
:val sp
:val ed
:val ScM
:val ScP
: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 ed
:val ScM
:val ScP

:comment  T13
:comment  Request processing when unicast announce not to me --> skip
:comment  node does not even see this!
:transition
:var x
:var j
:guard (= phi 2) (= cu[x] 0) (< I N) (not (= st[x] 0)) (= sp tp) (>= ed 0) (not (= ed x))  (not (= TS[x] 600))
: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 ed
:val ScM
:val ScP
: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 ed
:val ScM
:val ScP


:comment  T14
:comment  Request processing when unicast announce to me and source!=victim and source!=myIP --> skip
:comment  lines 25-30 Algorithm 1  --  just for configured nodes
:comment  it would call Allow() for a cache entry we don't look at
:transition
:var x
:var j
:guard (= phi 2) (= cu[x] 0) (< I N) (not (= st[x] 0)) (= sp tp) (= ed x) (not (= sp x)) (not (= sp 2)) (not (= TS[x] 600))
: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 ed
:val ScM
:val ScP
: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 ed
:val ScM
:val ScP


:comment  T15
:comment  Request processing when unicast announce to me and source=myIP --> skip
:comment  lines 25-30 and 47 Algorithm 1  --  just for configured nodes
:transition
:var x
:var j
:guard (= phi 2) (= cu[x] 0) (< I N) (not (= st[x] 0)) (= sp tp) (= ed x) (= sp x) (not (= TS[x] 600))
: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 ed
:val ScM
:val ScP
: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 ed
:val ScM
:val ScP


:comment  T16
:comment  Request processing when unicast announce to me and source=victim and source!=myIP
:comment  lines 25-30 Algorithm 1  --  just for configured nodes
:comment  it calls Refresh()
:transition
:var x
:var j
:guard (= phi 2) (= cu[x] 0) (< I N) (not (= st[x] 0)) (= sp tp) (= ed x) (not (= sp x)) (= sp 2) (not (= TS[x] 600))
:numcases 2
:case (= x j)
:val phi
:val (+ I 1)
:val GA
:val TS[j]
:val sm[j]
:val ScM
:val ScP
:val 1
:val st[j]
:val tp
:val sh
:val sp
:val ed
:val ScM
:val ScP
: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 ed
:val ScM
:val ScP


:comment  T17
:comment  Base Request processing when target and source!=myIP and source!=victim
:comment  lines 31-40 Algorithm 1  --  just for configured nodes
:comment  it generates a Reply (and updates via Allow() a cache entry not looked at)
:transition
:var x
:var j
:guard (= phi 2) (= cu[x] 0) (< I N) (not (= st[x] 0)) (not (= sp tp)) (not (= sp 0)) (= tp x) (not (= sp x)) (not (= sp 2)) (not (= TS[x] 600))
: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 ed
:val ScM
:val ScP
: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 ed
:val ScM
:val ScP


:comment  T18
:comment  Base Request processing when target and source!=myIP and source=victim
:comment  lines 31-40 Algorithm 1  --  just for configured nodes
:comment  it generates a Reply and calls Refresh()
:transition
:var x
:var j
:guard (= phi 2) (= cu[x] 0) (< I N) (not (= st[x] 0)) (not (= sp tp)) (not (= sp 0)) (= tp x) (not (= sp x)) (= sp 2) (not (= TS[x] 600))
:numcases 2
:case (= x j)
:val phi
:val (+ I 1)
:val GA
:val TS[j]
:val 1
:val ScM
:val ScP
:val 1
:val st[j]
:val tp
:val sh
:val sp
:val ed
:val ScM
:val ScP
: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 ed
:val ScM
:val ScP


:comment  T19
:comment  Base Request processing when target and source=myIP --> skip
:comment  lines 31-40 and 47 Algorithm 1  --  just for configured nodes
:transition
:var x
:var j
:guard (= phi 2) (= cu[x] 0) (< I N) (not (= st[x] 0)) (not (= sp tp)) (not (= sp 0)) (= tp x) (= sp x) (not (= TS[x] 600))
: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 ed
:val ScM
:val ScP
: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 ed
:val ScM
:val ScP


:comment  T20
:comment  Probe Request processing when target
:comment  lines 41-45 Algorithm 1  --  just for configured nodes
:comment  generates Probe Reply (conflict detected)
:transition
:var x
:var j
:guard (= phi 2) (= cu[x] 0) (< I N) (not (= st[x] 0)) (= sp 0) (= tp x) (not (= TS[x] 600))
: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 ed
:val ScM
:val ScP
: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 ed
:val ScM
:val ScP


:comment  T21
: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 2) (>= I N) (= sm[x] 1) (= cu[x] 1) (not (= TS[x] 600))
:numcases 2
:case (= x j)
:val 3
:val 1
:val GA
:val (+ TS[j] 1)
:val 0
:val CM[j]
:val CP[j]
:val 1
:val st[j]
:val sp
:val x
:val x
:val -1
:val ScM
:val ScP
: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 -1
:val ScM
:val ScP


:comment  T22
:comment  target generates honest Probe Reply (broadcast)
:comment  TS incremented of 1 tick for Request processing and Reply generation 
:transition
:var x
:var j
:guard (= phi 2) (>= I N) (= sm[x] 2) (= cu[x] 1) (not (= TS[x] 600))
:numcases 2
:case (= x j)
:val 3
: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 -1
:val ScM
:val ScP
: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 0
:val x
:val x
:val -1
:val ScM
:val ScP


:comment  T23
:comment  target may generate MALICIOUS poisoned Reply (unicast)
:comment  source != victim
:transition
:var x
:var j
:guard (= phi 2) (>= I N) (not (= x 2)) (= sm[x] 1) (= cu[x] 1) (not (= TS[x] 600))
:numcases 2
:case (= x j)
:val 3
:val 1
:val GA
:val (+ TS[j] 1)
:val 0
:val CM[j]
:val CP[j]
:val 1
:val st[j]
:val sp
:val x
:val 2
:val sp
:val ScM
:val ScP
: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 2
:val sp
:val ScM
:val ScP


:comment  T24
:comment  Reply processing when node not configured --> skip
:comment  also applies to Probe Reply
: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 ed
:val ScM
:val ScP
: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 ed
:val ScM
:val ScP


:comment  T25
:comment  Probe Reply processing when configuring node and replay raises conflict
:comment  goes back to configuration
:transition
:var x
:var j
:guard (= phi 3) (= cu[x] 0) (< I N) (= st[x] 1) (= tp 0) (not (= sh x)) (= sp x) (not (= TS[x] 600))
: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 ed
:val ScM
:val ScP
: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 ed
:val ScM
:val ScP


:comment  T26
:comment  Probe Reply processing when configuring node and replay for other node --> skip
:transition
:var x
:var j
:guard (= phi 3) (= cu[x] 0) (< I N) (= st[x] 1) (= tp 0) (not (= sp x)) (not (= TS[x] 600))
: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 ed
:val ScM
:val ScP
: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 ed
:val ScM
:val ScP


:comment  T27
:comment  Probe Reply processing when configured node --> skip
:transition
:var x
:var j
:guard (= phi 3) (= cu[x] 0) (< I N) (= st[x] 2) (= tp 0) (not (= TS[x] 600))
: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 ed
:val ScM
:val ScP
: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 ed
:val ScM
:val ScP


:comment  T28
:comment  Reply processing when node != target --> skip
:comment  just for configured nodes
:transition
:var x
:var j
:guard (= phi 3) (= cu[x] 0) (< I N) (not (= st[x] 0)) (not (= tp 0)) (not (= x tp)) (not (= TS[x] 600))
: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 ed
:val ScM
:val ScP
: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 ed
:val ScM
:val ScP


:comment  T29
:comment  Reply processing when node=target and source!=myIP and source!=victim --> skip
:comment  lines 25-30 Algorithm 1  --  just for configured nodes
:comment  it would call Allow() for a cache entry not looked at
:transition
:var x
:var j
:guard (= phi 3) (= cu[x] 0) (< I N) (not (= st[x] 0)) (not (= tp 0)) (= x tp) (not (= sp x)) (not (= sp 2)) (not (= TS[x] 600))
: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 ed
:val ScM
:val ScP
: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 ed
:val ScM
:val ScP


:comment  T30
:comment  Reply processing when node=target and source=myIP --> skip
:comment  just for configured nodes
:transition
:var x
:var j
:guard (= phi 3) (= cu[x] 0) (< I N) (not (= st[x] 0)) (not (= tp 0)) (= x tp) (= sp x) (not (= TS[x] 600))
: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 ed
:val ScM
:val ScP
: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 ed
:val ScM
:val ScP


:comment  T31
:comment  Reply processing when node=target and source!=myIP and source=victim
:comment  lines 25-30 Algorithm 1  --  just for configured nodes
:comment  it calls Refresh() for the cache entry about the victim
:transition
:var x
:var j
:guard (= phi 3) (= cu[x] 0) (< I N) (not (= st[x] 0)) (not (= tp 0)) (= x tp) (not (= sp x)) (= sp 2) (not (= TS[x] 600))
:numcases 2
:case (= x j)
:val phi
:val (+ I 1)
:val GA
:val TS[j]
:val sm[j]
:val ScM
:val ScP
:val 1
:val st[j]
:val tp
:val sh
:val sp
:val ed
:val ScM
:val ScP
: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 ed
:val ScM
:val ScP


:comment  T32
:comment  this corresponds to Update() policy
:comment  performed just for configured nodes; the other nodes can only execute T1
:transition
:var x
:var j
:guard (= TS[x] 600) (not (= st[x] 0))
:numcases 2
:case (= x j)
:val phi
:val I
:val GA
:val 0
:val sm[j]
:val ScM
:val ScP
:val cu[j]
:val st[j]
:val tp
:val sh
:val sp
:val ed
:val ScM
:val ScP
:case (not (= x j))
:val phi
:val I
:val GA
:val TS[j]
:val sm[j]
:val ScM
:val ScP
:val cu[j]
:val st[j]
:val tp
:val sh
:val sp
:val ed
:val ScM
:val ScP


:comment  T33
:comment  re-set everything but caches before new iteration
:transition
:var x
:var j
:guard (= phi 3) (>= I N) (= sm[x] 0) (= cu[x] 1) (not (= TS[x] 600))
:uguard (= 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 -1
:val ScM
:val ScP
: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 -1
:val ScM
:val ScP