Preconditions for Concurrent Activities

Extension Name: interfere.def

Primitive Lexicon: None

Defined Lexicon:

Relations:

(preserved_filter ?a ?a1 ?s)
(noninterfering ?a ?s)
(interfering ?a ?s)
(imperial ?a ?s)
(global_interfere ?a)

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

Definitional Extensions Required by this Extension: none

Definitions

Definition 1

(forall (?a ?a1 ?s) (iff (preserved_filter ?a ?a1 ?s)
(forall (?a2)
	(if	  (subactivity ?a ?a2)
		  (iff	(poss ?a2 ?s)
			(poss (conc ?a2 ?a1) ?s))))))

Definition 2

(forall (?a ?s) (iff (noninterfering ?a ?s)
(forall (?a1)
	(if	  (atomic ?a1)
		  (preserved_filter ?a ?a1 ?s)))))

Definition 3

(forall (?a ?s) (iff (interfering ?a ?s)
(exists (?a1)
	(and	(atomic ?a1)
		(not (preserved_filter ?a ?a1 ?s))))))

Definition 4

(forall (?a ?s) (iff (imperial ?a ?s)
(forall (?a1)
	(if	  (atomic ?a1)
		  (not (preserved_filter ?a ?a1 ?s))))))

Definition 5

(forall (?a) (iff (global_interfere ?a)
(forall (?a1)
	(if	  (atomic ?a1)
		  (forall (?s1 ?s2)
			(iff	(preserved_filter ?a ?a1 ?s1)
				(preserved_filter ?a ?a1 ?s2)))))))