[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,

Signature symbols in this unit

Symbol	Specification	Kind	Type
# .	list-data	f	List('a) → Nat
# .	set-basic	f	Set('a) → Nat
#oc	list-perm	f	'a × List('a) → Nat
. '	list	f	'a → List('a)
. + .	nat-basic	f	Nat × Nat → Nat
. + .	list-data	f	'a × List('a) → List('a)
. + .	list	f	List('a) × List('a) → List('a)
. + .	list	f	List('a) × 'a → List('a)
. ++ .	list-dup	f	List('a) × 'a → List('a)
. ++ .	set-basic	f	Set('a) × 'a → Set('a)
. +1	nat-basic	f	Nat → Nat
. +2 .	list	f	'a × 'a → List('a)
. - .	nat	pf	Nat × Nat → Nat with λ n, m. n ≥ m
. -- .	set-union	f	Set('a) × 'a → Set('a)
. -1	nat-basic	pf	Nat → Nat with λ n. n ≠ 0
. -1l .	list-del	f	List('a) × 'a → List('a)
. -l .	list-del	f	List('a) × 'a → List('a)
. -p .	list-del	f	List('a) × Nat → List('a)
. .FO?	FOW	p	FOW
. .W?	FOW	p	FOW
. .butlast	list-last	pf	List('a) → List('a) with λ x. x ≠ []
. .count ( . )	filter-count	f	List('a) × ('a → Bool) → Nat
. .count ( . )	filter-count	pf	List('a) × Nat × Nat × ('a → Bool) → Nat with λ x, m, n, p. m ≤ n ∧ n ≤ # x
. .ctr	FLITPSCweak	f	FLITPSCGState → L → Nat
. .ctr:= .	FLITPSCweak	f	FLITPSCGState × (L → Nat) → FLITPSCGState
. .distinct	list-dup	f	List('a) → List('a)
. .drop ( . )	list-del	pf	List('a) × Nat → List('a) with λ x, n. n ≤ # x
. .dropRight ( . )	list-last	pf	List('a) × Nat → List('a) with λ x, n. n ≤ # x
. .exists ( . )	forall-indexWhere	p	List('a) × ('a → Type(Bool))
. .filter ( . )	filter-count	f	List('a) × ('a → Bool) → List('a)
. .filter ( . )	set-union	f	Set('a) × ('a → Bool) → Set('a)
. .foldLeft ( . )	list	f	List('a) × 'b × ('b × 'a → 'b) → 'b
. .forall ( . )	forall-indexWhere	p	List('a) × ('a → Type(Bool))
. .gstate	FLITPSCweak	f	FLITPSCState → FLITPSCGState
. .gstate:= .	FLITPSCweak	f	FLITPSCState × FLITPSCGState → FLITPSCState
. .head	list-data	pf	List('a) → 'a with λ x. x ≠ []
. .indexOf ( . )	list-del	f	List('a) × 'a → Nat
. .indexWhere ( . )	forall-indexWhere	f	List('a) × ('a → Bool) → Nat
. .invFLITPSCREADl	FLITPSCweak	pf	FLITPSCAction → L with λ a. ∃ tid, l. a = invFLITPSCREAD(tid, l)
. .invFLITPSCWRITEl	FLITPSCweak	pf	FLITPSCAction → L with λ a. ∃ tid, l, v. a = invFLITPSCWRITE(tid, l, v)
. .invFLITPSCWRITEv	FLITPSCweak	pf	FLITPSCAction → V with λ a. ∃ tid, l, v. a = invFLITPSCWRITE(tid, l, v)
. .invPSCPERSIST_FOl	FLITPSCweak	pf	FLITPSCAction → L with λ a. ∃ l. a = globalPSCPERSIST_FO(l)
. .invPSCPERSIST_Wl	FLITPSCweak	pf	FLITPSCAction → L with λ a. ∃ l. a = globalPSCPERSIST_W(l)
. .l	FLITPSCweak	f	FLITPSCLState → L
. .l	FLITPSCweak	pf	FLITPSCAction → L with λ a. (∃ tid, l. a = pwbPSC(tid, l)) ∨ (∃ tid, l, v. a = doWritePSC(tid, l, v)) ∨ (∃ tid, l, v. a = doReadPSC(tid, l, v)) ∨ (∃ tid, l, n. a = ctrReadPSC(tid, l, n)) ∨ (∃ tid, l. a = ctrIncPSC(tid, l)) ∨ (∃ tid, l. a = ctrDecPSC(tid, l))
. .l:= .	FLITPSCweak	f	FLITPSCLState × L → FLITPSCLState
. .last	list-last	pf	List('a) → 'a with λ x. x ≠ []
. .lsf	FLITPSCweak	f	FLITPSCState → T → FLITPSCLState
. .lsf:= .	FLITPSCweak	f	FLITPSCState × (T → FLITPSCLState) → FLITPSCState
. .map ( . )	list	f	List('a) × ('a → 'b) → List('b)
. .map ( . )	set-union	f	Set('a) × ('a → 'b) → Set('b)
. .mem	FLITPSCweak	f	FLITPSCGState → L → V
. .mem:= .	FLITPSCweak	f	FLITPSCGState × (L → V) → FLITPSCGState
. .n	FLITPSCweak	pf	FLITPSCAction → Nat with λ a. ∃ tid, l, n. a = ctrReadPSC(tid, l, n)
. .p	FLITPSCweak	f	FLITPSCGState → L → List(FOW)
. .p:= .	FLITPSCweak	f	FLITPSCGState × (L → List(FOW)) → FLITPSCGState
. .pcf	FLITPSCweak	f	FLITPSCState → T → FLITPSCPC
. .pcf:= .	FLITPSCweak	f	FLITPSCState × (T → FLITPSCPC) → FLITPSCState
. .readers	FLITPSCweak	f	FLITPSCGState → L → Set(T)
. .readers:= .	FLITPSCweak	f	FLITPSCGState × (L → Set(T)) → FLITPSCGState
. .retFLITPSCREADv	FLITPSCweak	pf	FLITPSCAction → V with λ a. ∃ tid, v. a = retFLITPSCREAD(tid, v)
. .sublist ( . )	list-del	pf	List('a) × Nat × Nat → List('a) with λ x, n, m. n + m ≤ # x
. .t	FLITPSCweak	f	FLITPSCLState → T
. .t	FLITPSCweak	pf	FLITPSCAction → T with λ a. (∃ tid. a = retFLITPSCWRITE(tid)) ∨ (∃ tid, v. a = retFLITPSCREAD(tid, v)) ∨ (∃ tid, l, v. a = invFLITPSCWRITE(tid, l, v)) ∨ (∃ tid, l. a = invFLITPSCREAD(tid, l)) ∨ (∃ tid. a = callPSCRUN(tid)) ∨ (∃ tid. a = callPSCCOMPLETE(tid))
. .t:= .	FLITPSCweak	f	FLITPSCLState × T → FLITPSCLState
. .tail	list-data	pf	List('a) → List('a) with λ x. x ≠ []
. .take ( . )	list-del	pf	List('a) × Nat → List('a) with λ x, n. n ≤ # x
. .takeRight ( . )	list-del	pf	List('a) × Nat → List('a) with λ x, n. n ≤ # x
. .tid	FOW	f	FOW → T
. .tid	FLITPSCweak	pf	FLITPSCAction → T with λ a. (∃ tid. a = sfencePSC(tid)) ∨ (∃ tid, l. a = pwbPSC(tid, l)) ∨ (∃ tid, l, v. a = doWritePSC(tid, l, v)) ∨ (∃ tid, l, v. a = doReadPSC(tid, l, v)) ∨ (∃ tid, l, n. a = ctrReadPSC(tid, l, n)) ∨ (∃ tid, l. a = ctrIncPSC(tid, l)) ∨ (∃ tid, l. a = ctrDecPSC(tid, l))
. .v	FLITPSCweak	f	FLITPSCLState → V
. .v	FLITPSCweak	pf	FLITPSCAction → V with λ a. (∃ tid, l, v. a = doWritePSC(tid, l, v)) ∨ (∃ tid, l, v. a = doReadPSC(tid, l, v))
. .v:= .	FLITPSCweak	f	FLITPSCLState × V → FLITPSCLState
. .val	FOW	pf	FOW → V with λ fow. fow.W?
. .writers	FLITPSCweak	f	FLITPSCGState → L → Set(T)
. .writers:= .	FLITPSCweak	f	FLITPSCGState × (L → Set(T)) → FLITPSCGState
. < .	nat-basic	p	Nat × Nat
. < .	list-data	p	List('a) × List('a)
. > .	nat	p	Nat × Nat
. [ . := . ]	list-getput	pf	List('a) × Nat × 'a → List('a) with λ x, n, a. n < # x
. [ . ]	list-getput	pf	List('a) × Nat → 'a with λ x, n. n < # x
. \ .	list-set	f	List('a) × List('a) → List('a)
. \ .	set-union	f	Set('a) × Set('a) → Set('a)
. \| .	FLITPSC-preds	f	List(FOW) × T → List(FOW)
. \|FO	FLITPSC-preds	f	List(FOW) → List(FOW)
. \|W	FLITPSC-preds	f	List(FOW) → List(FOW)
. ∈ .	list	p	'a × List('a)
. ∈ .	set-basic	p	'a × Set('a)
. ∩ .	set-union	f	Set('a) × Set('a) → Set('a)
. ∪ .	list-set	f	List('a) × List('a) → List('a)
. ∪ .	set-union	f	Set('a) × Set('a) → Set('a)
. ≤ .	nat	p	Nat × Nat
. ≥ .	nat	p	Nat × Nat
. ⊆ .	list-set	p	List('a) × List('a)
. ⊆ .	set-basic	p	Set('a) × Set('a)
. ⊆m .	list-perm	p	List('a) × List('a)
. ⊑ .	list-last	p	List('a) × List('a)
. ⊒ .	list-last	p	List('a) × List('a)
. ⊒W .	FLITPSCweak-preds	p	List(FOW) × List(FOW)
. ⊕ .	FLITPSC-preds	f	V × List(FOW) → V
. ⊕ .	FLITPSC-preds	f	(L → V) × (L → List(FOW)) → L → V
. intersect .	list-set	f	List('a) × List('a) → List('a)
. zip .	filter-count	f	List('a) × List('b) → List(('a, 'b))
[]	list-data	c	List('a)
{ . }	set-union	f	'a → Set('a)
τ	FLITPSCweak	c	FLITPSCAction
∅	set-basic	c	Set('a)
∅	memory	f	L → V
FLITPSCAction	FLITPSCweak	s
FLITPSCGInv	FLITPSCweak	p	FLITPSCGState
FLITPSCGState	FLITPSCweak	s
FLITPSCInv	FLITPSCweak	p	FLITPSCGState × (T → Type(FLITPSCLState)) × (T → Type(FLITPSCPC))
FLITPSCLInv	FLITPSCweak	p	FLITPSCGState × FLITPSCLState × FLITPSCPC
FLITPSCLState	FLITPSCweak	s
FLITPSCPC	FLITPSCweak	s
FLITPSCREAD	FLITPSCweak	pr	L × T × (L → V) × (L → Nat) : (L → List(FOW)) × (L → Set(T)) : V
FLITPSCRely	FLITPSCweak	p	FLITPSCGState × T × FLITPSCGState
FLITPSCState	FLITPSCweak	s
FLITPSCWRITE	FLITPSCweak	pr	L × V × T : (L → List(FOW)) × (L → Nat) × (L → Set(T))
FO	FOW	f	T → FOW
FOFollowsW	FLITPSC-preds	p	T × List(FOW)
FOW	FOW	s
L	memory	s
List	list-data	s
Nat	nat-basic	s
O	memory	c	V
PSCCOMPLETE	FLITPSCweak	pr	T × (L → List(FOW)) :
PSCCRASH	FLITPSCweak	pr	: (L → List(FOW)) × (L → Nat) × (L → Set(T)) × (L → Set(T)) × (T → FLITPSCPC)
PSCPERSIST_FO	FLITPSCweak	pr	L : (L → List(FOW)) (nondeterministic)
PSCPERSIST_W	FLITPSCweak	pr	L : (L → V) × (L → List(FOW))
PSCRUN	FLITPSCweak	pr	:
R1	FLITPSCweak	c	FLITPSCPC
R2	FLITPSCweak	c	FLITPSCPC
R3	FLITPSCweak	c	FLITPSCPC
R4	FLITPSCweak	c	FLITPSCPC
Set	set-basic	s
T	memory	s
V	memory	s
W	FOW	f	V × T → FOW
W1	FLITPSCweak	c	FLITPSCPC
W2	FLITPSCweak	c	FLITPSCPC
W3	FLITPSCweak	c	FLITPSCPC
W4	FLITPSCweak	c	FLITPSCPC
W5	FLITPSCweak	c	FLITPSCPC
W6	FLITPSCweak	c	FLITPSCPC
W7	FLITPSCweak	c	FLITPSCPC
a	FLITPSCweak	v	FLITPSCAction
atomicW1	FLITPSCweak	c	FLITPSCAction
atomicW5	FLITPSCweak	c	FLITPSCAction
callPSCCOMPLETE	FLITPSCweak	f	T → FLITPSCAction
callPSCRUN	FLITPSCweak	f	T → FLITPSCAction
crashed	FLITPSCweak	c	FLITPSCPC
ctr	FLITPSCweak	v	L → Nat
ctrDecPSC	FLITPSCweak	f	T × L → FLITPSCAction
ctrIncPSC	FLITPSCweak	f	T × L → FLITPSCAction
ctrReadPSC	FLITPSCweak	f	T × L × Nat → FLITPSCAction
ctrok	FLITPSC-preds	p	(L → Type(Nat)) × (L → Type(Set(T)))
disj	list-dup	p	List('a) × List('a)
disjoint	set-union	p	Set('a) × Set('a)
doReadPSC	FLITPSCweak	f	T × L × V → FLITPSCAction
doWritePSC	FLITPSCweak	f	T × L × V → FLITPSCAction
dups	list-dup	p	List('a)
fillfirst	list-last	f	Nat × 'a × List('a) → List('a)
firstPersistW	FLITPSCweak-preds	f	List(FOW) → Nat
flitpscInit	FLITPSCweak	p	FLITPSCState
flitpscStep	FLITPSCweak	p	FLITPSCState × FLITPSCAction × FLITPSCState
fow	FLITPSCweak	v	FOW
fowl	FLITPSCweak	v	List(FOW)
frome	list-del	f	List('a) × 'a → List('a)
glb	FLITPSCweak	v	Nat
globalPSCCRASH	FLITPSCweak	c	FLITPSCAction
globalPSCPERSIST_FO	FLITPSCweak	f	L → FLITPSCAction
globalPSCPERSIST_W	FLITPSCweak	f	L → FLITPSCAction
gs	FLITPSCweak	v	FLITPSCGState
gstate	FLITPSCweak	v	FLITPSCGState
gstepf	FLITPSCweak	f	FLITPSCGState × FLITPSCLState × FLITPSCPC × FLITPSCAction → FLITPSCGState
idle	FLITPSCweak	c	FLITPSCPC
invFLITPSCREAD	FLITPSCweak	f	T × L → FLITPSCAction
invFLITPSCREADl	FLITPSCweak	v	L
invFLITPSCWRITE	FLITPSCweak	f	T × L × V → FLITPSCAction
invFLITPSCWRITEl	FLITPSCweak	v	L
invFLITPSCWRITEv	FLITPSCweak	v	V
invPSCPERSIST_FOl	FLITPSCweak	v	L
invPSCPERSIST_Wl	FLITPSCweak	v	L
isPersistFO	FLITPSCweak-preds	p	Nat × List(FOW)
l	FLITPSCweak	v	L
loc	FLITPSCweak	v	Nat
ls	FLITPSCweak	v	FLITPSCLState
lsf	FLITPSCweak	v	T → FLITPSCLState
lstep	FLITPSCweak	p	FLITPSCGState × FLITPSCLState × FLITPSCPC × FLITPSCAction × FLITPSCGState × FLITPSCLState × FLITPSCPC
lstepf	FLITPSCweak	f	FLITPSCGState × FLITPSCLState × FLITPSCPC × FLITPSCAction → FLITPSCLState
mem	FLITPSCweak	v	L → V
mkFLITPSCgs	FLITPSCweak	f	(L → V) × (L → List(FOW)) × (L → Nat) × (L → Set(T)) × (L → Set(T)) → FLITPSCGState
mkFLITPSCls	FLITPSCweak	f	T × L × V → FLITPSCLState
mklist	list-last	f	'a × Nat → List('a)
mkstate	FLITPSCweak	f	FLITPSCGState × (T → FLITPSCLState) × (T → FLITPSCPC) → FLITPSCState
n	FLITPSCweak	v	Nat
noPending	FLITPSC-preds	p	T × (L → Type(List(FOW)))
noPendingW	FLITPSC-preds	p	T × (L → Type(List(FOW)))
notMember	FLITPSC-preds	p	T × (L → Type(Set(T)))
oneMember	FLITPSC-preds	p	T × L × (L → Type(Set(T)))
onePendingW	FLITPSC-preds	p	T × L × (L → Type(List(FOW)))
p	FLITPSCweak	v	L → List(FOW)
pc	FLITPSCweak	v	FLITPSCPC
pcf	FLITPSCweak	v	T → FLITPSCPC
pcstepf	FLITPSCweak	f	FLITPSCGState × FLITPSCLState × FLITPSCPC × FLITPSCAction → FLITPSCPC
pendingOk	FLITPSC-preds	p	(L → Type(List(FOW)))
perm	list-perm	p	List('a) × List('a)
plin	FLITPSCweak	v	L → List(FOW)
pre	FLITPSCweak	p	FLITPSCGState × FLITPSCLState × FLITPSCPC × FLITPSCAction
pwbPSC	FLITPSCweak	f	T × L → FLITPSCAction
readers	FLITPSCweak	v	L → Set(T)
ready	FLITPSCweak	c	FLITPSCPC
rely	FLITPSCweak-preds	p	T × List(FOW) × List(FOW)
rely	FLITPSCweak-preds	p	T × (L → Type(List(FOW))) × (L → Type(List(FOW)))
relyp	FLITPSC-preds	p	T × List(FOW) × List(FOW)
relyp	FLITPSC-preds	p	T × (L → Type(List(FOW))) × (L → Type(List(FOW)))
relyws	FLITPSC-preds	p	T × (L → Type(Set(T))) × (L → Type(Set(T)))
relyws	FLITPSC-preds	p	T × Set(T) × Set(T)
retFLITPSCREAD	FLITPSCweak	f	T × V → FLITPSCAction
retFLITPSCREADv	FLITPSCweak	v	V
retFLITPSCWRITE	FLITPSCweak	f	T → FLITPSCAction
rev	list-last	f	List('a) → List('a)
s	FLITPSCweak	v	FLITPSCState
sfencePSC	FLITPSCweak	f	T → FLITPSCAction
t	FLITPSCweak	v	T
tid	FLITPSCweak	v	T
ts	FLITPSCweak	v	Set(T)
v	FLITPSCweak	v	V
wl	FLITPSCweak	v	L
writers	FLITPSCweak	v	L → Set(T)
writersOk	FLITPSC-preds	p	(L → Type(List(FOW))) × (L → Type(Set(T)))