Classes of Atomic Activities

Classes of Atomic Activities: Upwards Concurrency

Extension Name: up_concurrent.def

Primitive Lexicon: None

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

Defined Lexicon:

Predicates:

(natural ?a ?s)
(artificial ?a ?s)
(performed ?a ?s)
(up_ghost ?a ?s)
(up_conflict ?a ?s)
(quark ?a ?s)

Definitional Extensions Required by this Extension: None

Definitions

Definition 1 An activity is natural iff it is a subactivity of any activity that is possible whenever it is possible.

(forall (?a ?s) (iff (natural ?a ?s)
(forall (?a1)
	(if	  (and	(poss ?a ?s)
			(poss ?a1 ?s))
		  (subactivity ?a ?a1)))))

Definition 2 An activity is an artificial activity iff

(forall (?a ?s) (iff (artificial ?a ?s)
(forall (?a1)
	(if	  (and	(poss ?a ?s)
			(poss ?a1 ?s)
			(not (subactivity ?a1 ?a)))
		  (poss (conc ?a ?a1) ?s)))))

Definition 3 An activity is a performed activity iff

(forall (?a ?s) (iff (performed ?a ?s)
(exists (?a1 ?a2)
	(and	(subactivity ?a1 ?a)
		(subactivity ?a2 ?a)
		(poss ?a ?s)
		(not (poss (conc ?a1 ?a2) ?s))))))

Definition 4 An activity is an up_ghost activity iff

(forall (?a ?s) (iff (up_ghost ?a ?s)
(forall (?a1)
	(if	  (and	(poss ?a1 ?s)
			(subactivity ?a ?a1))
		  (poss ?a ?s)))))

Definition 5 An activity is an up_conflict activity iff

(forall (?a ?s) (iff (up_conflict ?a ?s)
(forall (?a1)
	(if	  (poss (conc ?a ?a1) ?s)
		  (or	(poss ?a ?s)
			(poss ?a1 ?s)
			(subactivity ?a ?a1))))))

Definition 6 An activity is a quark activity iff

(forall (?a ?s) (iff (quark ?a ?s)
(exists (?a1)
	(and	(atomic ?a1)
		(subactivity ?a ?a1)
		(poss ?a1 ?s)
		(not (poss ?a ?s))))))