From f2c00dff12bfa1f468848d173d81cb041774d121 Mon Sep 17 00:00:00 2001 From: Dave Parker Date: Sat, 15 Jan 2011 14:10:12 +0000 Subject: [PATCH] Better "badly-formed" error message during PTA forwards reachability. git-svn-id: https://www.prismmodelchecker.org/svn/prism/prism/trunk@2384 bbc10eb1-c90d-0410-af57-cb519fbb1720 --- prism/src/pta/ForwardsReach.java | 12 ++++++++++-- 1 file changed, 10 insertions(+), 2 deletions(-) diff --git a/prism/src/pta/ForwardsReach.java b/prism/src/pta/ForwardsReach.java index cfbeaf3c..db34517a 100644 --- a/prism/src/pta/ForwardsReach.java +++ b/prism/src/pta/ForwardsReach.java @@ -185,6 +185,7 @@ public class ForwardsReach dests = new int[transition.getNumEdges()]; boolean enabled = false; boolean unenabled = false; + Edge unenabledEdge = null; count = 0; for (Edge edge : transition.getEdges()) { // Do "discrete post" for this edge @@ -202,13 +203,20 @@ public class ForwardsReach dests[count] = dest; } else { unenabled = true; + // Store first unenabled edge + unenabledEdge = (unenabledEdge == null) ? edge : unenabledEdge; dests[count] = -1; } count++; } if (enabled) { - if (unenabled) - throw new PrismException("Badly formed PTA: state " + src); + if (unenabled) { + String s = "Badly formed PTA at location " + pta.getLocationNameString(lz.loc) + " when " + lz.zone; + s += ": \"" + transition.getAction() + "\"-labelled transition to "; + s += pta.getLocationNameString(unenabledEdge.getDestination()); + s += " leads to state where invariant is not satisfied"; + throw new PrismException(s); + } graph.addTransition(src, transition, dests, null); } }