[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
Set
using set-basic, tid
sorts Elem;
constants
⊥ : Elem;
variables
set : Set(Elem);
e : Elem;
le : Elem;
tid : Tid;
b : Bool;
lb : Bool;
state variables
set : Set(Elem);
local state variables
tid : Tid;
le : Elem;
lb : Bool;
thread id tid;
external labels
idle,
invMember,
retMember,
invInsert,
retInsert;
special actions
ADoInsert(. .tid : Tid;. .b : Bool) |
ADoMember(. .tid : Tid) |
AInvInsert(. .tid : Tid;. .e : Elem) |
AInvMember(. .tid : Tid;. .e : Elem) |
ARetInsert(. .tid : Tid;. .b : Bool) |
ARetMember(. .tid : Tid;. .b : Bool);
initial state
set = ∅ ∧ pcf = (λ tid. idle)
declarations
INVINSERT:
idle :- INVINSERT(e; le)
atomic with AInvInsert(tid, e)
precondition e ≠ ⊥;
{
le := e; return invInsert :-
}
;
DOINSERT:
invInsert :- DOINSERT(b, le; lb, set)
atomic with ADoInsert(tid, b)
{
if b then set := set ++ le, lb := true else lb := false; return retInsert :-
}
;
RETINSERT:
retInsert :- RETINSERT(lb; b)
atomic with ARetInsert(tid, b)
{
b := lb; return idle :-
}
;
INVMEMBER:
idle :- INVMEMBER(e; le)
atomic with AInvMember(tid, e)
precondition e ≠ ⊥;
{
le := e; return invMember :-
}
;
DOMEMBER:
invMember :- DOMEMBER(le, set; lb)
atomic with ADoMember(tid)
{
lb := le ∈ set; return retMember :-
}
;
RETMEMBER:
retMember :- RETMEMBER(lb; b)
atomic with ARetMember(tid, b)
{
b := lb; return idle :-
}
;
assertions
invInsert, retInsert, invMember, retMember : le ≠ ⊥;
retMember, retInsert : lb → le ∈ set;
rely condition
set ⊆ set0;
end automaton specification ;;; END
------------------------------------------------
base =
enrich
set-basic,
tid
with
sorts Elem;
constants
⊥ : Elem;
variables
set : Set(Elem);
e : Elem;
le : Elem;
tid : Tid;
b : Bool;
lb : Bool;
end enrich
pc =
data specification
SetPC = idle
| invInsert
| invMember
| retInsert
| retMember
;
variables
pc : SetPC;
end data specification
gs =
data specification
using base
SetGState := mkgs(. .set : Set(Elem))
;
variables
gs : SetGState;
set : Set(Elem);
end data specification
ls =
data specification
using base
SetLState := mkls(. .tid : Tid;. .le : Elem;. .lb : Bool)
;
variables
ls : SetLState;
tid : Tid;
le : Elem;
lb : Bool;
end data specification
state =
data specification
using pc, localstate,
globalstate
SetState := mkstate(. .gstate : SetGState;. .lsf : Tid → SetLState;. .pcf : Tid → SetPC)
;
variables
s : SetState;
lsf : Tid → SetLState;
pcf : Tid → SetPC;
gstate : SetGState;
end data specification
action =
data specification
using base
data types
SetAction = ADoInsert(. .tid : Tid;. .b : Bool)
| ADoMember(. .tid : Tid)
| AInvInsert(. .tid : Tid;. .e : Elem)
| AInvMember(. .tid : Tid;. .e : Elem)
| ARetInsert(. .tid : Tid;. .b : Bool)
| ARetMember(. .tid : Tid;. .b : Bool)
| τ
;
variables
a : SetAction;
tid : Tid;
b : Bool;
e : Elem;
end data specification
step =
enrich
state,
action
with
functions
lstepf : SetGState × SetLState × SetPC × SetAction → SetLState;
gstepf : SetGState × SetLState × SetPC × SetAction → SetGState;
pcstepf : SetGState × SetLState × SetPC × SetAction → SetPC;
predicates
SetRely : SetGState × Tid × SetGState;
setInit : SetState;
setStep : SetState × SetAction × SetState;
pre : SetGState × SetLState × SetPC × SetAction;
lstep : SetGState × SetLState × SetPC × SetAction × SetGState × SetLState × SetPC;
SetGInv : SetGState;
SetLInv : SetGState × SetLState × SetPC;
SetInv : SetGState × (Tid → SetLState) × (Tid → SetPC);
procedures INVINSERT Elem : Elem nonfunctional ;
DOINSERT Bool × Elem : Bool × Set(Elem) nonfunctional ;
RETINSERT Bool : : Bool ;
INVMEMBER Elem : Elem nonfunctional ;
DOMEMBER Elem × Set(Elem) : Bool nonfunctional ;
RETMEMBER Bool : : Bool ;
axioms
SetInv: SetInv(gs, lsf, pcf) ↔ SetGInv(gs) ∧ (∀ tid. lsf(tid).tid = tid ∧ SetLInv(gs, lsf(tid), pcf(tid)));
SetGInv: SetGInv(gs) ↔ true;
SetLInv:
SetLInv(gs, ls, pc)
↔ (pc = invInsert ∨ pc = retInsert ∨ pc = invMember ∨ pc = retMember → ls.le ≠ ⊥)
∧ (pc = retMember ∨ pc = retInsert → ls.lb → ls.le ∈ gs.set);
setInit: setInit(mkstate(gs, lsf, pcf)) ↔ (gs.set = ∅ ∧ pcf = (λ tid. idle)) ∧ (∀ tid. lsf(tid).tid = tid);
setStep:
setStep(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-idle: pre(gs, ls, idle, a) ↔ (∃ e. a = AInvInsert(ls.tid, e) ∧ e ≠ ⊥) ∨ (∃ e. a = AInvMember(ls.tid, e) ∧ e ≠ ⊥);
used for: s, ls;
pre-invInsert: pre(gs, ls, invInsert, a) ↔ (∃ b. a = ADoInsert(ls.tid, b));
used for: s, ls;
pre-invMember: pre(gs, ls, invMember, a) ↔ a = ADoMember(ls.tid);
used for: s, ls;
pre-retInsert: pre(gs, ls, retInsert, a) ↔ (∃ b0. a = ARetInsert(ls.tid, b0) ∧ (b0 ↔ ls.lb));
used for: s, ls;
pre-retMember: pre(gs, ls, retMember, a) ↔ (∃ b0. a = ARetMember(ls.tid, b0) ∧ (b0 ↔ ls.lb));
used for: s, ls;
lstepf-idle-INVINSERT: ls.tid = tid → lstepf(gs, ls, idle, AInvInsert(tid, e)) = ls.le:= e;
used for: s, ls;
lstepf-invInsert-DOINSERT: ls.tid = tid → lstepf(gs, ls, invInsert, ADoInsert(tid, b)) = (b ⊃ ls.lb:= true;ls.lb:= false);
used for: s, ls;
lstepf-retInsert-RETINSERT: ls.tid = tid → lstepf(gs, ls, retInsert, ARetInsert(tid, b0)) = ls;
used for: s, ls;
lstepf-idle-INVMEMBER: ls.tid = tid → lstepf(gs, ls, idle, AInvMember(tid, e)) = ls.le:= e;
used for: s, ls;
lstepf-invMember-DOMEMBER: ls.tid = tid → lstepf(gs, ls, invMember, ADoMember(tid)) = ls.lb:= (ls.le ∈ gs.set);
used for: s, ls;
lstepf-retMember-RETMEMBER: ls.tid = tid → lstepf(gs, ls, retMember, ARetMember(tid, b0)) = ls;
used for: s, ls;
gstepf-idle: gstepf(gs, ls, idle, a) = gs;
used for: s, ls;
gstepf-invInsert-DOINSERT: ls.tid = tid → gstepf(gs, ls, invInsert, ADoInsert(tid, b)) = (b ⊃ gs.set:= (gs.set ++ ls.le);gs);
used for: s, ls;
gstepf-invMember-DOMEMBER: ls.tid = tid → gstepf(gs, ls, invMember, ADoMember(tid)) = gs;
used for: s, ls;
gstepf-retInsert-RETINSERT: ls.tid = tid → gstepf(gs, ls, retInsert, ARetInsert(tid, b0)) = gs;
used for: s, ls;
gstepf-retMember-RETMEMBER: ls.tid = tid → gstepf(gs, ls, retMember, ARetMember(tid, b0)) = gs;
used for: s, ls;
pcstepf-idle-INVINSERT: ls.tid = tid → pcstepf(gs, ls, idle, AInvInsert(tid, e)) = invInsert;
used for: s, ls;
pcstepf-invInsert-DOINSERT: ls.tid = tid → pcstepf(gs, ls, invInsert, ADoInsert(tid, b)) = retInsert;
used for: s, ls;
pcstepf-retInsert-RETINSERT: ls.tid = tid → pcstepf(gs, ls, retInsert, ARetInsert(tid, b0)) = idle;
used for: s, ls;
pcstepf-idle-INVMEMBER: ls.tid = tid → pcstepf(gs, ls, idle, AInvMember(tid, e)) = invMember;
used for: s, ls;
pcstepf-invMember-DOMEMBER: ls.tid = tid → pcstepf(gs, ls, invMember, ADoMember(tid)) = retMember;
used for: s, ls;
pcstepf-retMember-RETMEMBER: ls.tid = tid → pcstepf(gs, ls, retMember, ARetMember(tid, b0)) = idle;
used for: s, ls;
SetRely: SetRely(gs, tid, gs0) ↔ gs.set ⊆ gs0.set;
end enrich