s14h
/
prism-accumulation
1
0
Fork 0
Code Releases Activity
Browse Source

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
master
Dave Parker 12 years ago
parent
89fab7269a
commit
946c767fb5
5 changed files with 306 additions and 268 deletions
Whitespace
Show all changes Ignore whitespace when comparing lines Ignore changes in amount of whitespace Ignore changes in whitespace at EOL
Split View
Diff Options
Show Stats Download Patch File Download Diff File
  1. 253
      prism/src/param/BigRational.java
  2. 61
      prism/src/param/Function.java
  3. 50
      prism/src/param/Point.java
  4. 146
      prism/src/param/RegionValues.java
  5. 64
      prism/src/param/StateValues.java

253
prism/src/param/BigRational.java
View File

@ -39,7 +39,8 @@ import java.math.BigInteger;
*
* @author Ernst Moritz Hahn <emhahn@cs.ox.ac.uk> (University of Oxford)
*/
final class BigRational implements Comparable<BigRational> {
public final class BigRational implements Comparable<BigRational>
{
/** the BigInteger "-1" */
private final static BigInteger BMONE = BigInteger.ONE.negate();
/** the BigInteger "2" */
@ -59,29 +60,29 @@ final class BigRational implements Comparable<BigRational> {
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<BigRational> {
* @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<BigRational> {
* @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<BigRational> {
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<BigRational> {
* @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<BigRational> {
*
* @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<BigRational> {
} 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<BigRational> {
{
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<BigRational> {
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<BigRational> {
* @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<BigRational> {
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<BigRational> {
* @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<BigRational> {
*
* @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<BigRational> {
* @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> {
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<BigRational> {
*
* @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<BigRational> {
*
* @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<BigRational> {
}
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<BigRational> {
* @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<BigRational> {
}
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<BigRational> {
{
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<BigRational> {
*
* @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<BigRational> {
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<BigRational> {
* @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<BigRational> {
* @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<BigRational> {
*
* @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<BigRational> {
*
* @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<BigRational> {
*
* @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<BigRational> {
*
* @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<BigRational> {
* @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<BigRational> {
*
* @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<BigRational> {
*
* @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<BigRational> {
*
* @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<BigRational> {
*
* @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<BigRational> {
*
* @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<BigRational> {
*
* @return true iff this object represents a special number
*/
boolean isSpecial()
public boolean isSpecial()
{
return isNaN() || isInf() || isMInf();
}

61
prism/src/param/Function.java
View File

@ -52,20 +52,22 @@ package param;
* @see FunctionFactory
* @author Ernst Moritz Hahn <emhahn@cs.ox.ac.uk> (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.
*

50
prism/src/param/Point.java
View File

@ -35,35 +35,37 @@ package param;
* @author Ernst Moritz Hahn <emhahn@cs.ox.ac.uk> (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.
*

146
prism/src/param/RegionValues.java
View File

@ -40,39 +40,40 @@ import java.util.Map.Entry;
*
* @author Ernst Moritz Hahn <emhahn@cs.ox.ac.uk> (University of Oxford)
*/
final class RegionValues implements Iterable<Entry<Region,StateValues>> {
public final class RegionValues implements Iterable<Entry<Region, StateValues>>
{
/** list of all regions */
private ArrayList<Region> regions;
/** assigning values to regions */
private HashMap<Region,StateValues> values;
private HashMap<Region, StateValues> values;
/** region factory this object belongs to */
private RegionFactory factory;
// constructors
RegionValues(RegionFactory factory)
public RegionValues(RegionFactory factory)
{
regions = new ArrayList<Region>();
values = new HashMap<Region,StateValues>();
values = new HashMap<Region, StateValues>();
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<Entry<Region,StateValues>> {
{
boolean changed = false;
ArrayList<Region> newRegions = new ArrayList<Region>();
HashMap<Region,StateValues> newValues = new HashMap<Region,StateValues>();
HashMap<Region, StateValues> newValues = new HashMap<Region, StateValues>();
HashSet<Region> done = new HashSet<Region>();
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<Entry<Region,StateValues>> {
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<Region> newRegions = new ArrayList<Region>();
HashMap<Region,StateValues> thisNewStateValues = new HashMap<Region,StateValues>();
HashMap<Region,StateValues> otherNewStateValues = new HashMap<Region,StateValues>();
HashMap<Region, StateValues> thisNewStateValues = new HashMap<Region, StateValues>();
HashMap<Region, StateValues> otherNewStateValues = new HashMap<Region, StateValues>();
for (Region thisRegion : this.regions) {
for (Region otherRegion : other.regions) {
Region newRegion = thisRegion.conjunct(otherRegion);
@ -165,15 +165,16 @@ final class RegionValues implements Iterable<Entry<Region,StateValues>> {
}
}
}
this.regions = new ArrayList<Region>(newRegions);
this.values = thisNewStateValues;
other.regions = new ArrayList<Region>(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<Entry<Region,StateValues>> {
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<Entry<Region,StateValues>> {
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<Entry<Region,StateValues>> {
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<Entry<Region,StateValues>> {
}
simplify();
}
void clearExceptInit()
public void clearExceptInit()
{
if (regions.isEmpty()) {
return;
@ -227,16 +229,17 @@ final class RegionValues implements Iterable<Entry<Region,StateValues>> {
}
@Override
public Iterator<Entry<Region, StateValues>> iterator() {
public Iterator<Entry<Region, StateValues>> 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<Entry<Region,StateValues>> {
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<Entry<Region,StateValues>> {
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<Entry<Region,StateValues>> {
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<Entry<Region,StateValues>> {
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<Entry<Region,StateValues>> {
}
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<Entry<Region,StateValues>> {
}
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<Entry<Region,StateValues>> {
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<Entry<Region,StateValues>> {
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<Entry<Region,StateValues>> {
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<Entry<Region,StateValues>> {
result.setStateValue(state, value);
}
return result;
}
}
}

64
prism/src/param/StateValues.java
View File

@ -38,12 +38,13 @@ import java.util.BitSet;
* @author Ernst Moritz Hahn <emhahn@cs.ox.ac.uk> (University of Oxford)
* @see RegionValues
*/
final class StateValues {
public final class StateValues
{
/** assigns values to each state of the model */
private ArrayList<StateValue> 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<StateValue>(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);

Write Preview
Loading…
Cancel
Save