From 154585b3b48c8fad1224e429d4d8df8733754888 Mon Sep 17 00:00:00 2001 From: "sven.schneider" Date: Fri, 29 Jan 2021 18:28:53 +0000 Subject: [PATCH 1/2] added a test for timelock --- prism/src/pta/ForwardsReach.java | 19 +++++++++++++++++++ 1 file changed, 19 insertions(+) diff --git a/prism/src/pta/ForwardsReach.java b/prism/src/pta/ForwardsReach.java index b0ae2edd1d..3dd8440c04 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,20 @@ 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(); lz2.dPost(edge); + { + LocZone lz3 = lz2.deepCopy(); + lz3.dPre(edge); + lz3.zone.createComplement().intersect(lz2.zone); + if (!lz3.zone.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 +230,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) From 98c0cbe16c35b7f8f639ae264404cffeec28f4e4 Mon Sep 17 00:00:00 2001 From: "sven.schneider" Date: Fri, 29 Jan 2021 19:13:48 +0000 Subject: [PATCH 2/2] added outputs for explanation --- prism/src/pta/ForwardsReach.java | 13 +++++++++++-- 1 file changed, 11 insertions(+), 2 deletions(-) diff --git a/prism/src/pta/ForwardsReach.java b/prism/src/pta/ForwardsReach.java index 3dd8440c04..0bd337b359 100644 --- a/prism/src/pta/ForwardsReach.java +++ b/prism/src/pta/ForwardsReach.java @@ -194,12 +194,21 @@ private ReachabilityGraph buildForwardsGraphFormats10(PTA pta, BitSet targetLocs // 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); - lz3.zone.createComplement().intersect(lz2.zone); - if (!lz3.zone.isEmpty()) { + 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; } }