--- a/model/prov-constraints.html Fri Aug 10 16:31:17 2012 +0100
+++ b/model/prov-constraints.html Fri Aug 10 16:40:46 2012 +0100
@@ -2022,7 +2022,9 @@
that <span class="name">used(use; a,e1,_t1,[])</span> and <span
class="name">wasDerivedFrom(id; e2,e1,a,gen,use,attrs)</span>.
</div>
-<p>This inference is justified by the fact that the entity denoted by <span class="name">e2</span> is generated by at most one activity
+<p>This inference is justified by the fact that the entity denoted by
+ <span class="name">e2</span> has a unique generation event
+ representing its generation by activity <span class="name">a</span>
(see <a class="rule-text" href="#unique-generation"><span>TBD</span></a>). Hence, this activity is also the one referred to by the usage of <span class="name">e1</span>.
</p>
@@ -2629,7 +2631,7 @@
<div class='constraint' id='unique-generation'>
<p>
-<span class='conditional'>IF</span> <span class="name">wasGeneratedBy(gen1; e,_a1,_t1,_attrs1)</span> and <span class="name">wasGeneratedBy(gen2; e,_a2,_t2,_attrs2)</span>,
+<span class='conditional'>IF</span> <span class="name">wasGeneratedBy(gen1; e,a,_t1,_attrs1)</span> and <span class="name">wasGeneratedBy(gen2; e,a,_t2,_attrs2)</span>,
<span class='conditional'>THEN</span> <span class="name">gen1</span> = <span class="name">gen2</span>.</p>
</div>
@@ -2638,7 +2640,7 @@
<div class='constraint' id='unique-invalidation'>
<p>
-<span class='conditional'>IF</span> <span class="name">wasInvalidatedBy(inv1; e,_a1,_t1,_attrs1)</span> and <span class="name">wasInvalidatedBy(inv2; e,_a2,_t2,_attrs2)</span>,
+<span class='conditional'>IF</span> <span class="name">wasInvalidatedBy(inv1; e,a,_t1,_attrs1)</span> and <span class="name">wasInvalidatedBy(inv2; e,a,_t2,_attrs2)</span>,
<span class='conditional'>THEN</span> <span class="name">inv1</span> = <span class="name">inv2</span>.</p>
</div>
@@ -2682,28 +2684,27 @@
<div class='constraint' id='unique-wasStartedBy'>
<p>
<span class='conditional'>IF</span> <span
- class="name">wasStartedBy(start1; a,_e1,_a1,_t1,_attrs1)</span> and <span
- class="name">wasStartedBy(start2; a,_e2,_a2,_t2,_attrs2)</span>, <span
+ class="name">wasStartedBy(start1; a,_e1,a0,_t1,_attrs1)</span> and <span
+ class="name">wasStartedBy(start2; a,_e2,a0,_t2,_attrs2)</span>, <span
class='conditional'>THEN</span> <span class="name">start1</span> = <span
class="name">start2</span>.</p>
</div>
-<hr />
<p id='unique-wasEndedBy_text'>
<div class='constraint' id='unique-wasEndedBy'>
<p>
<span class='conditional'>IF</span> <span
- class="name">wasEndedBy(end1; a,_e1,_a1,_t1,_attrs1)</span> and <span
- class="name">wasEndedBy(end2; a,_e2,_a2,_t2,_attrs2)</span>, <span
+ class="name">wasEndedBy(end1; a,_e1,a0,_t1,_attrs1)</span> and <span
+ class="name">wasEndedBy(end2; a,_e2,a0,_t2,_attrs2)</span>, <span
class='conditional'>THEN</span> <span class="name">end1</span> = <span
class="name">end2</span>.</p>
</div>
-
-
-<p>
+<hr />
+
+
@@ -2890,8 +2891,7 @@
</div>
-<p>
-
+
<hr />
<p id='start-precedes-end_text'>
@@ -2915,6 +2915,51 @@
</p>
</div>
<p>
+
+<hr />
+
+<p id='start-start-ordering_text'>
+If an activity is started by more than one activity, the events must all
+be simultaneous. The following constraint requires that if there are two start
+events that start the same activity, then one <a>precedes</a> the
+other. Using this constraint in both directions means that each event
+<a>precedes</a> the other.
+</p>
+<div class='constraint' id='start-start-ordering'>
+ <p>
+ <span class="conditional">IF</span>
+<span class="name">wasStartedBy(start1; a,_e1,_a1,_t1,_attrs1)</span>
+and
+<span class="name">wasStartedBy(start2; a,_e2,_a2,_t2,_attrs2)</span>
+<span class="conditional">THEN</span>
+<span class="name">start1</span>
+<a title="precedes">precedes</a>
+<span class="name">start2</span>.
+ </p>
+</div>
+
+<hr />
+
+<p id='end-end-ordering_text'>
+If an activity is ended by more than one activity, the events must all
+be simultaneous. The following constraint requires that if there are two start
+events that start the same activity, then one <a>precedes</a> the
+other. Using this constraint in both directions means that each event
+<a>precedes</a> the other, that is, they are simultaneous.
+</p>
+<div class='constraint' id='end-end-ordering'>
+ <p>
+ <span class="conditional">IF</span>
+<span class="name">wasEndedBy(end1; a,_e2,_a1,_t1,_attrs1)</span>
+and
+<span class="name">wasEndedBy(end2; a,_e2,_a2,_t2,_attrs2)</span>
+<span class="conditional">THEN</span>
+<span class="name">end1</span>
+<a title="precedes">precedes</a>
+<span class="name">end2</span>.
+ </p>
+</div>
+
<hr />
<p id='usage-within-activity_text'>A usage implies ordering of <a title="instantaneous event">events</a>, since the <a title="entity usage event">usage event</a> had to occur during the associated activity. This is
@@ -3237,49 +3282,6 @@
<hr />
-<p id='start-start-ordering_text'>
-If an activity is started by more than one activity, the events must all
-be simultaneous. The following constraint requires that if there are two start
-events that start the same activity, then one <a>precedes</a> the
-other. Using this constraint in both directions means that each event
-<a>precedes</a> the other.
-</p>
-<div class='constraint' id='start-start-ordering'>
- <p>
- <span class="conditional">IF</span>
-<span class="name">wasStartedBy(start1; a,_e1,_a1,_t1,_attrs1)</span>
-and
-<span class="name">wasStartedBy(start2; a,_e2,_a2,_t2,_attrs2)</span>
-<span class="conditional">THEN</span>
-<span class="name">start1</span>
-<a title="precedes">precedes</a>
-<span class="name">start2</span>.
- </p>
-</div>
-
-<hr />
-
-<p id='end-end-ordering_text'>
-If an activity is ended by more than one activity, the events must all
-be simultaneous. The following constraint requires that if there are two start
-events that start the same activity, then one <a>precedes</a> the
-other. Using this constraint in both directions means that each event
-<a>precedes</a> the other, that is, they are simultaneous.
-</p>
-<div class='constraint' id='end-end-ordering'>
- <p>
- <span class="conditional">IF</span>
-<span class="name">wasEndedBy(end1; a,_e2,_a1,_t1,_attrs1)</span>
-and
-<span class="name">wasEndedBy(end2; a,_e2,_a2,_t2,_attrs2)</span>
-<span class="conditional">THEN</span>
-<span class="name">end1</span>
-<a title="precedes">precedes</a>
-<span class="name">end2</span>.
- </p>
-</div>
-<hr />
-
<p id='wasStartedBy-ordering_text'>
The entity that triggered the start of an activity must exist before the activity starts.
This is