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

Improvements to import from tra files (explicit lib). 

git-svn-id: https://www.prismmodelchecker.org/svn/prism/prism/trunk@1591 bbc10eb1-c90d-0410-af57-cb519fbb1720
master
Dave Parker 16 years ago
parent
783dcc9863
commit
85bcef53d2
2 changed files with 58 additions and 45 deletions
Whitespace
Show all changes Ignore whitespace when comparing lines Ignore changes in amount of whitespace Ignore changes in whitespace at EOL
Unified View
Diff Options
Show Stats Download Patch File Download Diff File
  1. 38
      prism/src/explicit/DTMC.java
  2. 65
      prism/src/explicit/MDP.java

38
prism/src/explicit/DTMC.java
View File

@ -133,7 +133,7 @@ public class DTMC extends Model
transRewards = null; transRewards = null;
transRewardsConstant = null; transRewardsConstant = null;
} }
/** /**
* Set a constant reward for all transitions * Set a constant reward for all transitions
*/ */
@ -144,7 +144,7 @@ public class DTMC extends Model
// Store as a Double (because we use null to check for its existence) // Store as a Double (because we use null to check for its existence)
transRewardsConstant = new Double(r); transRewardsConstant = new Double(r);
} }
/** /**
* Set the reward for (all) transitions in state s to r. * Set the reward for (all) transitions in state s to r.
*/ */
@ -161,7 +161,7 @@ public class DTMC extends Model
// Set reward // Set reward
transRewards.set(s, r); transRewards.set(s, r);
} }
/** /**
* Get the number of nondeterministic choices in state s (always 1 for a DTMC). * Get the number of nondeterministic choices in state s (always 1 for a DTMC).
*/ */
@ -177,7 +177,7 @@ public class DTMC extends Model
{ {
return trans.get(s); return trans.get(s);
} }
/** /**
* Get the transition reward (if any) for the transitions in state s. * Get the transition reward (if any) for the transitions in state s.
*/ */
@ -189,7 +189,7 @@ public class DTMC extends Model
return 0.0; return 0.0;
return transRewards.get(s); return transRewards.get(s);
} }
/** /**
* Returns true if state s2 is a successor of state s1. * Returns true if state s2 is a successor of state s1.
*/ */
@ -197,7 +197,7 @@ public class DTMC extends Model
{ {
return trans.get(s1).contains(s2); return trans.get(s1).contains(s2);
} }
/** /**
* Get the total number of transitions in the model. * Get the total number of transitions in the model.
*/ */
@ -205,7 +205,7 @@ public class DTMC extends Model
{ {
return numTransitions; return numTransitions;
} }
/** /**
* Checks for deadlocks (states with no transitions) and throws an exception if any exist. * Checks for deadlocks (states with no transitions) and throws an exception if any exist.
* States in 'except' (If non-null) are excluded from the check. * States in 'except' (If non-null) are excluded from the check.
@ -217,7 +217,7 @@ public class DTMC extends Model
throw new PrismException("DTMC has a deadlock in state " + i); throw new PrismException("DTMC has a deadlock in state " + i);
} }
} }
/** /**
* Build (anew) from a list of transitions exported explicitly by PRISM (i.e. a .tra file). * Build (anew) from a list of transitions exported explicitly by PRISM (i.e. a .tra file).
*/ */
@ -225,7 +225,7 @@ public class DTMC extends Model
{ {
BufferedReader in; BufferedReader in;
String s, ss[]; String s, ss[];
int i, j, n;
int i, j, n, lineNum = 0;
double prob; double prob;
try { try {
@ -233,6 +233,7 @@ public class DTMC extends Model
in = new BufferedReader(new FileReader(new File(filename))); in = new BufferedReader(new FileReader(new File(filename)));
// Parse first line to get num states // Parse first line to get num states
s = in.readLine(); s = in.readLine();
lineNum = 1;
if (s == null) if (s == null)
throw new PrismException("Missing first line of .tra file"); throw new PrismException("Missing first line of .tra file");
ss = s.split(" "); ss = s.split(" ");
@ -241,13 +242,18 @@ public class DTMC extends Model
initialise(n); initialise(n);
// Go though list of transitions in file // Go though list of transitions in file
s = in.readLine(); s = in.readLine();
lineNum++;
while (s != null) { while (s != null) {
ss = s.split(" ");
i = Integer.parseInt(ss[0]);
j = Integer.parseInt(ss[1]);
prob = Double.parseDouble(ss[2]);
setProbability(i, j, prob);
s = s.trim();
if (s.length() > 0) {
ss = s.split(" ");
i = Integer.parseInt(ss[0]);
j = Integer.parseInt(ss[1]);
prob = Double.parseDouble(ss[2]);
setProbability(i, j, prob);
}
s = in.readLine(); s = in.readLine();
lineNum++;
} }
// Close file // Close file
in.close(); in.close();
@ -255,7 +261,7 @@ public class DTMC extends Model
System.out.println(e); System.out.println(e);
System.exit(1); System.exit(1);
} catch (NumberFormatException e) { } catch (NumberFormatException e) {
throw new PrismException("Problem in .tra file for " + modelType);
throw new PrismException("Problem in .tra file (line " + lineNum + ") for " + modelType);
} }
// Set initial state (assume 0) // Set initial state (assume 0)
initialStates.add(0); initialStates.add(0);
@ -276,7 +282,7 @@ public class DTMC extends Model
{ {
throw new PrismException("Export not yet supported"); throw new PrismException("Export not yet supported");
} }
/** /**
* Export to a dot file, highlighting states in 'mark'. * Export to a dot file, highlighting states in 'mark'.
*/ */

65
prism/src/explicit/MDP.java
View File

@ -46,7 +46,7 @@ public class MDP extends Model
// Action labels // Action labels
protected List<List<Object>> actions; protected List<List<Object>> actions;
// Rewards // Rewards
protected List<List<Double>> transRewards; protected List<List<Double>> transRewards;
protected Double transRewardsConstant; protected Double transRewardsConstant;
@ -249,7 +249,7 @@ public class MDP extends Model
{ {
return trans.get(s).size(); return trans.get(s).size();
} }
/** /**
* Get the list of choices (distributions) for state s. * Get the list of choices (distributions) for state s.
*/ */
@ -257,7 +257,7 @@ public class MDP extends Model
{ {
return trans.get(s); return trans.get(s);
} }
/** /**
* Get the ith choice (distribution) for state s. * Get the ith choice (distribution) for state s.
*/ */
@ -265,7 +265,7 @@ public class MDP extends Model
{ {
return trans.get(s).get(i); return trans.get(s).get(i);
} }
/** /**
* Get the action (if any) for choice i of state s. * Get the action (if any) for choice i of state s.
*/ */
@ -301,7 +301,7 @@ public class MDP extends Model
} }
return false; return false;
} }
/** /**
* Get the total number of choices (distributions) over all states. * Get the total number of choices (distributions) over all states.
*/ */
@ -309,7 +309,7 @@ public class MDP extends Model
{ {
return numDistrs; return numDistrs;
} }
/** /**
* Get the total number of transitions in the model. * Get the total number of transitions in the model.
*/ */
@ -317,7 +317,7 @@ public class MDP extends Model
{ {
return numTransitions; return numTransitions;
} }
/** /**
* Get the maximum number of choices (distributions) in any state. * Get the maximum number of choices (distributions) in any state.
*/ */
@ -331,7 +331,7 @@ public class MDP extends Model
} }
return maxNumDistrs; return maxNumDistrs;
} }
/** /**
* Checks for deadlocks (states with no choices) and throws an exception if any exist. * Checks for deadlocks (states with no choices) and throws an exception if any exist.
* States in 'except' (If non-null) are excluded from the check. * States in 'except' (If non-null) are excluded from the check.
@ -344,7 +344,7 @@ public class MDP extends Model
} }
// TODO: Check for empty distributions too? // TODO: Check for empty distributions too?
} }
/** /**
* Build (anew) from a list of transitions exported explicitly by PRISM (i.e. a .tra file). * Build (anew) from a list of transitions exported explicitly by PRISM (i.e. a .tra file).
*/ */
@ -353,7 +353,7 @@ public class MDP extends Model
BufferedReader in; BufferedReader in;
Distribution distr; Distribution distr;
String s, ss[]; String s, ss[];
int i, j, k, iLast, kLast, n;
int i, j, k, iLast, kLast, n, lineNum = 0;
double prob; double prob;
try { try {
@ -361,6 +361,7 @@ public class MDP extends Model
in = new BufferedReader(new FileReader(new File(filename))); in = new BufferedReader(new FileReader(new File(filename)));
// Parse first line to get num states // Parse first line to get num states
s = in.readLine(); s = in.readLine();
lineNum = 1;
if (s == null) if (s == null)
throw new PrismException("Missing first line of .tra file"); throw new PrismException("Missing first line of .tra file");
ss = s.split(" "); ss = s.split(" ");
@ -372,26 +373,31 @@ public class MDP extends Model
kLast = -1; kLast = -1;
distr = null; distr = null;
s = in.readLine(); s = in.readLine();
lineNum++;
while (s != null) { while (s != null) {
ss = s.split(" ");
i = Integer.parseInt(ss[0]);
k = Integer.parseInt(ss[1]);
j = Integer.parseInt(ss[2]);
prob = Double.parseDouble(ss[3]);
// For a new state or distribution
if (i != iLast || k != kLast) {
// Add any previous distribution to the last state, create new one
if (distr != null) {
addChoice(iLast, distr);
s = s.trim();
if (s.length() > 0) {
ss = s.split(" ");
i = Integer.parseInt(ss[0]);
k = Integer.parseInt(ss[1]);
j = Integer.parseInt(ss[2]);
prob = Double.parseDouble(ss[3]);
// For a new state or distribution
if (i != iLast || k != kLast) {
// Add any previous distribution to the last state, create new one
if (distr != null) {
addChoice(iLast, distr);
}
distr = new Distribution();
} }
distr = new Distribution();
// Add transition to the current distribution
distr.add(j, prob);
// Prepare for next iter
iLast = i;
kLast = k;
} }
// Add transition to the current distribution
distr.add(j, prob);
// Prepare for next iter
iLast = i;
kLast = k;
s = in.readLine(); s = in.readLine();
lineNum++;
} }
// Add previous distribution to the last state // Add previous distribution to the last state
addChoice(iLast, distr); addChoice(iLast, distr);
@ -401,7 +407,7 @@ public class MDP extends Model
System.out.println(e); System.out.println(e);
System.exit(1); System.exit(1);
} catch (NumberFormatException e) { } catch (NumberFormatException e) {
throw new PrismException("Problem in .tra file for " + modelType);
throw new PrismException("Problem in .tra file (line " + lineNum + ") for " + modelType);
} }
// Set initial state (assume 0) // Set initial state (assume 0)
initialStates.add(0); initialStates.add(0);
@ -645,7 +651,7 @@ public class MDP extends Model
throw new PrismException("Could not export " + modelType + " to file \"" + filename + "\"" + e); throw new PrismException("Could not export " + modelType + " to file \"" + filename + "\"" + e);
} }
} }
/** /**
* Export to a dot file, highlighting states in 'mark'. * Export to a dot file, highlighting states in 'mark'.
*/ */
@ -684,7 +690,8 @@ public class MDP extends Model
s += numStates + " states"; s += numStates + " states";
s += ", " + numDistrs + " distributions"; s += ", " + numDistrs + " distributions";
s += ", " + numTransitions + " transitions"; s += ", " + numTransitions + " transitions";
s += ", dist max/avg = " + getMaxNumChoices() + "/" + PrismUtils.formatDouble2dp(((double) numDistrs) / numStates);
s += ", dist max/avg = " + getMaxNumChoices() + "/"
+ PrismUtils.formatDouble2dp(((double) numDistrs) / numStates);
return s; return s;
} }

Write Preview
Loading…
Cancel
Save