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_delay_axiom > | < inner_delay_axiom}))

Auxiliary Rules

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

< leaf_delay_axiom > ::=	< leaf_delay_formula > |
				(not < leaf_delay_formula >)

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

< inner_delay_axiom > ::=	< inner_delay_formula > |
				(not < inner_delay_formula >)