Occurrence-based Precondition Axioms

Grammar Name: occ_precond.bnf

Extension Name: occ_precond.def

Grammars required by Process Descriptions: None

Process Descriptions

< occ_constrained_precond > ::=   
(forall (?s)
        ({if | iff} (and   (occurrence ?s < term >)
                                (legal ?s)
				(ubiquitous < term > < term >))
                         {< leaf_constrained_axiom > | < inner_constrained_axiom}))

Auxiliary Rules

< leaf_constrained_formula > ::=  (exists (?occ ?s1)
					(and	(occurrence ?occ < term >)
						(leaf_occ ?s1 ?occ)
						(= ?s (successor < term > ?s1))))

< leaf_constrained_axiom > ::=	< leaf_constrained_formula > |
				(not < leaf_constrained_formula >)

< inner_constrained_formula > ::=  (exists (?occ ?s1 ?s2)
					(and	(occurrence ?occ < term >)
						(subactivity_occurrence ?s1 ?occ)
						(subactivity_occurrence ?s2 ?occ)
						(precedes ?s1 ?s)
						(precedes ?s ?s2)))

< inner_constrained_axiom > ::=	< inner_constrained_formula > |
				(not < inner_constrained_formula >)