Variation of Clobbering Effects

Variation of Clobbering Effects

Extension Name: var_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: clobber.def, state_precond.def, time_precond.def

Grammar:

Definitions

Definition 1 
(forall (?a) (iff (state_clobber ?a) 
(forall (?a1 ?s1 ?s2)
        (if	  (and	(atomic ?a1)
			(state_equiv ?s1 ?s2))
		  (iff	(preserved_effects ?a1 ?a ?s1)
			(preserved_effects ?a1 ?a ?s2))))))
Definition 2 
(forall (?a) (iff (partial_clobber ?a) 
(and 	(exists (?s1 ?a1) 
		(forall (?s2)
			(if	  (and	(atomic ?a1)
					(state_equiv ?s1 ?s2))
		  		  (iff	(preserved_effects ?a1 ?a ?s1)
					(preserved_effects ?a1 ?a ?s2)))))
	(exists (?a2 ?s3 ?s4)
		(and	(atomic ?a2)
			(state_equiv ?s3 ?s4)
			(preserved_effects ?a2 ?a ?s3)
			(not (preserved_effects ?a2 ?a ?s4)))))))
Definition 3 
(forall (?a) (iff (unconditional_clobber ?a) 
(forall (?s1)
	(exists (?a1 ?s2)
		(and	(atomic ?a1)
			(state_equiv ?s1 ?s2)
		  	(iff	(preserved_effects ?a1 ?a ?s1)
				(not (preserved_effects ?a1 ?a ?s2))))))))
Definition 4 
(forall (?a) (iff (time_clobber ?a) 
(forall (?a1 ?s1 ?s2)
        (if	  (and	(atomic ?a1)
			(begin_equiv ?s1 ?s2))
		  (iff	(preserved_effects ?a1 ?a ?s1)
			(preserved_effects ?a1 ?a ?s2))))))
Definition 5 
(forall (?a) (iff (sometime_clobber ?a) 
(and 	(exists (?s1 ?a1) 
		(forall (?s2)
			(if	  (and	(atomic ?a1)
					(begin_equiv ?s1 ?s2))
		  		  (iff	(preserved_effects ?a1 ?a ?s1)
					(preserved_effects ?a1 ?a ?s2)))))
	(exists (?a2 ?s3 ?s4)
		(and	(atomic ?a2)
			(begin_equiv ?s3 ?s4)
			(preserved_effects ?a2 ?a ?s3)
			(not (preserved_effects ?a2 ?a ?s4)))))))
Definition 6 
(forall (?a) (iff (rigid_clobber ?a) 
(forall (?s1)
	(exists (?a1 ?s2)
		(and	(atomic ?a1)
			(begin_equiv ?s1 ?s2)
		  	(iff	(preserved_effects ?a1 ?a ?s1)
				(not (preserved_effects ?a1 ?a ?s2))))))))