diff --git a/prism/src/pta/ForwardsReach.java b/prism/src/pta/ForwardsReach.java
index b0ae2edd1d..0bd337b359 100644
--- a/prism/src/pta/ForwardsReach.java
+++ b/prism/src/pta/ForwardsReach.java
@@ -181,6 +181,7 @@ private ReachabilityGraph buildForwardsGraphFormats10(PTA pta, BitSet targetLocs
 					throw new PrismException(s);
 				}
 			}
+            boolean found_some_transition_guaranteed_to_be_enabled = false;
 			// For each outgoing transition...
 			for (Transition transition : pta.getTransitions(lz.loc)) {
 				dests = new int[transition.getNumEdges()];
@@ -188,11 +189,29 @@ private ReachabilityGraph buildForwardsGraphFormats10(PTA pta, BitSet targetLocs
 				boolean unenabled = false;
 				Edge unenabledEdge = null;
 				count = 0;
+                boolean found_some_edge_not_enabled = false;
 				for (Edge edge : transition.getEdges()) {
 					// Do "discrete post" for this edge
 					// (followed by c-closure)
 					lz2 = lz.deepCopy();
+					System.out.println("\nSS1: "+lz2);
 					lz2.dPost(edge);
+					System.out.println("SS2: "+lz2);
+                    {
+                        LocZone lz3 = lz2.deepCopy();
+						System.out.println("SS3: "+lz3);
+                        lz3.dPre(edge);
+						System.out.println("SS4: "+lz3);
+                        NCZone complement=lz3.zone.createComplement();
+						System.out.println("SS4b: "+complement);
+						complement.addConstraints(transition.getGuardConstraints());
+						System.out.println("SS5: "+complement);
+						complement.intersect(lz.zone);
+						System.out.println("SS6: "+complement);
+                        if (!complement.isEmpty()) {
+                            found_some_edge_not_enabled = true;
+                        }
+                    }
 					lz2.cClosure(pta);
 					// If non-empty, create edge, also adding state to X if new 
 					if (!lz2.zone.isEmpty()) {
@@ -220,7 +239,16 @@ private ReachabilityGraph buildForwardsGraphFormats10(PTA pta, BitSet targetLocs
 					}
 					graph.addTransition(src, transition, dests, null);
 				}
+                if (!found_some_edge_not_enabled) {
+                    found_some_transition_guaranteed_to_be_enabled = true;
+                }
 			}
+            if (!pta.getTransitions(lz.loc).isEmpty() && !found_some_transition_guaranteed_to_be_enabled) {
+                throw new PrismException(
+                        "Badly formed PTA at location " + pta.getLocationNameString(lz.loc) + " when " + lz.zone +
+                                " has exiting transitions but all may be disabled " +
+                                "by the invariants of some of their targets.");
+            }
 			// Check for another possible cause of timelock:
 			// no PTA transitions *enabled* and not possible for time to diverge
 			// (NB: This should be defunct now because of earlier timelock check)