State-based Effect Axioms

Grammar Name: state_effects.bnf

Extension Name: state_effects.def

Grammars required by Process Descriptions: state_precond.bnf

Process Descriptions

(markov_effects ?a)

< simple_state_effect > ::=	(forall (?s) 
					(if	 (and	(occurrence ?s )
							< simple_state_axiom >)
						 < simple_holds_axiom >)))

(partial_state_effects ?a)

< state_effect > ::=		(forall (< variable >*) 
					(if	  (and	(occurrence < variable > < term >)
							< state_axiom >)
						  < simple_holds_axiom >)))