Sascha Wunderlich
10 years ago
committed by
Sascha Wunderlich
Sascha Wunderlich
24 changed files with 1982 additions and 13 deletions
-
53prism/src/explicit/AccumulationModelChecker.java
-
121prism/src/explicit/AccumulationProduct.java
-
301prism/src/explicit/AccumulationProductCounting.java
-
345prism/src/explicit/AccumulationProductRegular.java
-
104prism/src/explicit/AccumulationState.java
-
83prism/src/explicit/AccumulationTrack.java
-
68prism/src/explicit/AccumulationTracker.java
-
162prism/src/explicit/AccumulationTransformation.java
-
13prism/src/explicit/DTMCModelChecker.java
-
9prism/src/explicit/MDPModelChecker.java
-
10prism/src/explicit/ProbModelChecker.java
-
45prism/src/explicit/StoragePool.java
-
136prism/src/parser/PrismParser.jj
-
67prism/src/parser/ast/AccumulationConstraint.java
-
59prism/src/parser/ast/AccumulationFactor.java
-
36prism/src/parser/ast/AccumulationFunction.java
-
38prism/src/parser/ast/AccumulationSymbol.java
-
44prism/src/parser/ast/Expression.java
-
142prism/src/parser/ast/ExpressionAccumulation.java
-
36prism/src/parser/visitor/ASTTraverse.java
-
36prism/src/parser/visitor/ASTTraverseModify.java
-
3prism/src/parser/visitor/ASTVisitor.java
-
67prism/src/parser/visitor/ReplaceAccumulationExpression.java
-
17prism/src/prism/IntegerBound.java
@ -0,0 +1,53 @@ |
|||
package explicit; |
|||
|
|||
import java.util.ArrayList; |
|||
import java.util.BitSet; |
|||
|
|||
import parser.ast.Expression; |
|||
import parser.ast.ExpressionLabel; |
|||
import parser.ast.ExpressionRegular; |
|||
import parser.type.TypeBool; |
|||
import prism.PrismComponent; |
|||
import prism.PrismException; |
|||
|
|||
public class AccumulationModelChecker extends PrismComponent { |
|||
public Expression checkMaximalStateFormulas(ProbModelChecker mc, Model model, Expression expr, ArrayList<BitSet> labelBS) |
|||
throws PrismException |
|||
{ |
|||
// This is basically copied from DM |
|||
// A state formula |
|||
if (expr.getType() instanceof TypeBool) { |
|||
// Model check |
|||
StateValues sv = mc.checkExpression(model, expr, null); |
|||
BitSet bs = sv.getBitSet(); |
|||
// Detect special cases (true, false) for optimisation |
|||
if (bs.isEmpty()) { |
|||
return Expression.False(); |
|||
} |
|||
if (bs.cardinality() == model.getNumStates()) { |
|||
return Expression.True(); |
|||
} |
|||
// See if we already have an identical result |
|||
// (in which case, reuse it) |
|||
int i = labelBS.indexOf(bs); |
|||
if (i != -1) { |
|||
sv.clear(); |
|||
return new ExpressionLabel("L" + i); |
|||
} |
|||
// Otherwise, add result to list, return new label |
|||
labelBS.add(bs); |
|||
return new ExpressionLabel("L" + (labelBS.size() - 1)); |
|||
} |
|||
// A path formula (recurse, modify, return) |
|||
else if (expr instanceof ExpressionRegular) { |
|||
ExpressionRegular reg = (ExpressionRegular)expr; |
|||
if(reg.getOperand1() != null) { |
|||
reg.setOperand1(checkMaximalStateFormulas(mc, model, reg.getOperand1(), labelBS)); |
|||
} |
|||
if(reg.getOperand2() != null) { |
|||
reg.setOperand2(checkMaximalStateFormulas(mc, model, reg.getOperand2(), labelBS)); |
|||
} |
|||
} |
|||
return expr; |
|||
} |
|||
} |
|||
@ -0,0 +1,121 @@ |
|||
package explicit; |
|||
|
|||
import java.util.ArrayList; |
|||
import java.util.BitSet; |
|||
import java.util.Iterator; |
|||
import java.util.Map; |
|||
|
|||
import prism.PrismException; |
|||
import prism.PrismFileLog; |
|||
import prism.PrismLog; |
|||
|
|||
/** |
|||
* An AccumulationProduct has ProductStates, where the first component is the |
|||
* stateId in the original model, and the second component is the index of an |
|||
* AccumulationTracker. |
|||
* |
|||
* @author Sascha Wunderlich |
|||
* |
|||
* @param <M> |
|||
*/ |
|||
|
|||
public abstract class AccumulationProduct<M extends Model,Component> extends ProductWithProductStates<M> |
|||
{ |
|||
final StoragePool<AccumulationTracker<Component>> trackers; |
|||
final StoragePool<AccumulationState> accStates; |
|||
|
|||
final BitSet goodStates; |
|||
|
|||
final ArrayList<BitSet> labels; |
|||
|
|||
int numberOfTracks; |
|||
int numberOfWeights; |
|||
|
|||
public AccumulationProduct(M originalModel) { |
|||
super(originalModel); |
|||
trackers = new StoragePool<>(); |
|||
accStates = new StoragePool<>(); |
|||
|
|||
goodStates = new BitSet(); |
|||
labels = new ArrayList<BitSet>(); |
|||
} |
|||
|
|||
public BitSet getGoodStates() { |
|||
return goodStates; |
|||
} |
|||
|
|||
public int getNumberOfTracks() { |
|||
return numberOfTracks; |
|||
} |
|||
|
|||
public void exportToDotFile(String filename) throws PrismException { |
|||
try (PrismFileLog log = PrismFileLog.create(filename)) { |
|||
exportToDotFile(log); |
|||
} |
|||
} |
|||
|
|||
public void exportToDotFile(PrismLog out) { |
|||
out.print(toDot()); |
|||
} |
|||
|
|||
public String quoteForDot(String original) { |
|||
String result = original; |
|||
result = result.replaceAll("&", "&"); |
|||
result = result.replaceAll("<", "<"); |
|||
result = result.replaceAll(">", ">"); |
|||
return result; |
|||
} |
|||
|
|||
public String toDot() { |
|||
StringBuffer result = new StringBuffer(); |
|||
|
|||
result.append("digraph " + originalModel.getModelType() + " {\n"); |
|||
|
|||
for(int i = 0; i < prod_states.size(); i++) { |
|||
ProductState fromState = prod_states.get(i); |
|||
AccumulationState accState = accStates.getById(fromState.getSecondState()); |
|||
AccumulationTracker<Component> tracker = trackers.getById(accState.getTrackerId()); |
|||
result.append("" |
|||
+ i |
|||
+ "[shape=box, color=black" |
|||
+ " label= < <TABLE BO8RDER=\"0\">" |
|||
+ "<TR>" |
|||
+ "<TD>" + i + "=" + fromState + "</TD>" |
|||
+ "</TR><TR>" |
|||
+ "<TD>" + accState + "</TD>" |
|||
+ "</TR><TR>" |
|||
+ "<TD>\"" + quoteForDot(tracker.toString()) + "\"</TD>" |
|||
+ "</TR>" |
|||
+ " </TABLE> >]\n"); |
|||
|
|||
switch(productModel.getModelType()) { |
|||
case DTMC: |
|||
DTMCExplicit castDTMC = (DTMCExplicit)productModel; |
|||
Iterator<Map.Entry<Integer, Double>> dtmcIter = castDTMC.getTransitionsIterator(i); |
|||
while (dtmcIter.hasNext()) { |
|||
Map.Entry<Integer, Double> e = dtmcIter.next(); |
|||
result.append(i + " -> " + e.getKey() + " [ label=\""); |
|||
result.append(e.getValue() + "\" ];\n"); |
|||
} |
|||
break; |
|||
case MDP: |
|||
MDPExplicit castMDP = (MDPExplicit)productModel; |
|||
for(int c = 0; c < castMDP.getNumChoices(i); c++) { |
|||
Iterator<Map.Entry<Integer, Double>> mdpIter = castMDP.getTransitionsIterator(i, c); |
|||
while (mdpIter.hasNext()) { |
|||
Map.Entry<Integer, Double> e = mdpIter.next(); |
|||
result.append(i + " -> " + e.getKey() + " [ label=\""); |
|||
result.append(c + "," + e.getValue() + "\" ];\n"); |
|||
} |
|||
} |
|||
break; |
|||
default: |
|||
break; |
|||
} |
|||
} |
|||
|
|||
result.append("}"); |
|||
|
|||
return result.toString(); |
|||
} |
|||
} |
|||
@ -0,0 +1,301 @@ |
|||
package explicit; |
|||
|
|||
import java.util.ArrayList; |
|||
import java.util.BitSet; |
|||
import java.util.Vector; |
|||
|
|||
import explicit.rewards.MCRewards; |
|||
import explicit.rewards.MDPRewards; |
|||
import explicit.rewards.Rewards; |
|||
import parser.ast.AccumulationFactor; |
|||
import parser.ast.ExpressionAccumulation; |
|||
import prism.IntegerBound; |
|||
import prism.PrismException; |
|||
|
|||
/** |
|||
* An AccumulationProduct has ProductStates, where the first component is the |
|||
* stateId in the original model, and the second component is the index of an |
|||
* AccumulationTracker. |
|||
* |
|||
* @author Sascha Wunderlich |
|||
* |
|||
* @param <M> |
|||
*/ |
|||
|
|||
public class AccumulationProductCounting<M extends Model> extends AccumulationProduct<M,Integer> |
|||
{ |
|||
|
|||
public AccumulationProductCounting(M originalModel) { |
|||
super(originalModel); |
|||
} |
|||
|
|||
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 |
|||
result.createAuxData(graph, accexp, rewards, mc); |
|||
|
|||
// Build an operator |
|||
class AccumulationDTMCProductOperator implements DTMCProductOperator |
|||
{ |
|||
@Override |
|||
public ProductState getInitialState(Integer dtmc_state) |
|||
throws PrismException { |
|||
int initialAccStateId = result.createInitialStateId(rewards.size()); |
|||
return new ProductState(dtmc_state, initialAccStateId); |
|||
} |
|||
|
|||
@Override |
|||
public ProductState getSuccessor(ProductState from_state, |
|||
Integer dtmc_to_state) throws PrismException { |
|||
// Get the current accumulation state |
|||
AccumulationState from_accstate = result.accStates.getById(from_state.getSecondState()); |
|||
|
|||
// Get step weights |
|||
double[] weights = new double[rewards.size()]; |
|||
|
|||
for (int i=0; i < rewards.size(); i++) { |
|||
weights[i] = rewards.get(i).getStateReward(from_state.getFirstState()); |
|||
} |
|||
|
|||
// Update accumulation product state, store it and get its ID. |
|||
AccumulationState to_accproduct = result.updateAccumulationState(from_state.getFirstState(), from_accstate, accexp, weights, mc); |
|||
int to_accproduct_id = result.accStates.findOrAdd(to_accproduct); |
|||
|
|||
return new ProductState(dtmc_to_state, to_accproduct_id); |
|||
} |
|||
|
|||
@Override |
|||
public void notify(ProductState state, Integer index) |
|||
throws PrismException { |
|||
AccumulationState accState = result.accStates.getById(state.getSecondState()); |
|||
if (result.isGoodAccState(accState, accexp, mc)) { |
|||
result.goodStates.set(index); |
|||
} |
|||
} |
|||
|
|||
@Override |
|||
public void finish() throws PrismException { |
|||
// Do nothing |
|||
} |
|||
|
|||
@Override |
|||
public DTMC getGraph() { |
|||
return graph; |
|||
} |
|||
} |
|||
|
|||
// Apply the operator |
|||
AccumulationDTMCProductOperator op = new AccumulationDTMCProductOperator(); |
|||
ProductWithProductStates.generate(op, result, statesOfInterest); |
|||
|
|||
return result; |
|||
} |
|||
|
|||
public static AccumulationProductCounting<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 AccumulationProductCounting<MDP> result = new AccumulationProductCounting<MDP>(graph); |
|||
|
|||
// Create auxiliary data |
|||
result.createAuxData(graph, accexp, rewards, mc); |
|||
|
|||
class AccumulationMDPProductOperator implements MDPProductOperator |
|||
{ |
|||
|
|||
@Override |
|||
public ProductState getInitialState(final Integer MDP_state) |
|||
throws PrismException { |
|||
int initialAccStateId = result.createInitialStateId(rewards.size()); |
|||
return new ProductState(MDP_state, initialAccStateId); |
|||
} |
|||
|
|||
@Override |
|||
public ProductState getSuccessor(final ProductState from_state, |
|||
final int choice_i, final Integer mdp_to_state) throws PrismException { |
|||
// Get the current accumulation state |
|||
AccumulationState from_accstate = result.accStates.getById(from_state.getSecondState()); |
|||
|
|||
// Get step weights |
|||
// THIS IS DIFFERENT FROM ABOVE! |
|||
double[] weights = new double[rewards.size()]; |
|||
|
|||
for (int i=0; i < rewards.size(); i++) { |
|||
double currentWeight = rewards.get(i).getStateReward(from_state.getFirstState()); |
|||
currentWeight += rewards.get(i).getTransitionReward(from_state.getFirstState(), choice_i); |
|||
weights[i] = currentWeight; |
|||
} |
|||
|
|||
// Update accumulation product state, store it and get its ID. |
|||
AccumulationState to_accproduct = result.updateAccumulationState(from_state.getFirstState(), from_accstate, accexp, weights, mc); |
|||
int to_accproduct_id = result.accStates.findOrAdd(to_accproduct); |
|||
return new ProductState(mdp_to_state, to_accproduct_id); |
|||
} |
|||
|
|||
@Override |
|||
public void notify(final ProductState state, final Integer index) |
|||
throws PrismException { |
|||
AccumulationState accState = result.accStates.getById(state.getSecondState()); |
|||
if (result.isGoodAccState(accState, accexp, mc)) { |
|||
result.goodStates.set(index); |
|||
} |
|||
} |
|||
|
|||
@Override |
|||
public void finish() throws PrismException { |
|||
// Do nothing |
|||
mc.getLog().println("."); |
|||
} |
|||
|
|||
@Override |
|||
public MDP getGraph() { |
|||
return graph; |
|||
} |
|||
} |
|||
|
|||
AccumulationMDPProductOperator op = new AccumulationMDPProductOperator(); |
|||
ProductWithProductStates.generate(op, result, statesOfInterest); |
|||
return result; |
|||
} |
|||
|
|||
private boolean isFinalTrack(final AccumulationTrack<Integer> track, final ExpressionAccumulation accexp, final ProbModelChecker mc) |
|||
throws PrismException { |
|||
boolean isFinal = false; |
|||
if ( track != null ) { |
|||
IntegerBound stepBound = IntegerBound.fromTemporalOperatorBound(accexp.getBoundExpression(), mc.getConstantValues(), true); |
|||
isFinal = stepBound.isInBounds(track.getComponent()); |
|||
} |
|||
return isFinal; |
|||
} |
|||
|
|||
private boolean isGoodAccState(final AccumulationState state, final ExpressionAccumulation accexp, final ProbModelChecker mc) |
|||
throws PrismException { |
|||
return state.hasGoodTrack(); |
|||
} |
|||
|
|||
private boolean isGoodTrack(final AccumulationTrack<Integer> track, final ExpressionAccumulation accexp, final ProbModelChecker mc) |
|||
throws PrismException { |
|||
// Only final tracks can be good |
|||
if (!isFinalTrack(track,accexp,mc)) { return false; } |
|||
boolean isGood = false; |
|||
|
|||
// Collect the weight linear combination, factor*weight+... |
|||
int lhs = 0; |
|||
int factorNr = 0; |
|||
for (AccumulationFactor factor : accexp.getConstraint().getFactors()) { |
|||
lhs += factor.getFactor().evaluateInt(mc.getConstantValues()) |
|||
* track.getWeight(factorNr); |
|||
} |
|||
|
|||
// Check the bound |
|||
IntegerBound rhs = IntegerBound.fromTemporalOperatorBound(accexp.getConstraint().getBound(), mc.getConstantValues(), true); |
|||
|
|||
// For DIA operators, we just check the bound. |
|||
// For BOX operators, we check the INVERTED bound. |
|||
switch(accexp.getSymbol()) { |
|||
case ACCBOXMINUS: |
|||
case ACCBOXPLUS: |
|||
if (!rhs.isInBounds(lhs)) { |
|||
isGood = true; |
|||
} |
|||
break; |
|||
case ACCDIAMINUS: |
|||
case ACCDIAPLUS: |
|||
if (rhs.isInBounds(lhs)) { |
|||
isGood = true; |
|||
} |
|||
break; |
|||
default: |
|||
throw new RuntimeException("Oh boy!"); |
|||
} |
|||
if(isGood) {mc.getLog().print("+");} else {mc.getLog().print("-");} |
|||
return isGood; |
|||
} |
|||
|
|||
private AccumulationState updateAccumulationState(final int modelFromStateId, |
|||
final AccumulationState accstate, final ExpressionAccumulation accexp, |
|||
final double[] weights, final ProbModelChecker mc) throws PrismException { |
|||
// We have the current accumulation state, the current model id and the accumulation expression. |
|||
|
|||
// Get the old tracker and tracks. |
|||
AccumulationTracker<Integer> oldTracker = trackers.getById(accstate.getTrackerId()); |
|||
ArrayList<AccumulationTrack<Integer>> oldTracks = oldTracker.getTracks(); |
|||
|
|||
BitSet oldGoodTracks = accstate.getGoodTracks(); |
|||
BitSet newGoodTracks = (BitSet) oldGoodTracks.clone(); |
|||
|
|||
// This restart will be... |
|||
int newLastRestartNr = accstate.getNextRestartNr(); |
|||
mc.getLog().print(newLastRestartNr); |
|||
|
|||
// Build the new tracks. |
|||
ArrayList<AccumulationTrack<Integer>> newTracks = new ArrayList<>(); |
|||
|
|||
int trackNr = 0; |
|||
for(AccumulationTrack<Integer> oldTrack : oldTracks) { |
|||
AccumulationTrack<Integer> newTrack; |
|||
|
|||
// restart or advance |
|||
if(trackNr == newLastRestartNr) { |
|||
//assert oldTrack == null : "Track " + newLastRestartNr + " is not null!"; |
|||
newTrack = new AccumulationTrack<Integer>(numberOfWeights, 0); //TODO: off-by-one? |
|||
newGoodTracks.clear(trackNr); |
|||
} else if (oldTrack == null) { |
|||
newTrack = null; |
|||
} else { |
|||
assert oldTrack != null; |
|||
newTrack = updateTrackBounds(oldTrack, accexp, weights, mc); |
|||
} |
|||
|
|||
// check whether the track is good |
|||
if(!newGoodTracks.get(trackNr)) { |
|||
newGoodTracks.set(trackNr, isGoodTrack(newTrack, accexp, mc)); |
|||
} |
|||
|
|||
newTracks.add(newTrack); |
|||
trackNr++; |
|||
} |
|||
|
|||
AccumulationTracker<Integer> newTracker = new AccumulationTracker<>(newTracks); |
|||
|
|||
|
|||
int newTrackerId = trackers.findOrAdd(newTracker); |
|||
|
|||
return new AccumulationState(newTrackerId, newLastRestartNr, numberOfTracks, newGoodTracks); |
|||
} |
|||
|
|||
private AccumulationTrack<Integer> updateTrackBounds(final AccumulationTrack<Integer> track, |
|||
final ExpressionAccumulation accexp, final double[] weights, final StateModelChecker mc) throws PrismException { |
|||
int currentStep = track.getComponent(); |
|||
int maxStep = IntegerBound.fromTemporalOperatorBound(accexp.getBoundExpression(), mc.getConstantValues(), true).getHighestInteger(); |
|||
|
|||
// If we are done, return null-Track |
|||
if (currentStep >= maxStep) { return null; } |
|||
|
|||
// Otherwise, we update the weights and increase the step. |
|||
double[] newweights = new double[weights.length]; |
|||
for (int i = 0; i < weights.length; i++) { |
|||
newweights[i] = weights[i] + track.getWeights()[i]; |
|||
} |
|||
|
|||
return new AccumulationTrack<Integer>(newweights, currentStep+1); |
|||
} |
|||
|
|||
protected int createInitialStateId(final int numberOfRewards) { |
|||
// The initial active track is the first one, all tracks are non-good by default |
|||
int initialActiveTrack = 0; |
|||
BitSet initialGoodTracks = new BitSet(); |
|||
|
|||
// Generate the initial tracker and product state |
|||
AccumulationTracker<Integer> initialTracker = new AccumulationTracker<>(numberOfTracks, numberOfRewards, 0); |
|||
int initialTrackerId = trackers.findOrAdd(initialTracker); |
|||
AccumulationState initialAccState = new AccumulationState(initialTrackerId, initialActiveTrack, numberOfTracks, initialGoodTracks); |
|||
int initialAccStateId = accStates.findOrAdd(initialAccState); |
|||
|
|||
return initialAccStateId; |
|||
} |
|||
|
|||
protected void createAuxData(final Model graph, final ExpressionAccumulation accexp, |
|||
final Vector<? extends Rewards> rewards, final ProbModelChecker mc) throws PrismException { |
|||
numberOfTracks = IntegerBound.fromTemporalOperatorBound(accexp.getBoundExpression(), mc.getConstantValues(), true).getHighestInteger()+1; |
|||
numberOfWeights = rewards.size(); |
|||
} |
|||
} |
|||
@ -0,0 +1,345 @@ |
|||
package explicit; |
|||
|
|||
import java.util.ArrayList; |
|||
import java.util.BitSet; |
|||
import java.util.Vector; |
|||
|
|||
import automata.finite.DeterministicFiniteAutomaton; |
|||
import automata.finite.EdgeLabel; |
|||
import automata.finite.NondeterministicFiniteAutomaton; |
|||
import automata.finite.State; |
|||
import explicit.rewards.MCRewards; |
|||
import explicit.rewards.MDPRewards; |
|||
import parser.ast.AccumulationFactor; |
|||
import parser.ast.ExpressionAccumulation; |
|||
import parser.ast.ExpressionRegular; |
|||
import prism.IntegerBound; |
|||
import prism.PrismException; |
|||
|
|||
/** |
|||
* An AccumulationProduct has ProductStates, where the first component is the |
|||
* stateId in the original model, and the second component is the index of an |
|||
* AccumulationTracker. |
|||
* |
|||
* @author Sascha Wunderlich |
|||
* |
|||
* @param <M> |
|||
*/ |
|||
|
|||
public class AccumulationProductRegular<M extends Model> extends AccumulationProduct<M,State> |
|||
{ |
|||
DeterministicFiniteAutomaton<String> automaton; |
|||
|
|||
public AccumulationProductRegular(M originalModel) { |
|||
super(originalModel); |
|||
} |
|||
|
|||
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 |
|||
result.createAuxData(graph, accexp, mc); |
|||
|
|||
// Build an operator |
|||
class AccumulationDTMCProductOperator implements DTMCProductOperator |
|||
{ |
|||
@Override |
|||
public ProductState getInitialState(Integer dtmc_state) |
|||
throws PrismException { |
|||
int initialAccStateId = result.createInitialStateId(rewards.size()); |
|||
return new ProductState(dtmc_state, initialAccStateId); |
|||
} |
|||
|
|||
@Override |
|||
public ProductState getSuccessor(ProductState from_state, |
|||
Integer dtmc_to_state) throws PrismException { |
|||
// Get the current accumulation state |
|||
AccumulationState from_accstate = result.accStates.getById(from_state.getSecondState()); |
|||
|
|||
// Get step weights |
|||
double[] weights = new double[rewards.size()]; |
|||
|
|||
for (int i=0; i < rewards.size(); i++) { |
|||
weights[i] = rewards.get(i).getStateReward(from_state.getFirstState()); |
|||
} |
|||
|
|||
// Update accumulation product state, store it and get its ID. |
|||
AccumulationState to_accproduct = result.updateAccumulationState(from_state.getFirstState(), from_accstate, accexp, weights, mc); |
|||
int to_accproduct_id = result.accStates.findOrAdd(to_accproduct); |
|||
|
|||
return new ProductState(dtmc_to_state, to_accproduct_id); |
|||
} |
|||
|
|||
@Override |
|||
public void notify(ProductState state, Integer index) |
|||
throws PrismException { |
|||
AccumulationState accState = result.accStates.getById(state.getSecondState()); |
|||
if (result.isGoodAccState(accState, accexp, mc)) { |
|||
result.goodStates.set(index); |
|||
} |
|||
} |
|||
|
|||
@Override |
|||
public void finish() throws PrismException { |
|||
// Do nothing |
|||
} |
|||
|
|||
@Override |
|||
public DTMC getGraph() { |
|||
return graph; |
|||
} |
|||
} |
|||
|
|||
// Apply the operator |
|||
AccumulationDTMCProductOperator op = new AccumulationDTMCProductOperator(); |
|||
ProductWithProductStates.generate(op, result, statesOfInterest); |
|||
|
|||
return result; |
|||
} |
|||
|
|||
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 |
|||
result.createAuxData(graph, accexp, mc); |
|||
|
|||
class AccumulationMDPProductOperator implements MDPProductOperator |
|||
{ |
|||
|
|||
@Override |
|||
public ProductState getInitialState(Integer MDP_state) |
|||
throws PrismException { |
|||
int initialAccStateId = result.createInitialStateId(rewards.size()); |
|||
return new ProductState(MDP_state, initialAccStateId); |
|||
} |
|||
|
|||
@Override |
|||
public ProductState getSuccessor(ProductState from_state, |
|||
int choice_i, Integer mdp_to_state) throws PrismException { |
|||
// Get the current accumulation state |
|||
AccumulationState from_accstate = result.accStates.getById(from_state.getSecondState()); |
|||
|
|||
// Get step weights |
|||
// THIS IS DIFFERENT FROM ABOVE! |
|||
double[] weights = new double[rewards.size()]; |
|||
|
|||
for (int i=0; i < rewards.size(); i++) { |
|||
double currentWeight = rewards.get(i).getStateReward(from_state.getFirstState()); |
|||
currentWeight += rewards.get(i).getTransitionReward(from_state.getFirstState(), choice_i); |
|||
weights[i] = currentWeight; |
|||
} |
|||
|
|||
// Update accumulation product state, store it and get its ID. |
|||
AccumulationState to_accproduct = result.updateAccumulationState(from_state.getFirstState(), from_accstate, accexp, weights, mc); |
|||
int to_accproduct_id = result.accStates.findOrAdd(to_accproduct); |
|||
|
|||
return new ProductState(mdp_to_state, to_accproduct_id); |
|||
} |
|||
|
|||
@Override |
|||
public void notify(ProductState state, Integer index) |
|||
throws PrismException { |
|||
AccumulationState accState = result.accStates.getById(state.getSecondState()); |
|||
if (result.isGoodAccState(accState, accexp, mc)) { |
|||
result.goodStates.set(index); |
|||
} |
|||
} |
|||
|
|||
@Override |
|||
public void finish() throws PrismException { |
|||
// Do nothing |
|||
|
|||
} |
|||
|
|||
@Override |
|||
public MDP getGraph() { |
|||
return graph; |
|||
} |
|||
} |
|||
|
|||
AccumulationMDPProductOperator op = new AccumulationMDPProductOperator(); |
|||
ProductWithProductStates.generate(op, result, statesOfInterest); |
|||
return result; |
|||
} |
|||
|
|||
private boolean isFinalTrack(AccumulationTrack<State> track, ExpressionAccumulation accexp, ProbModelChecker mc) throws PrismException { |
|||
boolean isFinal = false; |
|||
if ( track != null ) { |
|||
isFinal = automaton.isAcceptingState(track.getComponent()); |
|||
} |
|||
|
|||
return isFinal; |
|||
} |
|||
|
|||
private boolean isGoodAccState(AccumulationState state, ExpressionAccumulation accexp, ProbModelChecker mc) throws PrismException { |
|||
//TODO: fill me! |
|||
return false; |
|||
} |
|||
|
|||
private boolean isGoodTrack(AccumulationTrack<State> track, ExpressionAccumulation accexp, ProbModelChecker mc) throws PrismException { |
|||
//System.out.println("Checking " + track + " for goodness..."); |
|||
// Only final tracks can be good |
|||
if (!isFinalTrack(track,accexp,mc)) { return false; } |
|||
boolean isGood = false; |
|||
|
|||
//System.out.println("Final: " + track); |
|||
|
|||
// Collect the weight linear combination, factor*weight+... |
|||
int lhs = 0; |
|||
int factorNr = 0; |
|||
for (AccumulationFactor factor : accexp.getConstraint().getFactors()) { |
|||
lhs += factor.getFactor().evaluateInt(mc.getConstantValues()) |
|||
* track.getWeight(factorNr); |
|||
} |
|||
|
|||
// Check the bound |
|||
IntegerBound rhs = IntegerBound.fromTemporalOperatorBound(accexp.getConstraint().getBound(), mc.getConstantValues(), true); |
|||
|
|||
// For DIA operators, we just check the bound. |
|||
// For BOX operators, we check the INVERTED bound. |
|||
switch(accexp.getSymbol()) { |
|||
case ACCBOXMINUS: |
|||
case ACCBOXPLUS: |
|||
if (!rhs.isInBounds(lhs)) { |
|||
isGood = true; |
|||
} |
|||
break; |
|||
case ACCDIAMINUS: |
|||
case ACCDIAPLUS: |
|||
if (rhs.isInBounds(lhs)) { |
|||
isGood = true; |
|||
} |
|||
break; |
|||
default: |
|||
throw new RuntimeException("Oh boy!"); |
|||
} |
|||
|
|||
//System.out.println("Good? " + isGood); |
|||
|
|||
return isGood; |
|||
} |
|||
|
|||
private AccumulationState updateAccumulationState(final int modelFromStateId, |
|||
final AccumulationState accstate, final ExpressionAccumulation accexp, |
|||
final double[] weights, final ProbModelChecker mc) throws PrismException { |
|||
// We have the current accumulation state, the current model id and the accumulation expression. |
|||
|
|||
// Get the old tracker and tracks. |
|||
AccumulationTracker<State> oldTracker = trackers.getById(accstate.getTrackerId()); |
|||
ArrayList<AccumulationTrack<State>> oldTracks = oldTracker.getTracks(); |
|||
|
|||
BitSet oldGoodTracks = accstate.getGoodTracks(); |
|||
BitSet newGoodTracks = (BitSet) oldGoodTracks.clone(); |
|||
|
|||
// This restart will be... |
|||
int newLastRestartNr = accstate.getNextRestartNr(); |
|||
mc.getLog().print(newLastRestartNr); |
|||
|
|||
// Build the new tracks. |
|||
ArrayList<AccumulationTrack<State>> newTracks = new ArrayList<>(); |
|||
|
|||
int trackNr = 0; |
|||
for(AccumulationTrack<State> oldTrack : oldTracks) { |
|||
AccumulationTrack<State> newTrack; |
|||
|
|||
// restart or advance |
|||
if(trackNr == newLastRestartNr) { |
|||
//assert oldTrack == null : "Track " + newLastRestartNr + " is not null!"; |
|||
newTrack = new AccumulationTrack<State>(numberOfWeights, automaton.getInitialState()); //TODO: off-by-one? |
|||
newGoodTracks.clear(trackNr); |
|||
} else if (oldTrack == null) { |
|||
newTrack = null; |
|||
} else { |
|||
assert oldTrack != null; |
|||
newTrack = updateTrackRegular(modelFromStateId, oldTrack, accexp, weights, mc); |
|||
} |
|||
|
|||
// check whether the track is good |
|||
if(!newGoodTracks.get(trackNr)) { |
|||
newGoodTracks.set(trackNr, isGoodTrack(newTrack, accexp, mc)); |
|||
} |
|||
|
|||
newTracks.add(newTrack); |
|||
trackNr++; |
|||
} |
|||
|
|||
AccumulationTracker<State> newTracker = new AccumulationTracker<>(newTracks); |
|||
|
|||
|
|||
int newTrackerId = trackers.findOrAdd(newTracker); |
|||
|
|||
return new AccumulationState(newTrackerId, newLastRestartNr, numberOfTracks, newGoodTracks); |
|||
} |
|||
private AccumulationTrack<State> updateTrackRegular(Integer modelFromStateId, AccumulationTrack<State> track, ExpressionAccumulation accexp, double[] weights, StateModelChecker mc) { |
|||
State currentState = track.getComponent(); |
|||
|
|||
// Build EdgeLabel from labels. |
|||
// labels is a BitSet with labels L0,...,Ln |
|||
|
|||
ArrayList<String> edgeSymbols = new ArrayList<>(); |
|||
BitSet edgeValues = new BitSet(); |
|||
|
|||
for (int i=0; i < labels.size(); i++) { |
|||
// Each bitLabel contains one L |
|||
edgeSymbols.add(i, "L"+i); |
|||
if(labels.get(i).get(modelFromStateId)) { |
|||
edgeValues.set(i); |
|||
} |
|||
} |
|||
|
|||
EdgeLabel<String> edgeLabel = new EdgeLabel<>(edgeSymbols, edgeValues); |
|||
|
|||
State nextState = automaton.getSuccessor(currentState,edgeLabel); |
|||
//System.out.println("Successor of " + currentState + " via " + edgeLabel + ":" + nextState); |
|||
|
|||
// Undefined behavior, return the null-Track |
|||
if (nextState == null) { return null; } |
|||
|
|||
// If we have defined behavior, update the weights and get the new stateId. |
|||
double[] newweights = new double[weights.length]; |
|||
for (int i = 0; i < weights.length; i++) { |
|||
newweights[i] = weights[i] + track.getWeights()[i]; |
|||
} |
|||
|
|||
return new AccumulationTrack<State>(newweights, nextState); |
|||
} |
|||
|
|||
protected int createInitialStateId(int numberOfRewards) { |
|||
// Find the initial state id (0 or automaton state) |
|||
State initialState = automaton.getInitialState(); |
|||
|
|||
// The initial active track is the first one, all tracks are non-good by default |
|||
int initialActiveTrack = 0; |
|||
BitSet initialGoodTracks = new BitSet(); |
|||
|
|||
// Generate the initial track and product state |
|||
AccumulationTracker<State> initialTracker = new AccumulationTracker<>(numberOfTracks, numberOfRewards, initialState); |
|||
int initialTrackerId = trackers.findOrAdd(initialTracker); |
|||
AccumulationState initialAccState = new AccumulationState(initialTrackerId, initialActiveTrack, numberOfTracks, initialGoodTracks); |
|||
int initialAccStateId = accStates.findOrAdd(initialAccState); |
|||
|
|||
return initialAccStateId; |
|||
} |
|||
|
|||
public void createAuxData(final Model graph, final ExpressionAccumulation accexp, final ProbModelChecker mc) throws PrismException { |
|||
mc.getLog().println(" [AP] generating aux data for " + graph + "\n and " + accexp); |
|||
// Build labels and DFA |
|||
AccumulationModelChecker accMc = new AccumulationModelChecker(); |
|||
ExpressionRegular reg = (ExpressionRegular)accMc.checkMaximalStateFormulas(mc, graph, accexp.getRegularExpression(), labels); |
|||
|
|||
// Create and store the actual DFA |
|||
NondeterministicFiniteAutomaton<String> nfa = NondeterministicFiniteAutomaton.fromExpressionRegular(reg); |
|||
//System.out.println(nfa.toDot()); |
|||
|
|||
automaton = nfa.determinize(); |
|||
automaton.trim(); // This should remove cycles. |
|||
|
|||
System.out.println(nfa.toDot()); |
|||
|
|||
if (!automaton.isAcyclic()) { |
|||
throw new PrismException("Cannot handle cyclic automata!"); |
|||
} |
|||
|
|||
numberOfTracks = automaton.getLongestPathLength(); |
|||
} |
|||
} |
|||
@ -0,0 +1,104 @@ |
|||
package explicit; |
|||
|
|||
import java.util.BitSet; |
|||
|
|||
/** |
|||
* An AccumulationState contains a reference to an AccumulationTracker, a BitSet |
|||
* of successful tracks goodTracks, a pointer to the latest restart and the |
|||
* numberOfTracks in the tracker. |
|||
* |
|||
* @author Sascha Wunderlich |
|||
* |
|||
*/ |
|||
public class AccumulationState { |
|||
final int trackerId; |
|||
|
|||
final BitSet goodTracks; |
|||
|
|||
int lastRestartNr; |
|||
int numberOfTracks; |
|||
|
|||
public AccumulationState(int trackerId, int lastRestartNr, int numberOfTracks, |
|||
BitSet goodTracks) { |
|||
super(); |
|||
this.trackerId = trackerId; |
|||
this.lastRestartNr = lastRestartNr; |
|||
this.numberOfTracks = numberOfTracks; |
|||
this.goodTracks = goodTracks; |
|||
} |
|||
|
|||
public int getTrackerId() { |
|||
return trackerId; |
|||
} |
|||
|
|||
public int getLastRestartNr() { |
|||
return lastRestartNr; |
|||
} |
|||
|
|||
public void setLastRestartNr(int lastRestartNr) { |
|||
this.lastRestartNr = lastRestartNr; |
|||
} |
|||
|
|||
public BitSet getGoodTracks() { |
|||
return goodTracks; |
|||
} |
|||
|
|||
public boolean isGoodTrack(int trackNr) { |
|||
return goodTracks.get(trackNr); |
|||
} |
|||
|
|||
public boolean hasGoodTrack() { |
|||
return !goodTracks.isEmpty(); |
|||
} |
|||
|
|||
public int getNextRestartNr() { |
|||
return (lastRestartNr + 1) % numberOfTracks; |
|||
} |
|||
|
|||
public void advance() { |
|||
lastRestartNr = getNextRestartNr(); |
|||
} |
|||
|
|||
@Override |
|||
public int hashCode() { |
|||
final int prime = 31; |
|||
int result = 1; |
|||
result = prime * result + ((goodTracks == null) ? 0 : goodTracks.hashCode()); |
|||
result = prime * result + lastRestartNr; |
|||
result = prime * result + trackerId; |
|||
return result; |
|||
} |
|||
|
|||
@Override |
|||
public boolean equals(Object obj) { |
|||
if (this == obj) |
|||
return true; |
|||
if (obj == null) |
|||
return false; |
|||
if (getClass() != obj.getClass()) |
|||
return false; |
|||
AccumulationState other = (AccumulationState) obj; |
|||
if (goodTracks == null) { |
|||
if (other.goodTracks != null) |
|||
return false; |
|||
} else if (!goodTracks.equals(other.goodTracks)) |
|||
return false; |
|||
if (lastRestartNr != other.lastRestartNr) |
|||
return false; |
|||
if (trackerId != other.trackerId) |
|||
return false; |
|||
return true; |
|||
} |
|||
|
|||
@Override |
|||
public String toString() { |
|||
StringBuffer result = new StringBuffer(); |
|||
result.append("S"); |
|||
|
|||
result.append(trackerId); |
|||
result.append(goodTracks); |
|||
|
|||
return result.toString(); |
|||
} |
|||
|
|||
} |
|||
@ -0,0 +1,83 @@ |
|||
package explicit; |
|||
|
|||
import java.util.Arrays; |
|||
|
|||
/** |
|||
* An AccumulationTrack contains a double array of weights |
|||
* and a Component representing the current progress of the accumulation window. |
|||
* @author Sascha Wunderlich |
|||
* |
|||
* @param <Component> |
|||
*/ |
|||
public class AccumulationTrack<Component> { |
|||
final private double[] weights; |
|||
final private Component component; |
|||
|
|||
public AccumulationTrack(int numberOfWeights, Component component) { |
|||
weights = new double[numberOfWeights]; |
|||
for (int i=0; i<numberOfWeights; i++) { |
|||
weights[i] = 0.0; |
|||
} |
|||
|
|||
this.component = component; |
|||
} |
|||
|
|||
public AccumulationTrack(double[] weights, Component component) { |
|||
super(); |
|||
this.weights = weights; |
|||
this.component = component; |
|||
} |
|||
|
|||
public double[] getWeights() { |
|||
return weights; |
|||
} |
|||
|
|||
public Component getComponent() { |
|||
return component; |
|||
} |
|||
|
|||
public double getWeight(int index) { |
|||
return weights[index]; |
|||
} |
|||
|
|||
@Override |
|||
public int hashCode() { |
|||
final int prime = 31; |
|||
int result = 1; |
|||
result = prime * result + ((component == null) ? 0 : component.hashCode()); |
|||
result = prime * result + Arrays.hashCode(weights); |
|||
return result; |
|||
} |
|||
|
|||
@SuppressWarnings("rawtypes") |
|||
@Override |
|||
public boolean equals(Object obj) { |
|||
if (this == obj) |
|||
return true; |
|||
if (obj == null) |
|||
return false; |
|||
if (getClass() != obj.getClass()) |
|||
return false; |
|||
AccumulationTrack other = (AccumulationTrack) obj; |
|||
if (component == null) { |
|||
if (other.component != null) |
|||
return false; |
|||
} else if (!component.equals(other.component)) |
|||
return false; |
|||
if (!Arrays.equals(weights, other.weights)) |
|||
return false; |
|||
return true; |
|||
} |
|||
|
|||
@Override |
|||
public String toString() { |
|||
StringBuffer result = new StringBuffer(); |
|||
result.append("T"); |
|||
|
|||
result.append(Arrays.toString(weights)); |
|||
result.append("@"); |
|||
result.append(component); |
|||
|
|||
return result.toString(); |
|||
} |
|||
} |
|||
@ -0,0 +1,68 @@ |
|||
package explicit; |
|||
|
|||
import java.util.ArrayList; |
|||
|
|||
|
|||
/** |
|||
* An AccumulationTracker contains a Vector of AccumulationTracks. |
|||
* @author Sascha Wunderlich |
|||
* |
|||
* @param <Component> |
|||
*/ |
|||
public class AccumulationTracker<Component> { |
|||
final private ArrayList<AccumulationTrack<Component>> tracks; |
|||
|
|||
public AccumulationTracker(int numberOfTracks, int numberOfWeights, Component component) { |
|||
super(); |
|||
this.tracks = new ArrayList<AccumulationTrack<Component>>(numberOfTracks); |
|||
this.tracks.add(new AccumulationTrack<>(numberOfWeights, component)); |
|||
while(this.tracks.size() < numberOfTracks) { |
|||
this.tracks.add(null); |
|||
} |
|||
assert(this.tracks.size() == numberOfTracks); |
|||
} |
|||
|
|||
public AccumulationTracker(ArrayList<AccumulationTrack<Component>> tracks) { |
|||
super(); |
|||
this.tracks = new ArrayList<AccumulationTrack<Component>>(tracks.size()); |
|||
this.tracks.addAll(tracks); |
|||
} |
|||
|
|||
public ArrayList<AccumulationTrack<Component>> getTracks() { |
|||
return tracks; |
|||
} |
|||
|
|||
@Override |
|||
public int hashCode() { |
|||
final int prime = 31; |
|||
int result = 1; |
|||
result = prime * result + ((tracks == null) ? 0 : tracks.hashCode()); |
|||
return result; |
|||
} |
|||
|
|||
@SuppressWarnings("rawtypes") |
|||
@Override |
|||
public boolean equals(Object obj) { |
|||
if (this == obj) |
|||
return true; |
|||
if (obj == null) |
|||
return false; |
|||
if (getClass() != obj.getClass()) |
|||
return false; |
|||
AccumulationTracker other = (AccumulationTracker) obj; |
|||
if (tracks == null) { |
|||
if (other.tracks != null) |
|||
return false; |
|||
} else if (!tracks.equals(other.tracks)) |
|||
return false; |
|||
return true; |
|||
} |
|||
|
|||
|
|||
@Override |
|||
public String toString() { |
|||
StringBuffer result = new StringBuffer(); |
|||
result.append(tracks); |
|||
return result.toString(); |
|||
} |
|||
} |
|||
@ -0,0 +1,162 @@ |
|||
package explicit; |
|||
|
|||
import java.util.BitSet; |
|||
import java.util.Vector; |
|||
|
|||
import explicit.rewards.ConstructRewards; |
|||
import explicit.rewards.MCRewards; |
|||
import explicit.rewards.MDPRewards; |
|||
import parser.ast.Expression; |
|||
import parser.ast.ExpressionAccumulation; |
|||
import parser.ast.ExpressionReward; |
|||
import parser.ast.RewardStruct; |
|||
import parser.visitor.ReplaceAccumulationExpression; |
|||
import prism.PrismException; |
|||
|
|||
public class AccumulationTransformation<M extends Model> implements ModelExpressionTransformation<M, M> { |
|||
final private Expression originalExpression; |
|||
final private M originalModel; |
|||
final private BitSet statesOfInterest; |
|||
final ProbModelChecker mc; |
|||
|
|||
private Expression transformedExpression; |
|||
private AccumulationProduct<M,?> product; |
|||
|
|||
public AccumulationTransformation( |
|||
ProbModelChecker mc, |
|||
M originalModel, Expression expr, |
|||
BitSet statesOfInterest) throws PrismException{ |
|||
super(); |
|||
this.originalExpression = expr; |
|||
this.originalModel = originalModel; |
|||
this.mc = mc; |
|||
this.statesOfInterest = statesOfInterest; |
|||
doTransformation(); |
|||
} |
|||
|
|||
@Override |
|||
public M getOriginalModel() { |
|||
return originalModel; |
|||
} |
|||
@Override |
|||
public Expression getTransformedExpression() { |
|||
return transformedExpression; |
|||
} |
|||
@Override |
|||
public Expression getOriginalExpression() { |
|||
return originalExpression; |
|||
} |
|||
|
|||
@Override |
|||
public BitSet getTransformedStatesOfInterest() { |
|||
return product.getTransformedStatesOfInterest(); |
|||
} |
|||
|
|||
@Override |
|||
public M getTransformedModel() { |
|||
return product.getTransformedModel(); |
|||
} |
|||
@Override |
|||
public StateValues projectToOriginalModel(StateValues svTransformedModel) |
|||
throws PrismException { |
|||
return product.projectToOriginalModel(svTransformedModel); |
|||
} |
|||
|
|||
@SuppressWarnings("unchecked") |
|||
private void doTransformation() throws PrismException { |
|||
mc.getLog().println("Performing accumulation transformation..."); |
|||
// We work on a copy |
|||
transformedExpression = originalExpression.deepCopy(); |
|||
|
|||
// Get the first ExpressionAccumulation |
|||
ExpressionAccumulation accexp = transformedExpression.getFirstAccumulationExpression(); |
|||
|
|||
// 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>(); |
|||
|
|||
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!"); |
|||
} |
|||
|
|||
break; |
|||
default: |
|||
throw new PrismException("Can't handle weight functions for " + originalModel.getModelType()); |
|||
} |
|||
|
|||
// Transform the model |
|||
BitSet goodStates = product.getGoodStates(); |
|||
String label = gensymLabel("good", product.getTransformedModel()); |
|||
|
|||
((ModelExplicit)product.getTransformedModel()).addLabel(label, goodStates); |
|||
|
|||
//System.out.println("Good states " + goodStates); |
|||
|
|||
// Transform the expression |
|||
ReplaceAccumulationExpression replace = new ReplaceAccumulationExpression(accexp, label, product.getNumberOfTracks()); |
|||
transformedExpression = (Expression)transformedExpression.accept(replace); |
|||
mc.getLog().println("Transformed " + originalExpression.toString() + |
|||
"\n into " + transformedExpression.toString()); |
|||
//DEBUG: output dotfile |
|||
product.exportToDotFile("./out.dot"); |
|||
} |
|||
|
|||
public String gensymLabel(String prefix, Model model) { |
|||
int suffix = 0; |
|||
String label = prefix + "_" + suffix; |
|||
while(product.getTransformedModel().getLabels().contains(label)) { |
|||
suffix++; |
|||
label = prefix + "_" + suffix; |
|||
} |
|||
return label; |
|||
} |
|||
|
|||
@Override |
|||
public Integer mapToTransformedModel(int state) { |
|||
return product.mapToTransformedModel(state); |
|||
} |
|||
|
|||
@Override |
|||
public BitSet mapToTransformedModel(BitSet states) { |
|||
return product.mapToTransformedModel(states); |
|||
} |
|||
|
|||
} |
|||
@ -0,0 +1,45 @@ |
|||
package explicit; |
|||
|
|||
import java.util.ArrayList; |
|||
import java.util.HashMap; |
|||
import java.util.Iterator; |
|||
|
|||
/** |
|||
* A generic pool of things of type T, which can only grow. |
|||
* Uses an ArrayList and a HashMap internally. |
|||
* Provides a findOrAdd method. |
|||
* |
|||
* @author sw |
|||
* |
|||
* @param <T> |
|||
*/ |
|||
public class StoragePool<T> implements Iterable<T> { |
|||
final ArrayList<T> things; |
|||
final HashMap<T,Integer> thingIds; |
|||
|
|||
public StoragePool() { |
|||
things = new ArrayList<T>(); |
|||
thingIds = new HashMap<T,Integer>(); |
|||
} |
|||
|
|||
public T getById(final int thingId) { |
|||
return things.get(thingId); |
|||
} |
|||
|
|||
public int findOrAdd(final T thing) { |
|||
Integer thingId = thingIds.get(thing); |
|||
|
|||
if (thingId == null) { |
|||
thingId = things.size(); |
|||
things.add(thingId, thing); |
|||
thingIds.put(thing, thingId); |
|||
} |
|||
|
|||
return thingId; |
|||
} |
|||
|
|||
@Override |
|||
public Iterator<T> iterator() { |
|||
return things.iterator(); |
|||
} |
|||
} |
|||
@ -0,0 +1,67 @@ |
|||
package parser.ast; |
|||
|
|||
import java.util.ArrayList; |
|||
|
|||
import parser.visitor.ASTVisitor; |
|||
import prism.PrismLangException; |
|||
|
|||
public class AccumulationConstraint extends ASTElement { |
|||
|
|||
private ArrayList<AccumulationFactor> factors; |
|||
private TemporalOperatorBound bound; |
|||
|
|||
public AccumulationConstraint(ArrayList<AccumulationFactor> factors, |
|||
TemporalOperatorBound bound) { |
|||
this.factors = factors; |
|||
this.bound = bound; |
|||
} |
|||
|
|||
public ArrayList<AccumulationFactor> getFactors() { |
|||
return factors; |
|||
} |
|||
|
|||
public void setFactors(ArrayList<AccumulationFactor> factors) { |
|||
this.factors = factors; |
|||
} |
|||
|
|||
public TemporalOperatorBound getBound() { |
|||
return bound; |
|||
} |
|||
|
|||
public void setBound(TemporalOperatorBound bound) { |
|||
this.bound = bound; |
|||
} |
|||
|
|||
public AccumulationConstraint deepCopy() { |
|||
ArrayList<AccumulationFactor> factorscopy = new ArrayList<AccumulationFactor>(); |
|||
TemporalOperatorBound boundcopy = bound.deepCopy(); |
|||
|
|||
for (AccumulationFactor factor : factors) { |
|||
factorscopy.add(factor.deepCopy()); |
|||
} |
|||
|
|||
return new AccumulationConstraint(factorscopy,boundcopy); |
|||
} |
|||
|
|||
public String toString() |
|||
{ |
|||
boolean first = true; |
|||
String ret = ""; |
|||
|
|||
for (AccumulationFactor factor : factors) { |
|||
if (!first) ret += " + "; |
|||
first = false; |
|||
|
|||
ret += factor.toString(); |
|||
} |
|||
|
|||
ret += bound.toString(); |
|||
|
|||
return ret; |
|||
} |
|||
|
|||
@Override |
|||
public Object accept(ASTVisitor v) throws PrismLangException { |
|||
return v.visit(this); |
|||
} |
|||
} |
|||
@ -0,0 +1,59 @@ |
|||
package parser.ast; |
|||
|
|||
import parser.visitor.ASTVisitor; |
|||
import prism.PrismLangException; |
|||
import parser.type.TypeInt; |
|||
|
|||
public class AccumulationFactor extends ASTElement { |
|||
|
|||
private Expression factor; |
|||
private AccumulationFunction func; |
|||
|
|||
public AccumulationFactor(AccumulationFunction func) |
|||
{ |
|||
this(func, null); |
|||
} |
|||
|
|||
public AccumulationFactor(AccumulationFunction func, Expression factor) { |
|||
this.func = func; |
|||
if (factor != null) { |
|||
this.factor = factor; |
|||
} else { |
|||
this.factor = new ExpressionLiteral(TypeInt.getInstance(), 1); |
|||
} |
|||
} |
|||
|
|||
public Expression getFactor() { |
|||
return factor; |
|||
} |
|||
|
|||
public void setFactor(Expression factor) { |
|||
this.factor = factor; |
|||
} |
|||
|
|||
public AccumulationFunction getFunction() { |
|||
return func; |
|||
} |
|||
|
|||
public void setFunction(AccumulationFunction func) { |
|||
this.func = func; |
|||
} |
|||
|
|||
public AccumulationFactor deepCopy() { |
|||
return new AccumulationFactor(func,factor.deepCopy()); |
|||
} |
|||
|
|||
public String toString() |
|||
{ |
|||
if (factor != null) { |
|||
return factor.toString() + " * " + func.toString(); |
|||
} else { |
|||
return func.toString(); |
|||
} |
|||
} |
|||
|
|||
@Override |
|||
public Object accept(ASTVisitor v) throws PrismLangException { |
|||
return v.visit(this); |
|||
} |
|||
} |
|||
@ -0,0 +1,36 @@ |
|||
package parser.ast; |
|||
|
|||
public enum AccumulationFunction { |
|||
ACC_TIME, ACC_STEPS, ACC_REWARD; |
|||
|
|||
private Object rewardIndex = null; |
|||
|
|||
public Object getRewardIndex() { |
|||
return rewardIndex; |
|||
} |
|||
|
|||
public void setRewardIndex(Object index) { |
|||
rewardIndex = index; |
|||
} |
|||
|
|||
public String toString() { |
|||
switch(this) { |
|||
case ACC_REWARD: |
|||
return "reward" + indexString(); |
|||
case ACC_STEPS: |
|||
return "steps"; |
|||
case ACC_TIME: |
|||
return "time"; |
|||
default: |
|||
throw new RuntimeException("Unknown accumulation function"); |
|||
} |
|||
} |
|||
|
|||
private String indexString() { |
|||
if (rewardIndex == null) return ""; |
|||
|
|||
if (rewardIndex instanceof String) return "{\"" + rewardIndex + "\"}"; |
|||
else return "{" + rewardIndex.toString() + "}"; |
|||
|
|||
} |
|||
} |
|||
@ -0,0 +1,38 @@ |
|||
package parser.ast; |
|||
|
|||
public enum AccumulationSymbol { |
|||
ACCDIAPLUS, ACCDIAMINUS, ACCBOXPLUS, ACCBOXMINUS; |
|||
|
|||
public String toString() |
|||
{ |
|||
switch(this) { |
|||
case ACCBOXMINUS: |
|||
return "[-]"; |
|||
case ACCBOXPLUS: |
|||
return "[+]"; |
|||
case ACCDIAMINUS: |
|||
return "<->"; |
|||
case ACCDIAPLUS: |
|||
return "<+>"; |
|||
default: |
|||
throw new RuntimeException("Unknown accumulation symbol"); |
|||
} |
|||
} |
|||
|
|||
public boolean isDia() { |
|||
return (this == ACCDIAPLUS) || (this == ACCDIAMINUS); |
|||
} |
|||
|
|||
public boolean isBox() { |
|||
return (this == ACCBOXPLUS) || (this == ACCBOXMINUS); |
|||
} |
|||
|
|||
public boolean isMinus() { |
|||
return (this == ACCDIAMINUS) || (this == ACCBOXMINUS); |
|||
} |
|||
|
|||
public boolean isPlus() { |
|||
return (this == ACCDIAPLUS) || (this == ACCBOXPLUS); |
|||
} |
|||
|
|||
} |
|||
@ -0,0 +1,142 @@ |
|||
//============================================================================== |
|||
// |
|||
// Copyright (c) 2002- |
|||
// Authors: |
|||
// * Dave Parker <david.parker@comlab.ox.ac.uk> (University of Oxford, formerly 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 parser.ast; |
|||
|
|||
import parser.EvaluateContext; |
|||
import parser.type.TypePathBool; |
|||
import parser.visitor.ASTVisitor; |
|||
import prism.PrismLangException; |
|||
|
|||
public class ExpressionAccumulation extends Expression |
|||
{ |
|||
AccumulationSymbol symbol; |
|||
AccumulationConstraint constraint; |
|||
ExpressionRegular regexp; |
|||
TemporalOperatorBound bound; |
|||
|
|||
public ExpressionAccumulation(AccumulationSymbol symbol) { |
|||
this.symbol = symbol; |
|||
this.setType(TypePathBool.getInstance()); |
|||
} |
|||
|
|||
public boolean hasRegularExpression() { |
|||
return regexp != null; |
|||
} |
|||
|
|||
public boolean hasBoundExpression() { |
|||
return bound != null; |
|||
} |
|||
|
|||
public AccumulationSymbol getSymbol() { |
|||
return symbol; |
|||
} |
|||
public void setSymbol(AccumulationSymbol symbol) { |
|||
this.symbol = symbol; |
|||
} |
|||
public AccumulationConstraint getConstraint() { |
|||
return constraint; |
|||
} |
|||
public void setConstraint(AccumulationConstraint constraint) { |
|||
this.constraint = constraint; |
|||
} |
|||
public ExpressionRegular getRegularExpression() { |
|||
if ( hasRegularExpression() ) { return regexp; } |
|||
else throw new RuntimeException("getRegularExpression called without RegularExpression"); |
|||
} |
|||
public void setRegularExpression(ExpressionRegular regexp) { |
|||
this.bound = null; |
|||
this.regexp = regexp; |
|||
} |
|||
|
|||
public TemporalOperatorBound getBoundExpression() { |
|||
if ( hasBoundExpression() ) { return bound; } |
|||
else throw new RuntimeException("getBoundExpression called without BoundExpression"); |
|||
} |
|||
|
|||
public void setBoundExpression(TemporalOperatorBound bound) { |
|||
if ( bound.isDefaultBound() && bound.hasUpperBound() ) { |
|||
this.regexp= null; |
|||
this.bound = bound; |
|||
} else { |
|||
throw new RuntimeException("Bounds need to be upper and default."); |
|||
} |
|||
} |
|||
|
|||
// Add a toString |
|||
public String toString() { |
|||
String ret = ""; |
|||
ret += symbol.toString(); |
|||
if ( hasRegularExpression() ) { ret += "( Reg:" + regexp.toString() + ")"; } |
|||
else if ( hasBoundExpression() ) { ret += "(" + bound.toString() + ")"; } |
|||
else throw new RuntimeException("Cannot stringify AccumulationExpression without fragment bounds."); |
|||
ret += "(" + constraint.toString() + ")"; |
|||
return ret; |
|||
} |
|||
|
|||
@Override |
|||
public boolean isConstant() { |
|||
return false; |
|||
} |
|||
|
|||
@Override |
|||
public boolean isProposition() { |
|||
return false; |
|||
} |
|||
|
|||
@Override |
|||
public Object evaluate(EvaluateContext ec) throws PrismLangException { |
|||
return null; |
|||
} |
|||
|
|||
@Override |
|||
public boolean returnsSingleValue() { |
|||
return false; |
|||
} |
|||
|
|||
@Override |
|||
public Expression deepCopy() { |
|||
ExpressionAccumulation ret = new ExpressionAccumulation(this.getSymbol()); |
|||
|
|||
ret.setConstraint(this.getConstraint().deepCopy()); |
|||
if ( this.hasBoundExpression() ) { |
|||
ret.setBoundExpression(this.getBoundExpression().deepCopy()); |
|||
} |
|||
if ( this.hasRegularExpression() ) { |
|||
ret.setRegularExpression((ExpressionRegular) this.getRegularExpression().deepCopy()); |
|||
} |
|||
|
|||
return ret; |
|||
} |
|||
|
|||
@Override |
|||
public Object accept(ASTVisitor v) throws PrismLangException { |
|||
return v.visit(this); |
|||
} |
|||
|
|||
} |
|||
|
|||
//------------------------------------------------------------------------------ |
|||
@ -0,0 +1,67 @@ |
|||
package parser.visitor; |
|||
|
|||
import parser.ast.AccumulationSymbol; |
|||
import parser.ast.ExpressionAccumulation; |
|||
import parser.ast.ExpressionLabel; |
|||
import parser.ast.ExpressionTemporal; |
|||
import parser.ast.ExpressionUnaryOp; |
|||
import parser.ast.TemporalOperatorBound; |
|||
import parser.ast.TemporalOperatorBounds; |
|||
import prism.IntegerBound; |
|||
import prism.PrismLangException; |
|||
|
|||
|
|||
public class ReplaceAccumulationExpression extends ASTTraverseModify { |
|||
|
|||
private ExpressionAccumulation accexp; |
|||
private String replacementLabel; |
|||
private int replacementPosition; |
|||
|
|||
|
|||
|
|||
public ReplaceAccumulationExpression(ExpressionAccumulation accexp, String replacementLabel) { |
|||
super(); |
|||
this.accexp = accexp; |
|||
this.replacementLabel = replacementLabel; |
|||
this.replacementPosition = 0; |
|||
} |
|||
|
|||
public ReplaceAccumulationExpression(ExpressionAccumulation accexp, String replacementLabel, int replacementPosition) |
|||
{ |
|||
this(accexp, replacementLabel); |
|||
this.replacementPosition = replacementPosition; |
|||
} |
|||
|
|||
public Object visit(ExpressionAccumulation expr) throws PrismLangException |
|||
{ |
|||
ExpressionLabel label = new ExpressionLabel(replacementLabel); |
|||
//System.out.println("Replacing "+expr.toString()+" with "+label.toString()); |
|||
if (expr == accexp) { |
|||
AccumulationSymbol sym = expr.getSymbol(); |
|||
|
|||
if (sym.isPlus()) { |
|||
// We are looking into a bright future, wrap it in F=position |
|||
ExpressionTemporal fLabel = new ExpressionTemporal(ExpressionTemporal.P_F, null, label); |
|||
TemporalOperatorBounds fBounds = new TemporalOperatorBounds(); |
|||
TemporalOperatorBound fBound = IntegerBound.fromEqualBounds(replacementPosition).toTemporalOperatorBound(); |
|||
fBounds.setDefaultBound(fBound); |
|||
fLabel.setBounds(fBounds); |
|||
// If its a BOX, negate it |
|||
if (sym.isBox()) { |
|||
return new ExpressionUnaryOp(ExpressionUnaryOp.NOT, fLabel); |
|||
} else { |
|||
return fLabel; |
|||
} |
|||
} else { |
|||
// This is a MINUS, just check for negation |
|||
if (sym.isBox()) { |
|||
return new ExpressionUnaryOp(ExpressionUnaryOp.NOT, label); |
|||
} else { |
|||
return label; |
|||
} |
|||
} |
|||
} else { |
|||
return expr; |
|||
} |
|||
} |
|||
} |
|||
Write
Preview
Loading…
Cancel
Save
Reference in new issue