From 84649289fbf38050351bb04f7a3bdf668a2c387e Mon Sep 17 00:00:00 2001 From: Dave Parker Date: Wed, 25 Aug 2010 09:25:11 +0000 Subject: [PATCH] Better warning of deadlocks for PTAs. git-svn-id: https://www.prismmodelchecker.org/svn/prism/prism/trunk@2054 bbc10eb1-c90d-0410-af57-cb519fbb1720 --- prism/src/pta/ForwardsReach.java | 6 +++++- 1 file changed, 5 insertions(+), 1 deletion(-) diff --git a/prism/src/pta/ForwardsReach.java b/prism/src/pta/ForwardsReach.java index e48506d4..919529e0 100644 --- a/prism/src/pta/ForwardsReach.java +++ b/prism/src/pta/ForwardsReach.java @@ -149,7 +149,7 @@ public class ForwardsReach // First, check there is at least one transition // (don't want deadlocks in non-target states) if (pta.getTransitions(lz.loc).size() == 0) { - throw new PrismException("PTA deadlocks in location \"" + pta.getLocationNameString(lz.loc) + "\""); + throw new PrismException("Deadlock (no transitions) in PTA at location \"" + pta.getLocationNameString(lz.loc) + "\""); } // Add current state to reachability graph graph.addState(); @@ -183,6 +183,10 @@ public class ForwardsReach graph.addTransition(src, transition, dests, null); } } + // Check for deadlock (transitions exist but not enabled) + if (graph.trans.get(src).size() == 0) { + throw new PrismException("Deadlock (no enabled transitions) in PTA at location \"" + pta.getLocationNameString(lz.loc) + "\""); + } // Print some progress info occasionally if (System.currentTimeMillis() - timerProgress > 3000) { if (!progressDisplayed) {