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

accumulation: refactor some common function in product

accumulation
Sascha Wunderlich 9 years ago
committed by Sascha Wunderlich
parent
6740da5171
commit
90511afb27
4 changed files with 137 additions and 156 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. 107
      prism/src/explicit/AccumulationProduct.java
  2. 69
      prism/src/explicit/AccumulationProductCounting.java
  3. 111
      prism/src/explicit/AccumulationProductRegular.java
  4. 6
      prism/src/explicit/AccumulationTransformation.java

107
prism/src/explicit/AccumulationProduct.java
View File

@ -5,6 +5,9 @@ import java.util.BitSet;
import java.util.Iterator;
import java.util.Map;
import parser.ast.AccumulationFactor;
import parser.ast.ExpressionAccumulation;
import prism.IntegerBound;
import prism.PrismException;
import prism.PrismFileLog;
import prism.PrismLog;
@ -47,6 +50,110 @@ public abstract class AccumulationProduct<M extends Model,Component> extends Pro
public int getNumberOfTracks() {
return numberOfTracks;
}
protected abstract boolean isFinalTrack(final AccumulationTrack<Component> track, final ExpressionAccumulation accexp, final ProbModelChecker mc)
throws PrismException;
protected boolean isGoodTrack(final AccumulationTrack<Component> 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;
}
protected boolean isGoodAccState(final AccumulationState<Component> state, final ExpressionAccumulation accexp, final ProbModelChecker mc)
throws PrismException {
return state.hasGoodTrack();
}
protected abstract Component getInitialComponent();
protected abstract AccumulationTrack<Component> updateTrack(Integer modelFromStateId, final AccumulationTrack<Component> track,
final ExpressionAccumulation accexp, final double[] weights, final StateModelChecker mc);
protected AccumulationState<Component> updateAccumulationState(final int modelFromStateId,
final AccumulationState<Component> 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<Component> oldTracker = accstate.getTracker(trackers);
ArrayList<AccumulationTrack<Component>> 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<Component>> newTracks = new ArrayList<>();
int trackNr = 0;
for(AccumulationTrack<Component> oldTrack : oldTracks) {
AccumulationTrack<Component> newTrack;
// restart or advance
if(trackNr == newLastRestartNr) {
//assert oldTrack == null : "Track " + newLastRestartNr + " is not null!";
newTrack = new AccumulationTrack<Component>(numberOfWeights, getInitialComponent());
newGoodTracks.clear(trackNr);
} else if (oldTrack == null) {
newTrack = null;
} else {
assert oldTrack != null;
newTrack = updateTrack(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<Component> newTracker = new AccumulationTracker<>(newTracks);
int newTrackerId = trackers.findOrAdd(newTracker);
return new AccumulationState<>(newTrackerId, newLastRestartNr, numberOfTracks, newGoodTracks);
}
public void exportToDotFile(String filename) throws PrismException {
try (PrismFileLog log = PrismFileLog.create(filename)) {

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

@ -7,7 +7,6 @@ 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;
@ -142,7 +141,7 @@ public class AccumulationProductCounting<M extends Model> extends AccumulationPr
@Override
public void finish() throws PrismException {
// Do nothing
mc.getLog().println(".");
//mc.getLog().println(".");
}
@Override
@ -156,7 +155,8 @@ public class AccumulationProductCounting<M extends Model> extends AccumulationPr
return result;
}
private boolean isFinalTrack(final AccumulationTrack<Integer> track, final ExpressionAccumulation accexp, final ProbModelChecker mc)
@Override
protected boolean isFinalTrack(final AccumulationTrack<Integer> track, final ExpressionAccumulation accexp, final ProbModelChecker mc)
throws PrismException {
boolean isFinal = false;
if ( track != null ) {
@ -166,51 +166,12 @@ public class AccumulationProductCounting<M extends Model> extends AccumulationPr
return isFinal;
}
private boolean isGoodAccState(final AccumulationState<Integer> state, final ExpressionAccumulation accexp, final ProbModelChecker mc)
throws PrismException {
return state.hasGoodTrack();
@Override
protected Integer getInitialComponent() {
return 0;
}
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<Integer> updateAccumulationState(final int modelFromStateId,
protected AccumulationState<Integer> updateAccumulationState(final int modelFromStateId,
final AccumulationState<Integer> 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.
@ -224,7 +185,7 @@ public class AccumulationProductCounting<M extends Model> extends AccumulationPr
// This restart will be...
int newLastRestartNr = accstate.getNextRestartNr();
mc.getLog().print(newLastRestartNr);
//mc.getLog().print(newLastRestartNr);
// Build the new tracks.
ArrayList<AccumulationTrack<Integer>> newTracks = new ArrayList<>();
@ -242,7 +203,7 @@ public class AccumulationProductCounting<M extends Model> extends AccumulationPr
newTrack = null;
} else {
assert oldTrack != null;
newTrack = updateTrackBounds(oldTrack, accexp, weights, mc);
newTrack = updateTrack(modelFromStateId, oldTrack, accexp, weights, mc);
}
// check whether the track is good
@ -262,10 +223,16 @@ public class AccumulationProductCounting<M extends Model> extends AccumulationPr
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 {
@Override
protected AccumulationTrack<Integer> updateTrack(Integer modelFromStateId, final AccumulationTrack<Integer> track,
final ExpressionAccumulation accexp, final double[] weights, final StateModelChecker mc) {
int currentStep = track.getComponent();
int maxStep = IntegerBound.fromTemporalOperatorBound(accexp.getBoundExpression(), mc.getConstantValues(), true).getHighestInteger();
int maxStep = 0;
try {
maxStep = IntegerBound.fromTemporalOperatorBound(accexp.getBoundExpression(), mc.getConstantValues(), true).getHighestInteger();
} catch(PrismException e) {
throw new RuntimeException("...");
}
// If we are done, return null-Track
if (currentStep >= maxStep) { return null; }

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

@ -11,10 +11,8 @@ import automata.finite.State;
import explicit.rewards.MCRewards;
import explicit.rewards.MDPRewards;
import explicit.rewards.Rewards;
import parser.ast.AccumulationFactor;
import parser.ast.ExpressionAccumulation;
import parser.ast.ExpressionRegular;
import prism.IntegerBound;
import prism.PrismException;
/**
@ -163,7 +161,8 @@ public class AccumulationProductRegular<M extends Model> extends AccumulationPro
return result;
}
private boolean isFinalTrack(AccumulationTrack<State> track, ExpressionAccumulation accexp, ProbModelChecker mc) throws PrismException {
@Override
protected boolean isFinalTrack(AccumulationTrack<State> track, ExpressionAccumulation accexp, ProbModelChecker mc) throws PrismException {
boolean isFinal = false;
if ( track != null ) {
isFinal = automaton.isAcceptingState(track.getComponent());
@ -172,106 +171,13 @@ public class AccumulationProductRegular<M extends Model> extends AccumulationPro
return isFinal;
}
private boolean isGoodAccState(AccumulationState<State> state, ExpressionAccumulation accexp, ProbModelChecker mc) throws PrismException {
return state.hasGoodTrack();
@Override
protected State getInitialComponent() {
return automaton.getInitialState();
}
private boolean isGoodTrack(AccumulationTrack<State> track, ExpressionAccumulation accexp, ProbModelChecker mc) throws PrismException {
mc.getLog().println("Checking " + track + " for goodness...");
// Only final tracks can be good
mc.getLog().println("Final? " + isFinalTrack(track,accexp,mc));
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!");
}
mc.getLog().println("Good? " + lhs + rhs + " : " + isGood);
return isGood;
}
private AccumulationState<State> updateAccumulationState(final int modelFromStateId,
final AccumulationState<State> 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<State>(newTrackerId, newLastRestartNr, numberOfTracks, newGoodTracks);
}
private AccumulationTrack<State> updateTrackRegular(Integer modelFromStateId, AccumulationTrack<State> track, ExpressionAccumulation accexp, double[] weights, StateModelChecker mc) {
@Override
protected AccumulationTrack<State> updateTrack(Integer modelFromStateId, AccumulationTrack<State> track, ExpressionAccumulation accexp, double[] weights, StateModelChecker mc) {
State currentState = track.getComponent();
// Build EdgeLabel from labels.
@ -345,7 +251,8 @@ public class AccumulationProductRegular<M extends Model> extends AccumulationPro
automaton = nfa.determinize();
automaton.trim(); // This should remove cycles.
nfa.exportToDotFile("DEBUG-automaton-nfa.dot");
//DEBUG
//nfa.exportToDotFile("DEBUG-automaton-nfa.dot");
if (!automaton.isAcyclic()) {
throw new PrismException("Cannot handle cyclic automata!");

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

@ -133,10 +133,10 @@ public class AccumulationTransformation<M extends Model> implements ModelExpress
// Transform the expression
ReplaceAccumulationExpression replace = new ReplaceAccumulationExpression(accexp, label, product.getNumberOfTracks()-1);
transformedExpression = (Expression)transformedExpression.accept(replace);
mc.getLog().println("Transformed " + originalExpression.toString() +
"\n into " + transformedExpression.toString());
mc.getLog().println(" [AT] " + originalExpression.toString() + "\n" +
" -> " + transformedExpression.toString());
//DEBUG: output dotfile
product.exportToDotFile("DEBUG-product.dot");
//product.exportToDotFile("DEBUG-product.dot");
}
public String gensymLabel(String prefix, Model model) {

Write Preview
Loading…
Cancel
Save