s14h
/
prism-accumulation
1
0
Fork 0
Code Releases Activity
Browse Source

Clean up AccumulationTransformation

accumulation
Sascha Wunderlich 7 years ago
parent
1b6e9e5ac6
commit
1616ded046
3 changed files with 44 additions and 53 deletions
Whitespace
Show all changes Ignore whitespace when comparing lines Ignore changes in amount of whitespace Ignore changes in whitespace at EOL
Split View
Diff Options
Show Stats Download Patch File Download Diff File
  1. 12
      prism/src/explicit/AccumulationProductCounting.java
  2. 15
      prism/src/explicit/AccumulationProductRegular.java
  3. 70
      prism/src/explicit/AccumulationTransformation.java

12
prism/src/explicit/AccumulationProductCounting.java
View File

@ -27,6 +27,18 @@ public class AccumulationProductCounting<M extends Model> extends AccumulationPr
super(originalModel);
}
@SuppressWarnings("unchecked")
public static <T extends Model, R extends Rewards> AccumulationProductCounting<T> generate(final Model graph, final ExpressionAccumulation accexp, final Vector<R> rewards, final ProbModelChecker mc, BitSet statesOfInterest) throws PrismException {
switch(graph.getModelType()) {
case DTMC:
return (AccumulationProductCounting<T>)generate((DTMC) graph, accexp, (Vector<MCRewards>) rewards, mc, statesOfInterest);
case MDP:
return (AccumulationProductCounting<T>)generate((MDP) graph, accexp, (Vector<MDPRewards>) rewards, mc, statesOfInterest);
default:
throw new PrismException("Can't handle accumulation product for " + graph.getModelType());
}
}
public static AccumulationProductCounting<DTMC> generate(final DTMC graph, final ExpressionAccumulation accexp, final Vector<MCRewards> rewards, final ProbModelChecker mc, BitSet statesOfInterest) throws PrismException {
final AccumulationProductCounting<DTMC> result = new AccumulationProductCounting<DTMC>(graph);
// Create auxiliary data

15
prism/src/explicit/AccumulationProductRegular.java
View File

@ -34,6 +34,18 @@ public class AccumulationProductRegular<M extends Model> extends AccumulationPro
super(originalModel);
}
@SuppressWarnings("unchecked")
public static <T extends Model, R extends Rewards> AccumulationProductRegular<T> generate(final Model graph, final ExpressionAccumulation accexp, final Vector<R> rewards, final ProbModelChecker mc, BitSet statesOfInterest) throws PrismException {
switch(graph.getModelType()) {
case DTMC:
return (AccumulationProductRegular<T>)generate((DTMC) graph, accexp, (Vector<MCRewards>) rewards, mc, statesOfInterest);
case MDP:
return (AccumulationProductRegular<T>)generate((MDP) graph, accexp, (Vector<MDPRewards>) rewards, mc, statesOfInterest);
default:
throw new PrismException("Can't handle accumulation product for " + graph.getModelType());
}
}
public static AccumulationProductRegular<DTMC> generate(final DTMC graph, final ExpressionAccumulation accexp, final Vector<MCRewards> rewards, final ProbModelChecker mc, BitSet statesOfInterest) throws PrismException {
final AccumulationProductRegular<DTMC> result = new AccumulationProductRegular<DTMC>(graph);
// Create auxiliary data
@ -96,11 +108,8 @@ public class AccumulationProductRegular<M extends Model> extends AccumulationPro
public static AccumulationProductRegular<MDP> generate(final MDP graph, final ExpressionAccumulation accexp, final Vector<MDPRewards> rewards, final ProbModelChecker mc, BitSet statesOfInterest) throws PrismException {
// This is basically the same thing as for DTMCs
final AccumulationProductRegular<MDP> result = new AccumulationProductRegular<MDP>(graph);
// Create auxiliary data
mc.getLog().println(" [AP] generating aux data...");
result.createAuxData(graph, accexp, rewards, mc);
mc.getLog().println(" done.");
class AccumulationMDPProductOperator implements MDPProductOperator
{

70
prism/src/explicit/AccumulationTransformation.java
View File

@ -5,8 +5,7 @@ import java.util.BitSet;
import java.util.Vector;
import explicit.rewards.ConstructRewards;
import explicit.rewards.MCRewards;
import explicit.rewards.MDPRewards;
import explicit.rewards.Rewards;
import parser.ast.Expression;
import parser.ast.ExpressionAccumulation;
import parser.ast.ExpressionReward;
@ -77,57 +76,28 @@ public class AccumulationTransformation<M extends Model> implements ModelExpress
mc.getLog().println(" ... a simple expression.");
}
// Get the rewards and build the product
switch(originalModel.getModelType()) {
case DTMC:
Vector<MCRewards> dtmc_rewards = new Vector<MCRewards>();
for (int i=0; i < accexp.getConstraint().getFactors().size(); i++) {
Object rewardIndex = accexp.getConstraint().getFactors().get(i).getFunction().getRewardIndex();
RewardStruct rewStruct = ExpressionReward.getRewardStructByIndexObject(rewardIndex, mc.modulesFile, originalModel.getConstantValues());
ConstructRewards constructRewards = new ConstructRewards();
constructRewards.allowNegativeRewards();
MCRewards dtmc_reward = constructRewards.buildMCRewardStructure((DTMC)originalModel, rewStruct, mc.getConstantValues());
dtmc_rewards.add(i,dtmc_reward);
}
mc.getLog().println(" [AT] performing product construction...");
if(accexp.hasRegularExpression()) {
product = (AccumulationProductRegular<M>) AccumulationProductRegular.generate((DTMC)originalModel, accexp, dtmc_rewards, mc, statesOfInterest);
} else if (accexp.hasBoundExpression()) {
product = (AccumulationProductCounting<M>) AccumulationProductCounting.generate((DTMC)originalModel, accexp, dtmc_rewards, mc, statesOfInterest);
} else {
throw new PrismException("Accumulation Expression has no valid monitor!");
}
break;
case MDP:
Vector<MDPRewards> mdp_rewards = new Vector<MDPRewards>();
// Get the rewards and build the product
Vector<Rewards> rewards = new Vector<Rewards>();
for (int i=0; i < accexp.getConstraint().getFactors().size(); i++) {
Object rewardIndex = accexp.getConstraint().getFactors().get(i).getFunction().getRewardIndex();
for (int i=0; i < accexp.getConstraint().getFactors().size(); i++) {
Object rewardIndex = accexp.getConstraint().getFactors().get(i).getFunction().getRewardIndex();
RewardStruct rewStruct = ExpressionReward.getRewardStructByIndexObject(rewardIndex, mc.modulesFile, originalModel.getConstantValues());
ConstructRewards constructRewards = new ConstructRewards();
constructRewards.allowNegativeRewards();
MDPRewards mdp_reward = constructRewards.buildMDPRewardStructure((MDP)originalModel, rewStruct, mc.getConstantValues());
mdp_rewards.add(i,mdp_reward);
}
mc.getLog().println(" [AT] performing product construction...");
if(accexp.hasRegularExpression()) {
product = (AccumulationProductRegular<M>) AccumulationProductRegular.generate((MDP)originalModel, accexp, mdp_rewards, mc, statesOfInterest);
} else if (accexp.hasBoundExpression()) {
product = (AccumulationProductCounting<M>) AccumulationProductCounting.generate((MDP)originalModel, accexp, mdp_rewards, mc, statesOfInterest);
} else {
throw new PrismException("Accumulation Expression has no valid monitor!");
}
mc.getLog().println(" [AT] finished product construction: " + product.getTransformedModel().getNumStates());
RewardStruct rewStruct = ExpressionReward.getRewardStructByIndexObject(rewardIndex, mc.modulesFile, originalModel.getConstantValues());
ConstructRewards constructRewards = new ConstructRewards();
constructRewards.allowNegativeRewards();
break;
default:
throw new PrismException("Can't handle weight functions for " + originalModel.getModelType());
Rewards dtmc_reward = constructRewards.buildRewardStructure(originalModel, rewStruct, mc.getConstantValues());
rewards.add(i,dtmc_reward);
}
if(accexp.hasRegularExpression()) {
product = (AccumulationProductRegular<M>) AccumulationProductRegular.generate(originalModel, accexp, rewards, mc, statesOfInterest);
} else if (accexp.hasBoundExpression()) {
product = (AccumulationProductCounting<M>) AccumulationProductCounting.generate(originalModel, accexp, rewards, mc, statesOfInterest);
} else {
throw new PrismException("Accumulation Expression has no valid monitor!");
}
mc.getLog().println(" [AT] finished product construction: " + product.getTransformedModel().getNumStates());
// Transform the model
mc.getLog().println(" [AT] getting the init/run/goal states: ");

Write Preview
Loading…
Cancel
Save