mb
hybrid
Sections
GenAutomata
Doc
Def
switchable0(E)(P) == safetyR(E) preserves P & memorylessR(E) preserves P & (ternary) composableR(E) preserves P & send-enabledR(E) preserves P & asyncR(E) preserves P & delayableR(E) preserves P
is mentioned by
Thm*
E:EventStruct, P:TraceProperty(E). switchable0(E)(P)
switchable(E)(P
Causal(E)
No-dup-deliver(E))
[switchable0_switchable]
Thm*
E:EventStruct. switchable0(E)(totalorder(E))
[totalorder_switchable0]
Thm*
E:EventStruct. switchable0(E)(No-dup-deliver(E))
[P_no_dup_switchable0]
Thm*
E:EventStruct. switchable0(E)(Causal(E))
[P_causal_switchable0]
Thm*
E:EventStruct, P:((Label
(|E| List))
Prop). (
f,g:(Label
(|E| List)). (
p:Label. g(p)
f(p))
P(f)
P(g))
(
f,g:(Label
(|E| List)). (
a:|E|.
p:Label. g(p) = filter(
b.
(b =msg=(E) a);f(p)))
P(f)
P(g))
(
f,g,h:(Label
(|E| List)). (
p,q:Label. (
x
f(p).(
y
g(q).
(x =msg=(E) y))))
(
p:Label. h(p) = ((f(p)) @ (g(p))))
P(f)
P(g)
P(h))
switchable0(E)(local_deliver_property(E;P))
[local_deliver_switchable]
Try larger context:
GenAutomata
mb
hybrid
Sections
GenAutomata
Doc