From 85bcef53d24644593cd9e4d5c2f9bf074151cee7 Mon Sep 17 00:00:00 2001 From: Dave Parker Date: Tue, 1 Dec 2009 14:24:04 +0000 Subject: [PATCH] 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 --- prism/src/explicit/DTMC.java | 38 ++++++++++++--------- prism/src/explicit/MDP.java | 65 ++++++++++++++++++++---------------- 2 files changed, 58 insertions(+), 45 deletions(-) diff --git a/prism/src/explicit/DTMC.java b/prism/src/explicit/DTMC.java index 24e00aa9..9ad35bd5 100644 --- a/prism/src/explicit/DTMC.java +++ b/prism/src/explicit/DTMC.java @@ -133,7 +133,7 @@ public class DTMC extends Model transRewards = null; transRewardsConstant = null; } - + /** * 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) transRewardsConstant = new Double(r); } - + /** * Set the reward for (all) transitions in state s to r. */ @@ -161,7 +161,7 @@ public class DTMC extends Model // Set reward transRewards.set(s, r); } - + /** * 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); } - + /** * 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 transRewards.get(s); } - + /** * 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); } - + /** * Get the total number of transitions in the model. */ @@ -205,7 +205,7 @@ public class DTMC extends Model { return numTransitions; } - + /** * 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. @@ -217,7 +217,7 @@ public class DTMC extends Model 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). */ @@ -225,7 +225,7 @@ public class DTMC extends Model { BufferedReader in; String s, ss[]; - int i, j, n; + int i, j, n, lineNum = 0; double prob; try { @@ -233,6 +233,7 @@ public class DTMC extends Model in = new BufferedReader(new FileReader(new File(filename))); // Parse first line to get num states s = in.readLine(); + lineNum = 1; if (s == null) throw new PrismException("Missing first line of .tra file"); ss = s.split(" "); @@ -241,13 +242,18 @@ public class DTMC extends Model initialise(n); // Go though list of transitions in file s = in.readLine(); + lineNum++; 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(); + lineNum++; } // Close file in.close(); @@ -255,7 +261,7 @@ public class DTMC extends Model System.out.println(e); System.exit(1); } 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) initialStates.add(0); @@ -276,7 +282,7 @@ public class DTMC extends Model { throw new PrismException("Export not yet supported"); } - + /** * Export to a dot file, highlighting states in 'mark'. */ diff --git a/prism/src/explicit/MDP.java b/prism/src/explicit/MDP.java index 6f47adb9..b363ba8c 100644 --- a/prism/src/explicit/MDP.java +++ b/prism/src/explicit/MDP.java @@ -46,7 +46,7 @@ public class MDP extends Model // Action labels protected List> actions; - + // Rewards protected List> transRewards; protected Double transRewardsConstant; @@ -249,7 +249,7 @@ public class MDP extends Model { return trans.get(s).size(); } - + /** * Get the list of choices (distributions) for state s. */ @@ -257,7 +257,7 @@ public class MDP extends Model { return trans.get(s); } - + /** * Get the ith choice (distribution) for state s. */ @@ -265,7 +265,7 @@ public class MDP extends Model { return trans.get(s).get(i); } - + /** * Get the action (if any) for choice i of state s. */ @@ -301,7 +301,7 @@ public class MDP extends Model } return false; } - + /** * Get the total number of choices (distributions) over all states. */ @@ -309,7 +309,7 @@ public class MDP extends Model { return numDistrs; } - + /** * Get the total number of transitions in the model. */ @@ -317,7 +317,7 @@ public class MDP extends Model { return numTransitions; } - + /** * Get the maximum number of choices (distributions) in any state. */ @@ -331,7 +331,7 @@ public class MDP extends Model } return maxNumDistrs; } - + /** * 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. @@ -344,7 +344,7 @@ public class MDP extends Model } // TODO: Check for empty distributions too? } - + /** * 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; Distribution distr; String s, ss[]; - int i, j, k, iLast, kLast, n; + int i, j, k, iLast, kLast, n, lineNum = 0; double prob; try { @@ -361,6 +361,7 @@ public class MDP extends Model in = new BufferedReader(new FileReader(new File(filename))); // Parse first line to get num states s = in.readLine(); + lineNum = 1; if (s == null) throw new PrismException("Missing first line of .tra file"); ss = s.split(" "); @@ -372,26 +373,31 @@ public class MDP extends Model kLast = -1; distr = null; s = in.readLine(); + lineNum++; 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(); + lineNum++; } // Add previous distribution to the last state addChoice(iLast, distr); @@ -401,7 +407,7 @@ public class MDP extends Model System.out.println(e); System.exit(1); } 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) initialStates.add(0); @@ -645,7 +651,7 @@ public class MDP extends Model throw new PrismException("Could not export " + modelType + " to file \"" + filename + "\"" + e); } } - + /** * Export to a dot file, highlighting states in 'mark'. */ @@ -684,7 +690,8 @@ public class MDP extends Model s += numStates + " states"; s += ", " + numDistrs + " distributions"; 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; }