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

Added getMin and getMax to Zone classes + tidy. 

git-svn-id: https://www.prismmodelchecker.org/svn/prism/prism/trunk@2215 bbc10eb1-c90d-0410-af57-cb519fbb1720
master
Dave Parker 15 years ago
parent
8b7990d6ab
commit
bd3e821069
3 changed files with 131 additions and 79 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. 74
      prism/src/pta/DBM.java
  2. 116
      prism/src/pta/DBMList.java
  3. 20
      prism/src/pta/Zone.java

74
prism/src/pta/DBM.java
View File

@ -57,7 +57,7 @@ public class DBM extends Zone
return pta;
}
/* Zone operations */
// Zone operations (modify the zone)
/**
* Conjunction: add constraint x-y db
@ -225,6 +225,35 @@ public class DBM extends Zone
canonicalise();
}
// Zone operations (create new zone)
/**
* Complement this DBM; creates a new DBM list as result.
*/
public DBMList createComplement()
{
DBMList list = new DBMList(pta);
DBM dbmNew;
int i, j, n;
n = d.length - 1;
for (i = 0; i < n + 1; i++) {
for (j = 0; j < n + 1; j++) {
if (i == j)
continue;
if (DB.isInfty(d[i][j]))
continue;
dbmNew = (DBM) new DBMFactory().createTrue(pta);
dbmNew.addConstraint(j, i, DB.dual(d[i][j]));
if (!dbmNew.isEmpty()) {
list.addDBM(dbmNew);
}
}
}
return list;
}
// Zone queries (do not modify the zone)
/**
* Is this zone empty (i.e. inconsistent)?
*/
@ -276,31 +305,8 @@ public class DBM extends Zone
return DB.getSignedDiff(d[x][0]);
}
/**
* Complement this DBM; creates a new DBM list as result.
*/
public DBMList createComplement()
{
DBMList list = new DBMList(pta);
DBM dbmNew;
int i, j, n;
n = d.length - 1;
for (i = 0; i < n + 1; i++) {
for (j = 0; j < n + 1; j++) {
if (i == j)
continue;
if (DB.isInfty(d[i][j]))
continue;
dbmNew = (DBM) new DBMFactory().createTrue(pta);
dbmNew.addConstraint(j, i, DB.dual(d[i][j]));
if (!dbmNew.isEmpty()) {
list.addDBM(dbmNew);
}
}
}
return list;
}
// Misc
/**
* Clone this zone
*/
@ -318,6 +324,14 @@ public class DBM extends Zone
return copy;
}
/**
* Get storage info string
*/
public String storageInfo()
{
return "DBM with " + pta.numClocks + " clocks";
}
// Standard Java methods
public int hashCode()
@ -415,14 +429,6 @@ public class DBM extends Zone
return s;
}
/**
* Get storage info string
*/
public String storageInfo()
{
return "DBM with " + pta.numClocks + " clocks";
}
/* Private utility methods */
/**

116
prism/src/pta/DBMList.java
View File

@ -125,7 +125,7 @@ public class DBMList extends NCZone
return pta;
}
/* Zone operations */
// Zone operations (modify the zone)
/**
* Conjunction: add constraint x-y db
@ -181,20 +181,6 @@ public class DBMList extends NCZone
list = listNew.list;
}
/**
* Conjunction: with complement of another zone
*/
public void intersectComplement(Zone z)
{
if (z instanceof DBM)
z = new DBMList((DBM) z);
DBMList dbml = (DBMList) z;
for (DBM dbm : dbml.list) {
DBMList listTmp = dbm.createComplement();
intersect(listTmp);
}
}
/**
* Up, i.e. let time elapse, subject to some constraints
*/
@ -269,6 +255,8 @@ public class DBMList extends NCZone
throw new RuntimeException("Not implemented yet");
}
// Zone operations (create new zone)
/**
* Complement
* Creates non-convex zone so creates new one,
@ -281,33 +269,8 @@ public class DBMList extends NCZone
return dbml;
}
/**
* Complement
*/
public void complement()
{
DBMList listNew, res;
res = null;
// Special case: complement of empty DBM list is True
if (list.size() == 0)
addDBM(DBM.createTrue(pta));
// The complement of a list of DBMs is the intersection
// of the complement of each DBM (and the complement of
// of a DBM is a DBM list).
for (DBM dbm : list) {
listNew = dbm.createComplement();
if (res == null)
res = listNew;
else {
res.intersect(listNew);
}
// Stop early if res already empty
if (res.list.size() == 0)
break;
}
list = res.list;
}
// Zone queries (do not modify the zone)
/**
* Is this zone empty (i.e. inconsistent)?
*/
@ -344,6 +307,75 @@ public class DBMList extends NCZone
return false;
}
/**
* Get the minimum value of a clock.
*/
public int getMin(int x)
{
// Take min across all DBMs
int min = Integer.MAX_VALUE;
for (DBM dbm : list) {
min = Math.min(min, dbm.getMin(x));
}
return min;
}
/**
* Get the maximum value of a clock.
*/
public int getMax(int x)
{
// Take max across all DBMs
int max = Integer.MIN_VALUE;
for (DBM dbm : list) {
max = Math.max(max, dbm.getMax(x));
}
return max;
}
// Methods required for NCZone interface
/**
* Conjunction: with complement of another zone
*/
public void intersectComplement(Zone z)
{
if (z instanceof DBM)
z = new DBMList((DBM) z);
DBMList dbml = (DBMList) z;
for (DBM dbm : dbml.list) {
DBMList listTmp = dbm.createComplement();
intersect(listTmp);
}
}
/**
* Complement
*/
public void complement()
{
DBMList listNew, res;
res = null;
// Special case: complement of empty DBM list is True
if (list.size() == 0)
addDBM(DBM.createTrue(pta));
// The complement of a list of DBMs is the intersection
// of the complement of each DBM (and the complement of
// of a DBM is a DBM list).
for (DBM dbm : list) {
listNew = dbm.createComplement();
if (res == null)
res = listNew;
else {
res.intersect(listNew);
}
// Stop early if res already empty
if (res.list.size() == 0)
break;
}
list = res.list;
}
/**
* Clone this zone
*/

20
prism/src/pta/Zone.java
View File

@ -34,7 +34,7 @@ public abstract class Zone
public abstract PTA getPTA();
/* Zone operations */
// Zone operations (modify the zone)
/**
* Conjunction: add constraint x-y db
@ -102,6 +102,8 @@ public abstract class Zone
*/
public abstract void cClosure(int c);
// Zone operations (create new zone)
/**
* Complement
* Creates non-convex zone so creates new one,
@ -109,6 +111,8 @@ public abstract class Zone
*/
public abstract NCZone createComplement();
// Zone queries (do not modify the zone)
/**
* Is this zone empty (i.e. inconsistent)?
*/
@ -125,12 +129,22 @@ public abstract class Zone
public abstract boolean includes(DBM dbm);
/**
* Clone this zone
* Get the minimum value of a clock.
*/
public abstract Zone deepCopy();
public abstract int getMin(int x);
/**
* Get the maximum value of a clock.
*/
public abstract int getMax(int x);
// Misc
/**
* Clone this zone
*/
public abstract Zone deepCopy();
/**
* Get storage info string
*/

Write Preview
Loading…
Cancel
Save