From d193532115d02932b3bae8288ee6db464b88d8df Mon Sep 17 00:00:00 2001 From: Dave Parker Date: Tue, 16 Jul 2013 10:03:57 +0000 Subject: [PATCH] Code tidy git-svn-id: https://www.prismmodelchecker.org/svn/prism/prism/trunk@7045 bbc10eb1-c90d-0410-af57-cb519fbb1720 --- prism/src/prism/LTLModelChecker.java | 14 ++++++-------- 1 file changed, 6 insertions(+), 8 deletions(-) diff --git a/prism/src/prism/LTLModelChecker.java b/prism/src/prism/LTLModelChecker.java index a9a8bd09..174f8ef1 100644 --- a/prism/src/prism/LTLModelChecker.java +++ b/prism/src/prism/LTLModelChecker.java @@ -29,8 +29,6 @@ package prism; import java.util.*; -import mtbdd.PrismMTBDD; - import jdd.*; import parser.*; import parser.ast.*; @@ -120,7 +118,7 @@ public class LTLModelChecker * @param model: The DTMC/CTMC * @param labelDDs: BDDs giving the set of states for each AP in the DRA */ - public ProbModel constructProductMC(DRA dra, ProbModel model, Vector labelDDs) throws PrismException + public ProbModel constructProductMC(DRA dra, ProbModel model, Vector labelDDs) throws PrismException { return constructProductMC(dra, model, labelDDs, null, null, true); } @@ -133,7 +131,7 @@ public class LTLModelChecker * @param draDDRowVarsCopy: (Optionally) empty JDDVars object to obtain copy of DD row vars for DRA * @param draDDColVarsCopy: (Optionally) empty JDDVars object to obtain copy of DD col vars for DRA */ - public ProbModel constructProductMC(DRA dra, ProbModel model, Vector labelDDs, JDDVars draDDRowVarsCopy, JDDVars draDDColVarsCopy) + public ProbModel constructProductMC(DRA dra, ProbModel model, Vector labelDDs, JDDVars draDDRowVarsCopy, JDDVars draDDColVarsCopy) throws PrismException { return constructProductMC(dra, model, labelDDs, draDDRowVarsCopy, draDDColVarsCopy, true); @@ -149,7 +147,7 @@ public class LTLModelChecker * @param allInit: Do we assume that all states of the original model are initial states? * (just for the purposes of reachability) */ - public ProbModel constructProductMC(DRA dra, ProbModel model, Vector labelDDs, JDDVars draDDRowVarsCopy, JDDVars draDDColVarsCopy, boolean allInit) + public ProbModel constructProductMC(DRA dra, ProbModel model, Vector labelDDs, JDDVars draDDRowVarsCopy, JDDVars draDDColVarsCopy, boolean allInit) throws PrismException { // Existing model - dds, vars, etc. @@ -320,7 +318,7 @@ public class LTLModelChecker * @param model: The MDP * @param labelDDs: BDDs giving the set of states for each AP in the DRA */ - public NondetModel constructProductMDP(DRA dra, NondetModel model, Vector labelDDs) throws PrismException + public NondetModel constructProductMDP(DRA dra, NondetModel model, Vector labelDDs) throws PrismException { return constructProductMDP(dra, model, labelDDs, null, null, true, null); } @@ -333,7 +331,7 @@ public class LTLModelChecker * @param draDDRowVarsCopy: (Optionally) empty JDDVars object to obtain copy of DD row vars for DRA * @param draDDColVarsCopy: (Optionally) empty JDDVars object to obtain copy of DD col vars for DRA */ - public NondetModel constructProductMDP(DRA dra, NondetModel model, Vector labelDDs, JDDVars draDDRowVarsCopy, JDDVars draDDColVarsCopy) + public NondetModel constructProductMDP(DRA dra, NondetModel model, Vector labelDDs, JDDVars draDDRowVarsCopy, JDDVars draDDColVarsCopy) throws PrismException { return constructProductMDP(dra, model, labelDDs, draDDRowVarsCopy, draDDColVarsCopy, true, null); @@ -351,7 +349,7 @@ public class LTLModelChecker * @param init: The initial state(s) (of the original model) used to build the product; * if null; we just take the existing initial states from model.getStart(). */ - public NondetModel constructProductMDP(DRA dra, NondetModel model, Vector labelDDs, JDDVars draDDRowVarsCopy, JDDVars draDDColVarsCopy, + public NondetModel constructProductMDP(DRA dra, NondetModel model, Vector labelDDs, JDDVars draDDRowVarsCopy, JDDVars draDDColVarsCopy, boolean allInit, JDDNode init) throws PrismException { // Existing model - dds, vars, etc.