Skip to content
Permalink
Branch: master
Find file Copy path
Find file Copy path
Fetching contributors…
Cannot retrieve contributors at this time
162 lines (120 sloc) 4.25 KB
/*******************************************************************************
* Copyright (c) University of Toronto and others. All rights reserved.
* The content of this file is licensed under the Creative Commons Attribution-
* ShareAlike 4.0 Unported license. The legal text of this license can be
* found at http://creativecommons.org/licenses/by-sa/4.0/legalcode.
*
* Contributors:
* Michael Gruninger - initial implementation
*******************************************************************************/
(cl-text http://colore.oor.net/psl_occtree/occtree.clif
(cl-imports http://colore.oor.net/psl_core/psl_core.clif)
(forall (s)
(if (arboreal s)
(activity_occurrence s)))
(cl-comment 'The earlier relation is restricted to
arboreal activity occurrences (that is, activity occurrences that
are elements of the occurrence tree).')
(forall (s1 s2)
(if (earlier s1 s2)
(and (arboreal s1)
(arboreal s2))))
(cl-comment 'The ordering relation over occurrences is irreflexive.')
(forall (s1 s2)
(if (earlier s1 s2)
(not (earlier s2 s1))))
(cl-comment 'The ordering relation over occurrences is transitive.')
(forall (s1 s2 s3)
(if (and (earlier s1 s2)
(earlier s2 s3))
(earlier s1 s3)))
(cl-comment 'A branch in the occurrence tree is totally ordered.')
(forall (s1 s2 s3)
(if (and (earlier s1 s2)
(earlier s3 s2))
(or (earlier s1 s3)
(earlier s3 s1)
(= s3 s1))))
(cl-comment 'Every branch of the occurrence tree has an initial occurrence.')
(forall (s1 s2)
(if (earlier s1 s2)
(exists (sp)
(and (initial sp)
(earlierEq sp s1)))))
(cl-comment 'No two initial activity occurrences in the occurrence tree are occurrences
of the same activity.')
(forall (s1 s2 a)
(if (and (initial s1)
(initial s2)
(occurrence_of s1 a)
(occurrence_of s2 a))
(= s1 s2)))
(cl-comment 'An activity is a generator iff it has an initial occurrence in the
occurrence tree.')
(forall (a)
(if (generator a)
(exists (s)
(and (initial s)
(occurrence_of s a)))))
(cl-comment 'There is an initial occurrence of each activity.')
(forall (s a)
(if (occurrence_of s a)
(iff (arboreal s)
(generator a))))
(cl-comment 'The successor of an arboreal activity occurrence is an occurrence of a generator activity.')
(forall (a o)
(iff (occurrence_of (successor a o) a)
(and (generator a)
(arboreal o))))
(cl-comment 'Every non-initial activity occurrence is the successor of
another activity occurrence.')
(forall (s1 s2)
(if (earlier s1 s2)
(exists (a s3)
(and (generator a)
(= s2 (successor a s3))))))
(cl-comment 'An occurrence s1 is earlier than the successor occurrence
of s2 if and only if the occurrence s2 is later than s1.')
(forall (a s1 s2)
(if (generator a)
(iff (earlier s1 (successor a s2))
(earlierEq s1 s2))))
(cl-comment 'The legal relation restricts arboreal activity occurrences.')
(forall (s)
(if (legal s)
(arboreal s)))
(cl-comment 'If an activity occurrence is legal, all earlier activity
occurrences in the occurrence tree are also legal.')
(forall (s1 s2)
(if (and (legal s1)
(earlier s2 s1))
(legal s2)))
(cl-comment 'The endof an activity occurrence is before to the beginof
the successor of the activity occurrence.')
(forall (s1 s2)
(if (earlier s1 s2)
(before (endof s1) (beginof s2))))
(cl-comment 'An activity occurrence s1 precedes another activity occurrence s2
if and only if s1 is earlier than s2 in the occurrence tree and s2 is legal.')
(forall (s1 s2) (iff (precedes s1 s2)
(and (earlier s1 s2)
(legal s2))))
(cl-comment 'An activity occurrence s1 is EarlierEq than
an activity occurrence s2 if and only if it is either earlier than
s2 or it is equal to s2.')
(forall (s1 s2) (iff (earlierEq s1 s2)
(and (arboreal s1)
(arboreal s2)
(or (earlier s1 s2)
(= s1 s2)))))
(cl-comment 'An activity is poss at some occurrence if and only if the successor
occurrence of the activity is legal.')
(forall (a s) (iff (poss a s)
(legal (successor a s))))
(cl-comment 'No occurrence in the occurrence tree is earlier than an initial occurrence.')
(forall (s)
(iff (initial s)
(and (arboreal s)
(not (exists (sp)
(earlier sp s))))))
)
You can’t perform that action at this time.