diff --git a/annotations/pom.xml b/annotations/pom.xml index 03a7f6ffd..ae2b8cab9 100644 --- a/annotations/pom.xml +++ b/annotations/pom.xml @@ -56,6 +56,10 @@ + + org.apache.maven.plugins + maven-javadoc-plugin + org.apache.maven.plugins maven-source-plugin diff --git a/annotations/src/main/java/annotations/in/INDeadlineMetAnnotation.java b/annotations/src/main/java/annotations/in/INDeadlineMetAnnotation.java index c168fe7b9..7cd02a751 100644 --- a/annotations/src/main/java/annotations/in/INDeadlineMetAnnotation.java +++ b/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 & 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) * * See http://dx.doi.org/10.1109/HASE.2007.26. */ diff --git a/annotations/src/main/java/annotations/in/INSepRequireAnnotation.java b/annotations/src/main/java/annotations/in/INSepRequireAnnotation.java index 417d374de..51b48e007 100644 --- a/annotations/src/main/java/annotations/in/INSepRequireAnnotation.java +++ b/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 & 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) * * See http://dx.doi.org/10.1109/HASE.2007.26. */ diff --git a/annotations/src/main/java/annotations/in/INSeparateAnnotation.java b/annotations/src/main/java/annotations/in/INSeparateAnnotation.java index 8bb431836..dcf6cb93f 100644 --- a/annotations/src/main/java/annotations/in/INSeparateAnnotation.java +++ b/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 & 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) * * See http://dx.doi.org/10.1109/HASE.2007.26. */ diff --git a/annotations2/pom.xml b/annotations2/pom.xml index ef33c7b1d..37c760325 100644 --- a/annotations2/pom.xml +++ b/annotations2/pom.xml @@ -40,6 +40,10 @@ org.apache.maven.plugins maven-jar-plugin + + org.apache.maven.plugins + maven-javadoc-plugin + org.apache.maven.plugins maven-source-plugin diff --git a/cmd-plugins/pom.xml b/cmd-plugins/pom.xml index e660db641..ab360b528 100644 --- a/cmd-plugins/pom.xml +++ b/cmd-plugins/pom.xml @@ -41,6 +41,10 @@ org.apache.maven.plugins maven-jar-plugin + + org.apache.maven.plugins + maven-javadoc-plugin + org.apache.maven.plugins maven-source-plugin diff --git a/dbgp/pom.xml b/dbgp/pom.xml index f9cb9854a..5d3c5dace 100644 --- a/dbgp/pom.xml +++ b/dbgp/pom.xml @@ -83,6 +83,10 @@ + + org.apache.maven.plugins + maven-javadoc-plugin + org.apache.maven.plugins maven-source-plugin diff --git a/dbgpc/pom.xml b/dbgpc/pom.xml index 22ba2e9ff..2fe2dc389 100644 --- a/dbgpc/pom.xml +++ b/dbgpc/pom.xml @@ -68,6 +68,10 @@ + + org.apache.maven.plugins + maven-javadoc-plugin + org.apache.maven.plugins maven-source-plugin diff --git a/examples/csvreader/pom.xml b/examples/csvreader/pom.xml index 1b9a434fd..c6aa05f94 100644 --- a/examples/csvreader/pom.xml +++ b/examples/csvreader/pom.xml @@ -28,6 +28,10 @@ org.apache.maven.plugins maven-jar-plugin + + org.apache.maven.plugins + maven-javadoc-plugin + org.apache.maven.plugins maven-source-plugin diff --git a/examples/lspplugin/pom.xml b/examples/lspplugin/pom.xml index c63749211..f88ba8844 100644 --- a/examples/lspplugin/pom.xml +++ b/examples/lspplugin/pom.xml @@ -32,6 +32,10 @@ org.apache.maven.plugins maven-jar-plugin + + org.apache.maven.plugins + maven-javadoc-plugin + org.apache.maven.plugins maven-source-plugin diff --git a/examples/pdfreader/pom.xml b/examples/pdfreader/pom.xml index f514eb985..8cbfb016b 100644 --- a/examples/pdfreader/pom.xml +++ b/examples/pdfreader/pom.xml @@ -33,6 +33,10 @@ org.apache.maven.plugins maven-jar-plugin + + org.apache.maven.plugins + maven-javadoc-plugin + org.apache.maven.plugins maven-source-plugin diff --git a/examples/simulation/pom.xml b/examples/simulation/pom.xml index f487f1ef4..b7c53d818 100644 --- a/examples/simulation/pom.xml +++ b/examples/simulation/pom.xml @@ -31,6 +31,10 @@ org.apache.maven.plugins maven-jar-plugin + + org.apache.maven.plugins + maven-javadoc-plugin + org.apache.maven.plugins maven-source-plugin diff --git a/examples/simulation/src/main/java/simulation/TestSimulation.java b/examples/simulation/src/main/java/simulation/TestSimulation.java index a9a093741..3aef75ad4 100644 --- a/examples/simulation/src/main/java/simulation/TestSimulation.java +++ b/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 diff --git a/examples/v2c/pom.xml b/examples/v2c/pom.xml index f922e2603..a7e15c1ab 100644 --- a/examples/v2c/pom.xml +++ b/examples/v2c/pom.xml @@ -39,6 +39,10 @@ org.apache.maven.plugins maven-jar-plugin + + org.apache.maven.plugins + maven-javadoc-plugin + org.apache.maven.plugins maven-source-plugin diff --git a/examples/vdmjplugin/pom.xml b/examples/vdmjplugin/pom.xml index 3e256e72a..357711cef 100644 --- a/examples/vdmjplugin/pom.xml +++ b/examples/vdmjplugin/pom.xml @@ -29,6 +29,10 @@ org.apache.maven.plugins maven-jar-plugin + + org.apache.maven.plugins + maven-javadoc-plugin + org.apache.maven.plugins maven-source-plugin diff --git a/lsp/pom.xml b/lsp/pom.xml index 9c79120b0..c852c3693 100644 --- a/lsp/pom.xml +++ b/lsp/pom.xml @@ -80,6 +80,10 @@ + + org.apache.maven.plugins + maven-javadoc-plugin + org.apache.maven.plugins maven-source-plugin diff --git a/pom.xml b/pom.xml index ff76bca7a..e7943f1ba 100644 --- a/pom.xml +++ b/pom.xml @@ -104,6 +104,7 @@ false + false true 8 diff --git a/quickcheck/pom.xml b/quickcheck/pom.xml index 8637eeb72..f64c93e1f 100644 --- a/quickcheck/pom.xml +++ b/quickcheck/pom.xml @@ -60,6 +60,10 @@ + + org.apache.maven.plugins + maven-javadoc-plugin + org.apache.maven.plugins maven-source-plugin diff --git a/quickcheck/src/main/java/quickcheck/visitors/RangeCreator.java b/quickcheck/src/main/java/quickcheck/visitors/RangeCreator.java index 4bc9ca910..c0e6330a4 100644 --- a/quickcheck/src/main/java/quickcheck/visitors/RangeCreator.java +++ b/quickcheck/src/main/java/quickcheck/visitors/RangeCreator.java @@ -114,7 +114,7 @@ protected List 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 <= limit. If n < 2, * just return 1. */ protected int leastPower(int n, int limit) diff --git a/quickcheck/src/main/java/quickcheck/visitors/TrivialQCVisitor.java b/quickcheck/src/main/java/quickcheck/visitors/TrivialQCVisitor.java index 28d976032..1a505c4d2 100644 --- a/quickcheck/src/main/java/quickcheck/visitors/TrivialQCVisitor.java +++ b/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> diff --git a/stdlib/pom.xml b/stdlib/pom.xml index 1535548ce..533bb46ff 100644 --- a/stdlib/pom.xml +++ b/stdlib/pom.xml @@ -57,6 +57,10 @@ org.apache.maven.plugins maven-jar-plugin + + org.apache.maven.plugins + maven-javadoc-plugin + org.apache.maven.plugins maven-source-plugin diff --git a/vdmj/pom.xml b/vdmj/pom.xml index 879679d11..cf62b308d 100644 --- a/vdmj/pom.xml +++ b/vdmj/pom.xml @@ -115,6 +115,10 @@ + + org.apache.maven.plugins + maven-javadoc-plugin + org.apache.maven.plugins maven-source-plugin