--- a/model/prov-constraints.html Thu May 31 23:52:30 2012 +0100
+++ b/model/prov-constraints.html Fri Jun 01 10:28:08 2012 +0100
@@ -566,11 +566,14 @@
</figure>
</div>
-
-<p>Start of <span class="name">a2</span> by activity <span
+<p>
+
+<hr>
+
+<p id='wasStartedBy-definition_text'>Start of <span class="name">a2</span> by trigger <span class="name">e</span> and starter activity <span
class="name">a1</span> is <a title="definition">defined</a> as follows.</p>
-<div class='definition' id='wasStartedByActivity-definition'>
+<div class='definition' id='wasStartedBy-definition'>
<p>Given two activities with identifiers <span class="name">a1</span> and <span class="name">a2</span>,
<span class="name">wasStartedBy(-;a2,e,a1,-)</span>
holds <span class='conditional'>IF AND ONLY IF</span>
@@ -578,6 +581,22 @@
and <span class="name">wasStartedBy(-;a2,e,-,-)</span> hold.</p>
</div>
+<p>
+
+<hr>
+
+<p id='wasEndedBy-definition_text'>Likewise, end of <span class="name">a2</span> by
+by trigger <span class="name">e</span> and ender activity <span
+class="name">a1</span> is <a title="definition">defined</a> as follows.</p>
+
+<div class='definition' id='wasEndedBy-definition'>
+<p>Given two activities with identifiers <span class="name">a1</span> and <span class="name">a2</span>,
+ <span class="name">wasEndedBy(-;a2,e,a1,-)</span>
+holds <span class='conditional'>IF AND ONLY IF</span>
+ <span class="name">wasGeneratedBy(-;e,a1,-,-)</span>
+ and <span class="name">wasEndedBy(-;a2,e,-,-)</span> hold.</p>
+</div>
+
@@ -713,13 +732,14 @@
a1 is associated with all activities a2 is associated with?
</div>
-
-<p>Traceability allows an entity to be transitively linked to another entity it is derived from, to an agent it is attributed to, or another agent having some responsibility, or a trigger of an activity that generated it.</p>
-
-<p>Traceability can be inferred from existing statements, or can be asserted stating that a dependency path exists without its individual steps being expressed. This is captured
+<hr>
+
+<p id='trace-inference_text'>A trace allows an entity to be transitively linked to another entity it is derived from, to an agent it is attributed to, or another agent having some responsibility, or a trigger of an activity that generated it.</p>
+
+<p>A trace can be inferred from existing statements, or can be asserted stating that a dependency path exists without its individual steps being expressed. This is captured
by the following inferences:
-<div class='inference' id='traceability-inference'>
+<div class='inference' id='trace-inference'>
<p>
Given two identifiers <span class="name">e2</span> and <span class="name">e1</span> for entities,
the following statements hold:</p>
@@ -749,14 +769,12 @@
</ol>
</div>
-<p>We note that the inference rule <a
-href="#traceability-inference">traceability-inference</a> does not
+<p>We note that <a class="rule-text"
+href="#trace-inference"><span>TBD</span></a> does not
allow us to infer anything about the attributes of the related
entities, agents or events.
</p>
-
-
</section>
@@ -789,7 +807,11 @@
For any entity <span class='name'>e1</span>, <span class='name'>e2</span>, <span class='conditional'>IF</span> <span class='name'>alternateOf(e1,e2)</span> <span class='conditional'>THEN</span> <span class='name'>alternateOf(e2,e1)</span>.</p>
</div>
-<p>Similarly, specialization is a strict partial order: it is <a>irreflexive</a>,
+<p>
+
+<hr>
+
+<p id="specialization-irreflexive_text">Similarly, specialization is a strict partial order: it is <a>irreflexive</a>,
<a>anti-symmetric</a> and
<a>transitive</a>.</p>
@@ -816,9 +838,11 @@
<span class='name'>specializationOf(e2,e3)</span> <span class='conditional'>THEN</span> <span class='name'>specializationOf(e1,e3)</span>.</p>
</div>
-
-
- <p>Finally, if one entity specializes another, then they are also
+<p>
+
+<hr>
+
+ <p id="specialization-alternate_text">Finally, if one entity specializes another, then they are also
alternates:</p>
<div class='inference' id="specialization-alternate">
@@ -1093,6 +1117,9 @@
Attribute uniqueness constraints?
</div>
+<p>
+<hr>
+
<p id='entity-unique_text'> We assume that the various identified objects of PROV-DM have
unique statements describing them within a PROV instance.
</p>
@@ -1114,6 +1141,10 @@
derivation, revision, quotation. We should find a
way of saying this once concisely.
</div>
+
+<p>
+
+<hr>
<div id='generation-uniqueness_text'>
@@ -1145,7 +1176,11 @@
Invalidation uniqueness?
</div>
-<p>A generation can be used to indicate a generation time without having to specify the involved activity. A generation time is unique, as specified by the following constraint.<p>
+<p>
+
+<hr>
+
+<p id='unique-generation-time_text'>A generation can be used to indicate a generation time without having to specify the involved activity. A generation time is unique, as specified by the following constraint.<p>
<div class="note">
Seems redundant given generation-uniqueness
</div>
@@ -1156,7 +1191,24 @@
<span class='conditional'>IF</span> <span class="name">wasGeneratedBy(-;e, -, t1)</span> and <span class="name">wasGeneratedBy(-;e, -, t2)</span> hold, <span class='conditional'>THEN</span> <span class="name">t1</span>=<span class="name">t2</span>.</p>
</div>
-<p>An <a>activity start event</a> is the <a title="instantaneous event">instantaneous event</a> that marks the instant an activity starts. It allows for an optional time attribute. <span id="optional-start-time">Activities also allow for an optional start time attribute. If both are specified, they MUST be the same, as expressed by the following constraint.</span>
+<p>
+
+<hr>
+
+<p id='unique-invalidation-time_text'>An invalidation can be used to indicate an invalidation time without having to specify the involved activity. An invalidation time is unique, as specified by the following constraint.<p>
+
+<div class='constraint' id='unique-invalidation-time'>
+<p>Given an entity denoted by <span class="name">e</span> and
+two time instants <span class="name">t1</span> and <span
+class="name">t2</span>,
+<span class='conditional'>IF</span> <span class="name">wasInvalidatedBy(-;e, -, t1)</span> and <span class="name">wasInvalidatedBy(-;e, -, t2)</span> hold, <span class='conditional'>THEN</span> <span class="name">t1</span>=<span class="name">t2</span>.</p>
+</div>
+
+
+<p>
+<hr>
+
+<p id='unique-startTime_text'>An <a>activity start event</a> is the <a title="instantaneous event">instantaneous event</a> that marks the instant an activity starts. It allows for an optional time attribute. <span id="optional-start-time">Activities also allow for an optional start time attribute. If both are specified, they MUST be the same, as expressed by the following constraint.</span>
</p>
<div class='constraint' id='unique-startTime'>
@@ -1164,7 +1216,11 @@
<span class='conditional'>IF</span> <span class="name">activity(a,t1,t2)</span> and <span class="name">wasStartedBy(id;a,-,-,t)</span>, <span class='conditional'>THEN</span> <span class="name">t</span>=<span class="name">t1</span>.</p>
</div>
-<p>An <a>activity end event</a> is the <a title="instantaneous event">instantaneous event</a> that marks the instant an activity ends. It allows for an optional time attribute. <span id="optional-end-time">Activities also allow for an optional end time attribute. If both are specified, they MUST be the same, as expressed by the following constraint.</span>
+<p>
+
+<hr>
+
+<p id='unique-endTime_text'>An <a>activity end event</a> is the <a title="instantaneous event">instantaneous event</a> that marks the instant an activity ends. It allows for an optional time attribute. <span id="optional-end-time">Activities also allow for an optional end time attribute. If both are specified, they MUST be the same, as expressed by the following constraint.</span>
</p>
<div class='constraint' id='unique-endTime'>
@@ -1758,6 +1814,8 @@
Work on collections and on these constraints is deferred until after
the next working draft, so this section may not be stable.
</div>
+
+<hr>
<p id='membership-as-insertion_text'>Membership is a convenience notation, since it can be expressed in terms of an insertion into some collection. The membership definition is formalized by <a class="rule-ref" href="#membership-as-insertion"><span/></a>.</p>
@@ -1768,6 +1826,10 @@
<span class="name">derivedByInsertionFrom(c, c0, {(k1, v1), ...})</span>.</p>
</div>
+<p>
+
+<hr>
+
<p id='collection-unique-derivation_text'>A collection may be obtained by insertion or removal, or said to satisfy the membership relation.
To provide an interpretation of collections, PROV-DM
restricts one collection to be involved in a single derivation by insertion or removal, or to one membership relation.