From 946c767fb58cd55e4b62bf6278d660b12d96e118 Mon Sep 17 00:00:00 2001 From: Dave Parker Date: Thu, 24 Jul 2014 00:02:31 +0000 Subject: [PATCH] Change visibility of some classes/methods in the param package to allow use from outside the package. git-svn-id: https://www.prismmodelchecker.org/svn/prism/prism/trunk@8964 bbc10eb1-c90d-0410-af57-cb519fbb1720 --- prism/src/param/BigRational.java | 253 ++++++++++++++++-------------- prism/src/param/Function.java | 61 +++---- prism/src/param/Point.java | 50 +++--- prism/src/param/RegionValues.java | 146 +++++++++-------- prism/src/param/StateValues.java | 64 ++++---- 5 files changed, 306 insertions(+), 268 deletions(-) diff --git a/prism/src/param/BigRational.java b/prism/src/param/BigRational.java index b6fe79df..b8ba1254 100644 --- a/prism/src/param/BigRational.java +++ b/prism/src/param/BigRational.java @@ -39,7 +39,8 @@ import java.math.BigInteger; * * @author Ernst Moritz Hahn (University of Oxford) */ -final class BigRational implements Comparable { +public final class BigRational implements Comparable +{ /** the BigInteger "-1" */ private final static BigInteger BMONE = BigInteger.ONE.negate(); /** the BigInteger "2" */ @@ -59,29 +60,29 @@ final class BigRational implements Comparable { final static BigRational MINF = new BigRational(BMONE, BigInteger.ZERO); /** the BigRational "not a number" */ final static BigRational NAN = new BigRational(BigInteger.ZERO, BigInteger.ZERO); - + /** numerator */ private BigInteger num; /** denominator */ private BigInteger den; - + // constructors - + /** * Creates a new BigRational with value 0. */ - BigRational() + public BigRational() { this.num = BigInteger.ZERO; this.den = BigInteger.ONE; } - + /** * Creates a new BigRational with value {@code num}. * * @param num value of new rational as an integer value */ - BigRational(BigInteger num) + public BigRational(BigInteger num) { this.num = num; this.den = BigInteger.ONE; @@ -94,7 +95,7 @@ final class BigRational implements Comparable { * @param num numerator of this BigRational * @param den denominator of this BigRational */ - BigRational(BigInteger num, BigInteger den) + public BigRational(BigInteger num, BigInteger den) { this(num, den, true); } @@ -108,7 +109,7 @@ final class BigRational implements Comparable { * @param den denominator of this BigRational * @param cancel true to ensure resulting BigRational is coprime */ - BigRational(BigInteger num, BigInteger den, boolean cancel) + public BigRational(BigInteger num, BigInteger den, boolean cancel) { if (den.equals(BigInteger.ZERO)) { int cmp = num.compareTo(BigInteger.ZERO); @@ -138,7 +139,7 @@ final class BigRational implements Comparable { this.num = num; this.den = den; } - + /** * Creates a new BigRational with value {@code num} / {@code den}. * Cancellation of {@code num} and {@code den} is applied. @@ -146,21 +147,21 @@ final class BigRational implements Comparable { * @param num numerator of this BigRational * @param den denominator of this BigRational */ - BigRational(long num, long den) + public BigRational(long num, long den) { this(new BigInteger(Long.toString(num)), new BigInteger(Long.toString(den))); } - + /** * Creates a new BigRational with value {@code num}. * * @param num value of new rational as an integer value */ - BigRational(long num) + public BigRational(long num) { this(num, 1); } - + /** * Creates a new BigRational from string {@code string}. * Formats supported are num / den where num and den are integers, @@ -168,7 +169,7 @@ final class BigRational implements Comparable { * * @param string string to create BigRational from */ - BigRational(String string) + public BigRational(String string) { if (string.equals("Infinity") || string.equals("Inf")) { this.num = new BigInteger("1"); @@ -177,82 +178,83 @@ final class BigRational implements Comparable { } else if (string.equals("-Infinity") || string.equals("-Inf")) { this.num = new BigInteger("-1"); this.den = new BigInteger("0"); - return; + return; } - BigInteger num; - BigInteger den; - string = string.trim(); - int slashIdx = string.indexOf('/'); - if (slashIdx < 0) { - // decimal point notation - Double.parseDouble(string); // ensures correctness of format - boolean negate = false; - if (string.charAt(0) == '-') { - negate = true; - string = string.substring(1); - } - int ePos = string.indexOf("e"); - if (ePos < 0) { - ePos = string.indexOf("E"); - } - String coefficient = string.substring(0, ePos >= 0 ? ePos : string.length()); - int dotIdx = coefficient.indexOf('.'); - int expo = 0; - String noDotCoeff; - if (dotIdx >= 0) { - noDotCoeff = coefficient.substring(0, dotIdx); - noDotCoeff += coefficient.substring(dotIdx + 1); - expo = -coefficient.substring(dotIdx + 1).length(); - } else { - noDotCoeff = coefficient; - } - if (ePos >= 0) { - String eStr = string.substring(ePos + 1); - int eInt = Integer.parseInt(eStr); - expo += eInt; - } - num = new BigInteger((negate ? "-" : "") + noDotCoeff); - BigInteger ten = BITEN; - if (expo == 0) { - den = BigInteger.ONE; - } else if (expo > 0) { - den = BigInteger.ONE; - num = num.multiply(ten.pow(expo)); - } else { // expo < 0 - den = ten.pow(-expo); - } - BigRational result = new BigRational(num, den, true); - this.num = result.num; - this.den = result.den; - } else { - // fractional - num = new BigInteger(string.substring(0, slashIdx)); - den = new BigInteger(string.substring(slashIdx + 1, string.length())); - BigRational r = cancel(num, den); - this.num = r.num; - this.den = r.den; - return; - } - } - + BigInteger num; + BigInteger den; + string = string.trim(); + int slashIdx = string.indexOf('/'); + if (slashIdx < 0) { + // decimal point notation + Double.parseDouble(string); // ensures correctness of format + boolean negate = false; + if (string.charAt(0) == '-') { + negate = true; + string = string.substring(1); + } + int ePos = string.indexOf("e"); + if (ePos < 0) { + ePos = string.indexOf("E"); + } + String coefficient = string.substring(0, ePos >= 0 ? ePos : string.length()); + int dotIdx = coefficient.indexOf('.'); + int expo = 0; + String noDotCoeff; + if (dotIdx >= 0) { + noDotCoeff = coefficient.substring(0, dotIdx); + noDotCoeff += coefficient.substring(dotIdx + 1); + expo = -coefficient.substring(dotIdx + 1).length(); + } else { + noDotCoeff = coefficient; + } + if (ePos >= 0) { + String eStr = string.substring(ePos + 1); + int eInt = Integer.parseInt(eStr); + expo += eInt; + } + num = new BigInteger((negate ? "-" : "") + noDotCoeff); + BigInteger ten = BITEN; + if (expo == 0) { + den = BigInteger.ONE; + } else if (expo > 0) { + den = BigInteger.ONE; + num = num.multiply(ten.pow(expo)); + } else { // expo < 0 + den = ten.pow(-expo); + } + BigRational result = new BigRational(num, den, true); + this.num = result.num; + this.den = result.den; + } else { + // fractional + num = new BigInteger(string.substring(0, slashIdx)); + den = new BigInteger(string.substring(slashIdx + 1, string.length())); + BigRational r = cancel(num, den); + this.num = r.num; + this.den = r.den; + return; + } + } + // helper functions - + /** * Negates this number. * Negation of INF, MINF are as usual, negation of NAN is NAN. * * @return negated BigRational */ - BigRational negate() { + public BigRational negate() + { return new BigRational(num.negate(), den, false); } - + /** * Convert to coprime BigRational. * * @return coprime rational with the same value as this object */ - BigRational cancel() + public BigRational cancel() { return new BigRational(this.num, this.den, true); } @@ -270,10 +272,10 @@ final class BigRational implements Comparable { { return new BigRational(num, den); } - + // operations - - BigRational add(BigRational other, boolean cancel) + + public BigRational add(BigRational other, boolean cancel) { if (this.isNaN() || other.isNaN()) { return NAN; @@ -292,12 +294,12 @@ final class BigRational implements Comparable { return new BigRational(num, den, cancel); } - BigRational add(BigRational other) + public BigRational add(BigRational other) { return add(other, true); } - BigRational subtract(BigRational other) + public BigRational subtract(BigRational other) { if (this.isNaN() || other.isNaN()) { return NAN; @@ -328,7 +330,7 @@ final class BigRational implements Comparable { * @param other BigRational to multiply with * @return result of the multiplication */ - BigRational multiply(BigRational other, boolean cancel) + public BigRational multiply(BigRational other, boolean cancel) { if (this.isNaN() || other.isNaN()) { return NAN; @@ -343,8 +345,8 @@ final class BigRational implements Comparable { BigInteger den = this.den.multiply(other.den); return new BigRational(num, den, cancel); } - - BigRational multiply(BigRational other) + + public BigRational multiply(BigRational other) { return multiply(other, true); } @@ -356,7 +358,7 @@ final class BigRational implements Comparable { * @param cancel whether ensure result rational is comprime * @return result of the multiplication */ - BigRational multiply(long other, boolean cancel) + public BigRational multiply(long other, boolean cancel) { return multiply(new BigRational(other), cancel); } @@ -367,8 +369,8 @@ final class BigRational implements Comparable { * * @param other long to multiply with * @return result of the multiplication - */ - BigRational multiply(long other) + */ + public BigRational multiply(long other) { return multiply(other, true); } @@ -380,7 +382,7 @@ final class BigRational implements Comparable { * @param cancel whether ensure result rational is comprime * @return result of the division */ - BigRational divide(BigRational other, boolean cancel) + public BigRational divide(BigRational other, boolean cancel) { if (other.isInf() || other.isMInf()) { return NAN; @@ -388,15 +390,15 @@ final class BigRational implements Comparable { BigRational inverseOther = new BigRational(other.den, other.num, cancel); return multiply(inverseOther, cancel); } - + /** * Divides this BigRational with {@code other}. * Ensures result rational is coprime * * @param other long to divide by * @return result of the division - */ - BigRational divide(BigRational other) + */ + public BigRational divide(BigRational other) { return divide(other, true); } @@ -407,8 +409,8 @@ final class BigRational implements Comparable { * * @param other long to divide by * @return result of the division - */ - BigRational divide(long other) + */ + public BigRational divide(long other) { return divide(new BigRational(other)); } @@ -418,18 +420,18 @@ final class BigRational implements Comparable { * * @return -1, 0 or 1 as the value of this BigInteger is negative, zero or positive. */ - int signum() + public int signum() { return num.signum() * den.signum(); } - + /** * Returns a BigRational whose value is {@code this} to the {@code exponent}. * * @param exponent exponent to which this number is raised * @return {@code this} to the {@code exponent} */ - BigRational pow(int exponent) + public BigRational pow(int exponent) { BigInteger num; BigInteger den; @@ -444,7 +446,7 @@ final class BigRational implements Comparable { } return new BigRational(num, den, false); } - + /** * Compares {@code this} to {@code obj}. * Returns true iff {@code obj} is a BigRational which represents @@ -454,7 +456,8 @@ final class BigRational implements Comparable { * @return true iff {@code obj} is a BigRational which represents the same rational number as {@code this}. */ @Override - public boolean equals(Object obj) { + public boolean equals(Object obj) + { if (!(obj instanceof BigRational)) { return false; } @@ -470,7 +473,7 @@ final class BigRational implements Comparable { } return this.num.equals(other.num) && this.den.equals(other.den); } - + /** * Returns a hash code for this object. * @@ -481,7 +484,7 @@ final class BigRational implements Comparable { { return 37 * num.hashCode() + den.hashCode(); } - + /** * Returns a double approximation of value represented by this BigRational. * There are no guarantees on preciseness currently, so this function @@ -492,7 +495,7 @@ final class BigRational implements Comparable { * * @return a double approximation of the rational represented by this object */ - double doubleValue() + public double doubleValue() { if (isNaN()) { return Double.NaN; @@ -502,7 +505,7 @@ final class BigRational implements Comparable { return Double.NEGATIVE_INFINITY; } else if (isOne()) { return 1.0; - } else if (isZero()) { + } else if (isZero()) { return 0.0; } BigInteger shiftedNum; @@ -523,7 +526,8 @@ final class BigRational implements Comparable { * @return string representation of this rational number */ @Override - public String toString() { + public String toString() + { if (isNaN()) { return "NaN"; } else if (isInf()) { @@ -543,7 +547,8 @@ final class BigRational implements Comparable { * @return -1, 0 or 1 as this BigRational is numerically less than, equal to, or greater than {@code other}. */ @Override - public int compareTo(BigRational other) { + public int compareTo(BigRational other) + { if (this.isInf()) { if (other.isInf()) { return 0; @@ -566,7 +571,8 @@ final class BigRational implements Comparable { * * @return -1, 0 or 1 as this BigRational is numerically less than, equal to, or greater than {@code other}. */ - public int compareTo(long i) { + public int compareTo(long i) + { return this.compareTo(new BigRational(i)); } @@ -575,7 +581,8 @@ final class BigRational implements Comparable { * * @return numerator of this BigRational as a BigInteger */ - java.math.BigInteger getNum() { + public java.math.BigInteger getNum() + { return num; } @@ -584,7 +591,8 @@ final class BigRational implements Comparable { * * @return denominator of this BigRational as a BigInteger */ - java.math.BigInteger getDen() { + public java.math.BigInteger getDen() + { return den; } @@ -593,21 +601,23 @@ final class BigRational implements Comparable { * * @return absolute value of this BigRational */ - BigRational abs() { + public BigRational abs() + { if (num.signum() == -1) { return new BigRational(num.negate(), den); } else { return this; } } - + /** * Returns larger value of {@code this} and {@code other}. * * @param other rational number to compare to * @return {@code other} if {@code other} this is larger than {@code this} and {@code this} otherwise */ - BigRational max(BigRational other) { + public BigRational max(BigRational other) + { if (this.compareTo(other) >= 0) { return this; } else { @@ -621,7 +631,8 @@ final class BigRational implements Comparable { * @param other rational number to compare to * @return {@code other} if {@code other} this is smaller than {@code this} and {@code this} otherwise */ - BigRational min(BigRational other) { + public BigRational min(BigRational other) + { if (this.compareTo(other) <= 0) { return this; } else { @@ -634,7 +645,7 @@ final class BigRational implements Comparable { * * @return true iff this BigRational represents the number zero */ - boolean isZero() + public boolean isZero() { return num.equals(BigInteger.ZERO) && den.equals(BigInteger.ONE); } @@ -644,7 +655,7 @@ final class BigRational implements Comparable { * * @return true iff this BigRational represents the number one */ - boolean isOne() + public boolean isOne() { return num.equals(BigInteger.ONE) && den.equals(BigInteger.ONE); } @@ -654,17 +665,17 @@ final class BigRational implements Comparable { * * @return true iff this BigRational represents the special value not-a-number" */ - boolean isNaN() + public boolean isNaN() { return num.equals(BigInteger.ZERO) && den.equals(BigInteger.ZERO); } - + /** * Returns true iff this BigRational represents positive infinity. * * @return true iff this BigRational represents positive infinity */ - boolean isInf() + public boolean isInf() { return num.equals(BigInteger.ONE) && den.equals(BigInteger.ZERO); } @@ -674,11 +685,11 @@ final class BigRational implements Comparable { * * @return true iff this BigRational represents negative infinity */ - boolean isMInf() + public boolean isMInf() { return num.equals(BMONE) && den.equals(BigInteger.ZERO); } - + /** * Returns true iff this object represents a true rational number. * This excludes the values for not-a-number as well as positive @@ -686,11 +697,11 @@ final class BigRational implements Comparable { * * @return true iff this object represents a true rational number */ - boolean isRational() + public boolean isRational() { return !isNaN() && !isInf() && !isMInf(); } - + /** * Returns true iff this value represents a special number. * This is the case if this is either not-a-number, positive or @@ -698,7 +709,7 @@ final class BigRational implements Comparable { * * @return true iff this object represents a special number */ - boolean isSpecial() + public boolean isSpecial() { return isNaN() || isInf() || isMInf(); } diff --git a/prism/src/param/Function.java b/prism/src/param/Function.java index 94ca2c65..10559d43 100644 --- a/prism/src/param/Function.java +++ b/prism/src/param/Function.java @@ -52,20 +52,22 @@ package param; * @see FunctionFactory * @author Ernst Moritz Hahn (University of Oxford) */ -abstract class Function extends StateValue { +public abstract class Function extends StateValue +{ /** function factory for this function */ protected FunctionFactory factory; - + /** * Creates a new function. * For internal use. * * @param factory factory used for this function */ - protected Function(FunctionFactory factory) { + protected Function(FunctionFactory factory) + { this.factory = factory; } - + /** * Adds {@code other} to this function. * @@ -73,14 +75,14 @@ abstract class Function extends StateValue { * @return sum of {@code} this and {@other} */ abstract Function add(Function other); - + /** * Negates this rational function. * * @return negated rational function. */ abstract Function negate(); - + /** * Multiplies {@code other} with this function. * @@ -88,7 +90,7 @@ abstract class Function extends StateValue { * @return product of {@code} this and {@other} */ abstract Function multiply(Function other); - + /** * Divides this function by {@code other}. * @@ -96,7 +98,7 @@ abstract class Function extends StateValue { * @return {@code this} divided by {@other} */ abstract Function divide(Function other); - + /** * Performs the {@code star} operation with this function. * The value of the result is equal to 1/(1-{@code this}). @@ -107,7 +109,7 @@ abstract class Function extends StateValue { * @return result of star operation */ abstract Function star(); - + /** * Returns a simplified version for constraint checking. * The function returned shall be a polynomial which is above/equal to @@ -120,7 +122,7 @@ abstract class Function extends StateValue { * @return simplified form for constraint checking */ abstract Function toConstraint(); - + /** * Evaluate this function at a given point. * The {@code point} represents an evaluation of the parameters, with @@ -132,7 +134,7 @@ abstract class Function extends StateValue { * @return value at the given parameter evaluation */ abstract BigRational evaluate(Point point, boolean cancel); - + /** * Returns a BigRational representing the same number as this object. * Only works of this function is actually a rational number. Otherwise, @@ -141,78 +143,82 @@ abstract class Function extends StateValue { * @return BigRational representation of this function */ abstract BigRational asBigRational(); - + /** * Returns true iff this function represents not-a-number. * @return true iff this function represents not-a-number */ abstract boolean isNaN(); - + /** * Returns true iff this function represents positive infinity. * @return true iff this function represents positive infinity */ abstract boolean isInf(); - + /** * Returns true iff this function represents negative infinity. * @return true iff this function represents negative infinity */ abstract boolean isMInf(); - + /** * Returns true iff this function represents the number one. * @return true iff this function represents the number one */ abstract boolean isOne(); - + /** * Returns true iff this function represents the number zero. * @return true iff this function represents the number zero */ abstract boolean isZero(); - + /** * Multiplies {@code byNumber} with this function. * * @param number to multiply with this function * @return product of {@code} this and {@byNumber} */ - Function multiply(int byNumber) { + public Function multiply(int byNumber) + { Function byFunction = factory.fromLong(byNumber); return multiply(byFunction); } - + /** * Divides this function by {@code byNumber}. * * @param number to divide this function by * @return this function divided by {@code byNumber} */ - Function divide(int byNumber) { + public Function divide(int byNumber) + { Function byFunction = factory.fromLong(byNumber); return divide(byFunction); } - + /** * Returns the {@code FunctionFactory} of this function. * * @return {@code FunctionFactory} of this function */ - FunctionFactory getFactory() { + public FunctionFactory getFactory() + { return factory; } - + /** * Aubtracts {@code other} from this function. * * @param other function to subtract from this function * @return this function minus {@coce other} */ - Function subtract(Function other) { + public Function subtract(Function other) + { return add(other.negate()); } - + /** * Evaluate this function at a given point. * The {@code point} represents an evaluation of the parameters, with @@ -223,10 +229,11 @@ abstract class Function extends StateValue { * @param point parameter evaluation to evaluate * @return value at the given parameter evaluation */ - BigRational evaluate(Point point) { + public BigRational evaluate(Point point) + { return evaluate(point, true); } - + /** * Checks whether this function is {@code >= 0} / {@code >0} at the given point. * diff --git a/prism/src/param/Point.java b/prism/src/param/Point.java index 6817f746..2d7452ab 100644 --- a/prism/src/param/Point.java +++ b/prism/src/param/Point.java @@ -35,35 +35,37 @@ package param; * @author Ernst Moritz Hahn (University of Oxford) * @see Region */ -final class Point { +public final class Point +{ /** coordinates of point */ private BigRational[] dimensions; - + /** * Constructs a new point. * * @param dimensions coordinates of this point */ - Point(BigRational[] dimensions) + public Point(BigRational[] dimensions) { this.dimensions = new BigRational[dimensions.length]; - System.arraycopy(dimensions, 0, this.dimensions, 0, dimensions.length); + System.arraycopy(dimensions, 0, this.dimensions, 0, dimensions.length); } - + /** * Returns value of a given coordinate * @param dim coordinate to return value of * @return value of given coordinate */ - BigRational getDimension(int dim) + public BigRational getDimension(int dim) { return dimensions[dim]; } - + @Override - public String toString() { + public String toString() + { StringBuilder builder = new StringBuilder(); - + builder.append("("); for (int dim = 0; dim < dimensions.length; dim++) { builder.append(dimensions[dim].doubleValue()); @@ -72,38 +74,39 @@ final class Point { } } builder.append(")"); - + return builder.toString(); } - + /** * Returns array representation of point. * * @return array representation of point */ - BigRational[] toArray() + public BigRational[] toArray() { BigRational[] result = new BigRational[dimensions.length]; - System.arraycopy(this.dimensions, 0, result, 0, this.dimensions.length); + System.arraycopy(this.dimensions, 0, result, 0, this.dimensions.length); return result; } - + /** * Returns number of dimensions of point. * * @return number of dimensions of point */ - int size() + public int size() { return dimensions.length; } - + @Override - public boolean equals(Object obj) { + public boolean equals(Object obj) + { if (!(obj instanceof Point)) { return false; } - + Point other = (Point) obj; if (this.dimensions.length != other.dimensions.length) { return false; @@ -115,18 +118,19 @@ final class Point { } return true; } - + @Override - public int hashCode() { + public int hashCode() + { int hash = 0; - + for (int i = 0; i < dimensions.length; i++) { hash = dimensions[i].hashCode() + (hash << 6) + (hash << 16) - hash; } - + return hash; } - + /** * Returns array of doubles approximating this point. * diff --git a/prism/src/param/RegionValues.java b/prism/src/param/RegionValues.java index ac26c6e0..c1822dc3 100644 --- a/prism/src/param/RegionValues.java +++ b/prism/src/param/RegionValues.java @@ -40,39 +40,40 @@ import java.util.Map.Entry; * * @author Ernst Moritz Hahn (University of Oxford) */ -final class RegionValues implements Iterable> { +public final class RegionValues implements Iterable> +{ /** list of all regions */ private ArrayList regions; /** assigning values to regions */ - private HashMap values; + private HashMap values; /** region factory this object belongs to */ private RegionFactory factory; - + // constructors - - RegionValues(RegionFactory factory) + + public RegionValues(RegionFactory factory) { regions = new ArrayList(); - values = new HashMap(); + values = new HashMap(); this.factory = factory; } - - int getNumStates() + + public int getNumStates() { return factory.getNumStates(); } - - int getInitState() + + public int getInitState() { return factory.getInitialState(); } - - void add(Region region, StateValues result) + + public void add(Region region, StateValues result) { regions.add(region); values.put(region, result); } - + /** * Helper function for simplify. * Subsumes some of the regions. If it contains true, must be called @@ -84,13 +85,12 @@ final class RegionValues implements Iterable> { { boolean changed = false; ArrayList newRegions = new ArrayList(); - HashMap newValues = new HashMap(); + HashMap newValues = new HashMap(); HashSet done = new HashSet(); - + for (Region region1 : regions) { for (Region region2 : regions) { - if (values.get(region1).equals(values.get(region2)) && region1.adjacent(region2) - && !done.contains(region1) && !done.contains(region2)) { + if (values.get(region1).equals(values.get(region2)) && region1.adjacent(region2) && !done.contains(region1) && !done.contains(region2)) { done.add(region1); done.add(region2); Region newRegion = region1.glue(region2); @@ -107,54 +107,54 @@ final class RegionValues implements Iterable> { newValues.put(region, values.get(region)); } } - + regions.clear(); values.clear(); regions.addAll(newRegions); values.putAll(newValues); - + return changed; } - + /** * Simplify by subsuming adjacent regions with same value. */ - void simplify() + public void simplify() { if (factory.isSubsumeRegions()) { while (simplifyIter()) ; } } - - Region getRegion(int number) + + public Region getRegion(int number) { return regions.get(number); } - - int getNumRegions() + + public int getNumRegions() { return regions.size(); } - - StateValues getResult(int number) + + public StateValues getResult(int number) { return values.get(regions.get(number)); } - - StateValues getResult(Region region) + + public StateValues getResult(Region region) { return values.get(region); } - - void cosplit(RegionValues other) + + public void cosplit(RegionValues other) { this.simplify(); other.simplify(); - + ArrayList newRegions = new ArrayList(); - HashMap thisNewStateValues = new HashMap(); - HashMap otherNewStateValues = new HashMap(); + HashMap thisNewStateValues = new HashMap(); + HashMap otherNewStateValues = new HashMap(); for (Region thisRegion : this.regions) { for (Region otherRegion : other.regions) { Region newRegion = thisRegion.conjunct(otherRegion); @@ -165,15 +165,16 @@ final class RegionValues implements Iterable> { } } } - + this.regions = new ArrayList(newRegions); this.values = thisNewStateValues; other.regions = new ArrayList(newRegions); other.values = otherNewStateValues; } - + @Override - public String toString() { + public String toString() + { StringBuilder builder = new StringBuilder(); for (int i = 0; i < regions.size(); i++) { Region region = regions.get(i); @@ -182,11 +183,12 @@ final class RegionValues implements Iterable> { builder.append(values.get(region)); builder.append("\n"); } - + return builder.toString(); } - void addAll(RegionValues other) { + public void addAll(RegionValues other) + { int numOtherRegions = other.getNumRegions(); for (int i = 0; i < numOtherRegions; i++) { Region region = other.getRegion(i); @@ -194,8 +196,8 @@ final class RegionValues implements Iterable> { values.put(region, other.getResult(region)); } } - - void clearExcept(BitSet except) + + public void clearExcept(BitSet except) { for (Region region : regions) { StateValues vals = values.get(region); @@ -205,7 +207,7 @@ final class RegionValues implements Iterable> { if (oldValue instanceof StateBoolean) { vals.setStateValue(state, false); } else if (oldValue instanceof Function) { - vals.setStateValue(state, factory.getFunctionFactory().getZero()); + vals.setStateValue(state, factory.getFunctionFactory().getZero()); } else { throw new RuntimeException(); } @@ -214,8 +216,8 @@ final class RegionValues implements Iterable> { } simplify(); } - - void clearExceptInit() + + public void clearExceptInit() { if (regions.isEmpty()) { return; @@ -227,16 +229,17 @@ final class RegionValues implements Iterable> { } @Override - public Iterator> iterator() { + public Iterator> iterator() + { return values.entrySet().iterator(); } - - RegionFactory getRegionFactory() + + public RegionFactory getRegionFactory() { return factory; } - - boolean booleanValues() + + public boolean booleanValues() { if (regions.isEmpty()) { return true; @@ -244,7 +247,8 @@ final class RegionValues implements Iterable> { return values.get(regions.get(0)).getStateValue(0) instanceof StateBoolean; } - RegionValues binaryOp(int op, RegionValues other) { + public RegionValues binaryOp(int op, RegionValues other) + { RegionValues result = new RegionValues(factory); RegionValuesIntersections co = new RegionValuesIntersections(this, other); for (RegionIntersection inter : co) { @@ -257,7 +261,8 @@ final class RegionValues implements Iterable> { return result; } - RegionValues binaryOp(int op, BigRational p) { + public RegionValues binaryOp(int op, BigRational p) + { RegionValues result = new RegionValues(factory); Function pFn = factory.getFunctionFactory().fromBigRational(p); StateValues pValue = new StateValues(values.get(regions.get(0)).getNumStates(), factory.getInitialState(), pFn); @@ -269,7 +274,7 @@ final class RegionValues implements Iterable> { return result; } - RegionValues op(int op, BitSet whichStates) + public RegionValues op(int op, BitSet whichStates) { RegionValues result = new RegionValues(factory); if (op == Region.FIRST) { @@ -312,7 +317,7 @@ final class RegionValues implements Iterable> { Function countFn = factory.getFunctionFactory().fromLong(count); StateValues resValues = new StateValues(getNumStates(), getInitState(), countFn); result.add(region, resValues); - } + } } else if (op == Region.FORALL) { for (Region region : regions) { StateValues vals = values.get(region); @@ -327,7 +332,7 @@ final class RegionValues implements Iterable> { } StateValues resValues = new StateValues(getNumStates(), getInitState(), forall); result.add(region, resValues); - } + } } else if (op == Region.EXISTS) { for (Region region : regions) { StateValues vals = values.get(region); @@ -342,15 +347,15 @@ final class RegionValues implements Iterable> { } StateValues resValues = new StateValues(getNumStates(), getInitState(), exists); result.add(region, resValues); - } + } } else { throw new RuntimeException("unknown operator"); } - + return result; } - - boolean parameterIndependent() + + public boolean parameterIndependent() { simplify(); if (regions.size() > 1) { @@ -359,16 +364,17 @@ final class RegionValues implements Iterable> { if (!regions.get(0).volume().equals(factory.getFunctionFactory().getOne().asBigRational())) { return false; } - + return true; } - StateValues getStateValues() + public StateValues getStateValues() { return values.get(regions.get(0)); } - void clearNotNeeded(BitSet needStates) { + public void clearNotNeeded(BitSet needStates) + { for (Region region : regions) { StateValues vals = values.get(region); for (int state = 0; state < vals.getNumStates(); state++) { @@ -384,26 +390,27 @@ final class RegionValues implements Iterable> { simplify(); } - String filteredString(BitSet filter) { + public String filteredString(BitSet filter) + { StringBuilder builder = new StringBuilder(); - + for (Region region : regions) { builder.append(region); StateValues vals = values.get(region); for (int stateNr = filter.nextSetBit(0); stateNr >= 0; stateNr = filter.nextSetBit(stateNr + 1)) { builder.append(stateNr); builder.append(":"); -// builder.append(statesList.get(stateNr).toString()); + // builder.append(statesList.get(stateNr).toString()); builder.append("="); builder.append(vals.getStateValue(stateNr)); } } - + return builder.toString(); } - - RegionValues unaryOp(int parserUnaryOpToRegionOp) { + public RegionValues unaryOp(int parserUnaryOpToRegionOp) + { RegionValues result = new RegionValues(factory); for (Region region : regions) { StateValues value = unaryOp(parserUnaryOpToRegionOp, values.get(region)); @@ -412,7 +419,8 @@ final class RegionValues implements Iterable> { return result; } - private StateValues unaryOp(int op, StateValues stateValues) { + private StateValues unaryOp(int op, StateValues stateValues) + { StateValues result = new StateValues(getNumStates(), getInitState()); for (int state = 0; state < stateValues.getNumStates(); state++) { StateValue value = null; @@ -430,5 +438,5 @@ final class RegionValues implements Iterable> { result.setStateValue(state, value); } return result; - } + } } diff --git a/prism/src/param/StateValues.java b/prism/src/param/StateValues.java index b5c3dfa9..3a339d75 100644 --- a/prism/src/param/StateValues.java +++ b/prism/src/param/StateValues.java @@ -38,12 +38,13 @@ import java.util.BitSet; * @author Ernst Moritz Hahn (University of Oxford) * @see RegionValues */ -final class StateValues { +public final class StateValues +{ /** assigns values to each state of the model */ private ArrayList values; /** initial state of the model */ - int initState; - + private int initState; + /** * Constructs new set of state values. * Each state is mapped to {@code null}. @@ -51,7 +52,7 @@ final class StateValues { * @param numStates number of states of model * @param initState initial state of the model */ - StateValues(int numStates, int initState) + public StateValues(int numStates, int initState) { values = new ArrayList(numStates); for (int state = 0; state < numStates; state++) { @@ -59,7 +60,7 @@ final class StateValues { } this.initState = initState; } - + /** * Constructs new set of state values. * Each state is mapped to the given value. @@ -68,7 +69,8 @@ final class StateValues { * @param initState initial state of the model * @param value value to map all states to */ - StateValues(int numStates, int initState, StateValue value) { + public StateValues(int numStates, int initState, StateValue value) + { this(numStates, initState); for (int state = 0; state < numStates; state++) { values.set(state, value); @@ -82,37 +84,41 @@ final class StateValues { * @param numStates number of states of the model * @param initState initial state of the model * @param value value to map all states to - */ - StateValues(int numStates, int initState, boolean value) { + */ + public StateValues(int numStates, int initState, boolean value) + { this(numStates, initState, new StateBoolean(value)); } @Override - public String toString() { + public String toString() + { return values.get(initState).toString(); } - + @Override - public boolean equals(Object obj) { + public boolean equals(Object obj) + { if (!(obj instanceof StateValues)) { return false; } StateValues result = (StateValues) obj; - + for (int i = 0; i < values.size(); i++) { if (!values.get(i).equals(result.values.get(i))) { return false; } } - + return true; } - + @Override - public int hashCode() { + public int hashCode() + { int hash = 0; - + for (int i = 0; i < values.size(); i++) { hash = values.get(i).hashCode() + (hash << 6) + (hash << 16) - hash; } @@ -126,29 +132,29 @@ final class StateValues { * @param state state to get value of * @return value of given state */ - StateValue getStateValue(int state) + public StateValue getStateValue(int state) { return values.get(state); } - + /** * Set value of given state. * * @param state state to set value of * @param value value to set for state */ - void setStateValue(int state, StateValue value) + public void setStateValue(int state, StateValue value) { values.set(state, value); } - + /** * Set value of given state. * * @param state state to set value of * @param value value to set for state */ - void setStateValue(int state, boolean value) + public void setStateValue(int state, boolean value) { values.set(state, new StateBoolean(value)); } @@ -160,7 +166,7 @@ final class StateValues { * @param state state to get value of * @return value of the state as a function */ - Function getStateValueAsFunction(int state) + public Function getStateValueAsFunction(int state) { return (Function) values.get(state); } @@ -172,7 +178,7 @@ final class StateValues { * @param state state to get value of * @return value of the state as a boolean */ - boolean getStateValueAsBoolean(int state) + public boolean getStateValueAsBoolean(int state) { return ((StateBoolean) values.get(state)).getValue(); } @@ -183,7 +189,7 @@ final class StateValues { * * @return value of the initial state as a function */ - Function getInitStateValueAsFunction() + public Function getInitStateValueAsFunction() { return (Function) values.get(initState); } @@ -194,7 +200,7 @@ final class StateValues { * * @return value of the initial state as a boolean */ - boolean getInitStateValueAsBoolean() + public boolean getInitStateValueAsBoolean() { return ((StateBoolean) values.get(initState)).getValue(); } @@ -204,7 +210,7 @@ final class StateValues { * * @return number of states of the model */ - int getNumStates() + public int getNumStates() { return values.size(); } @@ -215,7 +221,8 @@ final class StateValues { * * @return bitset representing this state value assignment */ - BitSet toBitSet() { + public BitSet toBitSet() + { BitSet result = new BitSet(values.size()); for (int state = 0; state < values.size(); state++) { result.set(state, getStateValueAsBoolean(state)); @@ -230,7 +237,8 @@ final class StateValues { * @param point point to instantiate state values * @return array of {@code BigRational}s mapping each state to evaluated value */ - public BigRational[] instantiate(Point point) { + public BigRational[] instantiate(Point point) + { BigRational[] result = new BigRational[values.size()]; for (int state = 0; state < values.size(); state++) { result[state] = this.getStateValueAsFunction(state).evaluate(point);