[Imprint][Data Privacy Statement][E-Mail]

Back to the index. View project statistic. View project symbols. View KIV symbols to check that all symbols are available.

All project symbols

symbol	specification	entry
#	gen-secdomain-set	function, secdomainset → nat
#	gen-names	function, names → nat
#	gen-command-list	function, commandlist → nat
#	trace	function, trace → nat
#	store	function, store → nat
#	list-data	function, list → nat
#	set-basic	function, set → nat
#oc	trace	function, event × trace → nat
#oc	list-perm	function, elem × list → nat
'	gen-command-list	function, command → commandlist
'	trace	function, event → trace
'	list	function, elem → list
+	gen-command-list	function, command × commandlist → commandlist
+	gen-command-list	function, commandlist × commandlist → commandlist
+	gen-command-list	function, commandlist × command → commandlist
+	gen-command-list	function, command × command → commandlist
+	trace	function, event × trace → trace
+	trace	function, trace × trace → trace
+	trace	function, trace × event → trace
+	trace	function, event × event → trace
+	list	function, list × list → list
+	list	function, list × elem → list
+	list	function, elem × elem → list
+	list-data	function, elem × list → list
+	nat-basic2	function, nat × nat → nat
++	gen-secdomain-set	function, secdomainset × secdomain → secdomainset
++	gen-names	function, names × name → names
++	gen-command-list	function, commandlist × command → commandlist
++	trace	function, trace × event → trace
++	list-dup	function, list × elem → list
++	set-basic	function, set × elem → set
+1	nat-basic1	function, nat → nat
-	nat	function, nat × nat → nat
--	gen-secdomain-set	function, secdomainset × secdomain → secdomainset
--	gen-names	function, names × name → names
--	store	function, store × elem → store
--	set-union	function, set × elem → set
-1	nat-basic1	function, nat → nat
-1l	trace	function, trace × event → trace
-1l	trace	function, trace × nat → trace
-1l	list-del	function, list × elem → list
-1l	list-del	function, list × nat → list
-l	trace	function, trace × event → trace
-l	list-del	function, list × elem → list
.1	gen-sys-out	function, systemstateandoutput → systemstate
.1	pair	function, pair → elem
.2	gen-sys-out	function, systemstateandoutput → output
.2	pair	function, pair → data
.butlast	gen-command-list	function, commandlist → commandlist
.butlast	trace	function, trace → trace
.butlast	list-last	function, list → list
.er	xview	function, xview → event × event → bool
.first	gen-command-list	function, commandlist → command
.first	trace	function, trace → event
.first	list-data	function, list → elem
.last	gen-command-list	function, commandlist → command
.last	trace	function, trace → event
.last	list-last	function, list → elem
.rest	gen-command-list	function, commandlist → commandlist
.rest	trace	function, trace → trace
.rest	list-data	function, list → list
.view	xview	function, xview → event → viewstate
<	gen-command-list	predicate, commandlist × commandlist
<	trace	predicate, trace × trace
<	list-data	predicate, list × list
<	nat-basic1	predicate, nat × nat
<	oelem	predicate, elem × elem
>	nat	predicate, nat × nat
BSP_BSD	BSPs	predicate, event → viewstate × state × event × state → bool
BSP_BSD	MAKS-BSD	constant, bool
BSP_BSRA	BSPs	predicate, xview × state × event × state → bool
BSP_BSRA	MAKS-BSRA	constant, bool
BSP_D	BSPs	predicate, event → viewstate × state × event × state → bool
BSP_RA	BSPs	predicate, xview × state × event × state → bool
BSP_SD	BSPs	predicate, event → viewstate × state × event × state → bool
BSP_SR	BSPs	predicate, event → viewstate × state × event × state → bool
C	view	constant, viewstate
Cview	eventfunsHO	function, event → viewstate → event → bool
Cview	eventfuns	function, event → viewstate → event → bool
N	view	constant, viewstate
N2Vview	eventfunsHO	function, event → viewstate → event → viewstate
Nview	eventfunsHO	function, event → viewstate → event → bool
Nview	eventfuns	function, event → viewstate → event → bool
S0	state	constant, state
V	view	constant, viewstate
VCview	eventfunsHO	function, event → viewstate → event → bool
VCview	eventfuns	function, event → viewstate → event → bool
VNview	eventfunsHO	function, event → viewstate → event → bool
VNview	eventfuns	function, event → viewstate → event → bool
Vview	eventfunsHO	function, event → viewstate → event → bool
Vview	eventfuns	function, event → viewstate → event → bool
[]	gen-command-list	constant, commandlist
[]	trace	constant, trace
[]	list-data	constant, list
\	gen-secdomain-set	function, secdomainset × secdomainset → secdomainset
\	gen-names	function, names × names → names
\	trace	function, trace × trace → trace
\	list-set	function, list × list → list
\	set-union	function, set × set → set
]	trace	function, trace × nat → event
]	trace	function, trace × nat × event → trace
]	store	function, store × elem × data → store
]	store	function, store × elem → data
]	list-del	function, list × nat → elem
]	list-del	function, list × nat × elem → list
a	elem	variable, elem
a0	pair	variable, elem
a0	store	variable, elem
a0	list-data	variable, elem
adm	eventfunsHO	variable, event → bool
alter	AccessControl	predicate, name × secdomain
alter	gen-RMAIntrans	function, secdomain → names
alter	gen-RMATrans	function, secdomain → names
alter	AccessControl4Vars	predicate, name × secdomain
alter	AccessControlWithState	predicate, name × secdomain
b	elem	variable, elem
butlastn	gen-command-list	function, nat × commandlist → commandlist
butlastn	trace	function, nat × trace → trace
butlastn	list-last	function, nat × list → list
c	elem	variable, elem
cdom	AccessControl	function, command → secdomain
cdom	gen-execute	function, systemstate × command → secdomain
cdom	gen-execute	function, command → secdomain
cdom	LanguageBasedNIFTrans	function, name → secdomain
cdom	AccessControl4Vars	function, name → secdomain
cdom	AccessControl4Vars	function, command → secdomain
cdom	AccessControlWithState	function, command → secdomain
cdom	LanguageBasedNIFIntrans	function, name → secdomain
cl	gen-command-list	variable, commandlist
cl0	gen-command-list	variable, commandlist
cl1	gen-command-list	variable, commandlist
cl10	gen-command-list	variable, commandlist
cl2	gen-command-list	variable, commandlist
cl3	gen-command-list	variable, commandlist
cl4	gen-command-list	variable, commandlist
cl5	gen-command-list	variable, commandlist
cl6	gen-command-list	variable, commandlist
cl7	gen-command-list	variable, commandlist
cl8	gen-command-list	variable, commandlist
cl9	gen-command-list	variable, commandlist
co	gen-commands	variable, command
co0	gen-command-list	variable, command
co1	gen-command-list	variable, command
co2	gen-command-list	variable, command
command	gen-commands	sort,
commandlist	gen-command-list	sort,
contents	AccessControl	function, systemstate × name → value
contents	gen-RMAIntrans	function, systemstate × name → value
contents	gen-RMATrans	function, systemstate × name → value
contents	AccessControl4Vars	function, systemstate × name → value
contents	AccessControlWithState	function, systemstate × name → value
d	gen-secdomain	variable, secdomain
d	data	variable, data
d0	gen-secdomain	variable, secdomain
d0	data	variable, data
d1	gen-secdomain	variable, secdomain
d1	data	variable, data
d2	data	variable, data
data	data	sort,
disj	gen-command-list	predicate, commandlist × commandlist
disj	trace	predicate, trace × trace
disj	list-dup	predicate, list × list
ds	gen-secdomain-set	variable, secdomainset
ds0	gen-secdomain-set	variable, secdomainset
ds1	gen-secdomain-set	variable, secdomainset
ds2	gen-secdomain-set	variable, secdomainset
dups	gen-command-list	predicate, commandlist
dups	trace	predicate, trace
dups	list-dup	predicate, list
elem	elem	sort,
elemdata	store	sort,
elemdatavar	store	variable, elemdata
enabled	eventfunsHO	predicate, state × event × state → bool × state × trace
enabled	eventfuns	predicate, state × trace
eqS	AccessControlWithState	predicate, systemstate × systemstate
eqd	gen-CongTrans-wf	predicate, systemstate × secdomain × systemstate
eqd	AccessControl	predicate, systemstate × secdomain × systemstate
eqd	gen-CongTrans	predicate, systemstate × secdomain × systemstate
eqd	gen-RMAIntrans	predicate, systemstate × secdomain × systemstate
eqd	gen-RMATrans	predicate, systemstate × secdomain × systemstate
eqd	gen-CongIntrans	predicate, systemstate × secdomain × systemstate
eqd	AccessControl4Vars	predicate, systemstate × secdomain × systemstate
eqd	AccessControlWithState	predicate, systemstate × secdomain × systemstate
eqds	PurgeTransNoInitialstate	predicate, systemstate × secdomainset × systemstate
eqds	MeydenIntrans	predicate, systemstate × secdomainset × systemstate
eqds	PurgeTrans	predicate, systemstate × secdomainset × systemstate
eqds	PurgeIntrans	predicate, systemstate × secdomainset × systemstate
eqds	gen-RMAIntrans	predicate, systemstate × secdomainset × systemstate
eqds	MeydenTrans	predicate, systemstate × secdomainset × systemstate
eqds	Meyden4VarsTrans	predicate, systemstate × secdomainset × systemstate
eqds	MeydenIntransWithState	predicate, systemstate × secdomainset × systemstate
eqds	Meyden4VarsIntrans	predicate, systemstate × secdomainset × systemstate
eqlb	LanguageBasedNIFTrans	predicate, systemstate × secdomain × systemstate
eqlb	LanguageBasedNIFIntrans	predicate, systemstate × secdomain × systemstate
eqlbs	LanguageBasedNIFIntrans	predicate, systemstate × secdomainset × systemstate
eqrel	xview	variable, event × event → bool
eqrel	MAKS-BSRA-unwinding	predicate, event × event
eqrel0	xview	variable, event × event → bool
eqstate	unwinding	variable, state × state → bool
eqstate	MAKS-BSD-unwinding	predicate, state × state
eqstate	MAKS-BSRA-unwinding	predicate, state × state
ev	event	variable, event
ev0	event	variable, event
ev1	event	variable, event
ev2	event	variable, event
event	event	sort,
exec	gen-execute	function, systemstate × command → systemstateandoutput
execl	PurgeTrans	function, commandlist → systemstate
execl	PurgeIntrans	function, commandlist → systemstate
execl	gen-RMAIntrans	function, commandlist → systemstate
execl	gen-RMATrans	function, commandlist → systemstate
fillfirst	gen-command-list	function, nat × command × commandlist → commandlist
fillfirst	trace	function, nat × event × trace → trace
fillfirst	list-last	function, nat × elem × list → list
filter	trace	function, trace × trace → trace
filter	list-set	function, list × list → list
firstn	trace	function, nat × trace → trace
firstn	list-del	function, nat × list → list
frome	trace	function, trace × event → trace
frome	list-del	function, list × elem → list
inevs	eventfunsHO	variable, event → bool
inevs	eventfuns	variable, event → bool
initialstate	gen-systemstate	constant, systemstate
inv	gen-CongTrans-wf	predicate, systemstate
inv	gen-CongTrans	predicate, systemstate
inv	gen-CongIntrans	predicate, systemstate
ipurge	MeydenIntrans	function, commandlist × secdomain → commandlist
ipurge	gen-RMAIntrans	function, commandlist × secdomain → commandlist
ipurge	MeydenIntransWithState	function, commandlist × secdomain → commandlist
ipurge	Meyden4VarsIntrans	function, commandlist × secdomain → commandlist
ipurged	AccessControlWithState	function, command → command
isEqRel	unwinding	predicate, state × state → bool
isInput	eventfunsHO	predicate, event
isInput	eventfuns	predicate, event
isOutput	eventfunsHO	predicate, event
isOutput	eventfuns	predicate, event
isState	AccessControlWithState	predicate, name
isTransition	eventfunsHO	predicate, state × event × state → bool
lastn	trace	function, nat × trace → trace
lastn	list-del	function, nat × list → list
list	list-data	sort,
lrf	unwinding	predicate, event → viewstate × state × event × state → bool × state × state → bool
lrf	MAKS-BSD-unwinding	constant, bool
m	nat-basic2	variable, nat
mklist	gen-command-list	function, command × nat → commandlist
mklist	trace	function, event × nat → trace
mklist	list-last	function, elem × nat → list
mkxview	xview	function, event → viewstate × event × event → bool → xview
n	nat-basic1	variable, nat
n0	nat-basic1	variable, nat
n1	nat-basic1	variable, nat
nam	gen-name	variable, name
nam1	gen-names	variable, name
nam2	gen-names	variable, name
name	gen-name	sort,
names	gen-names	sort,
nams	gen-names	variable, names
nams0	gen-names	variable, names
nams1	gen-names	variable, names
nams2	gen-names	variable, names
nat	nat-basic1	sort,
null	gen-value	constant, value
obs	AccessControl	function, systemstate × secdomain → systemstate
obs	AccessControl4Vars	function, systemstate × secdomain → systemstate
obs	AccessControlWithState	function, systemstate × secdomain → systemstate
observe	AccessControl	predicate, name × secdomain
observe	gen-RMAIntrans	function, secdomain → names
observe	gen-RMATrans	function, secdomain → names
observe	AccessControl4Vars	predicate, name × secdomain
observe	AccessControlWithState	predicate, name × secdomain
osc	unwinding	predicate, event → viewstate × state × event × state → bool × state × state → bool
osc	MAKS-BSD-unwinding	constant, bool
out	gen-output	variable, output
out0	gen-sys-out	variable, output
out2	gen-sys-out	variable, output
out3	gen-sys-out	variable, output
output	gen-output	sort,
outputt	PurgeTransNoInitialstate	function, systemstate × command → output
outputt	PurgeTrans	function, systemstate × command → output
p	pair	variable, pair
p0	pair	variable, pair
p1	pair	variable, pair
p2	pair	variable, pair
pair	pair	sort,
perm	trace	predicate, trace × trace
perm	list-perm	predicate, list × list
pos	trace	function, event × trace → nat
pos	list-del	function, elem × list → nat
proj	eventfunsHO	function, trace × event → bool → trace
proj	eventfuns	function, trace × event → bool → trace
purge	PurgeTransNoInitialstate	function, commandlist × secdomain → commandlist
purge	PurgeTrans	function, commandlist × secdomain → commandlist
purge	PurgeIntrans	function, systemstate × commandlist × secdomain → commandlist
purge	gen-RMATrans	function, systemstate × commandlist × secdomain → commandlist
purge	MeydenTrans	function, commandlist × secdomain → commandlist
purge	Meyden4VarsTrans	function, commandlist × secdomain → commandlist
reachable	eventfunsHO	predicate, state × event × state → bool × state
reachable	eventfuns	predicate, state
restn	trace	function, nat × trace → trace
restn	list-del	function, nat × list → list
rev	gen-command-list	function, commandlist → commandlist
rev	trace	function, trace → trace
rev	list-last	function, list → list
rmdup	gen-command-list	function, commandlist → commandlist
rmdup	trace	function, trace → trace
rmdup	list-dup	function, list → list
run	PurgeTransNoInitialstate	function, systemstate × commandlist → systemstate
run	MeydenIntrans	function, systemstate × commandlist → systemstate
run	MeydenIntrans	function, commandlist → systemstate
run	PurgeTrans	function, systemstate × commandlist → systemstate
run	PurgeIntrans	function, systemstate × commandlist → systemstate
run	gen-RMAIntrans	function, systemstate × commandlist → systemstate
run	gen-RMATrans	function, systemstate × commandlist → systemstate
run	MeydenTrans	function, systemstate × commandlist → systemstate
run	MeydenTrans	function, commandlist → systemstate
run	Meyden4VarsTrans	function, systemstate × commandlist → systemstate
run	Meyden4VarsTrans	function, commandlist → systemstate
run	MeydenIntransWithState	function, systemstate × commandlist → systemstate
run	MeydenIntransWithState	function, commandlist → systemstate
run	Meyden4VarsIntrans	function, systemstate × commandlist → systemstate
run	Meyden4VarsIntrans	function, commandlist → systemstate
s	state	variable, state
s	set-basic	variable, set
s0	state	variable, state
s0	set-basic	variable, set
s1	state	variable, state
s1	set-basic	variable, set
s11	state	variable, state
s2	state	variable, state
s2	set-basic	variable, set
s22	state	variable, state
secdomain	gen-secdomain	sort,
secdomainset	gen-secdomain-set	sort,
secure	MeydenIntrans	predicate, systemstate
secure	MeydenTrans	predicate, systemstate
secure	Meyden4VarsTrans	predicate, systemstate
set	set-basic	sort,
so	gen-sys-out	variable, systemstateandoutput
so0	gen-sys-out	variable, systemstateandoutput
so1	gen-sys-out	variable, systemstateandoutput
so2	gen-sys-out	variable, systemstateandoutput
sources	MeydenIntrans	function, commandlist × secdomain → secdomainset
sources	PurgeIntrans	function, systemstate × commandlist × secdomain → secdomainset
sources	gen-RMAIntrans	function, commandlist × secdomain → secdomainset
sources	MeydenIntransWithState	function, commandlist × secdomain → secdomainset
sources	Meyden4VarsIntrans	function, commandlist × secdomain → secdomainset
st	store	variable, store
st0	store	variable, store
st1	store	variable, store
st2	store	variable, store
state	state	sort,
step	PurgeTransNoInitialstate	function, systemstate × command → systemstate
step	AccessControl	function, systemstate × command → systemstate
step	PurgeTrans	function, systemstate × command → systemstate
step	PurgeIntrans	function, systemstate × command → systemstate
step	gen-RMAIntrans	function, systemstate × command → systemstate
step	gen-RMATrans	function, systemstate × command → systemstate
step	AccessControl4Vars	function, systemstate × command → systemstate
step	AccessControlWithState	function, systemstate × command → systemstate
store	store	sort,
sublist	trace	function, nat × nat × trace → trace
sublist	list-del	function, nat × nat × list → list
sys	gen-systemstate	variable, systemstate
sys0	gen-systemstate	variable, systemstate
sys1	gen-systemstate	variable, systemstate
sys2	gen-sys-out	variable, systemstate
systemstate	gen-systemstate	sort,
systemstateandoutput	gen-sys-out	sort,
test	PurgeTransNoInitialstate	function, systemstate × commandlist × command → output
test	PurgeTrans	function, commandlist × command → output
test	PurgeIntrans	function, commandlist × command → output
test	gen-RMAIntrans	function, commandlist × command → output
test	gen-RMATrans	function, commandlist × command → output
tr	trace	variable, trace
tr0	trace	variable, trace
tr1	trace	variable, trace
tr10	trace	variable, trace
tr2	trace	variable, trace
tr3	trace	variable, trace
tr4	trace	variable, trace
tr5	trace	variable, trace
tr6	trace	variable, trace
tr7	trace	variable, trace
tr8	trace	variable, trace
tr9	trace	variable, trace
trace	trace	sort,
trans	eventfunsHO	variable, state × event × state → bool
trans	eventfuns	predicate, state × event × state
trans∃	eventfunsHO	predicate, state × event × state → bool × state × trace × state
trans∃	eventfuns	predicate, state × trace × state
usedName	AccessControl4Vars	predicate, name
v	gen-value	variable, value
v0	gen-value	variable, value
v1	gen-value	variable, value
validx	eventfunsHO	predicate, xview
validx	MAKS-BSRA-unwinding	constant, bool
value	gen-value	sort,
view	MAKS-BSD-unwinding	function, event → viewstate
view	xview	variable, event → viewstate
view	MAKS-BSRA-unwinding	function, event → viewstate
view0	xview	variable, event → viewstate
viewstate	view	sort,
viewvar	eventfuns	variable, event → viewstate
vstate	view	variable, viewstate
wf	gen-CongTrans-wf	predicate, command
wf	PurgeTransNoInitialstate	predicate, commandlist
x	list-data	variable, list
x0	list-data	variable, list
x1	list-data	variable, list
x2	list-data	variable, list
xlrf	unwinding	predicate, xview × state × event × state → bool × state × state → bool
xlrf	MAKS-BSRA-unwinding	constant, bool
xosc	unwinding	predicate, xview × state × event × state → bool × state × state → bool
xosc	MAKS-BSRA-unwinding	constant, bool
xview	xview	variable, xview
xview	xview	sort,
xview0	xview	variable, xview
xview1	xview	variable, xview
y	list-data	variable, list
y0	list-data	variable, list
y1	list-data	variable, list
y2	list-data	variable, list
z	list-data	variable, list
z0	list-data	variable, list
z1	list-data	variable, list
z2	list-data	variable, list
}	gen-secdomain-set	function, secdomain → secdomainset
}	gen-names	function, name → names
}	set-union	function, elem → set
≤	nat	predicate, nat × nat
≥	nat	predicate, nat × nat
∈	gen-secdomain-set	predicate, secdomain × secdomainset
∈	gen-names	predicate, name × names
∈	gen-command-list	predicate, command × commandlist
∈	trace	predicate, event × trace
∈	store	predicate, elem × store
∈	store	predicate, elemdata × store
∈	list	predicate, elem × list
∈	set-basic	predicate, elem × set
∈TR	eventfunsHO	predicate, trace × state × event × state → bool
∈TR	eventfuns	predicate, trace
∪	gen-secdomain-set	function, secdomainset × secdomainset → secdomainset
∪	gen-names	function, names × names → names
∪	trace	function, trace × trace → trace
∪	list-set	function, list × list → list
∪	set-union	function, set × set → set
∩	gen-secdomain-set	function, secdomainset × secdomainset → secdomainset
∩	gen-names	function, names × names → names
∩	set-union	function, set × set → set
⇒	gen-CongTrans-wf	predicate, secdomain × secdomain
⇒	AccessControl	predicate, secdomain × secdomain
⇒	gen-CongTrans	predicate, secdomain × secdomain
⇒	gen-RMAIntrans	predicate, secdomain × secdomain
⇒	gen-RMATrans	predicate, secdomain × secdomain
⇒	gen-CongIntrans	predicate, secdomain × secdomain
⇒	AccessControl4Vars	predicate, secdomain × secdomain
⇒	AccessControlWithState	predicate, secdomain × secdomain
⊆	gen-secdomain-set	predicate, secdomainset × secdomainset
⊆	gen-names	predicate, names × names
⊆	trace	predicate, trace × trace
⊆	store	predicate, store × store
⊆	list-set	predicate, list × list
⊆	set-basic	predicate, set × set
⊆m	trace	predicate, trace × trace
⊆m	list-perm	predicate, list × list
×	gen-sys-out	function, systemstate × output → systemstateandoutput
×	pair	function, elem × data → pair
×	store	function, elem × data → elemdata
⊑	gen-command-list	predicate, commandlist × commandlist
⊑	trace	predicate, trace × trace
⊑	list-last	predicate, list × list
⊒	gen-command-list	predicate, commandlist × commandlist
⊒	trace	predicate, trace × trace
⊒	list-last	predicate, list × list
∅	gen-secdomain-set	constant, secdomainset
∅	gen-names	constant, names
∅	store	constant, store
∅	set-basic	constant, set