mb
automata
2
Sections
GenAutomata
Doc
Def
t.smt == 2of(2of(2of(t)))
is mentioned by
Def
action_effect(a;es;fs) == < e.smt | e
< e
es |
e.kind =
a > > + < mk_smt(f.var, f.var, f.typ) | f
< f
fs |
a
f.acts > >
[action_effect]
Def
covers_var(A;x) ==
fr:frame(). fr
< fr
A.frame |
fr.var =
x > & (
a:Label. (a
fr.acts)
(
ef:eff(). ef
< ef
A.eff |
ef.kind =
a &
ef.smt.lbl =
x > ))
[covers_var]
Try larger context:
GenAutomata
mb
automata
2
Sections
GenAutomata
Doc