[Imprint][Data Privacy Statement][E-Mail]
Back to main index.
View the specification.
View theorem base summary,
View theorem base listing,
the used properties by spec,
the dependency list,
the symbol table,
automaton specification
Hashset
using hashset-preds
variables
ar : Array(Elem);
e : Elem;
tid : Tid;
n : Nat;
m : Nat;
sz : Nat;
b : Bool;
found : Bool;
state variables
ar : Array(Elem);
local state variables
tid : Tid;
thread id tid;
external labels
idle;
special actions
doINSERT(. .tid : Tid;. .b : Bool) |
doMEMBER(. .tid : Tid);
initial state
∃ n. n > 0 ∧ ar = mkar(n, ⊥) ∧ pcf = (λ tid. idle)
declarations
INSERT:
idle :- INSERT(e; ar; b)
precondition e ≠ ⊥;
postcondition b ↔ (∃ n. n < # ar ∧ ar[n] = e);
{
I1 :- let sz = # ar
in
I2 :- let n0 = get_hash(e, sz)
in
I3 :- let n = n0
in {
I4 :- b := false;
I5 :- while ¬ b
do {
I6 with (e = ar[n] ⊃ doINSERT(tid, true);τ) :-
let e0 = ar[n]
in
I7 :- if e = e0
then {
I8 :- b := true;
I9 :- return idle :-}
else
I10 :- if e0 ≠ ⊥
then
I11 :- n := (n + 1) % sz
else {
I12 with (ar[n] = ⊥ ∨ ar[n] = e ⊃ doINSERT(tid, true);τ) :-
if* ar[n] = ⊥ then e0 := e, ar[n] := e else e0 := ar[n];
I13 :- if e0 = e then {
I14 :- b := true;
I15 :- return idle :-} else
I16 :- n := (n + 1) % sz};
I17 :- if n = n0 then {
I18 with doINSERT(tid, false) :- b := false;
I19 :- return idle :-} else
I20 :- skip}};
I21 :- return idle :-
}
;
assertions
I7, I10 : e0 ≠ ⊥ → e0 = ar[n];
I8, I14 : e = e0;
I10, I11 : e ≠ e0;
I11 : e0 ≠ ⊥ ∧ e0 = ar[n];
I13 : ar[n] ≠ ⊥ ∧ ar[n] = e0;
I14, I15 : e = ar[n];
I16 : ar[n] ≠ ⊥ ∧ ar[n] ≠ e;
I4 -> I16, I20 : allslotsfull(ar, n0, n, e, false);
I17 : allslotsfull(ar, n0, n, e, true);
I18, I19 : allslotsfull(ar, n0, n0, e, true);
I20 : n ≠ n0;
I8, I9 : e = ar[n];
declarations
MEMBER:
idle :- MEMBER(e, ar; b)
precondition e ≠ ⊥;
postcondition b → (∃ n. n < # ar ∧ ar[n] = e);
{
M1 :- let sz = # ar
in
M2 :- let n0 = get_hash(e, sz)
in
M3 :- let n = n0
in {
M4 :- b := false;
M5 :- while ¬ b
do
M6 with (ar[n] = e ∨ ar[n] = ⊥ ∨ (n + 1) % sz = n0 ⊃ doMEMBER(tid);τ) :-
let e0 = ar[n]
in
M7 :- if e = e0
then {
M8 :- b := true;
M9 :- return idle :-}
else
M10 :- if e0 = ⊥
then {
M11 :- b := false;
M12 :- return idle :-}
else {
M13 :- n := (n + 1) % sz;
M14 :- if n = n0 then {
M15 :- b := false;
M16 :- return idle :-} else
M17 :- skip}};
M18 :- return idle :-
}
;
assertions
: # ar ≠ 0 ∧ htok(ar);
I4 -> I20, M4 -> M17 : n < # ar;
I1 -> I20, M1 -> M17 : e ≠ ⊥;
I2 -> I20, M2 -> M17 : sz = # ar;
I3 -> I20, M3 -> M17 : n0 < # ar ∧ n0 = get_hash(e, sz);
I4, M4 : n = n0;
I5 -> I8, I10 -> I14, I16 -> I20, M5 -> M7, M10 -> M17 : ¬ b;
I9, I15, M9 : b;
I21, M18 : false;
M7, M10 : e0 ≠ ⊥ → e0 = ar[n];
M8, M9 : ∃ n. n < # ar ∧ ar[n] = e;
M13 : ar[n] ≠ ⊥ ∧ ar[n] ≠ e;
M10 -> M13 : e ≠ e0;
M4 -> M10, M13, M17 : allslotsfull(ar, n0, n, e, false);
M14 : allslotsfull(ar, n0, n, e, true);
M15, M16 : allslotsfull(ar, n0, n0, e, true);
M17 : n ≠ n0;
rely condition
rely(ar, ar0);
end automaton specification ;;; END
------------------------------------------------
base =
enrich
hashset-preds
with
variables
ar : Array(Elem);
e : Elem;
tid : Tid;
n : Nat;
m : Nat;
sz : Nat;
b : Bool;
found : Bool;
end enrich
pc =
data specification
HashsetPC = I1
| I2
| I3
| I4
| I5
| I6
| I7
| I8
| I9
| I10
| I11
| I12
| I13
| I14
| I15
| I16
| I17
| I18
| I19
| I20
| I21
| M1
| M2
| M3
| M4
| M5
| M6
| M7
| M8
| M9
| M10
| M11
| M12
| M13
| M14
| M15
| M16
| M17
| M18
| idle
;
variables
pc : HashsetPC;
end data specification
gs =
data specification
using base
HashsetGState := mkgs(. .ar : Array(Elem))
;
variables
gs : HashsetGState;
ar : Array(Elem);
end data specification
ls =
data specification
using base
HashsetLState := mkls(. .tid : Tid;
. .e : Elem;
. .b : Bool;
. .sz : Nat;
. .n0 : Nat;
. .n : Nat;
. .e0 : Elem)
;
variables
ls : HashsetLState;
tid : Tid;
e : Elem;
b : Bool;
sz : Nat;
n : Nat;
end data specification
state =
data specification
using pc, localstate,
globalstate
HashsetState := mkstate(. .gstate : HashsetGState;. .lsf : Tid → HashsetLState;. .pcf : Tid → HashsetPC)
;
variables
s : HashsetState;
lsf : Tid → HashsetLState;
pcf : Tid → HashsetPC;
gstate : HashsetGState;
end data specification
action =
data specification
using base
data types
HashsetAction = doINSERT(. .tid : Tid;. .b : Bool)
| doMEMBER(. .tid : Tid)
| invINSERT(. .tid : Tid;. .invINSERTe : Elem)
| invMEMBER(. .tid : Tid;. .invMEMBERe : Elem)
| retINSERT(. .tid : Tid;. .retINSERTb : Bool)
| retMEMBER(. .tid : Tid;. .retMEMBERb : Bool)
| τ
;
variables
a : HashsetAction;
tid : Tid;
b : Bool;
invINSERTe : Elem;
invMEMBERe : Elem;
retINSERTb : Bool;
retMEMBERb : Bool;
end data specification
step =
enrich
state,
action
with
functions
lstepf : HashsetGState × HashsetLState × HashsetPC × HashsetAction → HashsetLState;
gstepf : HashsetGState × HashsetLState × HashsetPC × HashsetAction → HashsetGState;
pcstepf : HashsetGState × HashsetLState × HashsetPC × HashsetAction → HashsetPC;
predicates
HashsetRely : HashsetGState × Tid × HashsetGState;
hashsetInit : HashsetState;
hashsetStep : HashsetState × HashsetAction × HashsetState;
pre : HashsetGState × HashsetLState × HashsetPC × HashsetAction;
lstep : HashsetGState × HashsetLState × HashsetPC × HashsetAction × HashsetGState × HashsetLState × HashsetPC;
HashsetGInv : HashsetGState;
HashsetLInv : HashsetGState × HashsetLState × HashsetPC;
HashsetInv : HashsetGState × (Tid → HashsetLState) × (Tid → HashsetPC);
axioms
HashsetInv: HashsetInv(gs, lsf, pcf) ↔ HashsetGInv(gs) ∧ (∀ tid. lsf(tid).tid = tid ∧ HashsetLInv(gs, lsf(tid), pcf(tid)));
HashsetGInv: HashsetGInv(gs) ↔ # gs.ar ≠ 0 ∧ htok(gs.ar);
HashsetLInv:
HashsetLInv(gs, ls, pc)
↔ (pc = I7 ∨ pc = I10 → ls.e0 ≠ ⊥ → ls.e0 = gs.ar[ls.n]) ∧ (pc = I8 ∨ pc = I14 → ls.e = ls.e0) ∧ (pc = I10 ∨ pc = I11 → ls.e ≠ ls.e0)
∧ (pc = I11 → ls.e0 ≠ ⊥ ∧ ls.e0 = gs.ar[ls.n]) ∧ (pc = I13 → gs.ar[ls.n] ≠ ⊥ ∧ gs.ar[ls.n] = ls.e0)
∧ (pc = I14 ∨ pc = I15 → ls.e = gs.ar[ls.n]) ∧ (pc = I16 → gs.ar[ls.n] ≠ ⊥ ∧ gs.ar[ls.n] ≠ ls.e)
∧ ( pc = I4 ∨ pc = I5 ∨ pc = I6 ∨ pc = I7 ∨ pc = I8 ∨ pc = I9 ∨ pc = I10 ∨ pc = I11 ∨ pc = I12 ∨ pc = I13 ∨ pc = I14 ∨ pc = I15
∨ pc = I16 ∨ pc = I20
→ allslotsfull(gs.ar, ls.n0, ls.n, ls.e, false))
∧ (pc = I17 → allslotsfull(gs.ar, ls.n0, ls.n, ls.e, true)) ∧ (pc = I18 ∨ pc = I19 → allslotsfull(gs.ar, ls.n0, ls.n0, ls.e, true))
∧ (pc = I20 → ls.n ≠ ls.n0) ∧ (pc = I8 ∨ pc = I9 → ls.e = gs.ar[ls.n])
∧ ( pc = I4 ∨ pc = I5 ∨ pc = I6 ∨ pc = I7 ∨ pc = I8 ∨ pc = I9 ∨ pc = I10 ∨ pc = I11 ∨ pc = I12 ∨ pc = I13 ∨ pc = I14 ∨ pc = I15
∨ pc = I16 ∨ pc = I17 ∨ pc = I18 ∨ pc = I19 ∨ pc = I20 ∨ pc = M4 ∨ pc = M5 ∨ pc = M6 ∨ pc = M7 ∨ pc = M8 ∨ pc = M9 ∨ pc = M10
∨ pc = M11 ∨ pc = M12 ∨ pc = M13 ∨ pc = M14 ∨ pc = M15 ∨ pc = M16 ∨ pc = M17
→ ls.n < # gs.ar)
∧ ( pc = I1 ∨ pc = I2 ∨ pc = I3 ∨ pc = I4 ∨ pc = I5 ∨ pc = I6 ∨ pc = I7 ∨ pc = I8 ∨ pc = I9 ∨ pc = I10 ∨ pc = I11 ∨ pc = I12 ∨ pc = I13
∨ pc = I14 ∨ pc = I15 ∨ pc = I16 ∨ pc = I17 ∨ pc = I18 ∨ pc = I19 ∨ pc = I20 ∨ pc = M1 ∨ pc = M2 ∨ pc = M3 ∨ pc = M4 ∨ pc = M5
∨ pc = M6 ∨ pc = M7 ∨ pc = M8 ∨ pc = M9 ∨ pc = M10 ∨ pc = M11 ∨ pc = M12 ∨ pc = M13 ∨ pc = M14 ∨ pc = M15 ∨ pc = M16 ∨ pc = M17
→ ls.e ≠ ⊥)
∧ ( pc = I2 ∨ pc = I3 ∨ pc = I4 ∨ pc = I5 ∨ pc = I6 ∨ pc = I7 ∨ pc = I8 ∨ pc = I9 ∨ pc = I10 ∨ pc = I11 ∨ pc = I12 ∨ pc = I13 ∨ pc = I14
∨ pc = I15 ∨ pc = I16 ∨ pc = I17 ∨ pc = I18 ∨ pc = I19 ∨ pc = I20 ∨ pc = M2 ∨ pc = M3 ∨ pc = M4 ∨ pc = M5 ∨ pc = M6 ∨ pc = M7
∨ pc = M8 ∨ pc = M9 ∨ pc = M10 ∨ pc = M11 ∨ pc = M12 ∨ pc = M13 ∨ pc = M14 ∨ pc = M15 ∨ pc = M16 ∨ pc = M17
→ ls.sz = # gs.ar)
∧ ( pc = I3 ∨ pc = I4 ∨ pc = I5 ∨ pc = I6 ∨ pc = I7 ∨ pc = I8 ∨ pc = I9 ∨ pc = I10 ∨ pc = I11 ∨ pc = I12 ∨ pc = I13 ∨ pc = I14
∨ pc = I15 ∨ pc = I16 ∨ pc = I17 ∨ pc = I18 ∨ pc = I19 ∨ pc = I20 ∨ pc = M3 ∨ pc = M4 ∨ pc = M5 ∨ pc = M6 ∨ pc = M7 ∨ pc = M8
∨ pc = M9 ∨ pc = M10 ∨ pc = M11 ∨ pc = M12 ∨ pc = M13 ∨ pc = M14 ∨ pc = M15 ∨ pc = M16 ∨ pc = M17
→ ls.n0 < # gs.ar ∧ ls.n0 = get_hash(ls.e, ls.sz))
∧ (pc = I4 ∨ pc = M4 → ls.n = ls.n0)
∧ ( pc = I5 ∨ pc = I6 ∨ pc = I7 ∨ pc = I8 ∨ pc = I10 ∨ pc = I11 ∨ pc = I12 ∨ pc = I13 ∨ pc = I14 ∨ pc = I16 ∨ pc = I17 ∨ pc = I18
∨ pc = I19 ∨ pc = I20 ∨ pc = M5 ∨ pc = M6 ∨ pc = M7 ∨ pc = M10 ∨ pc = M11 ∨ pc = M12 ∨ pc = M13 ∨ pc = M14 ∨ pc = M15 ∨ pc = M16
∨ pc = M17
→ ¬ ls.b)
∧ (pc = I9 ∨ pc = I15 ∨ pc = M9 → ls.b) ∧ (pc = I21 ∨ pc = M18 → false) ∧ (pc = M7 ∨ pc = M10 → ls.e0 ≠ ⊥ → ls.e0 = gs.ar[ls.n])
∧ (pc = M8 ∨ pc = M9 → (∃ n. n < # gs.ar ∧ gs.ar[n] = ls.e)) ∧ (pc = M13 → gs.ar[ls.n] ≠ ⊥ ∧ gs.ar[ls.n] ≠ ls.e)
∧ (pc = M10 ∨ pc = M11 ∨ pc = M12 ∨ pc = M13 → ls.e ≠ ls.e0)
∧ ( pc = M4 ∨ pc = M5 ∨ pc = M6 ∨ pc = M7 ∨ pc = M8 ∨ pc = M9 ∨ pc = M10 ∨ pc = M13 ∨ pc = M17
→ allslotsfull(gs.ar, ls.n0, ls.n, ls.e, false))
∧ (pc = M14 → allslotsfull(gs.ar, ls.n0, ls.n, ls.e, true)) ∧ (pc = M15 ∨ pc = M16 → allslotsfull(gs.ar, ls.n0, ls.n0, ls.e, true))
∧ (pc = M17 → ls.n ≠ ls.n0);
hashsetInit: hashsetInit(mkstate(gs, lsf, pcf)) ↔ (∃ n. n > 0 ∧ gs.ar = mkar(n, ⊥) ∧ pcf = (λ tid. idle)) ∧ (∀ tid. lsf(tid).tid = tid);
hashsetStep:
hashsetStep(mkstate(gs, lsf, pcf), a, mkstate(gs0, lsf0, pcf0))
↔ (∃ tid, ls, pc. lstep(gs, lsf(tid), pcf(tid), a, gs0, ls, pc) ∧ lsf0 = lsf(tid := ls) ∧ pcf0 = pcf(tid := pc));
lstep:
lstep(gs, ls, pc, a, gs0, ls0, pc0)
↔ pre(gs, ls, pc, a) ∧ ls0 = lstepf(gs, ls, pc, a) ∧ gs0 = gstepf(gs, ls, pc, a) ∧ pc0 = pcstepf(gs, ls, pc, a);
pre-I1: pre(gs, ls, I1, a) ↔ a = τ;
used for: s, ls;
pre-I2: pre(gs, ls, I2, a) ↔ a = τ;
used for: s, ls;
pre-I3: pre(gs, ls, I3, a) ↔ a = τ;
used for: s, ls;
pre-I4: pre(gs, ls, I4, a) ↔ a = τ;
used for: s, ls;
pre-I5: pre(gs, ls, I5, a) ↔ a = τ;
used for: s, ls;
pre-I6: pre(gs, ls, I6, a) ↔ a = (ls.e = gs.ar[ls.n] ⊃ doINSERT(ls.tid, true);τ);
used for: s, ls;
pre-I7: pre(gs, ls, I7, a) ↔ a = τ;
used for: s, ls;
pre-I8: pre(gs, ls, I8, a) ↔ a = τ;
used for: s, ls;
pre-I9: pre(gs, ls, I9, a) ↔ a = retINSERT(ls.tid, ls.b);
used for: s, ls;
pre-I10: pre(gs, ls, I10, a) ↔ a = τ;
used for: s, ls;
pre-I11: pre(gs, ls, I11, a) ↔ a = τ;
used for: s, ls;
pre-I12: pre(gs, ls, I12, a) ↔ a = (gs.ar[ls.n] = ⊥ ∨ gs.ar[ls.n] = ls.e ⊃ doINSERT(ls.tid, true);τ);
used for: s, ls;
pre-I13: pre(gs, ls, I13, a) ↔ a = τ;
used for: s, ls;
pre-I14: pre(gs, ls, I14, a) ↔ a = τ;
used for: s, ls;
pre-I15: pre(gs, ls, I15, a) ↔ a = retINSERT(ls.tid, ls.b);
used for: s, ls;
pre-I16: pre(gs, ls, I16, a) ↔ a = τ;
used for: s, ls;
pre-I17: pre(gs, ls, I17, a) ↔ a = τ;
used for: s, ls;
pre-I18: pre(gs, ls, I18, a) ↔ a = doINSERT(ls.tid, false);
used for: s, ls;
pre-I19: pre(gs, ls, I19, a) ↔ a = retINSERT(ls.tid, ls.b);
used for: s, ls;
pre-I20: pre(gs, ls, I20, a) ↔ a = τ;
used for: s, ls;
pre-I21: pre(gs, ls, I21, a) ↔ a = retINSERT(ls.tid, ls.b);
used for: s, ls;
pre-M1: pre(gs, ls, M1, a) ↔ a = τ;
used for: s, ls;
pre-M2: pre(gs, ls, M2, a) ↔ a = τ;
used for: s, ls;
pre-M3: pre(gs, ls, M3, a) ↔ a = τ;
used for: s, ls;
pre-M4: pre(gs, ls, M4, a) ↔ a = τ;
used for: s, ls;
pre-M5: pre(gs, ls, M5, a) ↔ a = τ;
used for: s, ls;
pre-M6: pre(gs, ls, M6, a) ↔ a = (gs.ar[ls.n] = ls.e ∨ gs.ar[ls.n] = ⊥ ∨ (ls.n + 1) % ls.sz = ls.n0 ⊃ doMEMBER(ls.tid);τ);
used for: s, ls;
pre-M7: pre(gs, ls, M7, a) ↔ a = τ;
used for: s, ls;
pre-M8: pre(gs, ls, M8, a) ↔ a = τ;
used for: s, ls;
pre-M9: pre(gs, ls, M9, a) ↔ a = retMEMBER(ls.tid, ls.b);
used for: s, ls;
pre-M10: pre(gs, ls, M10, a) ↔ a = τ;
used for: s, ls;
pre-M11: pre(gs, ls, M11, a) ↔ a = τ;
used for: s, ls;
pre-M12: pre(gs, ls, M12, a) ↔ a = retMEMBER(ls.tid, ls.b);
used for: s, ls;
pre-M13: pre(gs, ls, M13, a) ↔ a = τ;
used for: s, ls;
pre-M14: pre(gs, ls, M14, a) ↔ a = τ;
used for: s, ls;
pre-M15: pre(gs, ls, M15, a) ↔ a = τ;
used for: s, ls;
pre-M16: pre(gs, ls, M16, a) ↔ a = retMEMBER(ls.tid, ls.b);
used for: s, ls;
pre-M17: pre(gs, ls, M17, a) ↔ a = τ;
used for: s, ls;
pre-M18: pre(gs, ls, M18, a) ↔ a = retMEMBER(ls.tid, ls.b);
used for: s, ls;
pre-idle: pre(gs, ls, idle, a) ↔ (∃ e1. a = invINSERT(ls.tid, e1) ∧ e1 ≠ ⊥) ∨ (∃ e1. a = invMEMBER(ls.tid, e1) ∧ e1 ≠ ⊥);
used for: s, ls;
lstepf-idle-INSERT: ls.tid = tid → lstepf(gs, ls, idle, invINSERT(tid, e1)) = ls.e:= e1;
used for: s, ls;
lstepf-I1: lstepf(gs, ls, I1, τ) = ls.sz:= # gs.ar;
used for: s, ls;
lstepf-I2: lstepf(gs, ls, I2, τ) = ls.n0:= get_hash(ls.e, ls.sz);
used for: s, ls;
lstepf-I3: lstepf(gs, ls, I3, τ) = ls.n:= ls.n0;
used for: s, ls;
lstepf-I4: lstepf(gs, ls, I4, τ) = ls.b:= false;
used for: s, ls;
lstepf-I5: lstepf(gs, ls, I5, τ) = ls;
used for: s, ls;
lstepf-I6: lstepf(gs, ls, I6, a) = ls.e0:= gs.ar[ls.n];
used for: s, ls;
lstepf-I7: lstepf(gs, ls, I7, τ) = ls;
used for: s, ls;
lstepf-I8: lstepf(gs, ls, I8, τ) = ls.b:= true;
used for: s, ls;
lstepf-I9: ls.tid = tid → lstepf(gs, ls, I9, retINSERT(tid, ls.b)) = ls;
used for: s, ls;
lstepf-I10: lstepf(gs, ls, I10, τ) = ls;
used for: s, ls;
lstepf-I11: lstepf(gs, ls, I11, τ) = ls.n:= ((ls.n + 1) % ls.sz);
used for: s, ls;
lstepf-I12: lstepf(gs, ls, I12, a) = (gs.ar[ls.n] = ⊥ ⊃ ls.e0:= ls.e;ls.e0:= gs.ar[ls.n]);
used for: s, ls;
lstepf-I13: lstepf(gs, ls, I13, τ) = ls;
used for: s, ls;
lstepf-I14: lstepf(gs, ls, I14, τ) = ls.b:= true;
used for: s, ls;
lstepf-I15: ls.tid = tid → lstepf(gs, ls, I15, retINSERT(tid, ls.b)) = ls;
used for: s, ls;
lstepf-I16: lstepf(gs, ls, I16, τ) = ls.n:= ((ls.n + 1) % ls.sz);
used for: s, ls;
lstepf-I17: lstepf(gs, ls, I17, τ) = ls;
used for: s, ls;
lstepf-I18: lstepf(gs, ls, I18, a) = ls.b:= false;
used for: s, ls;
lstepf-I19: ls.tid = tid → lstepf(gs, ls, I19, retINSERT(tid, ls.b)) = ls;
used for: s, ls;
lstepf-I20: lstepf(gs, ls, I20, τ) = ls;
used for: s, ls;
lstepf-I21: ls.tid = tid → lstepf(gs, ls, I21, retINSERT(tid, ls.b)) = ls;
used for: s, ls;
lstepf-idle-MEMBER: ls.tid = tid → lstepf(gs, ls, idle, invMEMBER(tid, e1)) = ls.e:= e1;
used for: s, ls;
lstepf-M1: lstepf(gs, ls, M1, τ) = ls.sz:= # gs.ar;
used for: s, ls;
lstepf-M2: lstepf(gs, ls, M2, τ) = ls.n0:= get_hash(ls.e, ls.sz);
used for: s, ls;
lstepf-M3: lstepf(gs, ls, M3, τ) = ls.n:= ls.n0;
used for: s, ls;
lstepf-M4: lstepf(gs, ls, M4, τ) = ls.b:= false;
used for: s, ls;
lstepf-M5: lstepf(gs, ls, M5, τ) = ls;
used for: s, ls;
lstepf-M6: lstepf(gs, ls, M6, a) = ls.e0:= gs.ar[ls.n];
used for: s, ls;
lstepf-M7: lstepf(gs, ls, M7, τ) = ls;
used for: s, ls;
lstepf-M8: lstepf(gs, ls, M8, τ) = ls.b:= true;
used for: s, ls;
lstepf-M9: ls.tid = tid → lstepf(gs, ls, M9, retMEMBER(tid, ls.b)) = ls;
used for: s, ls;
lstepf-M10: lstepf(gs, ls, M10, τ) = ls;
used for: s, ls;
lstepf-M11: lstepf(gs, ls, M11, τ) = ls.b:= false;
used for: s, ls;
lstepf-M12: ls.tid = tid → lstepf(gs, ls, M12, retMEMBER(tid, ls.b)) = ls;
used for: s, ls;
lstepf-M13: lstepf(gs, ls, M13, τ) = ls.n:= ((ls.n + 1) % ls.sz);
used for: s, ls;
lstepf-M14: lstepf(gs, ls, M14, τ) = ls;
used for: s, ls;
lstepf-M15: lstepf(gs, ls, M15, τ) = ls.b:= false;
used for: s, ls;
lstepf-M16: ls.tid = tid → lstepf(gs, ls, M16, retMEMBER(tid, ls.b)) = ls;
used for: s, ls;
lstepf-M17: lstepf(gs, ls, M17, τ) = ls;
used for: s, ls;
lstepf-M18: ls.tid = tid → lstepf(gs, ls, M18, retMEMBER(tid, ls.b)) = ls;
used for: s, ls;
gstepf-I1: gstepf(gs, ls, I1, τ) = gs;
used for: s, ls;
gstepf-I10: gstepf(gs, ls, I10, τ) = gs;
used for: s, ls;
gstepf-I11: gstepf(gs, ls, I11, τ) = gs;
used for: s, ls;
gstepf-I12: gstepf(gs, ls, I12, a) = (gs.ar[ls.n] = ⊥ ⊃ gs.ar:= gs.ar[ls.n := ls.e];gs);
used for: s, ls;
gstepf-I13: gstepf(gs, ls, I13, τ) = gs;
used for: s, ls;
gstepf-I14: gstepf(gs, ls, I14, τ) = gs;
used for: s, ls;
gstepf-I15: ls.tid = tid → gstepf(gs, ls, I15, retINSERT(tid, b)) = gs;
used for: s, ls;
gstepf-I16: gstepf(gs, ls, I16, τ) = gs;
used for: s, ls;
gstepf-I17: gstepf(gs, ls, I17, τ) = gs;
used for: s, ls;
gstepf-I18: gstepf(gs, ls, I18, a) = gs;
used for: s, ls;
gstepf-I19: ls.tid = tid → gstepf(gs, ls, I19, retINSERT(tid, b)) = gs;
used for: s, ls;
gstepf-I2: gstepf(gs, ls, I2, τ) = gs;
used for: s, ls;
gstepf-I20: gstepf(gs, ls, I20, τ) = gs;
used for: s, ls;
gstepf-I21: ls.tid = tid → gstepf(gs, ls, I21, retINSERT(tid, b)) = gs;
used for: s, ls;
gstepf-I3: gstepf(gs, ls, I3, τ) = gs;
used for: s, ls;
gstepf-I4: gstepf(gs, ls, I4, τ) = gs;
used for: s, ls;
gstepf-I5: gstepf(gs, ls, I5, τ) = gs;
used for: s, ls;
gstepf-I6: gstepf(gs, ls, I6, a) = gs;
used for: s, ls;
gstepf-I7: gstepf(gs, ls, I7, τ) = gs;
used for: s, ls;
gstepf-I8: gstepf(gs, ls, I8, τ) = gs;
used for: s, ls;
gstepf-I9: ls.tid = tid → gstepf(gs, ls, I9, retINSERT(tid, b)) = gs;
used for: s, ls;
gstepf-M1: gstepf(gs, ls, M1, τ) = gs;
used for: s, ls;
gstepf-M10: gstepf(gs, ls, M10, τ) = gs;
used for: s, ls;
gstepf-M11: gstepf(gs, ls, M11, τ) = gs;
used for: s, ls;
gstepf-M12: ls.tid = tid → gstepf(gs, ls, M12, retMEMBER(tid, b)) = gs;
used for: s, ls;
gstepf-M13: gstepf(gs, ls, M13, τ) = gs;
used for: s, ls;
gstepf-M14: gstepf(gs, ls, M14, τ) = gs;
used for: s, ls;
gstepf-M15: gstepf(gs, ls, M15, τ) = gs;
used for: s, ls;
gstepf-M16: ls.tid = tid → gstepf(gs, ls, M16, retMEMBER(tid, b)) = gs;
used for: s, ls;
gstepf-M17: gstepf(gs, ls, M17, τ) = gs;
used for: s, ls;
gstepf-M18: ls.tid = tid → gstepf(gs, ls, M18, retMEMBER(tid, b)) = gs;
used for: s, ls;
gstepf-M2: gstepf(gs, ls, M2, τ) = gs;
used for: s, ls;
gstepf-M3: gstepf(gs, ls, M3, τ) = gs;
used for: s, ls;
gstepf-M4: gstepf(gs, ls, M4, τ) = gs;
used for: s, ls;
gstepf-M5: gstepf(gs, ls, M5, τ) = gs;
used for: s, ls;
gstepf-M6: gstepf(gs, ls, M6, a) = gs;
used for: s, ls;
gstepf-M7: gstepf(gs, ls, M7, τ) = gs;
used for: s, ls;
gstepf-M8: gstepf(gs, ls, M8, τ) = gs;
used for: s, ls;
gstepf-M9: ls.tid = tid → gstepf(gs, ls, M9, retMEMBER(tid, b)) = gs;
used for: s, ls;
gstepf-idle: gstepf(gs, ls, idle, a) = gs;
used for: s, ls;
pcstepf-idle-INSERT: ls.tid = tid → pcstepf(gs, ls, idle, invINSERT(tid, e1)) = I1;
used for: s, ls;
pcstepf-I1: pcstepf(gs, ls, I1, a) = I2;
used for: s, ls;
pcstepf-I2: pcstepf(gs, ls, I2, a) = I3;
used for: s, ls;
pcstepf-I3: pcstepf(gs, ls, I3, a) = I4;
used for: s, ls;
pcstepf-I4: pcstepf(gs, ls, I4, a) = I5;
used for: s, ls;
pcstepf-I5: pcstepf(gs, ls, I5, a) = (¬ ls.b ⊃ I6;I21);
used for: s, ls;
pcstepf-I6: pcstepf(gs, ls, I6, a) = I7;
used for: s, ls;
pcstepf-I7: pcstepf(gs, ls, I7, a) = (ls.e = ls.e0 ⊃ I8;I10);
used for: s, ls;
pcstepf-I8: pcstepf(gs, ls, I8, a) = I9;
used for: s, ls;
pcstepf-I9: pcstepf(gs, ls, I9, a) = idle;
used for: s, ls;
pcstepf-I10: pcstepf(gs, ls, I10, a) = (ls.e0 ≠ ⊥ ⊃ I11;I12);
used for: s, ls;
pcstepf-I11: pcstepf(gs, ls, I11, a) = I17;
used for: s, ls;
pcstepf-I12: pcstepf(gs, ls, I12, a) = I13;
used for: s, ls;
pcstepf-I13: pcstepf(gs, ls, I13, a) = (ls.e0 = ls.e ⊃ I14;I16);
used for: s, ls;
pcstepf-I14: pcstepf(gs, ls, I14, a) = I15;
used for: s, ls;
pcstepf-I15: pcstepf(gs, ls, I15, a) = idle;
used for: s, ls;
pcstepf-I16: pcstepf(gs, ls, I16, a) = I17;
used for: s, ls;
pcstepf-I17: pcstepf(gs, ls, I17, a) = (ls.n = ls.n0 ⊃ I18;I20);
used for: s, ls;
pcstepf-I18: pcstepf(gs, ls, I18, a) = I19;
used for: s, ls;
pcstepf-I19: pcstepf(gs, ls, I19, a) = idle;
used for: s, ls;
pcstepf-I20: pcstepf(gs, ls, I20, a) = I5;
used for: s, ls;
pcstepf-I21: pcstepf(gs, ls, I21, a) = idle;
used for: s, ls;
pcstepf-idle-MEMBER: ls.tid = tid → pcstepf(gs, ls, idle, invMEMBER(tid, e1)) = M1;
used for: s, ls;
pcstepf-M1: pcstepf(gs, ls, M1, a) = M2;
used for: s, ls;
pcstepf-M2: pcstepf(gs, ls, M2, a) = M3;
used for: s, ls;
pcstepf-M3: pcstepf(gs, ls, M3, a) = M4;
used for: s, ls;
pcstepf-M4: pcstepf(gs, ls, M4, a) = M5;
used for: s, ls;
pcstepf-M5: pcstepf(gs, ls, M5, a) = (¬ ls.b ⊃ M6;M18);
used for: s, ls;
pcstepf-M6: pcstepf(gs, ls, M6, a) = M7;
used for: s, ls;
pcstepf-M7: pcstepf(gs, ls, M7, a) = (ls.e = ls.e0 ⊃ M8;M10);
used for: s, ls;
pcstepf-M8: pcstepf(gs, ls, M8, a) = M9;
used for: s, ls;
pcstepf-M9: pcstepf(gs, ls, M9, a) = idle;
used for: s, ls;
pcstepf-M10: pcstepf(gs, ls, M10, a) = (ls.e0 = ⊥ ⊃ M11;M13);
used for: s, ls;
pcstepf-M11: pcstepf(gs, ls, M11, a) = M12;
used for: s, ls;
pcstepf-M12: pcstepf(gs, ls, M12, a) = idle;
used for: s, ls;
pcstepf-M13: pcstepf(gs, ls, M13, a) = M14;
used for: s, ls;
pcstepf-M14: pcstepf(gs, ls, M14, a) = (ls.n = ls.n0 ⊃ M15;M17);
used for: s, ls;
pcstepf-M15: pcstepf(gs, ls, M15, a) = M16;
used for: s, ls;
pcstepf-M16: pcstepf(gs, ls, M16, a) = idle;
used for: s, ls;
pcstepf-M17: pcstepf(gs, ls, M17, a) = M5;
used for: s, ls;
pcstepf-M18: pcstepf(gs, ls, M18, a) = idle;
used for: s, ls;
HashsetRely: HashsetRely(gs, tid, gs0) ↔ rely(gs.ar, gs0.ar);
end enrich