Effects for Concurrent Activities

Effects for Concurrent Activities

Extension Name: clobber.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: none

Definitions

Definition 1 The effects of an activity ?a1 are preserved by an activity ?a if the effects of any superactivity of ?a are equivalent to the effects of that superactivity concurrently with ?a1. 
(forall (?a ?a1 ?s) (iff (preserved_effects ?a ?a1 ?s) 
(forall (?a2 ?f)
	(if  (subactivity ?a ?a2)
		  (iff	(holds ?f (successor ?a2 ?s))
			(holds ?f (successor (conc ?a2 ?a1) ?s)))))))
Definition 2 An activity ?a is nonclobbering iff it preserves the effects of any atomic activity. 
(forall (?a ?s) (iff (nonclobbering ?a ?s) 
(forall (?a1)
	(if  (atomic ?a1)
		  (preserved_effects ?a ?a1 ?s)))))
Definition 3 An activity ?a is clobbering iff there exists an atomic activity whose effects are not preserved by ?a. 
(forall (?a ?s) (iff (clobbering ?a ?s) 
(exists (?a1)
	(and	(atomic ?a1)
		(not (preserved_effects ?a ?a1 ?s))))))
Definition 4 An activity ?a is meddling iff it does not preserve the effects of any atomic activity. 
(forall (?a ?s) (iff (meddling ?a ?s) 
(forall (?a1)
	(if  (atomic ?a1)
		  (not (preserved_effects ?a ?a1 ?s))))))
Definition 5 An activity is a global clobber iff it preserves effects at all occurrences in the occurrence tree. 
(forall (?a) (iff (global_clobber ?a) 
(forall (?a1)
	(if  (atomic ?a1)
		  (forall (?s1 ?s2)
			(iff	(preserved_effects ?a ?a1 ?s1)
				(preserved_effects ?a ?a1 ?s2)))))))