--- a/model/working-copy/wd5-prov-dm-constraints-revised.html Mon Apr 16 17:30:36 2012 +0100
+++ b/model/working-copy/wd5-prov-dm-constraints-revised.html Mon Apr 16 17:50:41 2012 +0100
@@ -384,7 +384,7 @@
<p> Inferences have the following general form:
<div class='inference' id='inference-example'>
<span class='conditional'>IF</span> hyp_1 and ... and
-hyp_k <span class='conditional\'>THEN</span> there exists a_1,..., a_m such that conclusion_1 ... conclusion_n.
+hyp_k <span class='conditional'>THEN</span> there exists a_1,..., a_m such that conclusion_1 ... conclusion_n.
</div>
This means that if provenance expressions matching hyp_1... hyp_k
@@ -402,7 +402,7 @@
<p> Definitions have the following general form:
<div class='definition' id='definition-example'>
- defined_exp holds <span class='conditional\'>IF AND ONLY IF </span>
+ defined_exp holds <span class='conditional'>IF AND ONLY IF </span>
there exists a_1,..., a_m such that defining_exp_1 ... defining_exp_n.
</div>
@@ -440,7 +440,7 @@
<div class='definition' id='wasInformedBy-definition'>Given two activities identified by <span class="name">a1</span> and <span class="name">a2</span>,
<span class="name">wasInformedBy(a2,a1)</span>
-holds <span class='conditional'>if and only if</span>
+holds <span class='conditional'>IF AND ONLY IF</span>
there is an entity with some identifier <span class="name">e</span> and some sets of attribute-value pairs <span class="name">attrs1</span> and <span class="name">attrs2</span>,
such that <span class="name">wasGeneratedBy(-,e,a1,-,attrs1)</span> and <span class="name">used(-,a2,e,-,attrs2)</span> hold.
</div>
@@ -451,7 +451,7 @@
<div class='definition' id='wasStartedBy-definition'>Given two activities with identifiers <span class="name">a1</span> and <span class="name">a2</span>,
<span class="name">wasStartedBy(a2,a1)</span>
-holds <span class='conditional'>if and only if</span>
+holds <span class='conditional'>IF AND ONLY IF</span>
there exists an entity <span class="name">e</span>
such that
<span class="name">wasGeneratedBy(-,e,a1,-,-)</span>
@@ -475,10 +475,10 @@
<span class='conditional'>If</span>
<span class="name">wasAttributedTo(e,ag)</span> holds for some identifiers
<span class="name">e</span> and <span class="name">ag</span>,
-<span class='conditional'>then</span> there exists an activity with some identifier <span class="name">a</span> such that the following statements hold:
+<span class='conditional'>THEN</span> there exists an activity with some identifier <span class="name">a</span> such that the following statements hold:
<pre>
activity(a, -, -,-)
-wasGeneratedBy(-,e, a, -)
+wasGeneratedBy(-,e, a, -,_)
wasAssociatedWith(-,a, ag, -, -)
</pre>
</div>
@@ -495,8 +495,8 @@
<p>A further inference is permitted from derivations with an explicit activity and no usage: </p>
<div class='inference' id='derivation-use'>
<p>Given an activity <span class="name">a</span>, 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, a, -)</span> and <span class="name">wasGeneratedBy(-,e2,a,-,-)</span> hold, <span
-class='conditional'>then</span> <span class="name">used(-,a,e1,-,-)</span> also holds.
+<span class='conditional'>IF</span> <span class="name">wasDerivedFrom(-,e2,e1, a, -)</span> and <span class="name">wasGeneratedBy(-,e2,a,-,-)</span> hold, <span
+class='conditional'>THEN</span> <span class="name">used(-,a,e1,-,-)</span> also holds.
</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 in a given account
(see <a href="#generation-uniqueness">generation-uniqueness</a>). Hence, this activity is also the one referred to by the usage of <span class="name">e1</span>.
@@ -516,7 +516,7 @@
<div class='inference' id='wasRevision'>
Given two identifiers <span class="name">e1</span> and <span class="name">e2</span> identifying two entities, and an identifier <span class="name">ag</span> identifying an agent,
-<span class='conditional'>if</span> <span class="name">wasRevisionOf(-,e2,e1,ag)</span> holds, <span class='conditional'>then</span> the following
+<span class='conditional'>IF</span> <span class="name">wasRevisionOf(-,e2,e1,ag)</span> holds, <span class='conditional'>THEN</span> the following
hold:
<pre>
wasDerivedFrom(-,e2,e1,-)
@@ -542,10 +542,10 @@
Motivation for quotation inference
</div>
<div class='inference' id='quotation-implication'>
-<span class='conditional'>If</span>
+<span class='conditional'>IF</span>
<span class="name">wasQuotedFrom(e2,e1,ag2,ag1,attrs)</span> holds for some identifiers
<span class="name">e2</span>, <span class="name">e1</span>, <span class="name">ag2</span>, <span class="name">ag1</span>,
-<span class='conditional'>then</span> the following hold:
+<span class='conditional'>THEN</span> the following hold:
<pre>
wasDerivedFrom(e2,e1)
wasAttributedTo(e2,ag2)
@@ -573,23 +573,28 @@
the following statements hold:
<ol>
-<li><span class='conditional'>If</span> <span class="name">wasDerivedFrom(e2,e1,a,g2,u1)</span> holds, for some <span class="name">a</span>, <span class="name">g2</span>, <span
-class="name">u1</span>, <span class='conditional'>then</span> <span class="name">tracedTo(e2,e1)</span> also holds.</li>
-<li><span class='conditional'>If</span> <span class="name">wasDerivedFrom(e2,e1)</span> holds, <span class='conditional'>then</span> <span class="name">tracedTo(e2,e1)</span> also
+<li><span class='conditional'>IF</span> <span class="name">wasDerivedFrom(e2,e1,a,g2,u1)</span> holds, for some <span class="name">a</span>, <span class="name">g2</span>, <span
+class="name">u1</span>, <span class='conditional'>THEN</span> <span class="name">tracedTo(e2,e1)</span> also holds.</li>
+<li><span class='conditional'>IF</span> <span class="name">wasDerivedFrom(e2,e1)</span> holds, <span class='conditional'>THEN</span> <span class="name">tracedTo(e2,e1)</span> also
holds.</li>
-<li><span class='conditional'>If</span> <span class="name">wasAttributedTo(e2,ag1,aAttr)</span> holds, <span class='conditional'>then</span> <span class="name">tracedTo(e2,ag1)</span> also holds.</li>
-<li><span class='conditional'>If</span> <span class="name">wasAttributedTo(e2,ag2,aAttr)</span>, <span class="name">wasGeneratedBy(e2,a,gAttr)</span>, and <span
+<li><span class='conditional'>IF</span> <span
+class="name">wasAttributedTo(e2,ag1,aAttr)</span> holds, <span
+class='conditional'>THEN</span> <span
+class="name">tracedTo(e2,ag1)</span> also holds.
+</li>
+<li>
+<span class='conditional'>IF</span> <span class="name">wasAttributedTo(e2,ag2,aAttr)</span>, <span class="name">wasGeneratedBy(-,e2,a,-,gAttr)</span>, and <span
class="name">actedOnBehalfOf(ag2,ag1,a,rAttr)</span> hold, for some <span class="name">a</span>, <span class="name">ag2</span>, <span class="name">ag1</span>, <span class="name">aAttr</span>, <span class="name">gAttr</span>, and <span class="name">rAttr</span>, <span
-class='conditional'>then</span> <span class="name">tracedTo(e2,ag1)</span> also holds.</li>
-
-<li><span class='conditional'>If</span> <span
+class='conditional'>THEN</span> <span class="name">tracedTo(e2,ag1)</span> also holds.</li>
+
+<li><span class='conditional'>IF</span> <span
class="name">wasGeneratedBy(e2,a,gAttr)</span> and <span
class="name">wasStartedBy(a,e1,sAttr)</span> hold, for some <span
class="name">a</span>, <span class="name">gAttr</span> , <span
class="name">sAttr</span> then <span
class="name">tracedTo(e2,e1)</span> holds.</li>
-<li><span class='conditional'>If</span> <span class="name">tracedTo(e2,e)</span> and <span class="name">tracedTo(e,e1)</span> hold for some <span class="name">e</span>, <span
-class='conditional'>then</span> <span class="name">tracedTo(e2,e1)</span> also holds.</li>
+<li><span class='conditional'>IF</span> <span class="name">tracedTo(e2,e)</span> and <span class="name">tracedTo(e,e1)</span> hold for some <span class="name">e</span>, <span
+class='conditional'>THEN</span> <span class="name">tracedTo(e2,e1)</span> also holds.</li>
</ol>
</div>
@@ -619,11 +624,11 @@
<div class='inference' id="alternate-transitive">
For any entities <span class='name'>e1</span>, <span
- class='name'>e2</span>, <span class='name'>e3</span>, <span class="conditional">if</span> <span class='name'>alternateOf(e1,e2)</span> and
- <span class='name'>alternateOf(e2,e3)</span> <span class="conditional">then</span> <span class='name'>alternateOf(e1,e3)</span>.
+ class='name'>e2</span>, <span class='name'>e3</span>, <span class="conditional">IF</span> <span class='name'>alternateOf(e1,e2)</span> and
+ <span class='name'>alternateOf(e2,e3)</span> <span class="conditional">THEN</span> <span class='name'>alternateOf(e1,e3)</span>.
</div>
<div class='inference' id="alternate-symmetric">
- 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>.
+ 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>.
</div>
Similarly, specialization is a partial order: it is reflexive and
@@ -636,16 +641,16 @@
<div class='inference' id="specialization-transitive">
For any
- entities <span class='name'>e1</span>, <span class='name'>e2</span>, <span class='name'>e3</span>, <span class='conditional'>if</span> <span class='name'>specializationOf(e1,e2)</span>
+ entities <span class='name'>e1</span>, <span class='name'>e2</span>, <span class='name'>e3</span>, <span class='conditional'>IF</span> <span class='name'>specializationOf(e1,e2)</span>
and
- <span class='name'>specializationOf(e2,e3)</span> <span class='conditional'>then</span> <span class='name'>specializationOf(e1,e3)</span>.
+ <span class='name'>specializationOf(e2,e3)</span> <span class='conditional'>THEN</span> <span class='name'>specializationOf(e1,e3)</span>.
</div>
If one entity specializes another, then they are also alternates:
<div class='inference' id="specialization-alternate">
- For any entities <span class='name'>e1</span>, <span class='name'>e2</span>, <span class='conditional'>if</span> <span class='name'>specializationOf(e1,e2)</span> <span class='conditional'>then</span> <span class='name'>alternateOf(e1,e2)</span>.
+ For any entities <span class='name'>e1</span>, <span class='name'>e2</span>, <span class='conditional'>IF</span> <span class='name'>specializationOf(e1,e2)</span> <span class='conditional'>THEN</span> <span class='name'>alternateOf(e1,e2)</span>.
</div>
@@ -751,7 +756,8 @@
unique expressions describing them within a PROV-DM instance.
</p>
<div class='constraint' id='entity-unique'>
-<p>Given an entity identifier <span class="name">e</span>, there is at most oneexpression
+<p>Given an entity identifier <span class="name">e</span>, there is at
+ most one expression
<span class="name">entity(e,attrs)</span>, where <span
class="name">attrs</span> is some set of attribute-values.</p>
</div>
@@ -781,8 +787,8 @@
<div class='constraint' id='generation-uniqueness'>Given an entity denoted by <span class="name">e</span>, two activities denoted by <span class="name">a1</span> and <span
class="name">a2</span>, two time instants <span class="name">t1</span> and <span
class="name">t2</span>, and two sets of attribute-value pairs <span class="name">attrs1</span> and <span class="name">attrs2</span>,
-<span class='conditional'>if</span> <span class="name">wasGeneratedBy(id1, e, a1, t1, attrs1)</span> and <span class="name">wasGeneratedBy(id2, e, a2, t2, attrs2)</span> exist,
-<span class='conditional'>then</span> <span class="name">id1</span>=<span class="name">id2</span>, <span class="name">a1</span>=<span class="name">a2</span>, <span class="name">t1</span>=<span class="name">t2</span> and <span class="name">attrs1</span>=<span class="name">attrs2</span>.
+<span class='conditional'>IF</span> <span class="name">wasGeneratedBy(id1, e, a1, t1, attrs1)</span> and <span class="name">wasGeneratedBy(id2, e, a2, t2, attrs2)</span> exist,
+<span class='conditional'>THEN</span> <span class="name">id1</span>=<span class="name">id2</span>, <span class="name">a1</span>=<span class="name">a2</span>, <span class="name">t1</span>=<span class="name">t2</span> and <span class="name">attrs1</span>=<span class="name">attrs2</span>.
</div>
<div class="note">
@@ -801,21 +807,21 @@
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">wasGeneratedBy(e, -, t1)</span> and <span class="name">wasGeneratedBy(e, -, t2)</span> hold, then <span class="name">t1</span>=<span class="name">t2</span>.
+<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>.
</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-attributes2">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'>
-Given an activity <span class="name">activity(a,t1,t2,attrs1)</span> and its start <span class="name">wasStartedBy(id,a,e,t,attrs2)</span>, then <span class="name">t</span>=<span class="name">t1</span>.
+<span class='conditional'>IF</span> <span class="name">activity(a,t1,t2,-)</span> and <span class="name">wasStartedBy(id,a,e,t,-)</span>, <span class='conditional'>THEN</span> <span class="name">t</span>=<span class="name">t1</span>.
</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-attributes3">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'>
-Given an activity <span class="name">activity(a,t1,t2,attrs1)</span> and its end <span class="name">wasEndedBy(id,a,e,t,attrs2)</span>, then <span class="name">t</span>=<span class="name">t2</span>.
+<span class='conditional'>IF</span> <span class="name">activity(a,t1,t2,-)</span> and <span class="name">wasEndedBy(id,a,e,t,-)</span>, <span class='conditional'>THEN</span> <span class="name">t</span>=<span class="name">t1</span>.
</div>
@@ -825,8 +831,8 @@
<div class='inference' id='derivation-use'>
<p>Given an activity <span class="name">a</span>, entities denoted by <span class="name">e1</span> and <span class="name">e2</span>, and sets of attribute-value
pairs <span class="name">dAttrs</span>, <span class="name">gAttrs</span>,
-<span class='conditional'>if</span> <span class="name">wasDerivedFrom(e2,e1, a, dAttrs)</span> and <span class="name">wasGeneratedBy(e2,a,-,gAttrs)</span> hold, <span
-class='conditional'>then</span> <span class="name">used(a,e1,-,uAttrs)</span> also holds
+<span class='conditional'>IF</span> <span class="name">wasDerivedFrom(e2,e1, a, dAttrs)</span> and <span class="name">wasGeneratedBy(e2,a,-,gAttrs)</span> hold, <span
+class='conditional'>THEN</span> <span class="name">used(a,e1,-,uAttrs)</span> also holds
for some set of attribute-value pairs <span class="name">uAttrs</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
@@ -892,6 +898,10 @@
constraints are represented by triangles: an occurrence of a triangle between two <a title="instantaneous event">instantaneous event</a> vertical dotted lines represents that the event denoted by the left
line precedes the event denoted by the right line.</p>
+<div class="note">
+ TODO: Reorganize figure to match revised section structure.
+ </div>
+
<div style="text-align: center;">
<figure>
<figcaption id="constraint-summary">Summary of <a title="instantaneous event">instantaneous event</a> ordering constraints</figcaption>
@@ -899,6 +909,16 @@
</figure>
</div>
+<!-- Constraint template:
+<span class="conditional">IF</span>
+<span class="name">blah</span>
+and
+<span class="name">blah</span>
+<span class="conditional">THEN</span>
+<span class="name">XX</span>
+<a>precedes</a>
+<span class="name">YY</span>.
+-->
<section>
<h3>Activity constraints</h3>
@@ -917,17 +937,55 @@
<p>The existence of an activity implies that the <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='constraint' id='start-precedes-end'>The
+<div class='constraint' id='start-precedes-end'>
+ <!--
+ The
<a title="activity start event">start event</a> of any
-activity <a>precedes</a> its <a title="activity end event">end event</a>.</div>
+activity <a>precedes</a> its <a title="activity end event">end
+ event</a>.-->
+<span class="conditional">IF</span>
+<span class="name">wasStartedBy(start,a,-,-)</span>
+and
+<span class="name">wasEndedBy(end,a,-,-)</span>
+<span class="conditional">THEN</span>
+<span class="name">start</span>
+<a>precedes</a>
+<span class="name">end</span>.
+</div>
<p>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
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='constraint' 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>
- <span class="name">used(a,e,attrs,t)</span> holds, <span class='conditional'>then</span> the following ordering constraint holds:
+<div class='constraint' 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>
+ <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 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>.
+activity denoted by <span class="name">a</span> and <a>follows</a> its
+ <a title="activity start event">start</a>.
+ -->
+ <ol>
+ <li>
+ <span class="conditional">IF</span>
+<span class="name">used(use,a,e,-,-)</span>
+and
+<span class="name">wasStartedBy(start,a,-,-)</span>
+<span class="conditional">THEN</span>
+<span class="name">start</span>
+<a>precedes</a>
+<span class="name">use</span>.
+ </li>
+ <li>
+ <span class="conditional">IF</span>
+<span class="name">used(use,a,e,-,-)</span>
+and
+<span class="name">wasEndedBy(end,a,-,-)</span>
+<span class="conditional">THEN</span>
+<span class="name">use</span>
+<a>precedes</a>
+<span class="name">end</span>.
+ </li>
+ </ol>
</div>
@@ -935,11 +993,38 @@
<p>A generation implies ordering of <a title="instantaneous event">events</a>, 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='constraint' 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,t)</span> holds, <span class='conditional'>then</span> the following ordering constraint also holds: the <a title="entity generation
+<div class='constraint' 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,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>.
+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>.
+ -->
+ <ol>
+ <li>
+ <span class="conditional">IF</span>
+<span class="name">wasGeneratedBy(gen,a,e,-,-)</span>
+and
+<span class="name">wasStartedBy(start,a,-,-)</span>
+<span class="conditional">THEN</span>
+<span class="name">start</span>
+<a>precedes</a>
+<span class="name">gen</span>.
+ </li>
+ <li>
+ <span class="conditional">IF</span>
+<span class="name">wasGeneratedBy(gen,a,e,-,-)</span>
+and
+<span class="name">wasEndedBy(end,a,-,-)</span>
+<span class="conditional">THEN</span>
+<span class="name">gen</span>
+<a>precedes</a>
+<span class="name">end</span>.
+ </li>
+ </ol>
</div>
<p>Communication between two activities <span class="name">a1</span> and <span class="name">a2</span> also implies ordering of <a
@@ -948,11 +1033,24 @@
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='constraint' id='wasInformedBy-ordering'>
-Given two activities denoted by <span class="name">a1</span> and <span class="name">a2</span>, <span class='conditional'>if</span> <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:
+ holds, <span class='conditional'>THEN</span> the following ordering constraint holds:
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>.
+-->
+ <span class="conditional">IF</span>
+<span class="name">wasInformedBy(a2,a1)</span>
+and
+<span class="name">wasStartedBy(start,a1,-,-)</span>
+and
+<span class="name">wasEndedBy(end,a2,-,-)</span>
+<span class="conditional">THEN</span>
+<span class="name">start</span>
+<a>precedes</a>
+<span class="name">end</span>.
+
</div>
<p>Start of <span class="name">a2</span> by activity <span class="name">a1</span> also implies ordering of <a
@@ -960,12 +1058,25 @@
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='constraint' id='wasStartedBy-ordering'>
-Given two activities denoted by <span class="name">a1</span> and <span class="name">a2</span>, <span class='conditional'>if</span> <span
+<div class='constraint' id='wasStartedByActivity-ordering'>
+ <!--
+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
+ holds, <span class='conditional'>THEN</span> the following ordering constraint holds: the
<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>.
+ -->
+ <span class="conditional">IF</span>
+<span class="name">wasStartedBy(a2,a1)</span>
+and
+<span class="name">wasStartedBy(start1,a1,-,-)</span>
+and
+<span class="name">wasStartedBy(start2,a2,-,-)</span>
+<span class="conditional">THEN</span>
+<span class="name">start</span>
+<a>precedes</a>
+<span class="name">end</span>.
+
</div>
</section>
@@ -984,24 +1095,56 @@
explicitly to cover the case of an entity that is generated and
invalidated without being used.)</p>
-<div class='constraint' id='generation-precedes-invalidation'>The <a
+<div class='constraint' id='generation-precedes-invalidation'>
+ <!--The <a
title="entity generation event">generation</a> of an entity always
-<a>precedes</a> its <a title="entity invalidation event">invalidation</a>.
+<a>precedes</a> its <a title="entity invalidation
+ event">invalidation</a>.
+ -->
+ <span class="conditional">IF</span>
+<span class="name">wasGeneratedBy(gen,e,_,_)</span>
+and
+<span class="name">wasInvalidatedBy(inv,e,-,-)</span>
+<span class="conditional">THEN</span>
+<span class="name">gen</span>
+<a>precedes</a>
+<span class="name">inv</span>.
</div>
<p> A usage and a generation for a given entity implies ordering of <a title="instantaneous event">events</a>, 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>
-<div class='constraint' id='generation-precedes-usage'>The <a title="entity generation event">generation</a> of an entity always
-<a>precedes</a> any of its <a title="entity usage event">usages</a>.
+<div class='constraint' id='generation-precedes-usage'>
+ <!--
+ The <a title="entity generation event">generation</a> of an entity always
+<a>precedes</a> any of its <a title="entity usage event">usages</a>.-->
+ <span class="conditional">IF</span>
+<span class="name">wasGeneratedBy(gen,e,_,_)</span>
+and
+<span class="name">used(use,_,e,-)</span>
+<span class="conditional">THEN</span>
+<span class="name">gen</span>
+<a>precedes</a>
+<span class="name">use</span>.
</div>
<p>All usages of an entity precede its invalidation, which is captured by constraint <a href="#usage-precedes-invalidation">usage-precedes-invalidation</a> (without any explicit graphical representation).</p>
-<div class='constraint' id='usage-precedes-invalidation'>Any <a title="entity usage event">usage</a> of an entity always
-<a>precedes</a> its <a title="entity invalidation event">invalidation</a>.
+<div class='constraint' id='usage-precedes-invalidation'>
+ <!--
+ Any <a title="entity usage event">usage</a> of an entity always
+<a>precedes</a> its <a title="entity invalidation
+ event">invalidation</a>.-->
+ <span class="conditional">IF</span>
+<span class="name">used(use,_,e,-)</span>
+and
+<span class="name">wasInvalidatedBy(inv,e,_,_)</span>
+<span class="conditional">THEN</span>
+<span class="name">use</span>
+<a>precedes</a>
+<span class="name">inv</span>.
</div>
@@ -1021,14 +1164,23 @@
href="#derivation-usage-generation-ordering">derivation-usage-generation-ordering</a>.</p>
-<div class='constraint' id='derivation-usage-generation-ordering'>Given an activity with identifier <span class="name">a</span>, entities with identifier <span
+<div class='constraint' 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>
- holds, <span class='conditional'>then</span>
+class='conditional'>IF</span> <span class="name">wasDerivedFrom(e2,e1,a,g2,u1,attrs)</span>
+ holds, <span class='conditional'>THEN</span>
the following ordering constraint holds:
the <a title="entity usage event">usage</a>
of entity denoted by <span class="name">e1</span> <a>precedes</a> the <a title="entity generation event">generation</a> of
-the entity denoted by <span class="name">e2</span>.
+the entity denoted by <span class="name">e2</span>.-->
+ <span class="conditional">IF</span>
+<span class="name">wasDerivedFrom(d,e2,e1,a,g2,u1,-)</span>
+<span class="conditional">THEN</span>
+<span class="name">g2</span>
+<a>precedes</a>
+<span class="name">u1</span>.
+
</div>
<p>When the usage is unknown, a similar constraint exists, except that the constraint refers to its
@@ -1036,13 +1188,26 @@
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='constraint' id='derivation-generation-generation-ordering'>
-Given two entities denoted by <span class="name">e1</span> and <span class="name">e2</span>, <span class='conditional'>if</span> <span
+<div class='constraint'
+ id='derivation-generation-generation-ordering'>
+ <!--
+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, attrs)</span>
- holds, <span class='conditional'>then</span> the following ordering constraint holds:
+ 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>
of
the entity denoted by <span class="name">e2</span>.
+ -->
+ <span class="conditional">IF</span>
+<span class="name">wasDerivedFrom(e2,e1,attrs)</span>
+ and
+<span class="name">wasGeneratedBy(gen1,e1,_,_)</span>
+ and
+<span class="name">wasGeneratedBy(gen2,e2,_,_)</span>
+<span class="conditional">THEN</span>
+<span class="name">gen1</span>
+<a>precedes</a>
+<span class="name">gen2</span>.
</div>
<p>Note that event ordering is between generations of <span class="name">e1</span>
@@ -1077,13 +1242,39 @@
<div class='constraint' id='wasStartedBy-ordering'>
-Given an activity denoted by <span class="name">a</span> and an entity
-denoted by <span class="name">e</span>, <span class='conditional'>if</span> <span
+<!--Given an activity denoted by <span class="name">a</span> and an entity
+denoted by <span class="name">e</span>, <span class='conditional'>IF</span> <span
class="name">wasStartedBy(a,e)</span>
- holds, <span class='conditional'>then</span> the following ordering constraints hold: the
+ 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 entity <span class="name">e</span>, and
<a>precedes</a> the invalidation event of
-the same entity.
+the same entity.-->
+
+ <ol>
+ <li>
+ <span class="conditional">IF</span>
+<span class="name">wasStartedBy(a,e)</span>
+and
+<span class="name">wasStartedBy(start,a,-,-)</span>
+and
+<span class="name">wasGeneratedBy(gen,e,-,-)</span>
+<span class="conditional">THEN</span>
+<span class="name">gen</span>
+<a>precedes</a>
+<span class="name">start</span>.
+ </li><li>
+ <span class="conditional">IF</span>
+<span class="name">wasStartedBy(a,e)</span>
+and
+<span class="name">wasStartedBy(start,a,-,-)</span>
+and
+<span class="name">wasInvalidatedBy(inv,e,-,-)</span>
+<span class="conditional">THEN</span>
+<span class="name">start</span>
+<a>precedes</a>
+<span class="name">inv</span>.
+ </li>
+ </ol>
</div>
<p> Similarly, if an agent is associated with an activity then the
@@ -1092,12 +1283,38 @@
<div class='constraint' id='wasEndedBy-ordering'>
-Given an activity denoted by <span class="name">a</span> and an entity denoted by <span class="name">e</span>, <span class='conditional'>if</span> <span
+ <!--
+Given an activity denoted by <span class="name">a</span> and an entity denoted by <span class="name">e</span>, <span class='conditional'>IF</span> <span
class="name">wasEndedBy(a,e)</span>
- holds, <span class='conditional'>then</span> the following ordering constraints hold: the
+ holds, <span class='conditional'>THEN</span> the following ordering constraints hold: the
<a title="activity end event">end</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 entity <span class="name">e</span>, and
<a>precedes</a> the invalidation event of
-the same entity.
+the same entity.-->
+ <ol>
+ <li>
+ <span class="conditional">IF</span>
+<span class="name">wasEndedBy(a,e)</span>
+and
+<span class="name">wasEndedBy(end,a,-,-)</span>
+and
+<span class="name">wasGeneratedBy(gen,e,-,-)</span>
+<span class="conditional">THEN</span>
+<span class="name">gen</span>
+<a>precedes</a>
+<span class="name">end</span>.
+ </li><li>
+ <span class="conditional">IF</span>
+<span class="name">wasEndedBy(a,e)</span>
+and
+<span class="name">wasEndedBy(end,a,-,-)</span>
+and
+<span class="name">wasInvalidatedBy(inv,e,-,-)</span>
+<span class="conditional">THEN</span>
+<span class="name">end</span>
+<a>precedes</a>
+<span class="name">inv</span>.
+ </li>
+ </ol>
</div>
@@ -1107,14 +1324,39 @@
<div class='constraint' 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> <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
+ 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>
precedes the invalidation event of
the agent denoted by <span class="name">ag</span>, and
the <a title="entity generation event">generation event</a> for agent denoted by <span class="name">ag</span>
-<a>precedes</a> the activity <a title="activity end event">end</a> event.
+<a>precedes</a> the activity <a title="activity end event">end</a>
+ event.-->
+ <ol> <li>
+ <span class="conditional">IF</span>
+<span class="name">wasAssociatedWith(a,ag)</span>
+and
+<span class="name">wasStartedBy(start,a,-,-)</span>
+and
+<span class="name">wasInvalidatedBy(inv,ag,-,-)</span>
+<span class="conditional">THEN</span>
+<span class="name">start</span>
+<a>precedes</a>
+<span class="name">inv</span>.
+ </li><li>
+ <span class="conditional">IF</span>
+<span class="name">wasAssociatedWith(a,ag)</span>
+and
+<span class="name">wasGeneratedBy(gen,ag,-,-)</span>
+and
+<span class="name">wasEndedBy(end,a,-,-)</span>
+<span class="conditional">THEN</span>
+<span class="name">gen</span>
+<a>precedes</a>
+<span class="name">end</span>.
+ </li>
+ </ol>
</div>
@@ -1128,28 +1370,66 @@
<div class='constraint' id='wasAttributedTo-ordering'>
-Given an entity denoted by <span class="name">e</span> and an agent denoted by <span class="name">ag</span>, <span class='conditional'>if</span> <span
+<!--Given an entity denoted by <span class="name">e</span> and an agent denoted by <span class="name">ag</span>, <span class='conditional'>IF</span> <span
class="name">wasAttributedTo(e,ag)</span>
- holds, <span class='conditional'>then</span> the following ordering constraints hold: the
+ holds, <span class='conditional'>THEN</span> the following ordering constraints hold: the
<a title="entity generation event">generation</a> event of the entity denoted by <span class="name">e</span>
precedes the invalidation event of
the agent denoted by <span class="name">ag</span>, and
the <a title="entity generation event">generation event</a> for agent denoted by <span class="name">ag</span>
-<a>precedes</a> the entity <a title="entity invalidation event">invalidation</a> event.
+<a>precedes</a> the entity <a title="entity invalidation
+ event">invalidation</a> event.-->
+ <ol> <li>
+ <span class="conditional">IF</span>
+<span class="name">wasAttributedTo(e,ag)</span>
+and
+<span class="name">wasGeneratedBy(gen,e,-,-)</span>
+and
+<span class="name">wasInvalidatedBy(inv,ag,-,-)</span>
+<span class="conditional">THEN</span>
+<span class="name">gen</span>
+<a>precedes</a>
+<span class="name">inv</span>.
+ </li><li>
+ <span class="conditional">IF</span>
+<span class="name">wasAttributedTo(e,ag)</span>
+and
+<span class="name">wasGeneratedBy(gen,ag,-,-)</span>
+and
+<span class="name">wasInvalidatedBy(inv,e,-,-)</span>
+<span class="conditional">THEN</span>
+<span class="name">gen</span>
+<a>precedes</a>
+<span class="name">inv</span>.
+ </li>
+ </ol>
</div>
<p>For responsibility, two agents need to have some overlap in their lifetime.</p>
<div class='constraint' id='actedOnBehalfOf-ordering'>
-Given two agents <span class="name">ag1</span> and <span class="name">ag2</span>, <span class='conditional'>if</span> <span
+ <!--
+Given two agents <span class="name">ag1</span> and <span class="name">ag2</span>, <span class='conditional'>IF</span> <span
class="name">actedOnBehalfOf(ag2,ag1)</span>
- holds, <span class='conditional'>then</span> the following ordering constraints hold: the
+ holds, <span class='conditional'>THEN</span> the following ordering constraints hold: the
<a title="entity generation event">generation</a> event of the agent denoted by <span class="name">ag2</span>
precedes the invalidation event of
agent <span class="name">ag1</span>, and
the <a title="entity generation event">generation event</a> for agent denoted by <span class="name">ag1</span>
-<a>precedes</a> <a title="entity invalidation event">invalidation</a> event for <span class="name">ag2</span>.
+<a>precedes</a> <a title="entity invalidation event">invalidation</a>
+ event for <span class="name">ag2</span>.-->
+ <span class="conditional">IF</span>
+<span class="name">actedOnBehalfOf(ag2,ag1)</span>
+and
+<span class="name">wasGeneratedBy(gen,ag1,-,-)</span>
+and
+<span class="name">wasInvalidatedBy(inv,ag2,-,-)</span>
+<span class="conditional">THEN</span>
+<span class="name">gen</span>
+<a>precedes</a>
+<span class="name">inv</span>.
+
</div>
</section>
@@ -1165,7 +1445,7 @@
<div class='definition' id='membership-as-insertion'>
<span class="name">memberOf(c, {(k1, v1), ...})</span> holds
-<span class='conditional'>if and only if</span> there exists a collection <span class="name">c0</span>, such that
+<span class='conditional'>IF AND ONLY IF</span> there exists a collection <span class="name">c0</span>, such that
<span class="name">derivedByInsertionFrom(c, c0, {(k1, v1), ...})</span>.
</div>
@@ -1958,7 +2238,7 @@
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">wasGeneratedBy(e, -, t1)</span> and <span class="name">wasGeneratedBy(e, -, t2)</span> hold, then <span class="name">t1</span>=<span class="name">t2</span>.
+<span class='conditional'>IF</span> <span class="name">wasGeneratedBy(e, -, t1)</span> and <span class="name">wasGeneratedBy(e, -, t2)</span> hold, then <span class="name">t1</span>=<span class="name">t2</span>.
</div>
<p></p>
@@ -2038,7 +2318,7 @@
<div class='definition' id='wasInformedBy-Definition'>Given two activities identified by <span class="name">a1</span> and <span class="name">a2</span>,
<span class="name">wasInformedBy(a2,a1)</span>
-holds, <span class='conditional'>if and only if</span>
+holds, <span class='conditional'>IF AND ONLY IF</span>
there is an entity with some identifier <span class="name">e</span> and some sets of attribute-value pairs <span class="name">attrs1</span> and <span class="name">attrs2</span>,
such that <span class="name">wasGeneratedBy(-,e,a1,-,attrs1)</span> and <span class="name">used(-,a2,e,-,attrs2)</span> hold.
</div>
@@ -2085,7 +2365,7 @@
<div class='definition' id='wasStartedBy'>Given two activities with identifiers <span class="name">a1</span> and <span class="name">a2</span>,
<span class="name">wasStartedBy(a2,a1)</span>
-holds <span class='conditional'>if and only if</span>
+holds <span class='conditional'>IF AND ONLY IF</span>
there exist an entity with some identifier <span class="name">e</span>
and some attributes <span class="name">gAttr</span> and <span class="name">sAttr</span>,
such that
@@ -2120,10 +2400,10 @@
be inferred.
<div class='inference' id='attribution-implication'>
-<span class='conditional'>If</span>
+<span class='conditional'>IF</span>
<span class="name">wasAttributedTo(e,ag)</span> holds for some identifiers
<span class="name">e</span> and <span class="name">ag</span>,
-<span class='conditional'>then</span> there exists an activity with some identifier <span class="name">a</span> such that the following statements hold:
+<span class='conditional'>THEN</span> there exists an activity with some identifier <span class="name">a</span> such that the following statements hold:
<pre>
activity(a, t1, t2, attr1)
wasGeneratedBy(-,e, a, -)
@@ -2260,7 +2540,7 @@
<div class='inference' id='wasRevision'>
Given two identifiers <span class="name">e1</span> and <span class="name">e2</span> identifying two entities, and an identifier <span class="name">ag</span> identifying an agent,
-<span class='conditional'>if</span> <span class="name">wasRevisionOf(e2,e1,ag)</span> holds, <span class='conditional'>then</span>
+<span class='conditional'>IF</span> <span class="name">wasRevisionOf(e2,e1,ag)</span> holds, <span class='conditional'>THEN</span>
there exists an entity with some identifier <span class="name">e</span> and some attribute-values <span class="name">eAttrs</span>, <span class="name">dAttrs</span>, such that the following
hold:
<pre>
@@ -2290,10 +2570,10 @@
<div class='inference' id='quotation-implication'>
-<span class='conditional'>If</span>
+<span class='conditional'>IF</span>
<span class="name">wasQuotedFrom(e2,e1,ag2,ag1,attrs)</span> holds for some identifiers
<span class="name">e2</span>, <span class="name">e1</span>, <span class="name">ag2</span>, <span class="name">ag1</span>,
-<span class='conditional'>then</span> the following hold:
+<span class='conditional'>THEN</span> the following hold:
<pre>
wasDerivedFrom(e2,e1)
wasAttributedTo(e2,ag2)
@@ -2324,23 +2604,23 @@
the following statements hold:
<ol>
-<li><span class='conditional'>If</span> <span class="name">wasDerivedFrom(e2,e1,a,g2,u1)</span> holds, for some <span class="name">a</span>, <span class="name">g2</span>, <span
-class="name">u1</span>, <span class='conditional'>then</span> <span class="name">tracedTo(e2,e1)</span> also holds.</li>
-<li><span class='conditional'>If</span> <span class="name">wasDerivedFrom(e2,e1)</span> holds, <span class='conditional'>then</span> <span class="name">tracedTo(e2,e1)</span> also
+<li><span class='conditional'>IF</span> <span class="name">wasDerivedFrom(e2,e1,a,g2,u1)</span> holds, for some <span class="name">a</span>, <span class="name">g2</span>, <span
+class="name">u1</span>, <span class='conditional'>THEN</span> <span class="name">tracedTo(e2,e1)</span> also holds.</li>
+<li><span class='conditional'>IF</span> <span class="name">wasDerivedFrom(e2,e1)</span> holds, <span class='conditional'>THEN</span> <span class="name">tracedTo(e2,e1)</span> also
holds.</li>
-<li><span class='conditional'>If</span> <span class="name">wasAttributedTo(e2,ag1,aAttr)</span> holds, <span class='conditional'>then</span> <span class="name">tracedTo(e2,ag1)</span> also holds.</li>
-<li><span class='conditional'>If</span> <span class="name">wasAttributedTo(e2,ag2,aAttr)</span>, <span class="name">wasGeneratedBy(e2,a,gAttr)</span>, and <span
+<li><span class='conditional'>IF</span> <span class="name">wasAttributedTo(e2,ag1,aAttr)</span> holds, <span class='conditional'>THEN</span> <span class="name">tracedTo(e2,ag1)</span> also holds.</li>
+<li><span class='conditional'>IF</span> <span class="name">wasAttributedTo(e2,ag2,aAttr)</span>, <span class="name">wasGeneratedBy(e2,a,gAttr)</span>, and <span
class="name">actedOnBehalfOf(ag2,ag1,a,rAttr)</span> hold, for some <span class="name">a</span>, <span class="name">ag2</span>, <span class="name">ag1</span>, <span class="name">aAttr</span>, <span class="name">gAttr</span>, and <span class="name">rAttr</span>, <span
-class='conditional'>then</span> <span class="name">tracedTo(e2,ag1)</span> also holds.</li>
-
-<li><span class='conditional'>If</span> <span
+class='conditional'>THEN</span> <span class="name">tracedTo(e2,ag1)</span> also holds.</li>
+
+<li><span class='conditional'>IF</span> <span
class="name">wasGeneratedBy(e2,a,gAttr)</span> and <span
class="name">wasStartedBy(a,e1,sAttr)</span> hold, for some <span
class="name">a</span>, <span class="name">gAttr</span> , <span
class="name">sAttr</span> then <span
class="name">tracedTo(e2,e1)</span> holds.</li>
-<li><span class='conditional'>If</span> <span class="name">tracedTo(e2,e)</span> and <span class="name">tracedTo(e,e1)</span> hold for some <span class="name">e</span>, <span
-class='conditional'>then</span> <span class="name">tracedTo(e2,e1)</span> also holds.</li>
+<li><span class='conditional'>IF</span> <span class="name">tracedTo(e2,e)</span> and <span class="name">tracedTo(e,e1)</span> hold for some <span class="name">e</span>, <span
+class='conditional'>THEN</span> <span class="name">tracedTo(e2,e1)</span> also holds.</li>
</ol>
</div>
@@ -2350,9 +2630,9 @@
entities or events. </p>
<div class='constraint' id='traceability-assertion'>
-<span class='conditional'>If</span> <span
+<span class='conditional'>IF</span> <span
class="name">tracedTo(r2,r1,attrs)</span> holds for two entity identifiers <span class="name">r2</span> and <span class="name">r1</span>, and attribute-value pairs <span class="name">attrs</span>,
- <span class='conditional'>then</span> there exist
+ <span class='conditional'>THEN</span> there exist
<span class="name">e<sub>0</sub></span>, <span class="name">e<sub>1</sub></span>, ..., <span class="name">e<sub>n</sub></span> for <span class="name">n≥1</span>, with <span
class="name">e<sub>0</sub></span>=<span class="name">r2</span> and <span class="name">e<sub>n</sub></span>=<span class="name">r1</span>, and
for any i such that <span class="name">0≤i≤n-1</span>, at least