Browse Source

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
master
Dave Parker 14 years ago
parent
commit
fc4fcc4df6
  1. 4
      prism/src/pta/ForwardsReach.java

4
prism/src/pta/ForwardsReach.java

@ -226,7 +226,9 @@ public class ForwardsReach
// (NB2: Strictly speaking, don't need to check canDiverge - if it was // (NB2: Strictly speaking, don't need to check canDiverge - if it was
// true, we would have added a loop transition that is definitely enabled) // true, we would have added a loop transition that is definitely enabled)
if (!canDiverge && graph.trans.get(src).size() == 0) { 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 // Print some progress info occasionally
if (System.currentTimeMillis() - timerProgress > 3000) { if (System.currentTimeMillis() - timerProgress > 3000) {

Loading…
Cancel
Save