State-based Precondition Axioms

Grammar Name: state_precond.bnf

Extension Name: state_precond.def

Grammars required by Process Descriptions: None

Process Descriptions

< simple_state_precond > ::=	(forall (?s) 
					(if	 (and	(occurrence ?s )
							(legal ?s))
						 < simple_state_axiom >))) |
				(forall (?s)
					(if	  (and	(legal ?s)
							< simple_state_axiom >)
						  (legal (successor < term > ?s))))

< state_precond > ::=		(forall (< variable >*) 
					(if	  (and	(occurrence < variable > < term >)
							(legal < term >))
						  < state_axiom >))) |
				(forall (< variable >*)
					(if	  (and	(legal < term >)
							< state_axiom >)
						  (legal (successor < term > < term >))))

Auxiliary Rules

< simple_state_literal > ::= 	(prior < term  > ?s)

< simple_state_formula > ::=	< simple_state_literal > |
				(not < simple_state_formula >) |
				({and | or} < simple_state_formula >*) | 
				({if | iff} < simple_state_formula >) 

< simple_state_axiom > ::=	({forall | exists} < variable >*) 
					< simple_state_formula >)

< state_literal > ::=		(prior < term > < variable >)

< state_formula > ::=		< state_literal > |
				(not < state_formula >) |
				({and | or} < state_formula >) | 
				({if | iff} < state_formula >*) 

< state_axiom > ::=		(forall (< variable >+) < state_formula >)