
Grammar Name: preventable.bnf
Extension Name: preventable.def
Grammars required by Process Descriptions: occ_precond.bnf, state_precond.bnf

< preventable_precond > ::=
(forall (?s)
({if | iff} (and (occurrence ?s < term >)
(legal ?s)
(ubiquitous < term > < term >)
< simple_state_axiom >)
{< leaf_constrained_axiom > | < inner_constrained_axiom}))
(possibly_preventable ?a)
< possibly_preventable_precond > ::=
(forall (?s)
({if | iff} (and (occurrence ?s < term >)
(legal ?s)
(ubiquitous < term > < term >)
< state_axiom >)
{< leaf_constrained_axiom > | < inner_constrained_axiom}))