Time-based Precondition Axioms

Grammar Name: time_precond.bnf

Extension Name: time_precond.def

Grammars required by Process Descriptions: None

Process Descriptions

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

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

Auxiliary Rules

< simple_time_literal > ::=	(= (beginof ?s) < term >)

< simple_time_formula > ::=	(and < simple_time_literal >*) 

< simple_time_axiom > ::=	({forall | exists} < variable >*) < simple_time_formula >)

< ordered_time_literal > ::=	< simple_time_literal > |
				(before (beginof ?s) < term >) |
				(before < term > (beginof ?s)) 

< time_formula > ::=		< ordered_time_literal > |
				(not < time_formula >) |
				({and | or} < time_formula >*) | 
				({if | iff} < time_formula >) 

< time_axiom > ::=		({forall | exists} < variable >*) < time_formula >)