Variation of Interfering Preconditions

Variation of Interfering Preconditions

Extension Name: var_interfere.def

Primitive Lexicon: None

Defined Lexicon:

Relations:

Theories Required by this Extension: atomic.th, disc_state.th, occtree.th, psl_core.th

Definitional Extensions Required by this Extension: interfere.def, state_precond.def, time_precond.def

Grammar:

Definitions

Definition 1 
(forall (?a) (iff (state_interfere ?a)
(forall (?a1 ?s1 ?s2)
        (if	  (and	(atomic ?a1)
			(state_equiv ?s1 ?s2))
		  (iff	(preserved_filter ?a1 ?a ?s1)
			(preserved_filter ?a1 ?a ?s2))))))
Definition 2 
(forall (?a) (iff (partial_interfere ?a)
(and 	(exists (?s1 ?a1) 
		(forall (?s2)
			(if	  (and	(atomic ?a1)
					(state_equiv ?s1 ?s2))
		  		  (iff	(preserved_filter ?a1 ?a ?s1)
					(preserved_filter ?a1 ?a ?s2)))))
	(exists (?a2 ?s3 ?s4)
		(and	(atomic ?a2)
			(state_equiv ?s3 ?s4)
			(preserved_filter ?a2 ?a ?s3)
			(not (preserved_filter ?a2 ?a ?s4)))))))
Definition 3 
(forall (?a) (iff (unconditional_interfere ?a)
(forall (?s1)
	(exists (?a1 ?s2)
		(and	(atomic ?a1)
			(state_equiv ?s1 ?s2)
		  	(iff	(preserved_filter ?a1 ?a ?s1)
				(not (preserved_filter ?a1 ?a ?s2))))))))
Definition 4 
(forall (?a) (iff (time_interfere ?a)
(forall (?a1 ?s1 ?s2)
        (if	  (and	(atomic ?a1)
			(begin_equiv ?s1 ?s2))
		  (iff	(preserved_filter ?a1 ?a ?s1)
			(preserved_filter ?a1 ?a ?s2))))))
Definition 5 
(forall (?a) (iff (sometime_interfere ?a)
(and 	(exists (?s1 ?a1) 
		(forall (?s2)
			(if	  (and	(atomic ?a1)
					(begin_equiv ?s1 ?s2))
		  		  (iff	(preserved_filter ?a1 ?a ?s1)
					(preserved_filter ?a1 ?a ?s2)))))
	(exists (?a2 ?s3 ?s4)
		(and	(atomic ?a2)
			(begin_equiv ?s3 ?s4)
			(preserved_filter ?a2 ?a ?s3)
			(not (preserved_filter ?a2 ?a ?s4)))))))
Definition 6 
(forall (?a) (iff (rigid_interfere ?a)
(forall (?s1)
	(exists (?a1 ?s2)
		(and	(atomic ?a1)
			(begin_equiv ?s1 ?s2)
		  	(iff	(preserved_filter ?a1 ?a ?s1)
				(not (preserved_filter ?a1 ?a ?s2))))))))