From 951f0bd507314822bd4b56c7974b336e94092953 Mon Sep 17 00:00:00 2001 From: Dave Parker Date: Mon, 8 Jul 2013 09:13:03 +0000 Subject: [PATCH] First bits of code for improved strategy generation. git-svn-id: https://www.prismmodelchecker.org/svn/prism/prism/trunk@6994 bbc10eb1-c90d-0410-af57-cb519fbb1720 --- prism/src/explicit/MDPModelChecker.java | 6 +++ prism/src/explicit/ModelCheckerResult.java | 10 +++- prism/src/explicit/ProbModelChecker.java | 3 ++ prism/src/prism/Prism.java | 18 +++++++ prism/src/prism/PrismCL.java | 8 +++ prism/src/prism/Result.java | 23 +++++++++ prism/src/strat/MDStrategy.java | 47 ++++++++++++++++++ prism/src/strat/MDStrategyArray.java | 57 ++++++++++++++++++++++ prism/src/strat/Strategy.java | 41 ++++++++++++++++ prism/src/strat/package-info.java | 4 ++ 10 files changed, 216 insertions(+), 1 deletion(-) create mode 100644 prism/src/strat/MDStrategy.java create mode 100644 prism/src/strat/MDStrategyArray.java create mode 100644 prism/src/strat/Strategy.java create mode 100644 prism/src/strat/package-info.java diff --git a/prism/src/explicit/MDPModelChecker.java b/prism/src/explicit/MDPModelChecker.java index f5fea042..cd611c39 100644 --- a/prism/src/explicit/MDPModelChecker.java +++ b/prism/src/explicit/MDPModelChecker.java @@ -39,6 +39,7 @@ import prism.PrismException; import prism.PrismFileLog; import prism.PrismLog; import prism.PrismUtils; +import strat.MDStrategyArray; import explicit.rewards.MDPRewards; /** @@ -191,6 +192,7 @@ public class MDPModelChecker extends ProbModelChecker res = computeUntilProbs((MDP) model, b1, b2, min); probs = StateValues.createFromDoubleArray(res.soln, model); + result.setStrategy(res.strat); return probs; } @@ -435,6 +437,10 @@ public class MDPModelChecker extends ProbModelChecker timer = System.currentTimeMillis() - timer; mainLog.println("Probabilistic reachability took " + timer / 1000.0 + " seconds."); + // Store strategy + if (genStrat) { + res.strat = new MDStrategyArray(strat); + } // Export adversary if (genStrat && exportAdv) { // Prune strategy diff --git a/prism/src/explicit/ModelCheckerResult.java b/prism/src/explicit/ModelCheckerResult.java index fb916045..8ddd427e 100644 --- a/prism/src/explicit/ModelCheckerResult.java +++ b/prism/src/explicit/ModelCheckerResult.java @@ -26,6 +26,12 @@ package explicit; +import strat.Strategy; + +/** + * Class storing some info/data from a call to a model checking or + * numerical computation method in the explicit engine. + */ public class ModelCheckerResult { // Solution vector @@ -40,7 +46,9 @@ public class ModelCheckerResult public double timePre = 0.0; // Time taken for Prob0-type precomputation (secs) public double timeProb0 = 0.0; - + // Strategy + public Strategy strat = null; + /** * Clear all stored data, including setting of array pointers to null * (which may be helpful for garbage collection purposes). diff --git a/prism/src/explicit/ProbModelChecker.java b/prism/src/explicit/ProbModelChecker.java index 6024c782..4109c10a 100644 --- a/prism/src/explicit/ProbModelChecker.java +++ b/prism/src/explicit/ProbModelChecker.java @@ -70,6 +70,9 @@ public class ProbModelChecker extends StateModelChecker protected boolean exportAdv = false; protected String exportAdvFilename; + // Additional flags/settings not included in PrismSettings + protected boolean getStrat = false; + // Enums for flags/settings // Method used for numerical solution diff --git a/prism/src/prism/Prism.java b/prism/src/prism/Prism.java index 91b95d26..5bc39584 100644 --- a/prism/src/prism/Prism.java +++ b/prism/src/prism/Prism.java @@ -176,6 +176,8 @@ public class Prism implements PrismSettingsListener protected String exportProductTransFilename = null; protected boolean exportProductStates = false; protected String exportProductStatesFilename = null; + // Generate a strategy during model checking? + protected boolean genStrat = false; // A few miscellaneous options (i.e. defunct/hidden/undocumented/etc.) // See constructor below for default values @@ -558,6 +560,14 @@ public class Prism implements PrismSettingsListener exportProductStatesFilename = s; } + /** + * Specify whether or not a strategy should be generated during model checking. + */ + public void setGenStrat(boolean genStrat) + { + this.genStrat = genStrat; + } + public void setDoReach(boolean b) throws PrismException { doReach = b; @@ -840,6 +850,14 @@ public class Prism implements PrismSettingsListener return exportProductStatesFilename; } + /** + * Whether or not a strategy should be generated during model checking. + */ + public boolean getGenStrat() + { + return genStrat; + } + public boolean getDoReach() { return doReach; diff --git a/prism/src/prism/PrismCL.java b/prism/src/prism/PrismCL.java index c59a9673..de160835 100644 --- a/prism/src/prism/PrismCL.java +++ b/prism/src/prism/PrismCL.java @@ -350,6 +350,8 @@ public class PrismCL implements PrismModelListener // store result of model checking results[j].setResult(definedMFConstants, definedPFConstants, res.getResult()); + + // if a counterexample was generated, display it Object cex = res.getCounterexample(); if (cex != null) { mainLog.println("\nCounterexample/witness:"); @@ -366,6 +368,12 @@ public class PrismCL implements PrismModelListener } } + // if a strategy was generated, and we need to export it, do so + if (res.getStrategy() != null) { + mainLog.println("\nExporting strategy..."); + res.getStrategy().export(mainLog); + } + // if required, check result against expected value if (test) { try { diff --git a/prism/src/prism/Result.java b/prism/src/prism/Result.java index 0acdbedb..214a402e 100644 --- a/prism/src/prism/Result.java +++ b/prism/src/prism/Result.java @@ -28,8 +28,12 @@ package prism; +import strat.Strategy; + /** * This class stores the result of a single verification/simulation. + * It also stores other info/objects that may be passed back to the user, + * e.g. an explanation of the result, counterexample, or optimal strategy. */ public class Result { @@ -39,6 +43,8 @@ public class Result private String explanation; // Counterexample (optional) private Object cex; + // Strategy (optional) + private Strategy strat; /** * Construct an empty Result object. @@ -48,6 +54,7 @@ public class Result this.result = null; this.explanation = null; this.cex = null; + this.strat = null; } /** @@ -83,6 +90,14 @@ public class Result this.cex = cex; } + /** + * Set the strategy (null denotes n/a). + */ + public void setStrategy(Strategy strat) + { + this.strat = strat; + } + /** * Get the result. */ @@ -107,6 +122,14 @@ public class Result return cex; } + /** + * Get the strategy (null denotes n/a). + */ + public Strategy getStrategy() + { + return strat; + } + /** * Get a string of the result and (if present) explanatory text */ diff --git a/prism/src/strat/MDStrategy.java b/prism/src/strat/MDStrategy.java new file mode 100644 index 00000000..f762d64c --- /dev/null +++ b/prism/src/strat/MDStrategy.java @@ -0,0 +1,47 @@ +//============================================================================== +// +// Copyright (c) 2002- +// Authors: +// * Dave Parker (University of Birmingham/Oxford) +// * Aistis Simaitis (University of Oxford) +// +//------------------------------------------------------------------------------ +// +// This file is part of PRISM. +// +// PRISM is free software; you can redistribute it and/or modify +// it under the terms of the GNU General Public License as published by +// the Free Software Foundation; either version 2 of the License, or +// (at your option) any later version. +// +// PRISM is distributed in the hope that it will be useful, +// but WITHOUT ANY WARRANTY; without even the implied warranty of +// MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE. See the +// GNU General Public License for more details. +// +// You should have received a copy of the GNU General Public License +// along with PRISM; if not, write to the Free Software Foundation, +// Inc., 59 Temple Place, Suite 330, Boston, MA 02111-1307 USA +// +//============================================================================== + +package strat; + +import prism.PrismLog; + +/** + * Classes to store memoryless deterministic (MD) strategies. + */ +public abstract class MDStrategy implements Strategy +{ + public abstract int getNumStates(); + public abstract int getChoice(int i); + + public void export(PrismLog out) + { + int n = getNumStates(); + for (int i = 0; i < n; i++) { + out.println(i + ":" + getChoice(i)); + } + } +} diff --git a/prism/src/strat/MDStrategyArray.java b/prism/src/strat/MDStrategyArray.java new file mode 100644 index 00000000..82ef0262 --- /dev/null +++ b/prism/src/strat/MDStrategyArray.java @@ -0,0 +1,57 @@ +//============================================================================== +// +// Copyright (c) 2002- +// Authors: +// * Dave Parker (University of Birmingham/Oxford) +// * Aistis Simaitis (University of Oxford) +// +//------------------------------------------------------------------------------ +// +// This file is part of PRISM. +// +// PRISM is free software; you can redistribute it and/or modify +// it under the terms of the GNU General Public License as published by +// the Free Software Foundation; either version 2 of the License, or +// (at your option) any later version. +// +// PRISM is distributed in the hope that it will be useful, +// but WITHOUT ANY WARRANTY; without even the implied warranty of +// MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE. See the +// GNU General Public License for more details. +// +// You should have received a copy of the GNU General Public License +// along with PRISM; if not, write to the Free Software Foundation, +// Inc., 59 Temple Place, Suite 330, Boston, MA 02111-1307 USA +// +//============================================================================== + +package strat; + +/** + * Class to store a memoryless deterministic (MD) strategy, as a (Java) array of choice indices. + */ +public class MDStrategyArray extends MDStrategy +{ + private int choices[]; + + /** + * Creates an MDStrategyArray from an integer array of choices. + * The array may later be modified/delete - take a copy if you want to keep it. + */ + public MDStrategyArray(int choices[]) + { + this.choices = choices; + } + + public int getNumStates() + { + // Need? + return choices.length; + } + + @Override + public int getChoice(int i) + { + return choices[i]; + } +} diff --git a/prism/src/strat/Strategy.java b/prism/src/strat/Strategy.java new file mode 100644 index 00000000..8348fa87 --- /dev/null +++ b/prism/src/strat/Strategy.java @@ -0,0 +1,41 @@ +//============================================================================== +// +// Copyright (c) 2002- +// Authors: +// * Dave Parker (University of Birmingham/Oxford) +// * Aistis Simaitis (University of Oxford) +// +//------------------------------------------------------------------------------ +// +// This file is part of PRISM. +// +// PRISM is free software; you can redistribute it and/or modify +// it under the terms of the GNU General Public License as published by +// the Free Software Foundation; either version 2 of the License, or +// (at your option) any later version. +// +// PRISM is distributed in the hope that it will be useful, +// but WITHOUT ANY WARRANTY; without even the implied warranty of +// MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE. See the +// GNU General Public License for more details. +// +// You should have received a copy of the GNU General Public License +// along with PRISM; if not, write to the Free Software Foundation, +// Inc., 59 Temple Place, Suite 330, Boston, MA 02111-1307 USA +// +//============================================================================== + +package strat; + +import prism.PrismLog; + +/** + * Interface for classes to store strategies (for MDPs, games, etc.) + */ +public interface Strategy +{ + /** + * Export the strategy to a PrismLog. + */ + public void export(PrismLog out); +} diff --git a/prism/src/strat/package-info.java b/prism/src/strat/package-info.java new file mode 100644 index 00000000..07e5c338 --- /dev/null +++ b/prism/src/strat/package-info.java @@ -0,0 +1,4 @@ +/** + * Classes to represent/manipulate strategies (of MDPs, games, etc.) + */ +package strat;