--- a/model/ProvenanceModel.html Tue Dec 20 10:45:21 2011 +0000
+++ b/model/ProvenanceModel.html Tue Dec 20 11:18:35 2011 +0000
@@ -1163,7 +1163,7 @@
<p>One can assert an agent record or alternatively, one can infer an agent record
by its association with an activity. </p>
-<div class='constraint' id='association-agent'>
+<div class='inference' id='association-agent'>
<span class='conditional'>If</span> the records <span class="name">entity(e,attrs)</span>
and
<span class="name">wasAssociatedWith(a,e)</span> hold for some identifiers
@@ -1171,7 +1171,7 @@
the record <span class="name">agent(e,attrs)</span> also holds.
</div>
-<div class='issue'> Shouldn't we allow for entities (not agent) to be associated with an activity? Should we delete the constraint association-agent? <a href="http://www.w3.org/2011/prov/track/issues/203">ISSUE-203</a>.</div>
+<div class='issue'> Shouldn't we allow for entities (not agent) to be associated with an activity? Should we delete the inference association-agent? <a href="http://www.w3.org/2011/prov/track/issues/203">ISSUE-203</a>.</div>
</section>
@@ -1323,6 +1323,11 @@
</div>
-->
+<div class="structural-forward">
+See <a href="#generation-unicity">generation-unicity</a> for a structural constraint on generation records.
+</div>
+
+<!--
<p>A given entity record can be referred to in a single generation record in the scope of a given <a href="#record-Account">account</a>.
The rationale for this constraint is as follows.
If two activities sequentially set different values to some attribute by means of two different <a title="entity generation event">generation events</a>, then they generate distinct entities. Alternatively, for two activities to generate an entity simultaneously, they would require some synchronization by which they agree the entity is released for use; the end of this synchronization would constitute the actual generation of the entity, but is performed by a single activity. This unicity constraint is formalized as follows.
@@ -1333,7 +1338,7 @@
</div>
<div class='note'>TODO: Introduce the well-formed-ness constraint in a entirely separate section.</div>
-
+-->
</section>
@@ -1949,7 +1954,7 @@
<p>An precise-1 derivation record is richer than an imprecise-1 derivation record, itself, being more informative that an imprecise-n derivation record. Hence, the following implications hold.</p>
-<div class='constraint' id='derivation-implications'>
+<div class='inference' id='derivation-implications'>
Given two entity records denoted by <span class="name">e1</span> and <span class="name">e2</span>, <span class='conditional'>if</span> the assertion <span class="name">wasDerivedFrom(e2, e1, a, g2, u1, attrs)</span>
holds for some generation record identified by <span class="name">g2</span>, and usage record identified by <span class="name">u1</span>, then <span class="name">wasDerivedFrom(e2,e1,[prov:steps="1"] ∪ attrs)</span> also holds.<br>
@@ -2000,7 +2005,7 @@
is known to exist, though it does not need to be
asserted. This is formalized by the following inference rule,
referred to as <em>activity introduction</em>:</p>
-<div class='constraint' id="activity-introduction">
+<div class='inference' id="activity-introduction">
<span class='conditional'>If</span> <span class="name">wasDerivedFrom(e2,e1)</span> holds, <span class='conditional'>then</span> there exist an activity record identified by <span class="name">a</span>, a usage record identified by <span class="name">u</span>, and a generation record identified by <span class="name">g</span>
such that:
<pre class="codeexample">
@@ -2027,25 +2032,9 @@
of <span class="name">e1</span>.
</p>
-<div class="note">The following property holds for account where
-generation-unicity applies. Move it to separate section with all
-related material. </div>
-
-<p>A further inference is permitted from the imprecise-1 derivation record: </p>
-<div class='constraint' id='derivation-use'>
-<p>Given an activity record identified by <span class="name">pe</span>, entity records identified by <span class="name">e1</span> and <span class="name">e2</span>, and set of attribute-value pairs <span class="name">attrs2</span>,
-<span class='conditional'>if</span> <span class="name">wasDerivedFrom(e2,e1, [prov:steps="1"])</span> and <span class="name">wasGeneratedBy(e2,pe,attrs2)</span> hold, <span class='conditional'>then</span> <span class="name">used(pe,e1,attrs1)</span> also holds
-for some set of attribute-value pairs <span class="name">attrs1</span>.
+<div class="structural-forward">
+See <a href="#derivation-use">derivation-use</a> for a structural constraint on derivation records.
</div>
-<p>This inference is justified by the fact that the entity represented by entity record identified by <span class="name">e2</span> is generated by at most one activity in a given account (see <a href="#generation-unicity">generation-unicity</a>). Hence, this activity record is also the one referred to in the usage record of <span class="name">e1</span>.
-</p>
-
-
-
-<p>We note that the converse inference, does not hold.
-From <span class="name">wasDerivedFrom(e2,e1)</span> and <span class="name">used(pe,e1)</span>, one cannot
-derive <span class="name">wasGeneratedBy(e2,pe,attrs2)</span> because identifier <span class="name">e1</span> may occur in usage records referring to
-many activity records, but they may not be referred to in generation records containing identifier <span class="name">e2</span>.</p>
@@ -2412,9 +2401,10 @@
<p>In PROV-DM, an <dfn id="dfn-Account">account record</dfn> is a wrapper of records with a dual purpose: </p>
<ul>
-<li> It is the mechanism by which attribution of provenance can be assserted; it allows asserters to bundle up their assertions, and assert suitable attribution;
-<li> It provides a scoping mechanism for record identifiers and for some contraints (such as
- <a href="#generation-unicity">generation-unicity</a> and <a href="#derivation-use">derivation-use</a>).
+<li> It is the mechanism by which attribution of provenance can be assserted; it allows asserters to bundle up their assertions, and assert suitable attribution;</li>
+<li> It provides a scoping mechanism for record identifiers;</li>
+<li> It provides a scoping mechanism for structural contraints (such as
+ <a href="#generation-unicity">generation-unicity</a> and <a href="#derivation-use">derivation-use</a> discussed in Section <a href="#structural-constraints">structural-constraints</a>).</li>
</ul>
@@ -2491,6 +2481,8 @@
<p>Account records can be nested since an account record can occur among the records being wrapped by another account. </p>
+
+<!--
<p>
An account is said to be well-formed if
it satisfies the constraints <a href="#generation-unicity">generation-unicity</a> and <a href="#derivation-use">derivation-use</a>.</p>
@@ -2519,6 +2511,8 @@
<p>with identifier <span class="name">ex:acc2</span>, containing assertions by asserter by <span class="name">http://example.org/asserter2</span> stating that the entity represented by entity record identified by <span class="name">e0</span> was generated by an activity represented by activity record identified by <span class="name">a1</span> instead of <span class="name">a0</span> in the previous account <span class="name">ex:acc0</span>. If accounts <span class="name">ex:acc0</span> and <span class="name">ex:acc2</span> are merged together, the resulting set of records violates <a href="#generation-unicity">generation-unicity</a> if the two activities <span class="name">a0</span> and <span class="name">a1</span> are distinct.</p>
</div>
+-->
+
<p>Account records constitute a scope for record identifiers. Since accounts can be nested, scopes can also be nested; thus, the scope of record identifiers should be understood in the context of such nested scopes. When a record with an identifier occurs directly within an account, then its identifier denotes this record in the scope of this account, except in sub-accounts where records with the same identifier occur. </p>
<div class="anexample">
@@ -2543,6 +2537,10 @@
<p>The account record is the hook by which further meta information can be expressed about provenance, such as asserter, time of creation, signatures. The annotation mechanism can be used for this purpose, but how general meta-information is expressed is beyond the scope of this specification, except for asserters.</p>
+<div class="structural-forward">
+See Section <a href="#structural-constraints">structural-constraints</a> for a structural constraint on account records.
+</div>
+
</section>
@@ -2589,10 +2587,6 @@
</div>
-<div class='pending'>Asserter needs to be defined. This is <a href="http://www.w3.org/2011/prov/track/issues/51">ISSUE-51</a>.</div>
-
-
-<div class='pending'>Scope and Identifiers. This is <a href="http://www.w3.org/2011/prov/track/issues/81">ISSUE-81</a>.</div>
</section>
@@ -3586,13 +3580,71 @@
</section>
-<section id="account-constraints">
-<h3>PROV-DM Account Constraints</h3>
+<section id="structural-constraints">
+<h3>PROV-DM Structural Constraints</h3>
<div class="note">
-This section is in development and will group constraints associated with accounts here.
+This section, in development, is grouping all structural constraints.
</div>
+
+<p>A given entity record can be referred to in a single generation record in the scope of a given <a href="#record-Account">account</a>.
+The rationale for this constraint is as follows.
+If two activities sequentially set different values to some attribute by means of two different <a title="entity generation event">generation events</a>, then they generate distinct entities. Alternatively, for two activities to generate an entity simultaneously, they would require some synchronization by which they agree the entity is released for use; the end of this synchronization would constitute the actual generation of the entity, but is performed by a single activity. This unicity constraint is formalized as follows.
+
+<div class='constraint' id='generation-unicity'>Given an entity record denoted by <span class="name">e</span>, two activity records denoted by <span class="name">a1</span> and <span class="name">a2</span>, and two sets of attribute-value pairs <span class="name">attrs1</span> and <span class="name">attrs2</span>,
+<span class='conditional'>if</span> the records <span class="name">wasGeneratedBy(e,a1,attrs1)</span> and <span class="name">wasGeneratedBy(e,a2,attrs2)</span> exist in the scope of a given account,
+<span class='conditional'>then</span> <span class="name">a1</span>=<span class="name">a2</span> and <span class="name">attrs1</span>=<span class="name">attrs2</span>.
+</div>
+
+
+
+<p>A further inference is permitted from the imprecise-1 derivation record: </p>
+<div class='constraint' id='derivation-use'>
+<p>Given an activity record identified by <span class="name">pe</span>, entity records identified by <span class="name">e1</span> and <span class="name">e2</span>, and set of attribute-value pairs <span class="name">attrs2</span>,
+<span class='conditional'>if</span> <span class="name">wasDerivedFrom(e2,e1, [prov:steps="1"])</span> and <span class="name">wasGeneratedBy(e2,pe,attrs2)</span> hold, <span class='conditional'>then</span> <span class="name">used(pe,e1,attrs1)</span> also holds
+for some set of attribute-value pairs <span class="name">attrs1</span>.
+</div>
+<p>This inference is justified by the fact that the entity represented by entity record identified by <span class="name">e2</span> is generated by at most one activity in a given account (see <a href="#generation-unicity">generation-unicity</a>). Hence, this activity record is also the one referred to in the usage record of <span class="name">e1</span>.
+</p>
+
+
+
+<p>We note that the converse inference, does not hold.
+From <span class="name">wasDerivedFrom(e2,e1)</span> and <span class="name">used(pe,e1)</span>, one cannot
+derive <span class="name">wasGeneratedBy(e2,pe,attrs2)</span> because identifier <span class="name">e1</span> may occur in usage records referring to
+many activity records, but they may not be referred to in generation records containing identifier <span class="name">e2</span>.</p>
+
+
+<p>
+An account is said to be well-formed if
+it satisfies the constraints <a href="#generation-unicity">generation-unicity</a> and <a href="#derivation-use">derivation-use</a>.</p>
+
+<p> The union of two accounts is another account,
+containing the unions of their respective records, where
+ records with a same identifier should be understood according to constraint <a href="#identified-entity-in-account">identified-entity-in-account</a>. Well-formed
+accounts are not
+closed under union because the
+constraint <a href="#generation-unicity">generation-unicity</a> may no
+longer be satisfied in the resulting union. </p>
+
+<div class="anexample">
+<p>
+Indeed, let us consider another account record</p>
+<pre class="codeexample">
+account(ex:acc2,
+ http://example.org/asserter2,
+ entity(e0, [ prov:type="File", ex:path="/shared/crime.txt", ex:creator="Alice" ])
+ ...
+ activity(a1,t1,,[prov:type="createFile"])
+ ...
+ wasGeneratedBy(e0,a1,[ex:fct="create"])
+ ... )
+</pre>
+<p>with identifier <span class="name">ex:acc2</span>, containing assertions by asserter by <span class="name">http://example.org/asserter2</span> stating that the entity represented by entity record identified by <span class="name">e0</span> was generated by an activity represented by activity record identified by <span class="name">a1</span> instead of <span class="name">a0</span> in the previous account <span class="name">ex:acc0</span>. If accounts <span class="name">ex:acc0</span> and <span class="name">ex:acc2</span> are merged together, the resulting set of records violates <a href="#generation-unicity">generation-unicity</a> if the two activities <span class="name">a0</span> and <span class="name">a1</span> are distinct.</p>
+</div>
+
+
</section>