Skip to content

Commit

Permalink
Bugfix: Explicit import of rewards files for IMDPs.
Browse files Browse the repository at this point in the history
Previously, when importing rewards, the evaluator was copied
from the model. But, currently, for interval models that does
not work, because the evaluator is for intervals.

Later, when uncertain models are refactored, copying from
models could likely be reinstated if prefered.
  • Loading branch information
davexparker committed Sep 30, 2024
1 parent 9e1ebd0 commit ed80e0e
Show file tree
Hide file tree
Showing 5 changed files with 25 additions and 4 deletions.
Original file line number Diff line number Diff line change
@@ -1 +1 @@
-importmodel irobot.all -exportmodel irobot.sta,tra,lab -ex
-importmodel irobot.all -exportmodel irobot.all -ex
2 changes: 1 addition & 1 deletion prism-tests/functionality/import/irobot.prism.orig
Original file line number Diff line number Diff line change
Expand Up @@ -25,4 +25,4 @@ label "hazard" = s=1;
label "goal1" = s=5;
label "goal2" = s=2|s=3;

//rewards "time" true : 1; endrewards
rewards "time" true : 1; endrewards
9 changes: 9 additions & 0 deletions prism-tests/functionality/import/irobot.srew
Original file line number Diff line number Diff line change
@@ -0,0 +1,9 @@
# Reward structure "time"
# State rewards
6 6
0 1
1 1
2 1
3 1
4 1
5 1
3 changes: 3 additions & 0 deletions prism-tests/functionality/import/irobot.trew
Original file line number Diff line number Diff line change
@@ -0,0 +1,3 @@
# Reward structure "time"
# Transition rewards
6 10 0
13 changes: 11 additions & 2 deletions prism/src/explicit/ExplicitFiles2Rewards.java
Original file line number Diff line number Diff line change
Expand Up @@ -63,9 +63,19 @@ public class ExplicitFiles2Rewards<Value> extends PrismComponent implements Rewa
* The rewards are actually imported/stored later, on demand.
*/
public ExplicitFiles2Rewards(PrismComponent parent, ExplicitModelImporter importer) throws PrismException
{
this(parent, importer, (Evaluator<Value>) Evaluator.forDouble());
}

/**
* Construct a ExplicitFiles2Rewards object for a specified importer.
* The rewards are actually imported/stored later, on demand.
*/
public ExplicitFiles2Rewards(PrismComponent parent, ExplicitModelImporter importer, Evaluator<Value> eval) throws PrismException
{
super(parent);
this.importer = importer;
this.eval = eval;
rewardInfo = importer.getRewardInfo();
// Initialise storage
rewards = new RewardsSimple[rewardInfo.getNumRewardStructs()];
Expand All @@ -74,12 +84,11 @@ public ExplicitFiles2Rewards(PrismComponent parent, ExplicitModelImporter import
/**
* Provide access to the model for which the rewards are to be defined.
* Needed to look up information when storing transition rewards.
* The model's evaluator and attached states list is also stored.
* The model's attached states list is also stored.
*/
public void setModel(Model<Value> model)
{
this.model = model;
eval = model.getEvaluator();
setStatesList(model.getStatesList());
}

Expand Down

0 comments on commit ed80e0e

Please # to comment.