data specification
using memory
data types
Bevent = W(. .l : L;. .v : V) with .W?
| FO(. .l : L) with .FO?
| SF
;
variables
be : Bevent;
l : L;
v : V;
end data specification