From c7ee82d4bc654105f99020eb23a0553a6442a282 Mon Sep 17 00:00:00 2001 From: Dave Parker Date: Wed, 7 Aug 2013 17:09:26 +0000 Subject: [PATCH] More classes switched to PrismComponent. git-svn-id: https://www.prismmodelchecker.org/svn/prism/prism/trunk@7245 bbc10eb1-c90d-0410-af57-cb519fbb1720 --- .../src/explicit/PrismSTPGAbstractRefine.java | 27 ++++++++++++------- prism/src/explicit/QuantAbstractRefine.java | 9 +++---- .../explicit/QuantAbstractRefineExample.java | 11 +++++++- prism/src/pta/PTAAbstractRefine.java | 4 ++- prism/src/pta/PTAModelChecker.java | 3 +-- prism/src/pta/PTAModelCheckerCL.java | 2 +- 6 files changed, 36 insertions(+), 20 deletions(-) diff --git a/prism/src/explicit/PrismSTPGAbstractRefine.java b/prism/src/explicit/PrismSTPGAbstractRefine.java index f7341be5..bf3c8228 100644 --- a/prism/src/explicit/PrismSTPGAbstractRefine.java +++ b/prism/src/explicit/PrismSTPGAbstractRefine.java @@ -29,6 +29,7 @@ package explicit; import java.util.*; import prism.ModelType; +import prism.PrismComponent; import prism.PrismException; public class PrismSTPGAbstractRefine extends QuantAbstractRefine @@ -58,6 +59,14 @@ public class PrismSTPGAbstractRefine extends QuantAbstractRefine // Map from abstract P1 choices to concrete state sets protected List>> abstractToConcrete; + /** + * Default constructor. + */ + public PrismSTPGAbstractRefine(PrismComponent parent) throws PrismException + { + super(parent); + } + // Implementation of initialise() for abstraction-refinement loop; see superclass for details protected void initialise() throws PrismException @@ -447,16 +456,16 @@ public class PrismSTPGAbstractRefine extends QuantAbstractRefine String s, sw, sOpt, filenameBase; int i, j; - // Create abstraction-refinement engine - abstractRefine = new PrismSTPGAbstractRefine(); - abstractRefine.sanityChecks = true; - - // Parse command line args - if (args.length < 3) { - System.err.println("Usage: java ... [options] "); - System.exit(1); - } try { + // Create abstraction-refinement engine + abstractRefine = new PrismSTPGAbstractRefine(null); + abstractRefine.sanityChecks = true; + + // Parse command line args + if (args.length < 3) { + System.err.println("Usage: java ... [options] "); + System.exit(1); + } nonSwitches = new ArrayList(); for (i = 0; i < args.length; i++) { s = args[i]; diff --git a/prism/src/explicit/QuantAbstractRefine.java b/prism/src/explicit/QuantAbstractRefine.java index eec5b0db..b9d26ad2 100644 --- a/prism/src/explicit/QuantAbstractRefine.java +++ b/prism/src/explicit/QuantAbstractRefine.java @@ -50,10 +50,8 @@ import explicit.ProbModelChecker.ValIterDir; *

* The abstraction-refinement loop can then be started with {@link #abstractRefine}. */ -public abstract class QuantAbstractRefine +public abstract class QuantAbstractRefine extends PrismComponent { - // Log for output (default: just send to stdout) - protected PrismLog mainLog = new PrismPrintStreamLog(System.out); // Model checker protected ProbModelChecker mc; // Dummy model checker to store options @@ -147,10 +145,9 @@ public abstract class QuantAbstractRefine /** * Default constructor. */ - public QuantAbstractRefine() + public QuantAbstractRefine(PrismComponent parent) throws PrismException { - // By default, log output goes to System.out. - setLog(new PrismPrintStreamLog(System.out)); + super(parent); // Create dummy model checker to store options try { mcOptions = new ProbModelChecker(null); diff --git a/prism/src/explicit/QuantAbstractRefineExample.java b/prism/src/explicit/QuantAbstractRefineExample.java index 05474b39..d39f32d0 100644 --- a/prism/src/explicit/QuantAbstractRefineExample.java +++ b/prism/src/explicit/QuantAbstractRefineExample.java @@ -34,6 +34,7 @@ import parser.State; import parser.ast.*; import prism.ModelType; import prism.Prism; +import prism.PrismComponent; import prism.PrismException; import prism.PrismLog; import prism.PrismPrintStreamLog; @@ -58,6 +59,14 @@ public class QuantAbstractRefineExample extends QuantAbstractRefine // Map from abstract P1 choices to concrete state sets protected List>> abstractToConcrete; + /** + * Default constructor. + */ + public QuantAbstractRefineExample(PrismComponent parent) throws PrismException + { + super(parent); + } + // Implementation of initialise() for abstraction-refinement loop; see superclass for details @Override @@ -322,7 +331,7 @@ public class QuantAbstractRefineExample extends QuantAbstractRefine model.exportToPrismExplicitTra(args[1]); // Create/initialise abstraction-refinement engine - QuantAbstractRefineExample abstractRefine = new QuantAbstractRefineExample(); + QuantAbstractRefineExample abstractRefine = new QuantAbstractRefineExample(prism); abstractRefine.setModelType(ModelType.MDP); abstractRefine.setPropertyType(PropertyType.PROB_REACH); abstractRefine.sanityChecks = true; diff --git a/prism/src/pta/PTAAbstractRefine.java b/prism/src/pta/PTAAbstractRefine.java index 963f924a..53c96b08 100644 --- a/prism/src/pta/PTAAbstractRefine.java +++ b/prism/src/pta/PTAAbstractRefine.java @@ -29,6 +29,7 @@ package pta; import java.util.*; import prism.ModelType; +import prism.PrismComponent; import prism.PrismException; import explicit.*; @@ -55,8 +56,9 @@ public class PTAAbstractRefine extends QuantAbstractRefine /** * Default constructor. */ - public PTAAbstractRefine() + public PTAAbstractRefine(PrismComponent parent) throws PrismException { + super(parent); // Just do basic config for QuantAbstractRefine setModelType(ModelType.MDP); setPropertyType(QuantAbstractRefine.PropertyType.PROB_REACH); diff --git a/prism/src/pta/PTAModelChecker.java b/prism/src/pta/PTAModelChecker.java index dc0cc779..231d74e8 100644 --- a/prism/src/pta/PTAModelChecker.java +++ b/prism/src/pta/PTAModelChecker.java @@ -306,9 +306,8 @@ public class PTAModelChecker extends PrismComponent // Do probability computation through abstraction/refinement/stochastic games if (ptaMethod.equals("Stochastic games")) { PTAAbstractRefine ptaAR; - ptaAR = new PTAAbstractRefine(); + ptaAR = new PTAAbstractRefine(this); String arOptions = settings.getString(PrismSettings.PRISM_AR_OPTIONS); - ptaAR.setLog(mainLog); ptaAR.parseOptions(arOptions.split(",")); return ptaAR.forwardsReachAbstractRefine(pta, targetLocs, null, min); } diff --git a/prism/src/pta/PTAModelCheckerCL.java b/prism/src/pta/PTAModelCheckerCL.java index 6668da2e..105b13fb 100644 --- a/prism/src/pta/PTAModelCheckerCL.java +++ b/prism/src/pta/PTAModelCheckerCL.java @@ -83,7 +83,7 @@ public class PTAModelCheckerCL try { // Build PTAAbstractRefine object - abstractRefine = new PTAAbstractRefine(); + abstractRefine = new PTAAbstractRefine(null); // Parse command-line arguments parseCommandLineArgs(args);