Merge branch 'master' into highprecision

annotations/pom.xml

@@ -56,6 +56,10 @@
                     </execution>
 				</executions>
 			</plugin>
+			<plugin>
+				<groupId>org.apache.maven.plugins</groupId>
+				<artifactId>maven-javadoc-plugin</artifactId>
+			</plugin>
 			<plugin>
 				<groupId>org.apache.maven.plugins</groupId>
 				<artifactId>maven-source-plugin</artifactId>

annotations/src/main/java/annotations/in/INDeadlineMetAnnotation.java

@@ -49,11 +49,11 @@
  * and reaction event; if c holds, d is the maximum tolerable delay between stimulus and reaction.
  * The conjecture evaluates true over an execution trace if and only if:
  * 
- * forall i1, t1 & O(e1, i1, t1) and E(c, t1) =>
- *    exists i2, t2 & O(e2, i2, t2)
- *        and t1 <= t2 <= t1 + d
- *        and (m => i1 = i2)
- *        and (e1 = e2 => i2 = i1 + 1)
+ * forall i1, t1 &amp; O(e1, i1, t1) and E(c, t1) =&gt;
+ *    exists i2, t2 &amp; O(e2, i2, t2)
+ *        and t1 &lt;= t2 &lt;= t1 + d
+ *        and (m =&gt; i1 = i2)
+ *        and (e1 = e2 =&gt; i2 = i1 + 1)
  * 
  * See http://dx.doi.org/10.1109/HASE.2007.26.
  */

annotations/src/main/java/annotations/in/INSepRequireAnnotation.java

@@ -46,14 +46,14 @@
  * requires that the e2 event does occur. A conjecture SepRequire(e1, c, e2, d, m) evaluates
  * to true over an execution trace if and only if:
  * 
- * forall i1, t1 & O(e1, i1, t1) and E(c, t1) =>
- *     not exists i2, t2 & O(e2, i2, t2)
- *         and t1 <= t2 and t2 < t1 + d
- *         and (m => i1 = i2)
- *         and (e1 = e2 => i2 = i1 + 1)
- *     and exists i3, t3 & O(e2 , i3 , t3)
- *         and (m => i1 = i3 )
- *         and (e1 = e2 => i3 = i1 + 1)
+ * forall i1, t1 &amp; O(e1, i1, t1) and E(c, t1) =&gt;
+ *     not exists i2, t2 &amp; O(e2, i2, t2)
+ *         and t1 &lt;= t2 and t2 &lt; t1 + d
+ *         and (m =&gt; i1 = i2)
+ *         and (e1 = e2 =&gt; i2 = i1 + 1)
+ *     and exists i3, t3 &amp; O(e2 , i3 , t3)
+ *         and (m =&gt; i1 = i3 )
+ *         and (e1 = e2 =&gt; i3 = i1 + 1)
  * 
  * See http://dx.doi.org/10.1109/HASE.2007.26.
  */

annotations/src/main/java/annotations/in/INSeparateAnnotation.java

@@ -50,11 +50,11 @@
  * A validation conjecture Separate(e1, c, e2, d , m) evaluates true over an execution trace if
  * and only if:
  * 
- * forall i1, t1 & O(e1, i1, t1) and E(c, t1) =>
- *     not exists i2, t2 & O(e2, i2, t2)
- *         and t1 <= t2 and t2 < t1 + d
- *         and (m => i1 = i2)
- *         and (e1 = e2 => i2 = i1 + 1)
+ * forall i1, t1 &amp; O(e1, i1, t1) and E(c, t1) =&gt;
+ *     not exists i2, t2 &amp; O(e2, i2, t2)
+ *         and t1 &lt;= t2 and t2 &lt; t1 + d
+ *         and (m =&gt; i1 = i2)
+ *         and (e1 = e2 =&gt; i2 = i1 + 1)
  * 
  * See http://dx.doi.org/10.1109/HASE.2007.26.
  */

annotations2/pom.xml

@@ -40,6 +40,10 @@
 				<groupId>org.apache.maven.plugins</groupId>
 				<artifactId>maven-jar-plugin</artifactId>
 			</plugin>
+			<plugin>
+				<groupId>org.apache.maven.plugins</groupId>
+				<artifactId>maven-javadoc-plugin</artifactId>
+			</plugin>
 			<plugin>
 				<groupId>org.apache.maven.plugins</groupId>
 				<artifactId>maven-source-plugin</artifactId>

cmd-plugins/pom.xml

@@ -41,6 +41,10 @@
 				<groupId>org.apache.maven.plugins</groupId>
 				<artifactId>maven-jar-plugin</artifactId>
 			</plugin>
+			<plugin>
+				<groupId>org.apache.maven.plugins</groupId>
+				<artifactId>maven-javadoc-plugin</artifactId>
+			</plugin>
 			<plugin>
 				<groupId>org.apache.maven.plugins</groupId>
 				<artifactId>maven-source-plugin</artifactId>

dbgp/pom.xml

@@ -83,6 +83,10 @@
 					</execution>
 				</executions>
 			</plugin>
+			<plugin>
+				<groupId>org.apache.maven.plugins</groupId>
+				<artifactId>maven-javadoc-plugin</artifactId>
+			</plugin>
 			<plugin>
 				<groupId>org.apache.maven.plugins</groupId>
 				<artifactId>maven-source-plugin</artifactId>

dbgpc/pom.xml

@@ -68,6 +68,10 @@
 					</execution>
 				</executions>
 			</plugin>
+			<plugin>
+				<groupId>org.apache.maven.plugins</groupId>
+				<artifactId>maven-javadoc-plugin</artifactId>
+			</plugin>
 			<plugin>
 				<groupId>org.apache.maven.plugins</groupId>
 				<artifactId>maven-source-plugin</artifactId>

examples/csvreader/pom.xml

@@ -28,6 +28,10 @@
 				<groupId>org.apache.maven.plugins</groupId>
 				<artifactId>maven-jar-plugin</artifactId>
 			</plugin>
+			<plugin>
+				<groupId>org.apache.maven.plugins</groupId>
+				<artifactId>maven-javadoc-plugin</artifactId>
+			</plugin>
 			<plugin>
 				<groupId>org.apache.maven.plugins</groupId>
 				<artifactId>maven-source-plugin</artifactId>

examples/lspplugin/pom.xml

@@ -32,6 +32,10 @@
 				<groupId>org.apache.maven.plugins</groupId>
 				<artifactId>maven-jar-plugin</artifactId>
 			</plugin>
+			<plugin>
+				<groupId>org.apache.maven.plugins</groupId>
+				<artifactId>maven-javadoc-plugin</artifactId>
+			</plugin>
             <plugin>
                 <groupId>org.apache.maven.plugins</groupId>
                 <artifactId>maven-source-plugin</artifactId>

examples/pdfreader/pom.xml

@@ -33,6 +33,10 @@
 				<groupId>org.apache.maven.plugins</groupId>
 				<artifactId>maven-jar-plugin</artifactId>
 			</plugin>
+			<plugin>
+				<groupId>org.apache.maven.plugins</groupId>
+				<artifactId>maven-javadoc-plugin</artifactId>
+			</plugin>
             <plugin>
                 <groupId>org.apache.maven.plugins</groupId>
                 <artifactId>maven-source-plugin</artifactId>

examples/simulation/pom.xml

@@ -31,6 +31,10 @@
 				<groupId>org.apache.maven.plugins</groupId>
 				<artifactId>maven-jar-plugin</artifactId>
 			</plugin>
+			<plugin>
+				<groupId>org.apache.maven.plugins</groupId>
+				<artifactId>maven-javadoc-plugin</artifactId>
+			</plugin>
            <plugin>
                 <groupId>org.apache.maven.plugins</groupId>
                 <artifactId>maven-source-plugin</artifactId>

examples/simulation/src/main/java/simulation/TestSimulation.java

@@ -39,7 +39,7 @@
  * 
  * Then execute new Test().test() as usual. The output should be like:
  * 
- * > p new Test().test()
+ * > p new Test().test()
  * Last = 0
  * Updated = 1
  * Last = 1

examples/v2c/pom.xml

@@ -39,6 +39,10 @@
                 <groupId>org.apache.maven.plugins</groupId>
                 <artifactId>maven-jar-plugin</artifactId>
             </plugin>
+			<plugin>
+				<groupId>org.apache.maven.plugins</groupId>
+				<artifactId>maven-javadoc-plugin</artifactId>
+			</plugin>
             <plugin>
                 <groupId>org.apache.maven.plugins</groupId>
                 <artifactId>maven-source-plugin</artifactId>

examples/vdmjplugin/pom.xml

@@ -29,6 +29,10 @@
 				<groupId>org.apache.maven.plugins</groupId>
 				<artifactId>maven-jar-plugin</artifactId>
 			</plugin>
+			<plugin>
+				<groupId>org.apache.maven.plugins</groupId>
+				<artifactId>maven-javadoc-plugin</artifactId>
+			</plugin>
             <plugin>
                 <groupId>org.apache.maven.plugins</groupId>
                 <artifactId>maven-source-plugin</artifactId>

lsp/pom.xml

@@ -80,6 +80,10 @@
 					</execution>
 				</executions>
 			</plugin>
+			<plugin>
+				<groupId>org.apache.maven.plugins</groupId>
+				<artifactId>maven-javadoc-plugin</artifactId>
+			</plugin>
 			<plugin>
 				<groupId>org.apache.maven.plugins</groupId>
 				<artifactId>maven-source-plugin</artifactId>

pom.xml

@@ -104,6 +104,7 @@
                     </executions>
                     <configuration>
                         <failOnError>false</failOnError>
+                        <detectOfflineLinks>false</detectOfflineLinks>
                         <quiet>true</quiet>
                         <source>8</source>
                     </configuration>

quickcheck/pom.xml

@@ -60,6 +60,10 @@
 					</execution>
 				</executions>
 			</plugin>
+			<plugin>
+				<groupId>org.apache.maven.plugins</groupId>
+				<artifactId>maven-javadoc-plugin</artifactId>
+			</plugin>
 			<plugin>
 				<groupId>org.apache.maven.plugins</groupId>
 				<artifactId>maven-source-plugin</artifactId>

quickcheck/src/main/java/quickcheck/visitors/RangeCreator.java

@@ -114,7 +114,7 @@ protected List<ValueSet> powerLimit(ValueSet source, int limit, boolean incEmpty
 	}
 
 	/**
-	 * Return the lowest integer power of n that is <= limit. If n < 2,
+	 * Return the lowest integer power of n that is &lt;= limit. If n &lt; 2,
 	 * just return 1.
 	 */
 	protected int leastPower(int n, int limit)

quickcheck/src/main/java/quickcheck/visitors/TrivialQCVisitor.java

@@ -62,7 +62,7 @@
  * which are known to be true in the current context and they return true if they
  * are always true, given this stack.
  * 
- * eg. X => Y will pass "X" as a truth when evaluating Y. If Y is just X, then
+ * eg. X => Y will pass "X" as a truth when evaluating Y. If Y is just X, then
  * that will always be true and so the whole implication is always true, etc.
  */
 public class TrivialQCVisitor extends TCExpressionVisitor<Boolean, Stack<TCExpression>>

stdlib/pom.xml

@@ -57,6 +57,10 @@
 				<groupId>org.apache.maven.plugins</groupId>
 				<artifactId>maven-jar-plugin</artifactId>
 			</plugin>
+			<plugin>
+				<groupId>org.apache.maven.plugins</groupId>
+				<artifactId>maven-javadoc-plugin</artifactId>
+			</plugin>
             <plugin>
                 <groupId>org.apache.maven.plugins</groupId>
                 <artifactId>maven-source-plugin</artifactId>

vdmj/pom.xml

@@ -115,6 +115,10 @@
                     </execution>
 				</executions>
 			</plugin>
+			<plugin>
+				<groupId>org.apache.maven.plugins</groupId>
+				<artifactId>maven-javadoc-plugin</artifactId>
+			</plugin>
 			<plugin>
 				<groupId>org.apache.maven.plugins</groupId>
 				<artifactId>maven-source-plugin</artifactId>