Fix JavaDoc bugs.

git-svn-id: https://www.prismmodelchecker.org/svn/prism/prism/trunk@10217 bbc10eb1-c90d-0410-af57-cb519fbb1720

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;

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)
 	 * <br>[ REFS: <i>result</i>, 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 (&lt;-&gt;) variables in dd (cf. permute)
 	 * <br>[ REFS: <i>result</i>, 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 &gt; y for variables x, y
 	 * <br>[ REFS: <i>result</i>, DEREFS: <i>none</i> ]
 	 */
 	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 &gt;= y for variables x, y
 	 * <br>[ REFS: <i>result</i>, DEREFS: <i>none</i> ]
 	 */
 	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 &lt; y for variables x, y
 	 * <br>[ REFS: <i>result</i>, DEREFS: <i>none</i> ]
 	 */
 	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 &lt;= y for variables x, y
 	 * <br>[ REFS: <i>result</i>, DEREFS: <i>none</i> ]
 	 */
 	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)
-	 * <br>[ REFS: <i>result</i>, DEREFS: <dd> ]
+	 * <br>[ REFS: <i>result</i>, DEREFS: dd ]
 	 */
 	public static JDDNode RestrictToFirst(JDDNode dd, JDDVars vars)
 	{
@@ -941,7 +941,7 @@ public class JDD
 
 	/**
 	 * sets element in vector dd
-	 * <br>[ REFS: <i>result</i>, DEREFS: <dd> ]
+	 * <br>[ REFS: <i>result</i>, DEREFS: dd ]
 	 */
 	public static JDDNode SetVectorElement(JDDNode dd, JDDVars vars, long index, double value)
 	{
@@ -952,7 +952,7 @@ public class JDD
 	
 	/**
 	 * sets element in matrix dd
-	 * <br>[ REFS: <i>result</i>, DEREFS: <dd> ]
+	 * <br>[ REFS: <i>result</i>, DEREFS: dd ]
 	 */
 	public static JDDNode SetMatrixElement(JDDNode dd, JDDVars rvars, JDDVars cvars, long rindex, long cindex, double value)
 	{
@@ -963,7 +963,7 @@ public class JDD
 	
 	/**
 	 * sets element in 3d matrix dd
-	 * <br>[ REFS: <i>result</i>, DEREFS: <dd> ]
+	 * <br>[ REFS: <i>result</i>, DEREFS: dd ]
 	 */
 	public static JDDNode Set3DMatrixElement(JDDNode dd, JDDVars rvars, JDDVars cvars, JDDVars lvars, long rindex, long cindex, long lindex, double value)
 	{
@@ -992,7 +992,7 @@ public class JDD
 	
 	/**
 	 * returns transpose of matrix dd
-	 * <br>[ REFS: <i>result</i>, DEREFS: <dd> ]
+	 * <br>[ REFS: <i>result</i>, DEREFS: dd ]
 	 */
 	public static JDDNode Transpose(JDDNode dd, JDDVars rvars, JDDVars cvars)
 	{
@@ -1003,7 +1003,7 @@ public class JDD
 	
 	/**
 	 * returns matrix multiplication of matrices dd1 and dd2
-	 * <br>[ REFS: <i>result</i>, DEREFS: <dd1, dd2> ]
+	 * <br>[ REFS: <i>result</i>, DEREFS: dd1, dd2 ]
 	 */
 	public static JDDNode MatrixMultiply(JDDNode dd1, JDDNode dd2, JDDVars vars, int method)
 	{
@@ -1144,10 +1144,10 @@ public class JDD
 	 * For example, for a model with the variable
 	 * 	x : [0..2];
 	 * and transitions
-	 *  [a] (x=0) -> 0.3:(x'=1) + 0.7:(x'=2);
-	 *  [b] (x=0) -> 1:(x'=2);
-	 *  [a] (x=2) -> (x'=1);
-	 *  [a] (x=1) -> (x'=0);
+	 *  [a] (x=0) -&gt; 0.3:(x'=1) + 0.7:(x'=2);
+	 *  [b] (x=0) -&gt; 1:(x'=2);
+	 *  [a] (x=2) -&gt; (x'=1);
+	 *  [a] (x=1) -&gt; (x'=0);
 	 * the output would be (e.g.)
  	 *  4
 	 *	4

prism/src/parser/ast/ExpressionProb.java

@@ -69,7 +69,7 @@ public class ExpressionProb extends ExpressionQuant
 	}
 
 	/**
-	 * Get a string describing the type of P operator, e.g. "P=?" or "P<p".
+	 * Get a string describing the type of P operator, e.g. "P=?" or "P&lt;p".
 	 */
 	public String getTypeOfPOperator()
 	{

prism/src/parser/ast/ExpressionQuant.java

@@ -38,11 +38,11 @@ public abstract class ExpressionQuant extends Expression
 {
 	/** Optional "modifier" to specify variants of the P/R/S operator */
 	protected String modifier = null;
-	/** The attached relational operator (e.g. "<" in "P<0.1"). */
+	/** The attached relational operator (e.g. "&lt;" in "P&lt;0.1"). */
 	protected RelOp relOp = null;
-	/** The attached (probability/reward) bound, as an expression (e.g. "p" in "P<p"). Null if absent (e.g. "P=?"). */
+	/** The attached (probability/reward) bound, as an expression (e.g. "p" in "P&lt;p"). Null if absent (e.g. "P=?"). */
 	protected Expression bound = null;
-	/** The main operand of the operator (e.g. "F target=true" in "P<0.1[F target=true]. */
+	/** The main operand of the operator (e.g. "F target=true" in "P&lt;0.1[F target=true]. */
 	protected Expression expression = null;
 	/** Optional "old-style" filter. This is just for display purposes since
 	  *  the parser creates an (invisible) new-style filter around this expression. */
@@ -59,7 +59,7 @@ public abstract class ExpressionQuant extends Expression
 	}
 
 	/**
-	 * Set the attached relational operator (e.g. "<" in "P<0.1").
+	 * Set the attached relational operator (e.g. "&lt;" in "P&lt;0.1").
 	 * Uses the enum {@link RelOp}. For example: {@code setRelOp(RelOp.GT);}
 	 */
 	public void setRelOp(RelOp relOp)
@@ -68,8 +68,8 @@ public abstract class ExpressionQuant extends Expression
 	}
 
 	/**
-	 * Set the attached relational operator (e.g. "<" in "P<0.1").
-	 * The operator is passed as a string, e.g. "<" or ">=".
+	 * Set the attached relational operator (e.g. "&lt;" in "P&lt;0.1").
+	 * The operator is passed as a string, e.g. "&lt;" or "&gt;=".
 	 */
 	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<p"). Should be null if absent (e.g. "P=?").
+	 * Set the attached bound, as an expression (e.g. "p" in "P&lt;p"). Should be null if absent (e.g. "P=?").
 	 */
 	public void setBound(Expression bound)
 	{
@@ -85,7 +85,7 @@ public abstract class ExpressionQuant extends Expression
 	}
 
 	/**
-	 * Set the main operand of the operator (e.g. "F target=true" in "P<0.1[F target=true].
+	 * Set the main operand of the operator (e.g. "F target=true" in "P&lt;0.1[F target=true].
 	 */
 	public void setExpression(Expression expression)
 	{
@@ -120,7 +120,7 @@ public abstract class ExpressionQuant extends Expression
 	}
 
 	/**
-	 * Get the attached relational operator (e.g. "<" in "P<0.1"), as a {@link RelOp}.
+	 * Get the attached relational operator (e.g. "&lt;" in "P&lt;0.1"), as a {@link RelOp}.
 	 */
 	public RelOp getRelOp()
 	{
@@ -128,7 +128,7 @@ public abstract class ExpressionQuant extends Expression
 	}
 
 	/**
-	 * Get the attached bound, as an expression (e.g. "p" in "P<p"). Should be null if absent (e.g. "P=?").
+	 * Get the attached bound, as an expression (e.g. "p" in "P&lt;p"). Should be null if absent (e.g. "P=?").
 	 */
 	public Expression getBound()
 	{
@@ -136,7 +136,7 @@ public abstract class ExpressionQuant extends Expression
 	}
 
 	/**
-	 * Get the main operand of the operator (e.g. "F target=true" in "P<0.1[F target=true].
+	 * Get the main operand of the operator (e.g. "F target=true" in "P&lt;0.1[F target=true].
 	 */
 	public Expression getExpression()
 	{
@@ -145,7 +145,7 @@ public abstract class ExpressionQuant extends Expression
 
 	/**
 	 * Get an object storing info about the attached relational operator and bound, after evaluating the bound to a double.
-	 * For example "<0.1" in "P<p" where p=0.5 in {@code constantValues}.
+	 * For example "&lt;0.1" in "P&lt;p" where p=0.5 in {@code constantValues}.
 	 * Does some checks, e.g., throws an exception if a probability is not in the range [0,1]
 	 * 
 	 * @param constantValues Values for constants in order to evaluate any bound

prism/src/parser/ast/ExpressionStrategy.java

@@ -33,7 +33,7 @@ import parser.visitor.ASTVisitor;
 import prism.PrismLangException;
 
 /**
- * Class to represent ATL <<.>> and [[.]] operators, i.e. quantification over strategies
+ * Class to represent ATL &lt;&lt;.&gt;&gt; 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 ""&lt;&lt;&gt;&gt;"" or "[[]]" indicating type of quantification.
 	 */
 	public String getOperatorString()
 	{

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 &lt;= 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 &lt;= e or &lt; e
 	 * (null denotes no upper bound, i.e. infinity)
 	 */
 	public void setUpperBound(Expression e, boolean strict)

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. &lt;, &lt;=).
 	 * 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. &lt; or &gt;).
 	 */
 	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("&lt;=") returns RelOp.LEQ. Returns null if invalid.
 	 * @param symbol The symbol to look up
 	 * @return
 	 */

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
 {

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
 {

prism/src/prism/DA.java

@@ -244,7 +244,7 @@ public class DA<Symbol, Acceptance extends AcceptanceOmega>
 
 	/**
 	 * Switch the acceptance condition. This may change the acceptance type,
-	 * i.e., a DA<BitSet, AcceptanceRabin> may become a DA<BitSet, AcceptanceStreett>
+	 * i.e., a DA&lt;BitSet, AcceptanceRabin&gt; may become a DA&lt;BitSet, AcceptanceStreett&gt;
 	 * @param da the automaton
 	 * @param newAcceptance the new acceptance condition
 	 */

prism/src/prism/IntegerBound.java

@@ -41,9 +41,9 @@ public class IntegerBound
 
 	/** Create new bounds.
 	 * @param lower: The lower bound, {@code null} represents "no lower bound"
-	 * @param lower_strict: Is the lower bound strict (> lower) or non-strict (>= lower)
+	 * @param lower_strict: Is the lower bound strict (> lower) or non-strict (>= lower)
 	 * @param upper: The upper bound, {@code null} represents "no upper bound"
-	 * @param upper_strict: Is the upper bound strict (< upper) or non-strict (<= upper)
+	 * @param upper_strict: Is the upper bound strict (&lt; upper) or non-strict (&lt;= upper)
 	 */
 	public IntegerBound(Integer lower, boolean lower_strict, Integer upper, boolean upper_strict)
 	{
@@ -86,7 +86,7 @@ public class IntegerBound
 	 * If {@code check} is {@code true}, throws an exception for negative or empty bounds.
 	 *
 	 * @param expression the expression
-	 * @param values the values for constants (may be {@code null})
+	 * @param constantValues the values for constants (may be {@code null})
 	 * @param check check for non-negative bounds / non-emptiness?
 	 * @return the {@code IntegerBound} for the expression
 	 * @throws PrismException
@@ -181,7 +181,7 @@ public class IntegerBound
 	}
 
 	/** Get the maximal interesting value, i.e., the value v such that
-	 *  for _all_ i>=v either isInBound(i)=true or isInBound(i)=false */
+	 *  for _all_ i&gt;=v either isInBound(i)=true or isInBound(i)=false */
 	public int getMaximalInterestingValue()
 	{
 		int max = 0;

prism/src/prism/LTL2DA.java

@@ -64,7 +64,7 @@ public class LTL2DA extends PrismComponent
 	 * The LTL formula is represented as a PRISM Expression,
 	 * in which atomic propositions are represented by ExpressionLabel objects.
 	 * @param ltl the formula
-	 * @param constantValues the values of constants, may be {@code null}
+	 * @param constants the values of constants, may be {@code null}
 	 * @param allowedAcceptance the AcceptanceTypes that are allowed to be returned
 	 */
 	public DA<BitSet,? extends AcceptanceOmega> convertLTLFormulaToDA(Expression ltl, Values constants, AcceptanceType... allowedAcceptance) throws PrismException

prism/src/prism/LTL2RabinLibrary.java

@@ -76,7 +76,7 @@ public class LTL2RabinLibrary
 	 *     constructions {@code constructDRAFor....}
 	 * </ul>
 	 * Return {@code null} if the automaton can not be constructed using the library.
-	 * <br/> The LTL formula is represented as a PRISM Expression,
+	 * <br> 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<BitSet,AcceptanceRabin> for the given until formula.
+	 * Construct a prism.DA&lt;BitSet,AcceptanceRabin&gt; for the given until formula.
 	 * The expression is expected to have the form a U b, where
 	 * a and b are either ExpressionLabels or true/false.
 	 * The operator can have integer bounds.

prism/src/prism/LTLModelChecker.java

@@ -165,7 +165,7 @@ public class LTLModelChecker extends PrismComponent
 
 	/**
 	 * Construct the product of a DA and a DTMC/CTMC.
-	 * @param dra The DA
+	 * @param da The DA
 	 * @param model The  DTMC/CTMC
 	 * @param labelDDs BDDs giving the set of states for each AP in the DA
 	 * @param daDDRowVarsCopy (Optionally) empty JDDVars object to obtain copy of DD row vars for DA

prism/src/prism/MultiObjModelChecker.java

@@ -113,7 +113,7 @@ public class MultiObjModelChecker extends PrismComponent
 	 * 
 	 * @param modelProduct
 	 * @param rewardsIndex
-	 * @param relOpsReward
+	 * @param opsAndBounds
 	 * @return True if some transitions were removed
 	 */
 	protected boolean removeNonZeroRewardTrans(NondetModel modelProduct, List<JDDNode> rewardsIndex, OpsAndBoundsList opsAndBounds)

prism/src/prism/MultiObjUtils.java

@@ -49,7 +49,6 @@ public class MultiObjUtils
 	 * 
 	 * @param point A point which should be at one direction from the separating hyperplane.
 	 * @param computedPoints Set of points which should be at the other direction from the separating hyperplane.
-	 * @param tolerance
 	 * @return A vector orthogonal to the computed separating hyperplane.
 	 * @throws PrismException When the LP solver throws an exception or returns an unexpected result, an exception with a related message is thrown.
 	 */
@@ -249,11 +248,11 @@ public class MultiObjUtils
 	 * This method takes a list of computed points together with their associated directions, where points are possibly
 	 * repeated, and returns a map in which to each point from {@code computedPoints} corresponds the associated direction
 	 * from {@code directions} which has the most extreme slope. Which extreme is taken depends on the {@code horiz} parameter.
-	 * <p/>
-	 * Note that this method considers two points as "equal" if the method {@link #isCloseTo(Point)} returns {@code true}.
+	 * <br>
+	 * 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.
-	 * <p/>
+	 * <br>
 	 * 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

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

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)
 	{

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 &gt;= instead &lt;= 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 &lt;= by &gt;= in prob.
 	 */
 	//TODO: why not do prob also in main list?
 	public void makeAllProbUp()

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[])}.
- * <p/>
+ * passed in the constructor {@link #PermutedLexicographicComparator(int[],boolean[])}.
+ * <br>
  * 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

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<v2, 0 if v1=v2
+	 * Returns: 1 if v1&gt;v2, -1 if v1&lt;v2, 0 if v1=v2
 	 */
 	public static int compareVersions(String v1, String v2)
 	{
@@ -2931,7 +2931,7 @@ public class Prism extends PrismComponent implements PrismSettingsListener
 	 * Note: All constants in the model file must have already been defined.
 	 * @param propertiesFile Properties file containing property to check, constants defined
 	 * @param undefinedConstants Details of constant ranges defining the experiment
-	 * @param resultsCollection Where to store the results
+	 * @param results Where to store the results
 	 * @param expr The property to check
 	 * @param initialState Initial state (if null, is selected randomly)
 	 * @param maxPathLength The maximum path length for sampling

prism/src/prism/PrismLog.java

@@ -373,7 +373,7 @@ public abstract class PrismLog
 	
 	/**
 	 * Prints a warning message {@code s}, preceded by "\nWarning: " and followed by a newline character.
-	 * <p/>
+	 * <br>
 	 * 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.

prism/src/prism/PrismUtils.java

@@ -203,7 +203,7 @@ public class PrismUtils
 	}
 
 	/**
-	 * Format a double, as would be done by printf's %.<prec>g
+	 * Format a double, as would be done by printf's %.(prec)g
 	 */
 	public static String formatDouble(int prec, double d)
 	{
@@ -214,7 +214,7 @@ public class PrismUtils
 	
 	/**
 	 * Create a string for a list of objects, with a specified separator,
-	 * e.g. ["a","b","c"], "," -> "a,b,c"
+	 * e.g. ["a","b","c"], "," -&gt; "a,b,c"
 	 */
 	public static String joinString(List<?> objs, String separator)
 	{
@@ -233,7 +233,7 @@ public class PrismUtils
 	
 	/**
 	 * Create a string for an array of objects, with a specified separator,
-	 * e.g. ["a","b","c"], "," -> "a,b,c"
+	 * e.g. ["a","b","c"], "," -&gt; "a,b,c"
 	 */
 	public static String joinString(Object[] objs, String separator)
 	{

prism/src/prism/StateValuesMTBDD.java

@@ -429,7 +429,6 @@ public class StateValuesMTBDD implements StateValues
 	/**
 	* Sum up the elements of the vector, over a subset of its DD vars
 	* store the result in a new StateValues (for newModel)
-	* @throws PrismException (on out-of-memory)
 	*/
 	public StateValues sumOverDDVars(JDDVars sumVars, Model newModel)
 	{

prism/src/prism/Tile.java

@@ -117,7 +117,7 @@ public class Tile
 	
 	/**
 	 * Returns true if this tile will be changed when {@code point} is added
-	 * to a parent {@link TileList}. If {@updateUpperBounds} is set, then also
+	 * to a parent {@link TileList}. If {@code updateUpperBounds} is set, then also
 	 * the information about the tile lying on a pareto curve is updated
 	 *
 	 * @param updateUpperBounds If true, the new point does not split the tile, and

prism/src/prism/UndefinedConstants.java

@@ -459,7 +459,6 @@ public class UndefinedConstants
 	 *  @param sl If sh are ss are null, this is the value to be assigned. Otherwise, it is the lower bound for the range.
 	 *  @param sh The upper bound for the range.
 	 *  @param ss The step for the values. Null means 1.
-	 *  @param useAll If true, throw an exception if {@code name} is does not need to be defined
 	 *  
 	 *  @return True if the constant was defined before.
 	 */
@@ -659,7 +658,7 @@ public class UndefinedConstants
 	}
 
 	/**
-	 * Get the number of ranging constants (constants with range > 1) from the model file.
+	 * Get the number of ranging constants (constants with range greater than 1) from the model file.
 	 */
 	public int getNumModelRangingConstants()
 	{
@@ -685,7 +684,7 @@ public class UndefinedConstants
 	}
 
 	/**
-	 * Get the number of ranging constants (constants with range > 1) from the properties file.
+	 * Get the number of ranging constants (constants with range greater than 1) from the properties file.
 	 */
 	public int getNumPropertyRangingConstants()
 	{
@@ -706,7 +705,7 @@ public class UndefinedConstants
 
 	/**
 	 * Get a list of DefinedConstant objects: one for each ranging constant,
-	 * i.e. each constant that has range > 1.
+	 * i.e. each constant that has range greater than 1.
 	 */
 	public Vector<DefinedConstant> getRangingConstants()
 	{