--- a/model/working-copy/prov-dm-constraints.html Wed Feb 15 07:16:17 2012 +0000
+++ b/model/working-copy/prov-dm-constraints.html Wed Feb 15 09:49:38 2012 +0000
@@ -1221,44 +1221,43 @@
<p>Section <a href="#section-time-event">section-time-event</a>
introduces a notion of <a title="event">instantaneous event</a>
marking changes in the world, in its activities and entities. PROV-DM
-identifies four kinds of <a title="event">instantaneous events</a>, namely <a>entity generation
-event</a>, <a>entity usage event</a>, <a>activity start event</a>
+identifies five kinds of <a title="event">instantaneous events</a>, namely <a>entity generation
+event</a>, <a>entity usage event</a>, <a>entity destruction event</a>, <a>activity start event</a>
and <a>activity end event</a>. PROV-DM adopts Lamport's clock
assumptions [[CLOCK]] in the form of a reflexive, transitive partial order <a>follows</a>
(and its inverse <a>precedes</a>) between <a title="event">instantaneous events</a>. Furthermore,
PROV-DM assumes the existence of a mapping from <a title="event">instantaneous events</a> to time clocks,
though the actual mapping is not in scope of this specification.</p>
-<p>Given that provenance records offer a description of past entities
-and activities, to be meaningful provenance records MUST
+<p>Given that provenance consists of a description of past entities
+and activities, to be meaningful provenance descriptions MUST
satisfy <em>instantaneous event ordering constraints</em>, which we introduce in
this section. For instance, an entity can only be used after it was
generated; hence, we say that an entity's <a title="entity generation
event">generation event</a> precedes any of this
entity's <a title="entity usage event">usage event</a>. Should this
ordering constraint be proven invalid, the associated generation and
-usage records could not be credible. The rest of this section defines
-the <dfn>temporal interpretation</dfn> of provenance records as the
-set of instantaneous event ordering constraints associated with provenance
-records. </p>
+usage could not be credible. The rest of this section defines
+the <dfn>temporal interpretation</dfn> of provenance descriptions as a
+set of instantaneous event ordering constraints. </p>
<p>PROV-DM also allows for time observations to be inserted in
-specific provenance records, for each of the four kinds
+specific provenance descriptions, for each of the four kinds
of <a title="event">instantaneous events</a> introduced in this specification. The
presence of a time observation for a given <a>instantaneous event</a> fixes the
mapping of this <a>instantaneous event</a> to the timeline. The presence of time
-information in a provenance record instantiates the ordering constraint with
+information in a provenance description instantiates the ordering constraint with
that time information. It is expected that such instantiated
constraint can help corroborate provenance information. We anticipate
-that verification algorithms could be developed though this
+that verification algorithms could be developedm, though this
verification is outside the scope of this specification.
</p>
<p>The following figure summarizes the ordering constraints in a
graphical manner. For each subfigure, an event time line points to the
right. Activities are represented by rectangles, whereas entities are
-represented by circles. Usage, generation and derivation records are
+represented by circles. Usage, generation and derivation are
represented by the corresponding edges between entities and
activities. The four kind of <a title="event">instantaneous events</a> are represented by vertical
dotted lines (adjacent to the vertical sides of an activity's
@@ -1274,14 +1273,14 @@
</div>
-<p>The mere existence of an activity assertion entails some <a>event</a> ordering in the world, since an <a>activity start event</a> always <a>precedes</a> the corresponding <a>activity end
+<p>The mere existence of an activity entails some <a>event</a> ordering in the world, since an <a>activity start event</a> always <a>precedes</a> the corresponding <a>activity end
event</a>. This is
illustrated by Subfigure <a href="#constraint-summary">constraint-summary</a> (a) and expressed by constraint <a href="#start-precedes-end">start-precedes-end</a>.</p>
-<div class='interpretation' id='start-precedes-end'> The following ordering constraint holds for any activity record: the
+<div class='interpretation' id='start-precedes-end'> The following ordering constraint holds for any activity: the
<a title="activity start event">start event</a> <a>precedes</a> the <a title="activity end event">end event</a>.</div>
-<p> Assertion of a usage record and a generation record for a given entity implies ordering of <a title="event">events</a> in the world, since the <a title="entity generation
+<p> A usage and a generation for a given entity implies ordering of <a title="event">events</a> in the world, since the <a title="entity generation
event">generation event</a> had to precede the <a title="entity usage event">usage event</a>. This is
illustrated by Subfigure <a href="#constraint-summary">constraint-summary</a> (b) and expressed by constraint <a href="#generation-precedes-usage">generation-precedes-usage</a>.</p>
@@ -1289,31 +1288,32 @@
<a>precedes</a> any of its <a title="entity usage event">usages</a>.
</div>
-<p>The assertion of a usage record implies ordering of <a title="event">events</a> in the world, since the corresponding event had to occur during the associated activity. This is
+<p>A usage implies ordering of <a title="event">events</a> in the world, since the <a title="entity usage event">usage event</a> had to occur during the associated activity. This is
illustrated by Subfigure <a href="#constraint-summary">constraint-summary</a> (c) and expressed by constraint <a href="#usage-within-activity">usage-within-activity</a>.</p>
-<div class='interpretation' id='usage-within-activity'>Given an activity record identified by <span class="name">a</span>, an entity record identified by <span class="name">e</span>, a set
+<div class='interpretation' id='usage-within-activity'>Given an activity with identifier <span class="name">a</span>, an entity with identifier <span class="name">e</span>, a set
of attribute-value pairs <span class="name">attrs</span>, and optional time <span class="name">t</span>, <span class='conditional'>if</span>
assertion <span class="name">used(a,e,attrs)</span> or <span class="name">used(a,e,attrs,t)</span> holds, <span class='conditional'>then</span> the following ordering constraint holds:
- the <a title="entity usage event">usage</a> of the entity represented by entity record identified by <span class="name">e</span> <a>precedes</a> the <a title="activity end event">end</a> of
-activity represented by record identified by <span class="name">a</span> and <a>follows</a> its <a title="activity start event">start</a>.
+ the <a title="entity usage event">usage</a> of the entity denoted by <span class="name">e</span> <a>precedes</a> the <a title="activity end event">end</a> of
+activity denoted by <span class="name">a</span> and <a>follows</a> its <a title="activity start event">start</a>.
</div>
-<p>The assertion of a generation record implies ordering of <a title="event">events</a> in the world, since the corresponding event had to occur during the associated activity. This is
+<p>A generation implies ordering of <a title="event">events</a> in the world, since the <a title="entity generation event">generation event</a> had to occur during the associated activity. This is
illustrated by Subfigure <a href="#constraint-summary">constraint-summary</a> (d) and expressed by constraint <a href="#generation-within-activity">generation-within-activity</a>.</p>
-<div class='interpretation' id='generation-within-activity'><span class='conditional'>If</span> an assertion <span class="name">wasGeneratedBy(x,a,attrs)</span> or <span
-class="name">wasGeneratedBy(x,a,attrs,t)</span> holds, <span class='conditional'>then</span> the following ordering constraint also holds: the <a title="entity generation
-event">generation</a> of the entity denoted by <span class="name">x</span> <a>precedes</a> the <a title="activity end event">end</a>
-of <span class="name">a</span> and <a>follows</a> the <a title="activity start event">start</a> of <span class="name">a</span>.
+<div class='interpretation' id='generation-within-activity'>Given an activity with identifier <span class="name">a</span>, an entity with identifier <span class="name">e</span>, a set
+of attribute-value pairs <span class="name">attrs</span>, and optional time <span class="name">t</span>, <span class='conditional'>if</span> <span class="name">wasGeneratedBy(e,a,attrs)</span> or <span
+class="name">wasGeneratedBy(e,a,attrs,t)</span> holds, <span class='conditional'>then</span> the following ordering constraint also holds: the <a title="entity generation
+event">generation</a> of the entity denoted by <span class="name">e</span> <a>precedes</a> the <a title="activity end event">end</a>
+of activity <span class="name">a</span> and <a>follows</a> the <a title="activity start event">start</a> of <span class="name">a</span>.
</div>
-<p>If a derivation record holds for <span class="name">e2</span> and <span class="name">e1</span>, then
+<p>If there is a derivation between <span class="name">e2</span> and <span class="name">e1</span>, then
this means that the entity <span class="name">e1</span> had some form of influence on the entity <span class="name">e2</span>; for this to be possible, some event ordering must be satisfied.
First, we consider one-activity derivations. In that case, the <a title="entity usage event">usage</a> of <span class="name">e1</span> has to precede the <a title="entity generation
event">generation</a> of <span class="name">e2</span>.
@@ -1322,9 +1322,9 @@
href="#derivation-usage-generation-ordering">derivation-usage-generation-ordering</a>.</p>
-<div class='interpretation' id='derivation-usage-generation-ordering'>Given an activity record identified by <span class="name">a</span>, entity records identified by <span
-class="name">e1</span> and <span class="name">e2</span>, generation record identified by <span class="name">g2</span>, and usage record identified by <span class="name">u1</span>, <span
-class='conditional'>if</span> the record <span class="name">wasDerivedFrom(e2,e1,a,g2,u1,attrs)</span>
+<div class='interpretation' id='derivation-usage-generation-ordering'>Given an activity with identifier <span class="name">a</span>, entities with identifier <span
+class="name">e1</span> and <span class="name">e2</span>, a generation identified by <span class="name">g2</span>, and a usage identified by <span class="name">u1</span>, <span
+class='conditional'>if</span> <span class="name">wasDerivedFrom(e2,e1,a,g2,u1,attrs)</span>
or <span class="name">wasDerivedFrom(e2,e1,[prov:steps="single"] ∪ attrs)</span> holds, <span class='conditional'>then</span>
the following ordering constraint holds:
the <a title="entity usage event">usage</a>
@@ -1332,13 +1332,13 @@
the entity denoted by <span class="name">e2</span>.
</div>
-<p>For imprecise-n derivations, a similar constraint exists, but in this case, no usage record can be inferred for <span class="name">e1</span>. Instead, the constraint refers to its
+<p>For imprecise-n derivations, a similar constraint exists, but in this case, no usage can be inferred for <span class="name">e1</span>. Instead, the constraint refers to its
generation event, as
illustrated by Subfigure <a href="#constraint-summary">constraint-summary</a> (f) and expressed by constraint <a
href="#derivation-generation-generation-ordering">derivation-generation-generation-ordering</a>.</p>
<div class='interpretation' id='derivation-generation-generation-ordering'>
-Given two entity records denoted by <span class="name">e1</span> and <span class="name">e2</span>, <span class='conditional'>if</span> the record <span
+Given two entities denoted by <span class="name">e1</span> and <span class="name">e2</span>, <span class='conditional'>if</span> <span
class="name">wasDerivedFrom(e2,e1,[prov:steps="any"] ∪ attrs)</span>
holds, <span class='conditional'>then</span> the following ordering constraint holds:
the <a title="entity generation event">generation event</a> of the entity denoted by <span class="name">e1</span> <a>precedes</a> the <a title="entity generation event">generation event</a>
@@ -1353,30 +1353,30 @@
imprecise-n derivation, nothing is known about the usage of <span class="name">e1</span>,
since there is no associated activity.</p>
-<p>The assertion of an information flow ordering record between two activities of <span class="name">a1</span> and <span class="name">a2</span> also implies ordering of <a
+<p> Information flow ordering between two activities <span class="name">a1</span> and <span class="name">a2</span> also implies ordering of <a
title="event">events</a> in the world, since some entity must have been generated by the former and used by the later, which implies that the start event of <span class="name">a1</span>
cannot follow the end event of <span class="name">a2</span>. This is
illustrated by Subfigure <a href="#constraint-summary">constraint-summary</a> (g) and expressed by constraint <a href="#wasInformedBy-ordering">wasInformedBy-ordering</a>.</p>
<div class='interpretation' id='wasInformedBy-ordering'>
-Given two activity records denoted by <span class="name">a1</span> and <span class="name">a2</span>, <span class='conditional'>if</span> the record <span
+Given two activities denoted by <span class="name">a1</span> and <span class="name">a2</span>, <span class='conditional'>if</span> <span
class="name">wasInformedBy(a2,a1)</span>
holds, <span class='conditional'>then</span> the following ordering constraint holds:
-the <a title="activity start event">start event</a> of the activity record denoted by <span class="name">a1</span> <a>precedes</a> the <a title="activity end event">end event</a> of
-the activity record denoted by <span class="name">a2</span>.
+the <a title="activity start event">start event</a> of the activity denoted by <span class="name">a1</span> <a>precedes</a> the <a title="activity end event">end event</a> of
+the activity denoted by <span class="name">a2</span>.
</div>
-<p>The assertion of a control flow ordering record between two activities of <span class="name">a1</span> and <span class="name">a2</span> also implies ordering of <a
+<p>Control flow ordering between two activities <span class="name">a1</span> and <span class="name">a2</span> also implies ordering of <a
title="event">events</a> in the world, since <span class="name">a1</span> must have been active before <span class="name">a2</span> started. This is
illustrated by Subfigure <a href="#constraint-summary">constraint-summary</a> (h) and expressed by constraint <a href="#wasStartedBy-ordering">wasStartedBy-ordering</a>.</p>
<div class='interpretation' id='wasStartedBy-ordering'>
-Given two activity records denoted by <span class="name">a1</span> and <span class="name">a2</span>, <span class='conditional'>if</span> the record <span
+Given two activities denoted by <span class="name">a1</span> and <span class="name">a2</span>, <span class='conditional'>if</span> <span
class="name">wasStartedBy(a2,a1)</span>
holds, <span class='conditional'>then</span> the following ordering constraint holds: the
-<a title="activity start event">start</a> event of the activity record denoted by <span class="name">a1</span> <a>precedes</a> the <a title="activity start event">start event</a> of
-the activity record denoted by <span class="name">a2</span>.
+<a title="activity start event">start</a> event of the activity denoted by <span class="name">a1</span> <a>precedes</a> the <a title="activity start event">start event</a> of
+the activity denoted by <span class="name">a2</span>.
</div>
<div class='issue'>In the following, we assume that we can talk about the end of an entity (or agent)
@@ -1400,7 +1400,7 @@
<div class='interpretation' id='wasStartedByAgent-ordering'>
-Given an activity denoted by <span class="name">a</span> and an agent denoted by <span class="name">ag</span>, <span class='conditional'>if</span> the record <span
+Given an activity denoted by <span class="name">a</span> and an agent denoted by <span class="name">ag</span>, <span class='conditional'>if</span> <span
class="name">wasStartedBy(a,ag)</span>
holds, <span class='conditional'>then</span> the following ordering constraints hold: the
<a title="activity start event">start</a> event of the activity denoted by <span class="name">a</span> <a>follows</a> the <a title="entity generation event">generation event</a> for agent denoted by <span class="name">ag</span>, and
@@ -1415,7 +1415,7 @@
<div class='interpretation' id='wasAssociatedWith-ordering'>
-Given an activity denoted by <span class="name">a</span> and an agent denoted by <span class="name">ag</span>, <span class='conditional'>if</span> the record <span
+Given an activity denoted by <span class="name">a</span> and an agent denoted by <span class="name">ag</span>, <span class='conditional'>if</span> <span
class="name">wasAssociatedWith(a,ag)</span>
holds, <span class='conditional'>then</span> the following ordering constraints hold: the
<a title="activity start event">start</a> event of the activity denoted by <span class="name">a</span>