* Added constraint css
authorJames Cheney <jcheney@inf.ed.ac.uk>
Thu, 18 Aug 2011 16:01:52 +0100
changeset 170 f5343fac3df5
parent 169 4a4e5d5bf76a
child 171 09ac58672f56
* Added constraint css
* Added cross-references between formal model and provenance model
model/ProvenanceModel.html
model/extra.css
ontology/ProvenanceFormalModel.html
--- a/model/ProvenanceModel.html	Wed Aug 17 15:10:22 2011 +0100
+++ b/model/ProvenanceModel.html	Thu Aug 18 16:01:52 2011 +0100
@@ -465,7 +465,9 @@
 
 
 
-<p>From the assertion of a process execution, one can infer that the start precedes the end of the represented activity. </p>
+<div class='constraint'><a name="PIL:0001">From the assertion of a process execution, one can infer that the
+start precedes the end of the represented activity.</a> [<a
+href="../ontology/ProvenanceFormalModel.html#PIL:0001">PIL:0001</a>] </div>
 
 <div class='pending'>Should process execution be defined as a subclass of BOB. This is <a href="http://www.w3.org/2011/prov/track/issues/66">ISSUE-66</a>.</div>
 </section> 
@@ -500,18 +502,20 @@
 If two process executions sequentially set different values to some attribute by means of two different generate events, then they generate distinct entities. Alternatively,  for two process executions 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 process execution. </p>
 </p>
 
-<p>Given a process execution <b>pe</b>, entity <b>e</b>, role <b>r</b>, and optional time <b>t</b>,
+<div class='constraint'><a name="PIL:0002">Given a process execution <b>pe</b>, entity <b>e</b>, role <b>r</b>, and optional time <b>t</b>,
 if the assertion <b>isGeneratedBy(e,pe,r)</b>
 or <b>isGeneratedBy(e,pe,r,t)</b> holds, the values of <em>some</em> of <b>e</b>'s
 attributes are determined by the activity denoted by <b>pe</b> and the
 entities used by <b>pe</b>.
-Only some (possibly none) of the attributes values  may be determined since, in an open world, not all used entities may have been asserted.
-</p>
+Only some (possibly none) of the attributes values  may be determined
+since, in an open world, not all used entities may have been
+asserted.</a>  [<a href="../ontology/ProvenanceFormalModel.html#PIL:0002">PIL:0002</a>]
+</div>
 
-<p>Given an assertion <b>isGeneratedBy(x,pe,r)</b> or <b>isGeneratedBy(x,pe,r,t)</b>, one can
+<div class='constraint'><a name="PIL:0003">Given an assertion <b>isGeneratedBy(x,pe,r)</b> or <b>isGeneratedBy(x,pe,r,t)</b>, one can
 infer that the generation of the thing denoted by <b>x</b> precedes the end
-of <b>pe</b> and follows the beginning of <b>pe</b>. 
-</p> 
+of <b>pe</b> and follows the beginning of <b>pe</b>.</a> [<a href="../ontology/ProvenanceFormalModel.html#PIL:0003">PIL:0003</a>]
+</div> 
 
 
 <div class='pending'>Need to say identifiable activity. This is <a href="http://www.w3.org/2011/prov/track/issues/39">ISSUE-39</a>. The qualifier 'identifiable' is said to be implicit in section 4. </div>
@@ -558,19 +562,22 @@
 
 
 
-<p>
+<div class='constraint'><a name="PIL:0005">
 Given a process execution <b>pe</b>, entity <b>e</b>, role <b>r</b>, and optional time <b>t</b>, if
  assertion <b>uses(pe,e,r)</b> or <b>uses(pe,e,r,t)</b> holds, 
-the existence of the value of an attribute of <b>e</b>' is a pre-condition for the activity denoted by <b>pe</b> to terminate.</p>
+the existence of the value of an attribute of <b>e</b>' is a
+pre-condition for the activity denoted by <b>pe</b> to terminate.</a>
+[<a href="../ontology/ProvenanceFormalModel.html#PIL:0005">PIL:0005</a>]</div>
 
 
 
-<p>Given a process execution <b>pe</b>, entity <b>e</b>, role <b>r</b>, and optional time <b>t</b>, if
+<div class='constraint'><a name="PIL:0006">Given a process execution <b>pe</b>, entity <b>e</b>, role <b>r</b>, and optional time <b>t</b>, if
  assertion <b>uses(pe,e,r)</b> or <b>uses(pe,e,r,t)</b> holds, one can
 infer that the use of the thing denoted by <b>e</b> precedes the end
 of <b>pe</b> and follows the beginning of <b>pe</b>. Furthermore, we
 can infer that the generation of the thing denoted by <b>e</b> always precedes
-its use.  </p>
+its use.</a> 
+[<a href="../ontology/ProvenanceFormalModel.html#PIL:0006">PIL:0006</a>] </div>
 
 
 <div class='issue'>Should we define a taxonomy of use? This is <a href="http://www.w3.org/2011/prov/track/issues/23">ISSUE-23</a>.</div>
@@ -616,7 +623,9 @@
 </p>
 
 <div class="inference">
-If <b>isDerivedFrom(e2,e1,pe,r2,r1)</b> holds, then <b>isGeneratedBy(e2,pe,r2)</b> and <b>uses(pe,e1,r1)</b> also hold.
+<a name="PIL:0010">If <b>isDerivedFrom(e2,e1,pe,r2,r1)</b> holds, then
+  <b>isGeneratedBy(e2,pe,r2)</b> and <b>uses(pe,e1,r1)</b> also
+  hold. </a> [<a href=""../ontology/ProvenanceFormalModel.html#PIL:0010">PIL:0010</a>]
 </div>
 
 
@@ -631,9 +640,10 @@
 <p>The compact version has the same meaning as the fully formed process-execution linked derivation, except that a process execution is known to exist, though it does not need to be asserted.
 This is formalized by the following inference rule, referred to as <em>process execution introduction</em>:<br/>
 <div class='inference'>
+  <a name="PIL:0009">
 If <b>isDerivedFrom(e2,e1)</b> holds, then there exists a process execution <b>pe</b>, and roles <b>r1</b>,<b>r2</b>,
 such that:
-  <b>isGeneratedBy(e2,pe,r2)</b> and <b>uses(pe,e1,r1)</b>.
+  <b>isGeneratedBy(e2,pe,r2)</b> and <b>uses(pe,e1,r1)</b>. [<a href="../ontology/ProvenanceFormalModel.html#PIL:0009">PIL:0009</a>]
 </div></p>
 
 
@@ -642,22 +652,23 @@
 <p>If <b>e2</b> is derived from <b>e1</b>, then 
 this means that the thing represented by <b>e1</b> has an influence on the thing represented by <b>e2</b>, which is captured by a dependency between their attribute values; it also implies temporal ordering. These are specified as follows:</p>
 
-<p>Given a process execution <b>pe</b>, entities <b>e1</b> and <b>e2</b>, roles <b>r1</b> and <b>r2</b>, if the assertion <b>isDerivedFrom(e2,e1,pe,r2,r1)</b>
+<div class='constraint'><a name="PIL:0007">Given a process execution <b>pe</b>, entities <b>e1</b> and <b>e2</b>, roles <b>r1</b> and <b>r2</b>, if the assertion <b>isDerivedFrom(e2,e1,pe,r2,r1)</b>
 or <b>isDerivedFrom(e2,e1)</b> holds, if and only if:
  the values of some attributes
 of <b>e2</b> are partly or fully determined by the values of some
-attributes of <b>e1</b>.</li>
+attributes of <b>e1</b>.</a> [<a
+  href="../ontology/ProvenanceFormalModel.html#PIL:0007">PIL:0007</a>] </div>
 
 <div class='note'>Should this dependency of attributes be made explicit as argument of the derivation? By making it explicit, we would allow someone to verify the validity of the derivation.</div>
-</p>
 
 
-<p>Given a process execution <b>pe</b>, entities <b>e1</b> and <b>e2</b>, roles <b>r1</b> and <b>r2</b>, if the assertion <b>isDerivedFrom(e2,e1,pe,r2,r1)</b>
+
+<div class='constraint'><a name="PIL:0008">Given a process execution <b>pe</b>, entities <b>e1</b> and <b>e2</b>, roles <b>r1</b> and <b>r2</b>, if the assertion <b>isDerivedFrom(e2,e1,pe,r2,r1)</b>
 or <b>isDerivedFrom(e2,e1)</b> holds, then
 the use
 of characterized thing denoted by <b>e1</b> precedes the generation of
-the characterized thing denoted by <b>e2</b>.
-</p>
+the characterized thing denoted by <b>e2</b>.</a> [<a href="../ontology/ProvenanceFormalModel.html#PIL:0008">PIL:0008</a>]
+</div>
 
 
 
@@ -681,9 +692,10 @@
 
 <p>A further inference is permitted from the compact version of derivation: 
 <div class='inference'>
-Given a process execution <b>pe</b>, entities <b>e1</b> and <b>e2</b>, and role <b>r2</b>,
+<a name="PIL:0011">Given a process execution <b>pe</b>, entities <b>e1</b> and <b>e2</b>, and role <b>r2</b>,
 if <b>isDerivedFrom(e2,e1)</b> and <b>isGeneratedBy(e2,pe,r2)</b> hold, then there exists a role <b>r1</b>,
-such that <b>uses(pe,e1,r1)</b> also holds.
+such that <b>uses(pe,e1,r1)</b> also holds.</a>
+  [<a href="../ontology/ProvenanceFormalModel.html#PIL:0011">PIL:0011</a>]
 </div>
 This inference is justified by the fact that <b>e2</b> is generated by at most one process execution. Hence,  this process execution is also the one that uses <b>e1</b>.
 </p>
@@ -746,7 +758,7 @@
 
 <p>
 If <b>isDerivedFrom(e2,e1)</b> holds because attribute <b>a2.1</b> of <b>e2</b> is determined by attribute <b>a1.1</b> of <b>e1</b>,
-and if <b>isDerivedFrom(e3,e2)</b> holds because attribute <b>a3.1</b>of <b>e3</b> is determined by  attribute <b>a2.2</b> of <b>e1</b>, it is not necessary the case that an attribute of <b>e3</b> is determined by an attribute of <b>e1</b>, so, an asserter may not be able to assert <b>isDerivedFrom(e3,e1)</b>.  Hence, constraints on attributes invalidate transitivit in the general case.
+and if <b>isDerivedFrom(e3,e2)</b> holds because attribute <b>a3.1</b>of <b>e3</b> is determined by  attribute <b>a2.2</b> of <b>e1</b>, it is not necessary the case that an attribute of <b>e3</b> is determined by an attribute of <b>e1</b>, so, an asserter may not be able to assert <b>isDerivedFrom(e3,e1)</b>.  Hence, constraints on attributes invalidate transitivity in the general case.
 </p>
 
 <p>However, there is sense that <b>e3</b> still depends on <b>e1</b>, since <b>e3</b> could not be generated without <b>e1</b> existing. Hence, we introduce a weaker notion of derivation, which is transitive.</p>
--- a/model/extra.css	Wed Aug 17 15:10:22 2011 +0100
+++ b/model/extra.css	Thu Aug 18 16:01:52 2011 +0100
@@ -55,3 +55,21 @@
     background: #fff;
     padding:    3px 1em;
 }
+
+.constraint {
+    padding:    1em;
+    margin: 1em 0em 0em;
+    border: 1px solid #00f;
+    background: #fff;
+}
+
+.constraint::before {
+    content:    "Constraint";
+    display:    block;
+    width:  150px;
+    margin: -1.5em 0 0.5em 0;
+    font-weight:    bold;
+    border: 1px solid #00f;
+    background: #fff;
+    padding:    3px 1em;
+}
--- a/ontology/ProvenanceFormalModel.html	Wed Aug 17 15:10:22 2011 +0100
+++ b/ontology/ProvenanceFormalModel.html	Thu Aug 18 16:01:52 2011 +0100
@@ -305,17 +305,55 @@
   Provenance Model, to make it easier to keep the definitions
   consistent (and ensure we don't forget some properties).
   </div>
-<ul><li> "From the assertion of a process execution, one can infer that the start precedes the end of the represented activity. "
-</li><li> "Given an assertion isGeneratedBy(x,pe,r) or isGeneratedBy(x,pe,r,t), the activity denoted by pe and the entities used by pe dermine values of some of x's attributes."
-</li><li>"Given an assertion isGeneratedBy(x,pe,r) or isGeneratedBy(x,pe,r,t), one can infer that the generation of the entity denoted by x precedes the end of pe and follows the beginning of pe. "
-</li><li> "Use represents the consumption of a characterized entity by an activity."
+<ul><li> <a name="PIL:0001" href="#PIL:0001">PIL:0001</a> "From the
+  assertion of a process execution, one can infer that the start
+  precedes the end of the represented activity." (<a href="../model/ProvenanceModel.html#PIL:0001">link</a>)
+</li><li> <a name="PIL:0002" href="#PIL:0002">PIL:0002</a> "Given a process execution <b>pe</b>, entity <b>e</b>, role <b>r</b>, and optional time <b>t</b>,
+if the assertion <b>isGeneratedBy(e,pe,r)</b>
+or <b>isGeneratedBy(e,pe,r,t)</b> holds, the values of <em>some</em> of <b>e</b>'s
+attributes are determined by the activity denoted by <b>pe</b> and the
+entities used by <b>pe</b>.
+Only some (possibly none) of the attributes values  may be determined
+since, in an open world, not all used entities may have been
+asserted."
+ (<a href="../model/ProvenanceModel.html#PIL:0002">link</a>)
+</li><li><a name="PIL:0003" href="#PIL:0003">PIL:0003</a> "Given an assertion <b>isGeneratedBy(x,pe,r)</b> or <b>isGeneratedBy(x,pe,r,t)</b>, one can
+infer that the generation of the thing denoted by <b>x</b> precedes the end
+of <b>pe</b> and follows the beginning of <b>pe</b> "
+ (<a href="../model/ProvenanceModel.html#PIL:0003">link</a>)
 
-</li><li> "Given an assertion uses(pe,x,r) or uses(pe,x,r,t), at least one value of x's attributes is a pre-condition for the activity denoted by pe to terminate."
-</li><li> "Given an assertion uses(pe,x,r) or uses(pe,x,r,t), one can infer that the use of the entity denoted by x precedes the end of pe and follows the beginning of pe. Furthermore, we can infer that the generation of the entity x always precedes its use. * "From an assertion isDerivedFrom(B,A), the values of some attributes of B are at least partially determined by the values of some attributes of A."
-</li><li> "Given an assertion isDerivedFrom(B,A), one can infer that the use of characterized entity denoted by A precedes the generation of the characterized entity denoted by B. "
-</li><li> "if isDerivedFrom(e1,e0) holds, then there exists a process execution pe, and roles r0,r1, such that: isGeneratedBy(e1,pe,r1) and uses(pe,e0,r0)."
-</li><li> "The relationship isDerivedFrom is transitive. "
-</li><li> "The relationship isDerivedFrom+ is the transitive closure of isDerivedFrom."
+</li><li><a name="PIL:0004" href="#PIL:0004">PIL:0004</a> "Use
+represents the consumption of a characterized entity by an activity."
+(Defunct.)
+
+</li><li><a name="PIL:0005" href="#PIL:0005">PIL:0005</a> "Given a process execution <b>pe</b>, entity <b>e</b>, role <b>r</b>, and optional time <b>t</b>, if
+ assertion <b>uses(pe,e,r)</b> or <b>uses(pe,e,r,t)</b> holds, 
+the existence of the value of an attribute of <b>e</b>' is a pre-condition for the activity denoted by <b>pe</b> to terminate."  (<a href="../model/ProvenanceModel.html#PIL:0005">link</a>)
+</li><li><a name="PIL:0006" href="#PIL:0006">PIL:0006</a> "Given a process execution <b>pe</b>, entity <b>e</b>, role <b>r</b>, and optional time <b>t</b>, if
+ assertion <b>uses(pe,e,r)</b> or <b>uses(pe,e,r,t)</b> holds, one can
+infer that the use of the thing denoted by <b>e</b> precedes the end
+of <b>pe</b> and follows the beginning of <b>pe</b>. Furthermore, we
+can infer that the generation of the thing denoted by <b>e</b> always precedes
+its use."  (<a href="../model/ProvenanceModel.html#PIL:0006">link</a>)
+</li><li> <a name="PIL:0007" href="#PIL:0007">PIL:0007</a> "Given a process execution <b>pe</b>, entities <b>e1</b> and <b>e2</b>, roles <b>r1</b> and <b>r2</b>, if the assertion <b>isDerivedFrom(e2,e1,pe,r2,r1)</b>
+or <b>isDerivedFrom(e2,e1)</b> holds, if and only if:
+ the values of some attributes
+of <b>e2</b> are partly or fully determined by the values of some
+attributes of <b>e1</b>."  (<a href="../model/ProvenanceModel.html#PIL:0007">link</a>)
+</li><li><a name="PIL:0008" href="#PIL:0008">PIL:0008</a> "Given a process execution <b>pe</b>, entities <b>e1</b> and <b>e2</b>, roles <b>r1</b> and <b>r2</b>, if the assertion <b>isDerivedFrom(e2,e1,pe,r2,r1)</b>
+or <b>isDerivedFrom(e2,e1)</b> holds, then
+the use
+of characterized thing denoted by <b>e1</b> precedes the generation of
+the characterized thing denoted by <b>e2</b>."  (<a href="../model/ProvenanceModel.html#PIL:0008">link</a>)
+</li><li><a name="PIL:0009" href="#PIL:0009">PIL:0009</a> "If <b>isDerivedFrom(e2,e1)</b> holds, then there exists a process execution <b>pe</b>, and roles <b>r1</b>,<b>r2</b>,
+such that:
+  <b>isGeneratedBy(e2,pe,r2)</b> and <b>uses(pe,e1,r1)</b>."  (<a href="../model/ProvenanceModel.html#PIL:0009">link</a>)
+</li><li><a name="PIL:0010" href="#PIL:0010">PIL:0010</a> "If <b>isDerivedFrom(e2,e1,pe,r2,r1)</b> holds, then <b>isGeneratedBy(e2,pe,r2)</b> and <b>uses(pe,e1,r1)</b> also hold." (<a href="../model/ProvenanceModel.html#PIL:0010">link</a>)
+</li><li><a name="PIL:0011" href="#PIL:0011">PIL:0011</a> "Given a process execution <b>pe</b>, entities <b>e1</b> and <b>e2</b>, and role <b>r2</b>,
+if <b>isDerivedFrom(e2,e1)</b> and <b>isGeneratedBy(e2,pe,r2)</b> hold, then there exists a role <b>r1</b>,
+such that <b>uses(pe,e1,r1)</b> also holds." (<a href="../model/ProvenanceModel.html#PIL:0011">link</a>)
+</li><li><a name="PIL:XXXX" href="#PIL:XXXX">PIL:XXXX</a> "Template
+ for more constraints" (<a href="../model/ProvenanceModel.html#PIL:XXXX">link</a>)
 </li><li> Various things involving IVP-of
 </li></ul>