From fc4fcc4df61e5c85fea32083bc4f68634b1ba5d8 Mon Sep 17 00:00:00 2001 From: Dave Parker Date: Fri, 16 Mar 2012 15:46:52 +0000 Subject: [PATCH] More info on one of the PTA timelock error messages. git-svn-id: https://www.prismmodelchecker.org/svn/prism/prism/trunk@4857 bbc10eb1-c90d-0410-af57-cb519fbb1720 --- prism/src/pta/ForwardsReach.java | 4 +++- 1 file changed, 3 insertions(+), 1 deletion(-) diff --git a/prism/src/pta/ForwardsReach.java b/prism/src/pta/ForwardsReach.java index cf7fa7cb..3bd7243c 100644 --- a/prism/src/pta/ForwardsReach.java +++ b/prism/src/pta/ForwardsReach.java @@ -226,7 +226,9 @@ public class ForwardsReach // (NB2: Strictly speaking, don't need to check canDiverge - if it was // true, we would have added a loop transition that is definitely enabled) if (!canDiverge && graph.trans.get(src).size() == 0) { - throw new PrismException("Timelock (no enabled transitions) in PTA at location " + pta.getLocationNameString(lz.loc)); + String s = "Timelock in PTA (no enabled transitions) at location " + pta.getLocationNameString(lz.loc); + s += " when " + lz.zone; + throw new PrismException(s); } // Print some progress info occasionally if (System.currentTimeMillis() - timerProgress > 3000) {