Browse Source

Push lifting of (explicit) reward structures into Reward classes.

git-svn-id: https://www.prismmodelchecker.org/svn/prism/prism/trunk@10354 bbc10eb1-c90d-0410-af57-cb519fbb1720
master
Dave Parker 11 years ago
parent
commit
21d663816a
  1. 2
      prism/src/explicit/MDPModelChecker.java
  2. 34
      prism/src/explicit/Product.java
  3. 6
      prism/src/explicit/rewards/MCRewards.java
  4. 9
      prism/src/explicit/rewards/MCRewardsFromMDPRewards.java
  5. 10
      prism/src/explicit/rewards/MDPRewards.java
  6. 28
      prism/src/explicit/rewards/MDPRewardsSimple.java
  7. 11
      prism/src/explicit/rewards/Rewards.java
  8. 6
      prism/src/explicit/rewards/StateRewards.java
  9. 15
      prism/src/explicit/rewards/StateRewardsArray.java
  10. 11
      prism/src/explicit/rewards/StateRewardsConstant.java
  11. 17
      prism/src/explicit/rewards/StateRewardsSimple.java

2
prism/src/explicit/MDPModelChecker.java

@ -158,7 +158,7 @@ public class MDPModelChecker extends ProbModelChecker
product = mcLtl.constructProductMDP(this, (MDP)model, expr, statesOfInterest, allowedAcceptance);
// Adapt reward info to product model
productRewards = product.liftFromModel((MDPRewards) modelRewards);
productRewards = ((MDPRewards) modelRewards).liftFromModel(product);
// Output product, if required
if (getExportProductTrans()) {

34
prism/src/explicit/Product.java

@ -29,9 +29,6 @@ package explicit;
import java.util.BitSet;
import explicit.rewards.MDPRewards;
import explicit.rewards.MDPRewardsSimple;
import explicit.rewards.StateRewardsConstant;
import parser.type.TypeBool;
import parser.type.TypeDouble;
import parser.type.TypeInt;
@ -145,37 +142,6 @@ public abstract class Product<M extends Model> implements ModelTransformation<M,
return result;
}
/**
* Lifts an MDP reward structure over states in the original model to one
* over states in the product model: The rewards for a product state are
* copied from those the parameter for the corresponding original model state.
* It is assumed that the original model in the product was an MDP.
* It is also assume that nondeterministic choices in each state of the product
* are ordered in the same way as in the original model.
* @param mdpRewards an MDPRewards over states of the original model for this product.
*/
public MDPRewards liftFromModel(MDPRewards mdpRewards)
{
MDP productMDP = (MDP)productModel;
// Special case: constant state rewards
if (mdpRewards instanceof StateRewardsConstant) {
return ((StateRewardsConstant) mdpRewards).deepCopy();
}
// Normal: state and transition rewards
else {
int numStates = productMDP.getNumStates();
MDPRewardsSimple rewSimple = new MDPRewardsSimple(numStates);
for (int productState = 0; productState < numStates; productState++) {
rewSimple.setStateReward(productState, mdpRewards.getStateReward(getModelState(productState)));
int numChoices = productMDP.getNumChoices(productState);
for (int i = 0; i < numChoices; i++) {
rewSimple.setTransitionReward(productState, i, mdpRewards.getTransitionReward(getModelState(productState), i));
}
}
return rewSimple;
}
}
/**
* Project state values from the product model back to the original model. This function
* assumes that the product model has at most one initial state per state in the original

6
prism/src/explicit/rewards/MCRewards.java

@ -26,6 +26,9 @@
package explicit.rewards;
import explicit.Model;
import explicit.Product;
/**
* Classes that provide (read) access to explicit-state rewards for a Markov chain (DTMC/CTMC).
*/
@ -35,4 +38,7 @@ public interface MCRewards extends Rewards
* Get the state reward for state {@code s}.
*/
public abstract double getStateReward(int s);
@Override
public MCRewards liftFromModel(Product<? extends Model> product);
}

9
prism/src/explicit/rewards/MCRewardsFromMDPRewards.java

@ -26,6 +26,9 @@
package explicit.rewards;
import explicit.Model;
import explicit.Product;
/**
* Explicit-state representation of a DTMC rewards structure, constructed (implicitly)
@ -55,4 +58,10 @@ public class MCRewardsFromMDPRewards implements MCRewards
// This works fine for cumulative rewards, but not instantaneous ones
return mdpRewards.getStateReward(s) + mdpRewards.getTransitionReward(s, strat[s]);
}
@Override
public MCRewards liftFromModel(Product<? extends Model> product)
{
throw new UnsupportedOperationException();
}
}

10
prism/src/explicit/rewards/MDPRewards.java

@ -26,6 +26,9 @@
package explicit.rewards;
import explicit.Model;
import explicit.Product;
/**
* Classes that provide (read) access to explicit-state rewards for an MDP.
*/
@ -35,9 +38,12 @@ public interface MDPRewards extends Rewards
* Get the state reward for state {@code s}.
*/
public abstract double getStateReward(int s);
/**
* Get the transition reward for the {@code i}th choice from state {@code s}.
*/
public abstract double getTransitionReward(int s, int i);
public abstract double getTransitionReward(int s, int i);
@Override
public MDPRewards liftFromModel(Product<? extends Model> product);
}

28
prism/src/explicit/rewards/MDPRewardsSimple.java

@ -29,6 +29,10 @@ package explicit.rewards;
import java.util.ArrayList;
import java.util.List;
import explicit.Model;
import explicit.NondetModel;
import explicit.Product;
/**
* Simple explicit-state storage of rewards for an MDP.
* Like the related class MDPSimple, this is not especially efficient, but mutable (in terms of size).
@ -184,6 +188,30 @@ public class MDPRewardsSimple implements MDPRewards
return list.get(i);
}
// Converters
@Override
public MDPRewards liftFromModel(Product<? extends Model> product)
{
Model modelProd = product.getProductModel();
int numStatesProd = modelProd.getNumStates();
MDPRewardsSimple rewardsProd = new MDPRewardsSimple(numStatesProd);
if (stateRewards != null) {
for (int s = 0; s < numStatesProd; s++) {
rewardsProd.setStateReward(s, stateRewards.get(product.getModelState(s)));
}
}
if (transRewards != null) {
for (int s = 0; s < numStatesProd; s++) {
int numChoices = transRewards.get(s).size();
for (int i = 0; i < numChoices; i++) {
rewardsProd.setTransitionReward(s, i, transRewards.get(product.getModelState(s)).get(i));
}
}
}
return rewardsProd;
}
@Override
public String toString()
{

11
prism/src/explicit/rewards/Rewards.java

@ -27,10 +27,17 @@
package explicit.rewards;
import explicit.Model;
import explicit.Product;
/**
* A dummy interface implemented by all reward classes.
* Interface implemented by all reward classes.
*/
public interface Rewards
{
/**
* Create a new reward structure that lifts this one such that it is defined over states of a
* model that is a product of the one that this reward structure is defined over.
*/
public Rewards liftFromModel(Product<? extends Model> product);
}

6
prism/src/explicit/rewards/StateRewards.java

@ -26,6 +26,9 @@
package explicit.rewards;
import explicit.Model;
import explicit.Product;
/**
* Explicit-state storage of just state rewards.
*/
@ -54,6 +57,9 @@ public abstract class StateRewards implements MCRewards, MDPRewards, STPGRewards
return deepCopy();
}
@Override
public abstract StateRewards liftFromModel(Product<? extends Model> product);
/**
* Perform a deep copy.
*/

15
prism/src/explicit/rewards/StateRewardsArray.java

@ -27,6 +27,7 @@
package explicit.rewards;
import explicit.Model;
import explicit.Product;
/**
* Explicit-state storage of just state rewards (as an array).
@ -87,6 +88,20 @@ public class StateRewardsArray extends StateRewards
return stateRewards[s];
}
// Converters
@Override
public StateRewards liftFromModel(Product<? extends Model> product)
{
Model modelProd = product.getProductModel();
int numStatesProd = modelProd.getNumStates();
StateRewardsArray rewardsProd = new StateRewardsArray(numStatesProd);
for (int s = 0; s < numStatesProd; s++) {
rewardsProd.setStateReward(s, stateRewards[product.getModelState(s)]);
}
return rewardsProd;
}
// Other
@Override

11
prism/src/explicit/rewards/StateRewardsConstant.java

@ -26,6 +26,9 @@
package explicit.rewards;
import explicit.Model;
import explicit.Product;
/**
* Explicit-state storage of constant state rewards.
*/
@ -49,6 +52,14 @@ public class StateRewardsConstant extends StateRewards
return stateReward;
}
// Converters
@Override
public StateRewards liftFromModel(Product<? extends Model> product)
{
return deepCopy();
}
// Other
@Override

17
prism/src/explicit/rewards/StateRewardsSimple.java

@ -28,6 +28,9 @@ package explicit.rewards;
import java.util.ArrayList;
import explicit.Model;
import explicit.Product;
/**
* Explicit-state storage of just state rewards (mutable).
*/
@ -93,6 +96,20 @@ public class StateRewardsSimple extends StateRewards
}
}
// Converters
@Override
public StateRewards liftFromModel(Product<? extends Model> product)
{
Model modelProd = product.getProductModel();
int numStatesProd = modelProd.getNumStates();
StateRewardsSimple rewardsProd = new StateRewardsSimple();
for (int s = 0; s < numStatesProd; s++) {
rewardsProd.setStateReward(s, getStateReward(product.getModelState(s)));
}
return rewardsProd;
}
// Other
@Override

Loading…
Cancel
Save