From f790b47bf1abc29715d5af97120266fcb9cfdbda Mon Sep 17 00:00:00 2001 From: Dave Parker Date: Thu, 11 Nov 2010 15:56:09 +0000 Subject: [PATCH] Better detection of timelocks (in forwards reach) + some additions/fixes to DBMs. git-svn-id: https://www.prismmodelchecker.org/svn/prism/prism/trunk@2236 bbc10eb1-c90d-0410-af57-cb519fbb1720 --- prism/src/pta/DBM.java | 5 +++ prism/src/pta/DBMList.java | 35 +++++++++++++++ prism/src/pta/ForwardsReach.java | 65 +++++++++++++++++++++------- prism/src/pta/NCZone.java | 2 + prism/src/pta/PTAAbstractRefine.java | 16 +++---- 5 files changed, 99 insertions(+), 24 deletions(-) diff --git a/prism/src/pta/DBM.java b/prism/src/pta/DBM.java index ba4561a9..fa4139de 100644 --- a/prism/src/pta/DBM.java +++ b/prism/src/pta/DBM.java @@ -235,6 +235,11 @@ public class DBM extends Zone DBMList list = new DBMList(pta); DBM dbmNew; int i, j, n; + // Special case: complement of empty DBM is True + if (isEmpty()) { + list.addDBM(createTrue(pta)); + return list; + } n = d.length - 1; for (i = 0; i < n + 1; i++) { for (j = 0; j < n + 1; j++) { diff --git a/prism/src/pta/DBMList.java b/prism/src/pta/DBMList.java index 6bc72c0c..db70d366 100644 --- a/prism/src/pta/DBMList.java +++ b/prism/src/pta/DBMList.java @@ -404,6 +404,30 @@ public class DBMList extends NCZone list = res.list; } + /** + * Disjunction: with another zone + */ + public void union(Zone z) + { + if (z instanceof DBM) { + addDBM((DBM) z); + } + else { + addDBMs((DBMList) z); + } + } + + /** + * Get some (any) convex zone contained within this zone. + * Returns null if this zone is empty. + */ + public Zone getAZone() + { + if (list.size() > 0) + return list.get(0); + else return null; + } + /** * Clone this zone */ @@ -460,6 +484,17 @@ public class DBMList extends NCZone return "List of " + list.size() + " DBMs with " + pta.numClocks + " clocks"; } + // Static zone creation methods + + /** + * Create empty DBM list (i.e. false) + */ + public static DBMList createFalse(PTA pta) + { + DBMList dbml = new DBMList(pta); + return dbml; + } + // Private utility methods private void removeInclusions() diff --git a/prism/src/pta/ForwardsReach.java b/prism/src/pta/ForwardsReach.java index 16ddf88b..15a396ea 100644 --- a/prism/src/pta/ForwardsReach.java +++ b/prism/src/pta/ForwardsReach.java @@ -91,13 +91,13 @@ public class ForwardsReach private ReachabilityGraph buildForwardsGraphFormats10(PTA pta, BitSet targetLocs, Constraint targetConstraint) throws PrismException { - Zone z; LocZone init, lz, lz2; LinkedList X; IndexedSet Yset; //LocZoneSetOld Zset; ReachabilityGraph graph; - int src, dest, count; + int src, dest, count, dests[]; + boolean canDiverge; long timer, timerProgress; boolean progressDisplayed; @@ -121,8 +121,7 @@ public class ForwardsReach target = new BitSet(); // Build initial symbolic state (NB: assume initial location = 0) - z = DBM.createZero(pta); - init = new LocZone(0, z); + init = new LocZone(0, DBM.createZero(pta)); // Reachability loop Yset.add(init); @@ -138,24 +137,56 @@ public class ForwardsReach // Compute timed post for this zone (NB: do this before checking if target) lz = lz.deepCopy(); lz.tPost(pta); - // Is this a target state? + // Is this a target state? (If so, don't explore) if (targetLocs.get(lz.loc) && (targetConstraint == null || lz.zone.isSatisfied(targetConstraint))) { target.set(src); // Add null for this state (no need to store info) graph.addState(); continue; } - // Otherwise, explore this symbolic state - // 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("Deadlock (no transitions) in PTA at location \"" + pta.getLocationNameString(lz.loc) + "\""); + // Check if time can diverge in this state + // (note we already did tPost above) + canDiverge = lz.zone.allClocksAreUnbounded(); + // Explore this symbolic state + // First, check for one possible cause of timelock: + // no PTA transitions and not possible for time to diverge + if (!canDiverge && pta.getTransitions(lz.loc).size() == 0) { + throw new PrismException("Timelock (no transitions) in PTA at location " + pta.getLocationNameString(lz.loc)); } // Add current state to reachability graph graph.addState(); + // For unbounded case, add a special self-loop transition to model divergence + if (canDiverge) { + dests = new int[1]; + dests[0] = src; + Transition trNew = new Transition(pta, lz.loc, "_diverge"); + trNew.addEdge(1.0, lz.loc); + graph.addTransition(src, trNew, dests, null); + } + // And for the non-unbounded case, need to do a check for time-locks + else { + Zone zone; + NCZone ncZone; + // Build union of tPre of each guard + ncZone = DBMList.createFalse(pta); + for (Transition transition : pta.getTransitions(lz.loc)) { + zone = DBM.createFromConstraints(pta, transition.getGuardConstraints()); + zone.down(); + ncZone.union(zone); + } + // Make sure tPost of this zone is not bigger (tPost done above) + // (i.e. intersection with complement of union is empty) + ncZone.complement(); + ncZone.intersect(lz.zone); + if (!ncZone.isEmpty()) { + String s = "Timelock in PTA at location " + pta.getLocationNameString(lz.loc); + s += " when " + ncZone.getAZone(); + throw new PrismException(s); + } + } // For each outgoing transition... for (Transition transition : pta.getTransitions(lz.loc)) { - int[] dests = new int[transition.getNumEdges()]; + dests = new int[transition.getNumEdges()]; boolean enabled = false; boolean unenabled = false; count = 0; @@ -185,9 +216,13 @@ 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) + "\""); + // 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) + // (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)); } // Print some progress info occasionally if (System.currentTimeMillis() - timerProgress > 3000) { @@ -292,7 +327,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("PTA deadlocks in location " + pta.getLocationNameString(lz.loc)); } // For each outgoing transition... graph.addState(); diff --git a/prism/src/pta/NCZone.java b/prism/src/pta/NCZone.java index 078d313b..49c3ed2f 100644 --- a/prism/src/pta/NCZone.java +++ b/prism/src/pta/NCZone.java @@ -30,5 +30,7 @@ public abstract class NCZone extends Zone { public abstract void intersectComplement(Zone z); public abstract void complement(); + public abstract void union(Zone z); + public abstract Zone getAZone(); public abstract NCZone deepCopy(); } diff --git a/prism/src/pta/PTAAbstractRefine.java b/prism/src/pta/PTAAbstractRefine.java index d152a440..76e37eaa 100644 --- a/prism/src/pta/PTAAbstractRefine.java +++ b/prism/src/pta/PTAAbstractRefine.java @@ -194,13 +194,10 @@ public class PTAAbstractRefine extends STPGAbstractRefine if (level == numValids) { // Check this combination of transitions is non-empty if (!valid.isEmpty()) { - // Check for the case where it is possible that no transitions are enabled. - // We disallow this (time-divergence restrictions on PTAs that we can handle). - if (bitSet.cardinality() == 0) { - String s = "Possibility of time divergence in PTA location "; - s += pta.getLocationNameString(graph.states.get(src).loc); - throw new PrismException(s); - } + // Ignore the case where no transitions are enabled + // (has been dealt with earlier by adding explicit "diverge" transition) + if (bitSet.cardinality() == 0) + return; // Create distribution set for this combination of transitions distrSet = stpg.newDistributionSet(null); // If using BitSets for action labels (as opposed to storing the zones directly) @@ -238,13 +235,14 @@ public class PTAAbstractRefine extends STPGAbstractRefine distrSet.setAction(actionBitSet); stpg.addDistributionSet(src, distrSet); } - } else { // Recursive step // Note that the construction of the validity constraint for // transition combinations is done recursively - this gives big gains in efficiency. // Note also that, the first thing added to the conjunction (i.e. the validity constraint) - // before recursion starts is the symbolic state zone. Generally, it is better to + // before recursion starts is the symbolic state zone. We can only do this because at + // least one transition is enabled in this combination, so its validity will need to include + // the symbolic state zone. Generally, it is better to // add non-complemented zones, like this, early to avoid blowups // (in terms of conjunctions on complements, which are typically large DBM lists). // Finally, note that use of combined intersectComplement operation is, like