From be0b0550a2956f67a3ed1413a961779f163c9774 Mon Sep 17 00:00:00 2001 From: Joachim Klein Date: Wed, 19 Jul 2017 12:25:49 +0000 Subject: [PATCH] symbolic LTL model checking: perform DA product constructions from the statesOfInterest In general, this should provide a significant performance benefit, as the reachable state space of the product model becomes smaller in the usual cases (i.e., where we are only interested in the results from the initial states or for some filter). git-svn-id: https://www.prismmodelchecker.org/svn/prism/prism/trunk@12050 bbc10eb1-c90d-0410-af57-cb519fbb1720 --- prism/src/prism/MultiObjModelChecker.java | 2 +- prism/src/prism/NondetModelChecker.java | 17 ++++++++--------- prism/src/prism/ProbModelChecker.java | 10 ++-------- 3 files changed, 11 insertions(+), 18 deletions(-) diff --git a/prism/src/prism/MultiObjModelChecker.java b/prism/src/prism/MultiObjModelChecker.java index 6a3c7256..3b5ea157 100644 --- a/prism/src/prism/MultiObjModelChecker.java +++ b/prism/src/prism/MultiObjModelChecker.java @@ -103,7 +103,7 @@ public class MultiObjModelChecker extends PrismComponent // Build product of MDP and automaton mainLog.println("\nConstructing MDP-DRA product..."); - NondetModel modelNew = mcLtl.constructProductMDP(dra[i], model, labelDDs, draDDRowVars, draDDColVars, false, i == 0 ? ddStateIndex : model.getStart()); + NondetModel modelNew = mcLtl.constructProductMDP(dra[i], model, labelDDs, draDDRowVars, draDDColVars, (i == 0 ? ddStateIndex : model.getStart()).copy()); modelNew.printTransInfo(mainLog, prism.getExtraDDInfo()); // Deref label BDDs diff --git a/prism/src/prism/NondetModelChecker.java b/prism/src/prism/NondetModelChecker.java index f67fea25..1d1a5e22 100644 --- a/prism/src/prism/NondetModelChecker.java +++ b/prism/src/prism/NondetModelChecker.java @@ -1200,9 +1200,6 @@ public class NondetModelChecker extends NonProbModelChecker int i; long l; - // currently, ignore statesOfInterest - JDD.Deref(statesOfInterest); - // For min probabilities, need to negate the formula // (But check fairness setting since this may affect min/max) // (add parentheses to allow re-parsing if required) @@ -1225,14 +1222,19 @@ public class NondetModelChecker extends NonProbModelChecker AcceptanceType.GENERALIZED_RABIN, AcceptanceType.REACH }; - da = mcLtl.constructDAForLTLFormula(this, model, expr, labelDDs, allowedAcceptance); + try { + da = mcLtl.constructDAForLTLFormula(this, model, expr, labelDDs, allowedAcceptance); + } catch (Exception e) { + JDD.Deref(statesOfInterest); + throw e; + } // Build product of MDP and automaton l = System.currentTimeMillis(); mainLog.println("\nConstructing MDP-"+da.getAutomataType()+" product..."); daDDRowVars = new JDDVars(); daDDColVars = new JDDVars(); - modelProduct = mcLtl.constructProductMDP(da, model, labelDDs, daDDRowVars, daDDColVars); + modelProduct = mcLtl.constructProductMDP(da, model, labelDDs, daDDRowVars, daDDColVars, statesOfInterest); l = System.currentTimeMillis() - l; mainLog.println("Time for product construction: " + l / 1000.0 + " seconds."); mainLog.println(); @@ -1458,9 +1460,6 @@ public class NondetModelChecker extends NonProbModelChecker int i; long l; - // currently, ignore statesOfInterest - JDD.Deref(statesOfInterest); - if (Expression.containsTemporalTimeBounds(expr)) { if (model.getModelType().continuousTime()) { throw new PrismException("DA construction for time-bounded operators not supported for " + model.getModelType()+"."); @@ -1518,7 +1517,7 @@ public class NondetModelChecker extends NonProbModelChecker daDDRowVars = new JDDVars(); daDDColVars = new JDDVars(); l = System.currentTimeMillis(); - modelProduct = mcLtl.constructProductMDP(da, model, labelDDs, daDDRowVars, daDDColVars); + modelProduct = mcLtl.constructProductMDP(da, model, labelDDs, daDDRowVars, daDDColVars, statesOfInterest); l = System.currentTimeMillis() - l; mainLog.println("Time for product construction: " + l / 1000.0 + " seconds."); mainLog.println(); diff --git a/prism/src/prism/ProbModelChecker.java b/prism/src/prism/ProbModelChecker.java index 17cde16c..c8982acb 100644 --- a/prism/src/prism/ProbModelChecker.java +++ b/prism/src/prism/ProbModelChecker.java @@ -552,9 +552,6 @@ public class ProbModelChecker extends NonProbModelChecker JDDVars daDDRowVars, daDDColVars; int i; - // TODO: take statesOfInterest into account for product construction - JDD.Deref(statesOfInterest); - AcceptanceType[] allowedAcceptance = { AcceptanceType.REACH, AcceptanceType.BUCHI, @@ -571,7 +568,7 @@ public class ProbModelChecker extends NonProbModelChecker mainLog.println("\nConstructing MC-"+da.getAutomataType()+" product..."); daDDRowVars = new JDDVars(); daDDColVars = new JDDVars(); - modelProduct = mcLtl.constructProductMC(da, model, labelDDs, daDDRowVars, daDDColVars); + modelProduct = mcLtl.constructProductMC(da, model, labelDDs, daDDRowVars, daDDColVars, statesOfInterest); mainLog.println(); modelProduct.printTransInfo(mainLog, prism.getExtraDDInfo()); // Output product, if required @@ -968,9 +965,6 @@ public class ProbModelChecker extends NonProbModelChecker int i; long l; - // currently, ignore statesOfInterest - JDD.Deref(statesOfInterest); - if (Expression.containsTemporalTimeBounds(expr)) { if (model.getModelType().continuousTime()) { throw new PrismException("DA construction for time-bounded operators not supported for " + model.getModelType()+"."); @@ -1020,7 +1014,7 @@ public class ProbModelChecker extends NonProbModelChecker daDDRowVars = new JDDVars(); daDDColVars = new JDDVars(); l = System.currentTimeMillis(); - modelProduct = mcLtl.constructProductMC(da, model, labelDDs, daDDRowVars, daDDColVars); + modelProduct = mcLtl.constructProductMC(da, model, labelDDs, daDDRowVars, daDDColVars, statesOfInterest); l = System.currentTimeMillis() - l; mainLog.println("Time for product construction: " + l / 1000.0 + " seconds."); mainLog.println();