[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-datafList('a) → Nat
#oclist-permf'a × List('a) → Nat
. 'listf'a → List('a)
. + .nat-basicfNat × Nat → Nat
. + .list-dataf'a × List('a) → List('a)
. + .listfList('a) × List('a) → List('a)
. + .listfList('a) × 'a → List('a)
. ++ .list-dupfList('a) × 'a → List('a)
. +1nat-basicfNat → Nat
. +2 .listf'a × 'a → List('a)
. - .natpfNat × Nat → Nat with λ n, m. n ≥ m
. -1nat-basicpfNat → Nat with λ n. n ≠ 0
. -1l .list-delfList('a) × 'a → List('a)
. -l .list-delfList('a) × 'a → List('a)
. -p .list-delfList('a) × Nat → List('a)
. .R?RWeventpRWevent
. .W?RWeventpRWevent
. .butlastlist-lastpfList('a) → List('a) with λ x. x ≠ []
. .count ( . )filter-countfList('a) × ('a → Bool) → Nat
. .count ( . )filter-countpfList('a) × Nat × Nat × ('a → Bool) → Nat with λ x, m, n, p. m ≤ n ∧ n ≤ # x
. .distinctlist-dupfList('a) → List('a)
. .drop ( . )list-delpfList('a) × Nat → List('a) with λ x, n. n ≤ # x
. .dropRight ( . )list-lastpfList('a) × Nat → List('a) with λ x, n. n ≤ # x
. .exists ( . )forall-indexWherepList('a) × ('a → Type(Bool))
. .filter ( . )filter-countfList('a) × ('a → Bool) → List('a)
. .foldLeft ( . )listfList('a) × 'b × ('b × 'a → 'b) → 'b
. .forall ( . )forall-indexWherepList('a) × ('a → Type(Bool))
. .gstatePLIBfPLIBState → PLIBGState
. .gstate:= .PLIBfPLIBState × PLIBGState → PLIBState
. .hPLIBfPLIBGState → List((RWevent, Bool))
. .h:= .PLIBfPLIBGState × List((RWevent, Bool)) → PLIBGState
. .headlist-datapfList('a) → 'a with λ x. x ≠ []
. .ilPLIBfPLIBLState → L
. .il:= .PLIBfPLIBLState × L → PLIBLState
. .indexOf ( . )list-delfList('a) × 'a → Nat
. .indexWhere ( . )forall-indexWherefList('a) × ('a → Bool) → Nat
. .invAPersistlPLIBpfPLIBAction → L with λ a. ∃ l. a = globalAPersist(l)
. .ivPLIBfPLIBLState → V
. .iv:= .PLIBfPLIBLState × V → PLIBLState
. .lRWeventfRWevent → L
. .lPLIBpfPLIBAction → L with λ a. ∃ t, l. a = AInvRead(t, l)
. .lastlist-lastpfList('a) → 'a with λ x. x ≠ []
. .lastPersistedOrElse ( . )PLIB-predspList((RWevent, Bool)) × L × Bool
. .locPLIBpfPLIBAction → L with λ a. ∃ t, l, v. a = AInvWrite(t, l, v)
. .lsfPLIBfPLIBState → T → PLIBLState
. .lsf:= .PLIBfPLIBState × (T → PLIBLState) → PLIBState
. .map ( . )listfList('a) × ('a → 'b) → List('b)
. .ovPLIBfPLIBLState → V
. .ov:= .PLIBfPLIBLState × V → PLIBLState
. .pcfPLIBfPLIBState → T → PLIBPC
. .pcf:= .PLIBfPLIBState × (T → PLIBPC) → PLIBState
. .pmPLIBfPLIBGState → L → V
. .pm:= .PLIBfPLIBGState × (L → V) → PLIBGState
. .sublist ( . )list-delpfList('a) × Nat × Nat → List('a) with λ x, n, m. n + m ≤ # x
. .tRWeventfRWevent → T
. .tPLIBfPLIBLState → T
. .tPLIBpfPLIBAction → T with λ a. (∃ t. a = callTSync(t)) ∨ (∃ t. a = callARun(t)) ∨ (∃ t. a = ARetWrite(t)) ∨ (∃ t, v. a = ARetRead(t, v)) ∨ (∃ t, l, v. a = AInvWrite(t, l, v)) ∨ (∃ t, l. a = AInvRead(t, l)) ∨ (∃ t. a = ADoWrite(t)) ∨ (∃ t. a = ADoRead(t))
. .t:= .PLIBfPLIBLState × T → PLIBLState
. .taillist-datapfList('a) → List('a) with λ x. x ≠ []
. .take ( . )list-delpfList('a) × Nat → List('a) with λ x, n. n ≤ # x
. .takeRight ( . )list-delpfList('a) × Nat → List('a) with λ x, n. n ≤ # x
. .vRWeventfRWevent → V
. .vPLIBpfPLIBAction → V with λ a. ∃ t, v. a = ARetRead(t, v)
. .valPLIBpfPLIBAction → V with λ a. ∃ t, l, v. a = AInvWrite(t, l, v)
. .vmPLIBfPLIBGState → L → V
. .vm:= .PLIBfPLIBGState × (L → V) → PLIBGState
. < .nat-basicpNat × Nat
. < .list-datapList('a) × List('a)
. > .natpNat × Nat
. [ . := . ]list-getputpfList('a) × Nat × 'a → List('a) with λ x, n, a. n < # x
. [ . ]list-getputpfList('a) × Nat → 'a with λ x, n. n < # x
. \ .list-setfList('a) × List('a) → List('a)
. | .PLIB-predsfList((RWevent, Bool)) × T → List((RWevent, Bool))
. | .PLIB-predsfList((RWevent, Bool)) × Bool → List((RWevent, Bool))
. | .PLIB-predsfList((RWevent, Bool)) × L → List((RWevent, Bool))
. |RPLIB-predsfList((RWevent, Bool)) → List((RWevent, Bool))
. |WPLIB-predsfList((RWevent, Bool)) → List((RWevent, Bool))
. ∈ .listp'a × List('a)
. ∪ .list-setfList('a) × List('a) → List('a)
. ≤ .natpNat × Nat
. ≥ .natpNat × Nat
. ⊆ .list-setpList('a) × List('a)
. ⊆m .list-permpList('a) × List('a)
. ⊑ .list-lastpList('a) × List('a)
. ⊑p .PLIB-predspList((RWevent, Bool)) × List((RWevent, Bool))
. ⊒ .list-lastpList('a) × List('a)
. ⊕ .PLIB-predsf(L → V) × List((RWevent, Bool)) → L → V
. intersect .list-setfList('a) × List('a) → List('a)
. zip .filter-countfList('a) × List('b) → List(('a, 'b))
[]list-datacList('a)
τPLIBcPLIBAction
∅memoryfL → V
ACrashPLIBpr(L → V) : (L → V) × List((RWevent, Bool)) × (T → PLIBPC)
ADOREADPLIBprT × L × (L → V) : V × List((RWevent, Bool))
ADoReadPLIBfT → PLIBAction
ADoWritePLIBfT → PLIBAction
AInvReadPLIBfT × L → PLIBAction
AInvWritePLIBfT × L × V → PLIBAction
APersistPLIBprL : (L → V) × List((RWevent, Bool))
ARETREADPLIBprV : : V
ARetReadPLIBfT × V → PLIBAction
ARetWritePLIBfT → PLIBAction
ARunPLIBpr :
DOWRITEPLIBprT × L × V : (L → V) × List((RWevent, Bool))
INVREADPLIBprL : L
INVWRITEPLIBprL × V : L × V
Lmemorys
Listlist-datas
Natnat-basics
OmemorycV
PLIBActionPLIBs
PLIBGInvPLIBpPLIBGState
PLIBGStatePLIBs
PLIBInvPLIBpPLIBGState × (T → Type(PLIBLState)) × (T → Type(PLIBPC))
PLIBLInvPLIBpPLIBGState × PLIBLState × PLIBPC
PLIBLStatePLIBs
PLIBPCPLIBs
PLIBRelyPLIBpPLIBGState × T × PLIBGState
PLIBStatePLIBs
RRWeventfT × L × V → RWevent
RETWRITEPLIBpr :
RWeventRWevents
Tmemorys
TSyncPLIBprT × List((RWevent, Bool)) :
Vmemorys
WRWeventfT × L × V → RWevent
aPLIBvPLIBAction
allReadsOKPLIB-predspList((RWevent, Bool))
allReadsOKIndPLIB-predsp(L → Type(V)) × (L → Type(Bool)) × List((RWevent, Bool))
allWritesOKPLIB-predspList((RWevent, Bool))
allWritesOKIndPLIB-predsp(T → Type(Bool)) × (L → Type(Bool)) × List((RWevent, Bool))
bPLIBvBool
callARunPLIBfT → PLIBAction
callTSyncPLIBfT → PLIBAction
crashedPLIBcPLIBPC
disjlist-duppList('a) × List('a)
dupslist-duppList('a)
ePLIBvRWevent
eventsPLIB-predsfList((RWevent, Bool)) → List(RWevent)
fillfirstlist-lastfNat × 'a × List('a) → List('a)
firstVolWritePLIB-predsfL × List((RWevent, Bool)) → Nat
fromelist-delfList('a) × 'a → List('a)
globalACrashPLIBcPLIBAction
globalAPersistPLIBfL → PLIBAction
gsPLIBvPLIBGState
gstatePLIBvPLIBGState
gstepfPLIBfPLIBGState × PLIBLState × PLIBPC × PLIBAction → PLIBGState
hPLIBvList((RWevent, Bool))
idlePLIBcPLIBPC
ilPLIBvL
invAPersistlPLIBvL
invReadPLIBcPLIBPC
invWritePLIBcPLIBPC
ivPLIBvV
lPLIBvL
locPLIBvL
lsPLIBvPLIBLState
lsfPLIBvT → PLIBLState
lstepPLIBpPLIBGState × PLIBLState × PLIBPC × PLIBAction × PLIBGState × PLIBLState × PLIBPC
lstepfPLIBfPLIBGState × PLIBLState × PLIBPC × PLIBAction → PLIBLState
mPLIBvNat
mkPLIBgsPLIBf(L → V) × (L → V) × List((RWevent, Bool)) → PLIBGState
mkPLIBlsPLIBfT × L × V × V → PLIBLState
mklistlist-lastf'a × Nat → List('a)
mkstatePLIBfPLIBGState × (T → PLIBLState) × (T → PLIBPC) → PLIBState
nPLIBvNat
ovPLIBvV
pcPLIBvPLIBPC
pcfPLIBvT → PLIBPC
pcstepfPLIBfPLIBGState × PLIBLState × PLIBPC × PLIBAction → PLIBPC
permlist-permpList('a) × List('a)
persistDependentReadsPLIB-predsfL × List((RWevent, Bool)) → List((RWevent, Bool))
plibInitPLIBpPLIBState
plibStepPLIBpPLIBState × PLIBAction × PLIBState
pmPLIBvL → V
prePLIBpPLIBGState × PLIBLState × PLIBPC × PLIBAction
readyPLIBcPLIBPC
relyPLIB-predspT × List((RWevent, Bool)) × List((RWevent, Bool))
resReadPLIBcPLIBPC
resWritePLIBcPLIBPC
revlist-lastfList('a) → List('a)
sPLIBvPLIBState
tPLIBvT
tidPLIBvT
vPLIBvV
valPLIBvV
vmPLIBvL → V
vpePLIBv(RWevent, Bool)