Skip to content
Permalink
Browse files

updated comments in PSL hierarchies with single quotes

  • Loading branch information...
carmenchui committed Jun 20, 2018
1 parent ff671b7 commit 3efef9a15e4fd0a715129bd02a3c355b73eadc1e

Large diffs are not rendered by default.

Oops, something went wrong.
@@ -17,9 +17,9 @@
(and (activity_occurrence o1)
(activity_occurrence o2))))

(cl-comment "There exists an occurrence of an activity a for every branch of an activity
(cl-comment 'There exists an occurrence of an activity a for every branch of an activity
tree for a. All atomic subactivity occurrences on the branch are subactivity
occurrences of the occurrence of a.")
occurrences of the occurrence of a.')

(forall (a s1 s2)
(if (min_precedes s1 s2 a)
@@ -28,9 +28,9 @@ occurrences of the occurrence of a.")
(subactivity_occurrence s1 occ)
(subactivity_occurrence s2 occ)))))

(cl-comment "There exists an occurrence of an activity a for every branch of an activity
(cl-comment 'There exists an occurrence of an activity a for every branch of an activity
tree for a. All root subactivity occurrences on the branch are subactivity
occurrences of the occurrence of a.")
occurrences of the occurrence of a.')

(forall (a s)
(if (and (root s a)
@@ -40,8 +40,8 @@ occurrences of the occurrence of a.")
(subactivity_occurrence s occ)))))


(cl-comment "Every occurrence of a complex activity a contains an atomic subactivity
occurrence that is the root of an activity tree for a.")
(cl-comment 'Every occurrence of a complex activity a contains an atomic subactivity
occurrence that is the root of an activity tree for a.')

(forall (occ a)
(if (and (occurrence_of occ a)
@@ -51,7 +51,7 @@ occurrence that is the root of an activity tree for a.")
(subactivity_occurrence s occ)))))


(cl-comment "Distinct occurrences of an activity correspond to distinct branches of an activity tree.")
(cl-comment 'Distinct occurrences of an activity correspond to distinct branches of an activity tree.')

(forall (a s1 occ1 occ2)
(if (and (occurrence_of occ1 a)
@@ -62,8 +62,8 @@ occurrence that is the root of an activity tree for a.")
(subactivity_occurrence s occ1)
(not (subactivity_occurrence s occ2))))))

(cl-comment "All atomic subactivity occurrences of a complex activity occurrence
are elements of the same branch of the activity tree.")
(cl-comment 'All atomic subactivity occurrences of a complex activity occurrence
are elements of the same branch of the activity tree.')

(forall (a occ s1 s2)
(if (and (occurrence_of occ a)
@@ -75,16 +75,16 @@ are elements of the same branch of the activity tree.")
(min_precedes s2 s1 a)
(= s1 s2))))

(cl-comment "All elements of the same branch of an activity tree are atomic
subactivity occurrences of the same activity occurrences.")
(cl-comment 'All elements of the same branch of an activity tree are atomic
subactivity occurrences of the same activity occurrences.')

(forall (a s1 s2 occ)
(if (and (min_precedes s1 s2 a)
(occurrence_of occ a)
(subactivity_occurrence s2 occ))
(subactivity_occurrence s1 occ)))

(cl-comment "The subactivity_occurrence relation preserves the subactivity relation.")
(cl-comment 'The subactivity_occurrence relation preserves the subactivity relation.')

(forall (a1 a2 occ1 occ2)
(if (and (occurrence_of occ1 a1)
@@ -93,15 +93,15 @@ subactivity occurrences of the same activity occurrences.")
(subactivity_occurrence occ1 occ2))
(subactivity a1 a2)))

(cl-comment "The subactivity_occurrence relation is transitive.")
(cl-comment 'The subactivity_occurrence relation is transitive.')

(forall (occ1 occ2 occ3)
(if (and (subactivity_occurrence occ1 occ2)
(subactivity_occurrence occ2 occ3))
(subactivity_occurrence occ1 occ3)))

(cl-comment "Occurrences of subactivities are subactivity occurrences if the
occurrences satisfy branch containment.")
(cl-comment 'Occurrences of subactivities are subactivity occurrences if the
occurrences satisfy branch containment.')

(forall (a1 a2 occ1 occ2)
(if (and (occurrence_of occ1 a1)
@@ -112,28 +112,28 @@ occurrences satisfy branch containment.")
(and (subactivity_occurrence s occ1)
(not (subactivity_occurrence s occ2))))))

(cl-comment "The beginof timepoint for a complex activity occurrence is
equal to the beginof timepoint of its root occurrence.")
(cl-comment 'The beginof timepoint for a complex activity occurrence is
equal to the beginof timepoint of its root occurrence.')

(forall (s occ)
(if (root_occ s occ)
(= (beginof occ) (beginof s))))

(cl-comment "The endof timepoint for a complex activity occurrence is
equal to the endof timepoint of its leaf occurrence.")
(cl-comment 'The endof timepoint for a complex activity occurrence is
equal to the endof timepoint of its leaf occurrence.')

(forall (s occ)
(if (leaf_occ s occ)
(= (endof occ) (endof s))))

(cl-comment "The mono relation is a branch homomorphism.")
(cl-comment 'The mono relation is a branch homomorphism.')

(forall (s1 s2 a)
(if (mono s1 s2 a)
(hom s1 s2 a)))

(cl-comment "If an atomic subactivity occurrence is mapped in a branch homomorphism,
then there exists another atomic subactivity occurrence that is mono with it.")
(cl-comment 'If an atomic subactivity occurrence is mapped in a branch homomorphism,
then there exists another atomic subactivity occurrence that is mono with it.')

(forall (s1 s2 a)
(if (and (hom s1 s2 a)
@@ -144,30 +144,30 @@ then there exists another atomic subactivity occurrence that is mono with it.")
(and (min_precedes s3 s1 a)
(mono s2 s3 a))))))

(cl-comment "The mono relation is restricted to one-to-one homomorphisms between different
branches of the activity tree.")
(cl-comment 'The mono relation is restricted to one-to-one homomorphisms between different
branches of the activity tree.')

(forall (s1 s2 s3 a)
(if (and (mono s1 s2 a)
(mono s3 s2 a))
(not (or (min_precedes s1 s3 a)
(min_precedes s3 s1 a)))))

(cl-comment "The mono relation is symmetric on activity occurrences.")
(cl-comment 'The mono relation is symmetric on activity occurrences.')

(forall (s1 s2 a)
(if (mono s1 s2 a)
(mono s2 s1 a)))

(cl-comment "The mono relation is transitive on activity occurrences.")
(cl-comment 'The mono relation is transitive on activity occurrences.')

(forall (s1 s2 s3 a)
(if (and (mono s1 s2 a)
(mono s2 s3 a))
(mono s1 s3 a)))

(cl-comment "Two activity occurrences are occurrence isomorphic iff they are occurrences of
atomic activities that have a common subactivity with the complex activity a.")
(cl-comment 'Two activity occurrences are occurrence isomorphic iff they are occurrences of
atomic activities that have a common subactivity with the complex activity a.')

(forall (s1 s2 a) (iff (iso_occ s1 s2 a)
(exists (a1 a2 a3)
@@ -184,8 +184,8 @@ atomic activities that have a common subactivity with the complex activity a.")
(or (subactivity a3 a4)
(= a3 a4))))))))

(cl-comment "For every two occurrences of the same activity on different branches of an
activity tree, there exist homomorphic occurrences on those branches.")
(cl-comment 'For every two occurrences of the same activity on different branches of an
activity tree, there exist homomorphic occurrences on those branches.')

(forall (s1 s2 a) (iff (hom s1 s2 a)
(exists (occ1 occ2)
@@ -197,8 +197,8 @@ activity tree, there exist homomorphic occurrences on those branches.")
(occurrence_of occ1 a)
(occurrence_of occ2 a)))))

(cl-comment "An occurrence occ1 is the root occurrence of an occurrence of a if and only if
it is a subactivity occurrence and it is the root of an activity tree for a.")
(cl-comment 'An occurrence occ1 is the root occurrence of an occurrence of a if and only if
it is a subactivity occurrence and it is the root of an activity tree for a.')

(forall (s occ)
(iff (root_occ s occ)
@@ -207,8 +207,8 @@ it is a subactivity occurrence and it is the root of an activity tree for a.")
(subactivity_occurrence s occ)
(root s a)))))

(cl-comment "An occurrence occ1 is the leaf occurrence of an occurrence of a if and only if
it is a subactivity occurrence and it is the leaf of an activity tree for a.")
(cl-comment 'An occurrence occ1 is the leaf occurrence of an occurrence of a if and only if
it is a subactivity occurrence and it is the leaf of an activity tree for a.')

(forall (s occ)
(iff (leaf_occ s occ)
@@ -217,9 +217,9 @@ it is a subactivity occurrence and it is the leaf of an activity tree for a.")
(subactivity_occurrence s occ)
(leaf s a)))))

(cl-comment "Two complex activity occurrences are in the same grove
(cl-comment 'Two complex activity occurrences are in the same grove
iff they are occurrences of the same activity and their
root occurrences are siblings.")
root occurrences are siblings.')

(forall (occ1 occ2)
(iff (same_grove occ1 occ2)
@@ -13,58 +13,58 @@
(cl-text http://colore.oor.net/psl_actors/psl_actors
(cl-imports http://colore.oor.net/psl_actocc/actocc.clif)

(cl-comment "ax1: an actor is a type of object")
(cl-comment 'ax1: an actor is a type of object')
(forall (x)
(if (actor x)
(object x)))

(cl-comment "ax2: performed_in is a specialization of the participates_in relation")
(cl-comment 'ax2: performed_in is a specialization of the participates_in relation')
(forall (x o)
(if (performed_in x o)
(exists t)
(participates x o t)))

(cl-comment "ax3: performs defines the relationship between actors and activities, where an actor performs the activity")
(cl-comment 'ax3: performs defines the relationship between actors and activities, where an actor performs the activity')
(forall (x a)
(if (performs x a)
(and (actor x)
(activity a))))

(cl-comment "ax4: performed_in defines the relationship between actors and occurrences, where an actor performed_in an occurrence of an activity")
(cl-comment "technically the last term is unnecessary as we can infer it based on axiom 2")
(cl-comment 'ax4: performed_in defines the relationship between actors and occurrences, where an actor performed_in an occurrence of an activity')
(cl-comment 'technically the last term is unnecessary as we can infer it based on axiom 2')
(forall (x o)
(if (performed_in x o)
(and (actor x)
(activity_occurrence o))))

(cl-comment "ax5: if an actor performed in some occ, then it performed in any occurrences that the occ is a subocc of")
(cl-comment 'ax5: if an actor performed in some occ, then it performed in any occurrences that the occ is a subocc of')
(forall (x o1 o2)
(if (and (performed_in x o1)
(subactivity_occurrence o1 o2))
(performed_in x o2)))

(cl-comment "ax6: if an actor performed in som occ, then that occ has a subactivity in which the actor performed in")
(cl-comment "do we want to assert that it performed in some occ of an atomic activity?"
(cl-comment 'ax6: if an actor performed in som occ, then that occ has a subactivity in which the actor performed in')
(cl-comment 'do we want to assert that it performed in some occ of an atomic activity?'
(forall (x o1)
(if (performs x o1)
(exists (o2) (and (subactivity_occurrence o2 o1)
(performed_in x o2)))))

(cl-comment "are ax5 and ax6 consequences of ax7 ax8 and ax9? is there a reason not to define ax7, ax8?")
(cl-comment "ax7: if an actor performs some activity, then it performs in all activities that the activity is a subactivity of")
(cl-comment 'are ax5 and ax6 consequences of ax7 ax8 and ax9? is there a reason not to define ax7, ax8?')
(cl-comment 'ax7: if an actor performs some activity, then it performs in all activities that the activity is a subactivity of')
(forall (x a1 a2)
(if (and (performs x a1)
(subactivity a1 a2))
(performs x a2)))

(cl-comment "ax8: if an actor performs some activity, then there must be an atomic? subactivity that the actor performs")
(cl-comment 'ax8: if an actor performs some activity, then there must be an atomic? subactivity that the actor performs')
(forall (x a1)
(if (performs x a1)
(exists (a2) (and (subactivity a2 a1)
(atomic a2)
(performs x a2)))))

(cl-comment "ax9: performs indicates the planned or intended occurrences of an activity")
(cl-comment 'ax9: performs indicates the planned or intended occurrences of an activity')
(forall (x a o)
(if (and (performs x a)
(occurrence_of o a))
@@ -13,45 +13,45 @@
(cl-imports http://colore.oor.net/psl_occtree/occtree.clif)
(cl-imports http://colore.oor.net/psl_subactivity/subactivity.clif)

(cl-comment "Primitive activities are atomic.")
(cl-comment 'Primitive activities are atomic.')

(forall (a)
(if (primitive a)
(atomic a)))

(cl-comment "The function conc is idempotent.")
(cl-comment 'The function conc is idempotent.')

(forall (a)
(= a (conc a a)))

(cl-comment "The function conc is commutative.")
(cl-comment 'The function conc is commutative.')

(forall (a1 a2)
(= (conc a1 a2) (conc a2 a1)))

(cl-comment "The function conc is associative.")
(cl-comment 'The function conc is associative.')

(forall (a1 a2 a3)
(= (conc a1 (conc a2 a3)) (conc (conc a1 a2) a3)))

(cl-comment "The concurrent aggregation of atomic action is an atomic action.")
(cl-comment 'The concurrent aggregation of atomic action is an atomic action.')

(forall (a1 a2)
(iff (atomic (conc a1 a2))
(and (atomic a1)
(atomic a2))))

(cl-comment "An atomic activity a1 is a subactivity of an atomic activity a2 if and only if
a2 is an idempotent for a1.")
(cl-comment 'An atomic activity a1 is a subactivity of an atomic activity a2 if and only if
a2 is an idempotent for a1.')

(forall (a1 a2)
(if (and (atomic a1)
(atomic a2))
(iff (subactivity a1 a2)
(= a2 (conc a1 a2)))))

(cl-comment "An atomic action has a proper subactivity if and only if there exists another atomic
activity which can be concurrently aggregated.")
(cl-comment 'An atomic action has a proper subactivity if and only if there exists another atomic
activity which can be concurrently aggregated.')

(forall (a1 a2)
(if (and (atomic a2)
@@ -65,7 +65,7 @@ activity which can be concurrently aggregated.")
(subactivity a4 a1)
(subactivity a4 a3))))))))

(cl-comment "The semilattice of atomic activities is distributive.")
(cl-comment 'The semilattice of atomic activities is distributive.')

(forall (a b0 b1)
(if (and (atomic a)
@@ -78,15 +78,15 @@ activity which can be concurrently aggregated.")
(subactivity a1 a)
(= a (conc a0 a1))))))

(cl-comment "Only atomic activities can be generator activities.
(cl-comment 'Only atomic activities can be generator activities.
Equivalently, only occurrences of atomic activities can be
elements of an occurrence tree.")
elements of an occurrence tree.')

(forall (a)
(if (generator a)
(atomic a)))

(cl-comment "Atomic activities are activities.")
(cl-comment 'Atomic activities are activities.')

(forall (a)
(if (atomic a)
Oops, something went wrong.

0 comments on commit 3efef9a

Please sign in to comment.
You can’t perform that action at this time.
You signed in with another tab or window. Reload to refresh your session. You signed out in another tab or window. Reload to refresh your session.