From 3dde812e48aa724746a400f5c8aa348a1e8ce3d6 Mon Sep 17 00:00:00 2001 From: Dave Parker Date: Tue, 28 May 2019 19:00:23 +0100 Subject: [PATCH] State reward import from files for explicit engine. --- .../import/dice.pm.importexport.auto | 4 +- .../import/poll2.sm.importexport.auto | 4 +- .../import/robot.prism.importexport.auto | 4 +- .../prism/ExplicitFilesRewardGenerator.java | 137 ++++++++++++++++++ prism/src/prism/Prism.java | 7 +- 5 files changed, 145 insertions(+), 11 deletions(-) create mode 100644 prism/src/prism/ExplicitFilesRewardGenerator.java diff --git a/prism-tests/functionality/import/dice.pm.importexport.auto b/prism-tests/functionality/import/dice.pm.importexport.auto index 5ff4cd07..c51605df 100644 --- a/prism-tests/functionality/import/dice.pm.importexport.auto +++ b/prism-tests/functionality/import/dice.pm.importexport.auto @@ -1,3 +1,3 @@ -dtmc -importmodel dice.all -exportmodel dice.sta,tra,lab,srew --dtmc -importmodel dice.all -exportmodel dice.sta,tra,lab -ex --importmodel dice.all -exportmodel dice.sta,tra,lab -ex +-dtmc -importmodel dice.all -exportmodel dice.sta,tra,lab,srew -ex +-importmodel dice.all -exportmodel dice.sta,tra,lab,srew -ex diff --git a/prism-tests/functionality/import/poll2.sm.importexport.auto b/prism-tests/functionality/import/poll2.sm.importexport.auto index 45d9e506..6a36d059 100644 --- a/prism-tests/functionality/import/poll2.sm.importexport.auto +++ b/prism-tests/functionality/import/poll2.sm.importexport.auto @@ -1,3 +1,3 @@ -ctmc -importmodel poll2.all -exportmodel poll2.sta,tra,lab,srew --ctmc -importmodel poll2.all -exportmodel poll2.sta,tra,lab -ex --importmodel poll2.all -exportmodel poll2.sta,tra,lab -ex +-ctmc -importmodel poll2.all -exportmodel poll2.sta,tra,lab,srew -ex +-importmodel poll2.all -exportmodel poll2.sta,tra,lab,srew -ex diff --git a/prism-tests/functionality/import/robot.prism.importexport.auto b/prism-tests/functionality/import/robot.prism.importexport.auto index f2451568..622f5609 100644 --- a/prism-tests/functionality/import/robot.prism.importexport.auto +++ b/prism-tests/functionality/import/robot.prism.importexport.auto @@ -1,3 +1,3 @@ -mdp -importmodel robot.all -exportmodel robot.sta,tra,lab,srew --mdp -importmodel robot.all -exportmodel robot.sta,tra,lab -ex --importmodel robot.all -exportmodel robot.sta,tra,lab -ex +-mdp -importmodel robot.all -exportmodel robot.sta,tra,lab,srew -ex +-importmodel robot.all -exportmodel robot.sta,tra,lab,srew -ex diff --git a/prism/src/prism/ExplicitFilesRewardGenerator.java b/prism/src/prism/ExplicitFilesRewardGenerator.java new file mode 100644 index 00000000..5475b26d --- /dev/null +++ b/prism/src/prism/ExplicitFilesRewardGenerator.java @@ -0,0 +1,137 @@ +//============================================================================== +// +// Copyright (c) 2019- +// Authors: +// * Dave Parker (University of Birmingham) +// +//------------------------------------------------------------------------------ +// +// 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 prism; + +import java.io.BufferedReader; +import java.io.File; +import java.io.FileReader; +import java.io.IOException; +import java.util.Collections; +import java.util.List; + +public class ExplicitFilesRewardGenerator extends PrismComponent implements RewardGenerator +{ + // File(s) to read in rewards from + private File stateRewardsFile; + // Model info + private int numStates; + // Local storage of rewards + private boolean stateRewardsLoaded = false; + private double[] stateRewards; + + /** + * Constructor + */ + public ExplicitFilesRewardGenerator(PrismComponent parent) + { + super(parent); + } + + /** + * Constructor + */ + public ExplicitFilesRewardGenerator(PrismComponent parent, File stateRewardsFile, int numStates) throws PrismException + { + this(parent); + this.stateRewardsFile = stateRewardsFile; + this.numStates = numStates; + } + + /** + * Extract the state rewards from the file and store locally. + */ + private void extractStateRewards() throws PrismException + { + int lineNum = -1; + stateRewards = new double[numStates]; + // open file for reading, automatic close when done + try (BufferedReader in = new BufferedReader(new FileReader(stateRewardsFile))) { + // skip first line + in.readLine(); + lineNum = 1; + // read remaining lines + String s = in.readLine(); + lineNum++; + while (s != null) { + // skip blank lines + s = s.trim(); + if (s.length() > 0) { + // split into two parts + String[] ss = s.split(" "); + // determine which state this line describes + int i = Integer.parseInt(ss[0]); + if (i < 0 || i >= numStates) { + throw new PrismException("Invalid state index " + i); + } + // determine which state this line describes + double d = Double.parseDouble(ss[1]); + // store + stateRewards[i] = d; + } + // read next line + s = in.readLine(); + lineNum++; + } + } catch (IOException e) { + throw new PrismException("File I/O error reading from \"" + stateRewardsFile + "\""); + } catch (NumberFormatException e) { + throw new PrismException("Error detected " + e.getMessage() + "at line " + lineNum + " of states file \"" + stateRewardsFile + "\""); + } + } + + // Methods to implement RewardGenerator + + @Override + public List getRewardStructNames() + { + return Collections.singletonList(""); + } + + @Override + public boolean rewardStructHasTransitionRewards(int r) + { + return false; + } + + @Override + public boolean isRewardLookupSupported(RewardLookup lookup) + { + return lookup == RewardLookup.BY_STATE_INDEX; + } + + @Override + public double getStateReward(int r, int s) throws PrismException + { + if (r != 0) { + throw new PrismException("Only one reward structure has been imported"); + } + if (!stateRewardsLoaded) { + extractStateRewards(); + } + return stateRewards[s]; + } +} diff --git a/prism/src/prism/Prism.java b/prism/src/prism/Prism.java index 2b08c89a..933194a4 100644 --- a/prism/src/prism/Prism.java +++ b/prism/src/prism/Prism.java @@ -2086,6 +2086,8 @@ public class Prism extends PrismComponent implements PrismSettingsListener currentModelInfo, explicitFilesNumStates); } else { currentModelExpl = new ExplicitFiles2Model(this).build(explicitFilesStatesFile, explicitFilesTransFile, explicitFilesLabelsFile, currentModelInfo, explicitFilesNumStates); + currentModelGenerator = null; + currentRewardGenerator = new ExplicitFilesRewardGenerator(this, explicitFilesStateRewardsFile, explicitFilesNumStates); } break; default: @@ -2431,11 +2433,6 @@ public class Prism extends PrismComponent implements PrismSettingsListener return; } - if (currentModelSource == ModelSource.EXPLICIT_FILES && getExplicit()) { - mainLog.println("\nOmitting state reward export (not supported when importing files using the explicit engine)"); - return; - } - // Rows format does not apply to vectors if (exportType == EXPORT_ROWS) exportType = EXPORT_PLAIN;