diff --git a/prism/src/explicit/Model.java b/prism/src/explicit/Model.java
index 8a420a52..79626f87 100644
--- a/prism/src/explicit/Model.java
+++ b/prism/src/explicit/Model.java
@@ -164,7 +164,7 @@ public interface Model
* Find all deadlock states and store this information in the model.
* If requested (if fix=true) and if needed (i.e. for DTMCs/CTMCs),
* fix deadlocks by adding self-loops in these states.
- * The set of deadlocks (before any possible fixing) can be obtained from {@link #getDeadlocks()}.
+ * The set of deadlocks (before any possible fixing) can be obtained from {@link #getDeadlockStates()}.
* @throws PrismException if the model is unable to fix deadlocks because it is non-mutable.
*/
public void findDeadlocks(boolean fix) throws PrismException;
diff --git a/prism/src/jdd/JDD.java b/prism/src/jdd/JDD.java
index b3e114ca..e2284547 100644
--- a/prism/src/jdd/JDD.java
+++ b/prism/src/jdd/JDD.java
@@ -473,7 +473,7 @@ public class JDD
// wrapper methods for dd_vars
/**
- * permute (->) variables in dd (cf. swap)
+ * permute (->) variables in dd (cf. swap)
*
[ REFS: result, DEREFS: dd ]
*/
public static JDDNode PermuteVariables(JDDNode dd, JDDVars old_vars, JDDVars new_vars)
@@ -484,7 +484,7 @@ public class JDD
}
/**
- * swap (<->) variables in dd (cf. permute)
+ * swap (<->) variables in dd (cf. permute)
*
[ REFS: result, DEREFS: dd ]
*/
public static JDDNode SwapVariables(JDDNode dd, JDDVars old_vars, JDDVars new_vars)
@@ -495,7 +495,7 @@ public class JDD
}
/**
- * build x > y for variables x, y
+ * build x > y for variables x, y
*
[ REFS: result, DEREFS: none ]
*/
public static JDDNode VariablesGreaterThan(JDDVars x_vars, JDDVars y_vars)
@@ -504,7 +504,7 @@ public class JDD
}
/**
- * build x >= y for variables x, y
+ * build x >= y for variables x, y
*
[ REFS: result, DEREFS: none ]
*/
public static JDDNode VariablesGreaterThanEquals(JDDVars x_vars, JDDVars y_vars)
@@ -513,7 +513,7 @@ public class JDD
}
/**
- * build x < y for variables x, y
+ * build x < y for variables x, y
*
[ REFS: result, DEREFS: none ]
*/
public static JDDNode VariablesLessThan(JDDVars x_vars, JDDVars y_vars)
@@ -522,7 +522,7 @@ public class JDD
}
/**
- * build x <= y for variables x, y
+ * build x <= y for variables x, y
*
[ REFS: result, DEREFS: none ]
*/
public static JDDNode VariablesLessThanEquals(JDDVars x_vars, JDDVars y_vars)
@@ -715,7 +715,7 @@ public class JDD
/**
* returns dd restricted to first non-zero path (cube)
- *
[ REFS: result, DEREFS:
=". + * Set the attached relational operator (e.g. "<" in "P<0.1"). + * The operator is passed as a string, e.g. "<" or ">=". */ public void setRelOp(String relOpString) { @@ -77,7 +77,7 @@ public abstract class ExpressionQuant extends Expression } /** - * Set the attached bound, as an expression (e.g. "p" in "P
> and [[.]] operators, i.e. quantification over strategies
+ * Class to represent ATL <<.>> and [[.]] operators, i.e. quantification over strategies
* ("there exists a strategy" or "for all strategies").
*/
public class ExpressionStrategy extends Expression
@@ -94,7 +94,7 @@ public class ExpressionStrategy extends Expression
}
/**
- * Get a string ""<<>>"" or "[[]]" indicating type of quantification.
+ * Get a string ""<<>>"" or "[[]]" indicating type of quantification.
*/
public String getOperatorString()
{
diff --git a/prism/src/parser/ast/ExpressionTemporal.java b/prism/src/parser/ast/ExpressionTemporal.java
index 909a1efe..476c1cce 100644
--- a/prism/src/parser/ast/ExpressionTemporal.java
+++ b/prism/src/parser/ast/ExpressionTemporal.java
@@ -91,7 +91,7 @@ public class ExpressionTemporal extends Expression
}
/**
- * Set lower time bound to be of form >= e
+ * Set lower time bound to be of form >= e
* (null denotes no lower bound, i.e. zero)
*/
public void setLowerBound(Expression e)
@@ -100,7 +100,7 @@ public class ExpressionTemporal extends Expression
}
/**
- * Set lower time bound to be of form >= e or > e
+ * Set lower time bound to be of form >= e or > e
* (null denotes no lower bound, i.e. zero)
*/
public void setLowerBound(Expression e, boolean strict)
@@ -110,7 +110,7 @@ public class ExpressionTemporal extends Expression
}
/**
- * Set upper time bound to be of form <= e
+ * Set upper time bound to be of form <= e
* (null denotes no upper bound, i.e. infinity)
*/
public void setUpperBound(Expression e)
@@ -119,7 +119,7 @@ public class ExpressionTemporal extends Expression
}
/**
- * Set upper time bound to be of form <= e or < e
+ * Set upper time bound to be of form <= e or < e
* (null denotes no upper bound, i.e. infinity)
*/
public void setUpperBound(Expression e, boolean strict)
diff --git a/prism/src/parser/ast/RelOp.java b/prism/src/parser/ast/RelOp.java
index 4608e38c..4cf5100e 100644
--- a/prism/src/parser/ast/RelOp.java
+++ b/prism/src/parser/ast/RelOp.java
@@ -31,7 +31,7 @@ public enum RelOp {
}
/**
- * Returns true if this corresponds to a lower bound (i.e. >, >=).
+ * Returns true if this corresponds to a lower bound (i.e. >, >=).
* NB: "min=?" does not return true for this.
*/
public boolean isLowerBound()
@@ -46,7 +46,7 @@ public enum RelOp {
}
/**
- * Returns true if this corresponds to an upper bound (i.e. <, <=).
+ * Returns true if this corresponds to an upper bound (i.e. <, <=).
* NB: "max=?" does not return true for this.
*/
public boolean isUpperBound()
@@ -61,7 +61,7 @@ public enum RelOp {
}
/**
- * Returns true if this is a strict bound (i.e. < or >).
+ * Returns true if this is a strict bound (i.e. < or >).
*/
public boolean isStrict()
{
@@ -102,7 +102,7 @@ public enum RelOp {
/**
* Returns the RelOp object corresponding to a (string) symbol,
- * e.g. parseSymbol("<=") returns RelOp.LEQ. Returns null if invalid.
+ * e.g. parseSymbol("<=") returns RelOp.LEQ. Returns null if invalid.
* @param symbol The symbol to look up
* @return
*/
diff --git a/prism/src/parser/ast/Update.java b/prism/src/parser/ast/Update.java
index 2e31cfc4..a3f0eff6 100644
--- a/prism/src/parser/ast/Update.java
+++ b/prism/src/parser/ast/Update.java
@@ -35,7 +35,7 @@ import prism.PrismLangException;
/**
* Class to store a single update, i.e. a mapping from variables to expressions.
- * e.g. (s'=1)&(x'=x+1)
+ * e.g. (s'=1)&(x'=x+1)
*/
public class Update extends ASTElement
{
diff --git a/prism/src/parser/ast/Updates.java b/prism/src/parser/ast/Updates.java
index 9de5e19c..ef924210 100644
--- a/prism/src/parser/ast/Updates.java
+++ b/prism/src/parser/ast/Updates.java
@@ -34,7 +34,7 @@ import prism.PrismLangException;
/**
* Class to store a list of updates with associated probabilities (or rates).
- * e.g. 0.5:(s'=1)&(x'=x+1) + 0.5:(s'=2)&(x'=x-1)
+ * e.g. 0.5:(s'=1)&(x'=x+1) + 0.5:(s'=2)&(x'=x-1)
*/
public class Updates extends ASTElement
{
diff --git a/prism/src/prism/DA.java b/prism/src/prism/DA.java
index de816f67..7bd0ff80 100644
--- a/prism/src/prism/DA.java
+++ b/prism/src/prism/DA.java
@@ -244,7 +244,7 @@ public class DA
The LTL formula is represented as a PRISM Expression,
+ *
The LTL formula is represented as a PRISM Expression,
* in which atomic propositions are represented by ExpressionLabel objects.
* @param ltl the LTL formula
* @param constants values for constants in the formula (may be {@code null})
@@ -136,7 +136,7 @@ public class LTL2RabinLibrary
}
/**
- * Construct a prism.DA
+ * Note that this method considers two points as "equal" if the method {@code isCloseTo(Point)} returns {@code true}.
* So the returned map will not contain two keys which are too close to each other, which should be fine w.r.t. roundoff
* errors, but might theoretically cause trouble if the corner points of the Pareto curve are very close to each other.
- *
+ *
* It is guaranteed that if there are two points {@code p1} and {@code p2} in {@code computedPoints} such that
* {@code p1.isCloseTo{p2}} is {@code true} and {@code p1} occurs in {@code computedPoints} before
* {@code p2}, then {@code p1} will be given precedence when picking a representative for the key in the map. This is crucial
@@ -291,7 +290,7 @@ public class MultiObjUtils
/**
* This method takes a list of points and returns a sub-list in which points that are very close to
- * each other (where {@link #isCloseTo(Point)} is used to determine what is "very close") are removed.
+ * each other (where {@code isCloseTo(Point)} is used to determine what is "very close") are removed.
* The order of elements is preserved.
*
* It is guaranteed that if there are two points {@code p1} and {@code p2} in {@code list} such that
@@ -328,7 +327,7 @@ public class MultiObjUtils
/**
* This method takes the set of some corner points of a pareto curve {@code computedPoints} together
- * with associated orthogonal lines {@directions} that determine current over-approximation,
+ * with associated orthogonal lines {@code directions} that determine current over-approximation,
* and returns the points which determine the over-approximation. (These points are in fact the intersecting
* points of the directions which are not covered by other points.)
* @param computedPoints Corner points of the Pareto curve
diff --git a/prism/src/prism/NativeIntArray.java b/prism/src/prism/NativeIntArray.java
index 28106364..fa344ffa 100644
--- a/prism/src/prism/NativeIntArray.java
+++ b/prism/src/prism/NativeIntArray.java
@@ -83,7 +83,6 @@ public class NativeIntArray
/**
* Returns the {@code index}-th element of the aray
* @param index
- * @return
* @throws IndexOutOfBoundsException If the index is outside of the bounds of the array
*/
public int get(int index) throws IndexOutOfBoundsException
@@ -96,7 +95,7 @@ public class NativeIntArray
/**
* Sets the {@code index}-th element of the array to {@code val}.
* @param index
- * @return
+ * @param value
* @throws IndexOutOfBoundsException If the index is outside of the bounds of the array
*/
public void set(int index, int value) throws IndexOutOfBoundsException
diff --git a/prism/src/prism/Operator.java b/prism/src/prism/Operator.java
index f936a673..5e2f27e9 100644
--- a/prism/src/prism/Operator.java
+++ b/prism/src/prism/Operator.java
@@ -42,8 +42,8 @@ public enum Operator {
}
/**
- * Returns {@code true} if op is one {@link Operator.P_MIN},
- * {@link Operator.R_MIN}, {@link Operator.P_LE}, or {@link Operator.R_LE}.
+ * Returns {@code true} if op is one {@code Operator.P_MIN},
+ * {@code Operator.R_MIN}, {@code Operator.P_LE}, or {@code Operator.R_LE}.
*/
public static boolean isMinOrLe(Operator op)
{
diff --git a/prism/src/prism/OpsAndBoundsList.java b/prism/src/prism/OpsAndBoundsList.java
index c047b89d..90fd8195 100644
--- a/prism/src/prism/OpsAndBoundsList.java
+++ b/prism/src/prism/OpsAndBoundsList.java
@@ -35,8 +35,8 @@ import java.util.List;
*
* The instance keeps an ordered instance of (operator,bound) values.
* These are currently held in two separate lists internally. A tuple
- * is added using {@link add(Operator,bound)} method, and retrieved using
- * {@link getOperator(int)} and {@link getBound(double} methods.
+ * is added using {@link add(OpRelOpBound, Operator,double,int)} method, and retrieved using
+ * {@link getOperator(int)} and {@link getBound(int)} methods.
*
* The class also provides methods for accessing i-th elements in the
* subsequence containing only the tuples in which operator is a probabilistic
@@ -226,7 +226,7 @@ public class OpsAndBoundsList
/**
* True if the ith probabilistic objective is negation of what the user required
- * (i.e. formula is negated and we use >= instead <= or max instead of min).
+ * (i.e. formula is negated and we use >= instead <= or max instead of min).
* Used to determine what values to display to the user.
* @param i
* @return
@@ -237,7 +237,7 @@ public class OpsAndBoundsList
}
/**
- * Replace min by max and <= by >= in prob.
+ * Replace min by max and <= by >= in prob.
*/
//TODO: why not do prob also in main list?
public void makeAllProbUp()
diff --git a/prism/src/prism/PermutedLexicographicComparator.java b/prism/src/prism/PermutedLexicographicComparator.java
index 61ac9314..934db980 100644
--- a/prism/src/prism/PermutedLexicographicComparator.java
+++ b/prism/src/prism/PermutedLexicographicComparator.java
@@ -32,8 +32,8 @@ import java.util.Comparator;
/**
* A class that allows to compare points w.r.g. a lexicographic order.
* The order of elements is given by the array {@code dimensionPermutation}
- * passed in the constructor {@link #PermutedLexicographicComparator(int[])}.
- *
+ * passed in the constructor {@link #PermutedLexicographicComparator(int[],boolean[])}.
+ *
* Note that the comparator is only capable of comparing points with equal
* dimension. This probably violates the specification of the {@link Comparator}
* class, but it shouldn't be any problem as comparing points of different dimensions
diff --git a/prism/src/prism/Prism.java b/prism/src/prism/Prism.java
index b83ec76a..0e3aef35 100644
--- a/prism/src/prism/Prism.java
+++ b/prism/src/prism/Prism.java
@@ -1095,7 +1095,7 @@ public class Prism extends PrismComponent implements PrismSettingsListener
/**
* Compare two version numbers of PRISM (strings).
* Example ordering: { "1", "2.0", "2.1.alpha", "2.1.alpha.r5555", "2.1.alpha.r5557", "2.1.beta", "2.1.beta4", "2.1", "2.1.dev", "2.1.dev.r6666", "2.1.dev1", "2.1.dev2", "2.1.2", "2.9", "3", "3.4"};
- * Returns: 1 if v1>v2, -1 if v1
* Also increases {@link #numberOfWarnings} by one. This variable can then be
* queried using {@link #getNumberOfWarnings()} at the end of computation
* and the user can be appropriately informed that there were warnings generated.
diff --git a/prism/src/prism/PrismUtils.java b/prism/src/prism/PrismUtils.java
index e9ed9360..0326db64 100644
--- a/prism/src/prism/PrismUtils.java
+++ b/prism/src/prism/PrismUtils.java
@@ -203,7 +203,7 @@ public class PrismUtils
}
/**
- * Format a double, as would be done by printf's %.