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

accumulation: support single track mode

accumulation
Sascha Wunderlich 8 years ago
parent
eae5aa9de1
commit
b45fcb02b7
9 changed files with 95 additions and 54 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. 6
      prism/src/explicit/AccumulationProduct.java
  2. 11
      prism/src/explicit/AccumulationProductComplex.java
  3. 18
      prism/src/explicit/AccumulationProductComplexCounting.java
  4. 18
      prism/src/explicit/AccumulationProductComplexRegular.java
  5. 10
      prism/src/explicit/AccumulationProductSimple.java
  6. 18
      prism/src/explicit/AccumulationProductSimpleCounting.java
  7. 18
      prism/src/explicit/AccumulationProductSimpleRegular.java
  8. 25
      prism/src/explicit/AccumulationTransformation.java
  9. 25
      prism/src/parser/ast/Expression.java

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

@ -32,12 +32,16 @@ public abstract class AccumulationProduct<M extends Model,Component> extends Pro
protected int numberOfTracks;
protected int numberOfWeights;
public AccumulationProduct(M originalModel) {
protected boolean singleTrack;
public AccumulationProduct(M originalModel, boolean singleTrack) {
super(originalModel);
trackers = new StoragePool<>();
accStates = new StoragePool<>();
labels = new ArrayList<BitSet>();
this.singleTrack = singleTrack;
}
public final int getNumberOfTracks() {

11
prism/src/explicit/AccumulationProductComplex.java
View File

@ -27,8 +27,8 @@ public abstract class AccumulationProductComplex<M extends Model,Component> exte
protected final ArrayList<BitSet> runStates;
protected final ArrayList<BitSet> goalStates;
public AccumulationProductComplex(M originalModel) {
super(originalModel);
public AccumulationProductComplex(M originalModel, boolean singleTrack) {
super(originalModel, singleTrack);
initStates = new ArrayList<>();
runStates = new ArrayList<>();
goalStates = new ArrayList<>();
@ -165,6 +165,9 @@ public abstract class AccumulationProductComplex<M extends Model,Component> exte
protected final AccumulationState<Component> updateAccumulationState(final int modelFromStateId,
final AccumulationState<Component> accstate, final ExpressionAccumulation accexp,
final double[] weights, final ProbModelChecker mc) throws PrismException {
// If we are in singleTrack mode and the last restart is the numberOfTracks, we can stop...
if(singleTrack && (accstate.lastRestartNr == numberOfTracks-1)) { return accstate; }
// Check if we even need to fire here.
if(accexp.hasFireOn()) {
@ -198,12 +201,12 @@ public abstract class AccumulationProductComplex<M extends Model,Component> exte
AccumulationTrack<Component> newTrack;
// restart or advance
if(trackNr == newLastRestartNr) {
if(trackNr == newLastRestartNr && !singleTrack) {
// If we have a restart, we produce an initial track and let it advance.
AccumulationTrack<Component> freshTrack = new AccumulationTrack<Component>(numberOfWeights, getInitialComponent());
//newTrack = updateTrack(modelFromStateId, freshTrack, accexp, weights, mc);
newTrack = freshTrack;
} else if (oldTrack == null) {
} else if (oldTrack == null || (singleTrack && trackNr>0)) {
// If the old track is undefined, the new track is as well.
newTrack = null;
} else {

18
prism/src/explicit/AccumulationProductComplexCounting.java
View File

@ -23,24 +23,24 @@ import prism.PrismException;
public class AccumulationProductComplexCounting<M extends Model> extends AccumulationProductComplex<M,Integer>
{
public AccumulationProductComplexCounting(M originalModel) {
super(originalModel);
public AccumulationProductComplexCounting(M originalModel, boolean singleTrack) {
super(originalModel, singleTrack);
}
@SuppressWarnings("unchecked")
public static <T extends Model, R extends Rewards> AccumulationProductComplexCounting<T> generate(final Model graph, final ExpressionAccumulation accexp, final Vector<R> rewards, final ProbModelChecker mc, BitSet statesOfInterest) throws PrismException {
public static <T extends Model, R extends Rewards> AccumulationProductComplexCounting<T> generate(final Model graph, final ExpressionAccumulation accexp, final Vector<R> rewards, final boolean singleTrack, final ProbModelChecker mc, BitSet statesOfInterest) throws PrismException {
switch(graph.getModelType()) {
case DTMC:
return (AccumulationProductComplexCounting<T>)generate((DTMC) graph, accexp, (Vector<MCRewards>) rewards, mc, statesOfInterest);
return (AccumulationProductComplexCounting<T>)generate((DTMC) graph, accexp, (Vector<MCRewards>) rewards, singleTrack, mc, statesOfInterest);
case MDP:
return (AccumulationProductComplexCounting<T>)generate((MDP) graph, accexp, (Vector<MDPRewards>) rewards, mc, statesOfInterest);
return (AccumulationProductComplexCounting<T>)generate((MDP) graph, accexp, (Vector<MDPRewards>) rewards, singleTrack, mc, statesOfInterest);
default:
throw new PrismException("Can't handle accumulation product for " + graph.getModelType());
}
}
public static AccumulationProductComplexCounting<DTMC> generate(final DTMC graph, final ExpressionAccumulation accexp, final Vector<MCRewards> rewards, final ProbModelChecker mc, BitSet statesOfInterest) throws PrismException {
final AccumulationProductComplexCounting<DTMC> result = new AccumulationProductComplexCounting<DTMC>(graph);
public static AccumulationProductComplexCounting<DTMC> generate(final DTMC graph, final ExpressionAccumulation accexp, final Vector<MCRewards> rewards, final boolean singleTrack, final ProbModelChecker mc, BitSet statesOfInterest) throws PrismException {
final AccumulationProductComplexCounting<DTMC> result = new AccumulationProductComplexCounting<DTMC>(graph, singleTrack);
// Create auxiliary data
result.createAuxData(graph, accexp, rewards, mc);
@ -98,9 +98,9 @@ public class AccumulationProductComplexCounting<M extends Model> extends Accumul
return result;
}
public static AccumulationProductComplexCounting<MDP> generate(final MDP graph, final ExpressionAccumulation accexp, final Vector<MDPRewards> rewards, final ProbModelChecker mc, BitSet statesOfInterest) throws PrismException {
public static AccumulationProductComplexCounting<MDP> generate(final MDP graph, final ExpressionAccumulation accexp, final Vector<MDPRewards> rewards, final boolean singleTrack, final ProbModelChecker mc, BitSet statesOfInterest) throws PrismException {
// This is basically the same thing as for DTMCs
final AccumulationProductComplexCounting<MDP> result = new AccumulationProductComplexCounting<MDP>(graph);
final AccumulationProductComplexCounting<MDP> result = new AccumulationProductComplexCounting<MDP>(graph, singleTrack);
// Create auxiliary data
result.createAuxData(graph, accexp, rewards, mc);

18
prism/src/explicit/AccumulationProductComplexRegular.java
View File

@ -30,24 +30,24 @@ public class AccumulationProductComplexRegular<M extends Model> extends Accumula
{
protected DeterministicFiniteAutomaton<String> automaton;
public AccumulationProductComplexRegular(M originalModel) {
super(originalModel);
public AccumulationProductComplexRegular(M originalModel, boolean singleTrack) {
super(originalModel, singleTrack);
}
@SuppressWarnings("unchecked")
public static <T extends Model, R extends Rewards> AccumulationProductComplexRegular<T> generate(final Model graph, final ExpressionAccumulation accexp, final Vector<R> rewards, final ProbModelChecker mc, BitSet statesOfInterest) throws PrismException {
public static <T extends Model, R extends Rewards> AccumulationProductComplexRegular<T> generate(final Model graph, final ExpressionAccumulation accexp, final Vector<R> rewards, final boolean singleTrack, final ProbModelChecker mc, BitSet statesOfInterest) throws PrismException {
switch(graph.getModelType()) {
case DTMC:
return (AccumulationProductComplexRegular<T>)generate((DTMC) graph, accexp, (Vector<MCRewards>) rewards, mc, statesOfInterest);
return (AccumulationProductComplexRegular<T>)generate((DTMC) graph, accexp, (Vector<MCRewards>) rewards, singleTrack, mc, statesOfInterest);
case MDP:
return (AccumulationProductComplexRegular<T>)generate((MDP) graph, accexp, (Vector<MDPRewards>) rewards, mc, statesOfInterest);
return (AccumulationProductComplexRegular<T>)generate((MDP) graph, accexp, (Vector<MDPRewards>) rewards, singleTrack, mc, statesOfInterest);
default:
throw new PrismException("Can't handle accumulation product for " + graph.getModelType());
}
}
public static AccumulationProductComplexRegular<DTMC> generate(final DTMC graph, final ExpressionAccumulation accexp, final Vector<MCRewards> rewards, final ProbModelChecker mc, BitSet statesOfInterest) throws PrismException {
final AccumulationProductComplexRegular<DTMC> result = new AccumulationProductComplexRegular<DTMC>(graph);
public static AccumulationProductComplexRegular<DTMC> generate(final DTMC graph, final ExpressionAccumulation accexp, final Vector<MCRewards> rewards, final boolean singleTrack, final ProbModelChecker mc, BitSet statesOfInterest) throws PrismException {
final AccumulationProductComplexRegular<DTMC> result = new AccumulationProductComplexRegular<DTMC>(graph, singleTrack);
// Create auxiliary data
result.createAuxData(graph, accexp, rewards, mc);
@ -105,9 +105,9 @@ public class AccumulationProductComplexRegular<M extends Model> extends Accumula
return result;
}
public static AccumulationProductComplexRegular<MDP> generate(final MDP graph, final ExpressionAccumulation accexp, final Vector<MDPRewards> rewards, final ProbModelChecker mc, BitSet statesOfInterest) throws PrismException {
public static AccumulationProductComplexRegular<MDP> generate(final MDP graph, final ExpressionAccumulation accexp, final Vector<MDPRewards> rewards, final boolean singleTrack, final ProbModelChecker mc, BitSet statesOfInterest) throws PrismException {
// This is basically the same thing as for DTMCs
final AccumulationProductComplexRegular<MDP> result = new AccumulationProductComplexRegular<MDP>(graph);
final AccumulationProductComplexRegular<MDP> result = new AccumulationProductComplexRegular<MDP>(graph, singleTrack);
// Create auxiliary data
result.createAuxData(graph, accexp, rewards, mc);

10
prism/src/explicit/AccumulationProductSimple.java
View File

@ -24,8 +24,8 @@ public abstract class AccumulationProductSimple<M extends Model,Component> exten
{
protected final BitSet goodStates;
public AccumulationProductSimple(M originalModel) {
super(originalModel);
public AccumulationProductSimple(M originalModel, boolean singleTrack) {
super(originalModel, singleTrack);
goodStates = new BitSet();
}
@ -152,6 +152,8 @@ public abstract class AccumulationProductSimple<M extends Model,Component> exten
protected final AccumulationState<Component> updateAccumulationState(final int modelFromStateId,
final AccumulationState<Component> accstate, final ExpressionAccumulation accexp,
final double[] weights, final ProbModelChecker mc) throws PrismException {
// If we are in singleTrack mode and the last restart is the numberOfTracks, we can stop...
if(singleTrack && (accstate.lastRestartNr == numberOfTracks-1)) { return accstate; }
// Get the old tracker and tracks.
AccumulationTracker<Component> oldTracker = accstate.getTracker(trackers);
@ -171,14 +173,14 @@ public abstract class AccumulationProductSimple<M extends Model,Component> exten
AccumulationTrack<Component> newTrack;
// restart or advance
if(trackNr == newLastRestartNr) {
if(trackNr == newLastRestartNr && !singleTrack) {
// If we have a restart, we produce an initial track and let it advance.
// The goodness is cleared.
AccumulationTrack<Component> freshTrack = new AccumulationTrack<Component>(numberOfWeights, getInitialComponent());
//newTrack = updateTrack(modelFromStateId, freshTrack, accexp, weights, mc);
newTrack = freshTrack;
newGoodTracks.clear(trackNr);
} else if (oldTrack == null) {
} else if (oldTrack == null || (singleTrack && trackNr>0)) {
// If the old track is undefined, the new track is as well.
// Goodness stays!
newTrack = null;

18
prism/src/explicit/AccumulationProductSimpleCounting.java
View File

@ -23,24 +23,24 @@ import prism.PrismException;
public class AccumulationProductSimpleCounting<M extends Model> extends AccumulationProductSimple<M,Integer>
{
public AccumulationProductSimpleCounting(M originalModel) {
super(originalModel);
public AccumulationProductSimpleCounting(M originalModel, boolean singleTrack) {
super(originalModel, singleTrack);
}
@SuppressWarnings("unchecked")
public static <T extends Model, R extends Rewards> AccumulationProductSimpleCounting<T> generate(final Model graph, final ExpressionAccumulation accexp, final Vector<R> rewards, final ProbModelChecker mc, BitSet statesOfInterest) throws PrismException {
public static <T extends Model, R extends Rewards> AccumulationProductSimpleCounting<T> generate(final Model graph, final ExpressionAccumulation accexp, final Vector<R> rewards, final boolean singleTrack, final ProbModelChecker mc, BitSet statesOfInterest) throws PrismException {
switch(graph.getModelType()) {
case DTMC:
return (AccumulationProductSimpleCounting<T>)generate((DTMC) graph, accexp, (Vector<MCRewards>) rewards, mc, statesOfInterest);
return (AccumulationProductSimpleCounting<T>)generate((DTMC) graph, accexp, (Vector<MCRewards>) rewards, singleTrack, mc, statesOfInterest);
case MDP:
return (AccumulationProductSimpleCounting<T>)generate((MDP) graph, accexp, (Vector<MDPRewards>) rewards, mc, statesOfInterest);
return (AccumulationProductSimpleCounting<T>)generate((MDP) graph, accexp, (Vector<MDPRewards>) rewards, singleTrack, mc, statesOfInterest);
default:
throw new PrismException("Can't handle accumulation product for " + graph.getModelType());
}
}
public static AccumulationProductSimpleCounting<DTMC> generate(final DTMC graph, final ExpressionAccumulation accexp, final Vector<MCRewards> rewards, final ProbModelChecker mc, BitSet statesOfInterest) throws PrismException {
final AccumulationProductSimpleCounting<DTMC> result = new AccumulationProductSimpleCounting<DTMC>(graph);
public static AccumulationProductSimpleCounting<DTMC> generate(final DTMC graph, final ExpressionAccumulation accexp, final Vector<MCRewards> rewards, final boolean singleTrack, final ProbModelChecker mc, BitSet statesOfInterest) throws PrismException {
final AccumulationProductSimpleCounting<DTMC> result = new AccumulationProductSimpleCounting<DTMC>(graph,singleTrack);
// Create auxiliary data
result.createAuxData(graph, accexp, rewards, mc);
@ -98,9 +98,9 @@ public class AccumulationProductSimpleCounting<M extends Model> extends Accumula
return result;
}
public static AccumulationProductSimpleCounting<MDP> generate(final MDP graph, final ExpressionAccumulation accexp, final Vector<MDPRewards> rewards, final ProbModelChecker mc, BitSet statesOfInterest) throws PrismException {
public static AccumulationProductSimpleCounting<MDP> generate(final MDP graph, final ExpressionAccumulation accexp, final Vector<MDPRewards> rewards, final boolean singleTrack, final ProbModelChecker mc, BitSet statesOfInterest) throws PrismException {
// This is basically the same thing as for DTMCs
final AccumulationProductSimpleCounting<MDP> result = new AccumulationProductSimpleCounting<MDP>(graph);
final AccumulationProductSimpleCounting<MDP> result = new AccumulationProductSimpleCounting<MDP>(graph, singleTrack);
// Create auxiliary data
result.createAuxData(graph, accexp, rewards, mc);

18
prism/src/explicit/AccumulationProductSimpleRegular.java
View File

@ -30,24 +30,24 @@ public class AccumulationProductSimpleRegular<M extends Model> extends Accumulat
{
protected DeterministicFiniteAutomaton<String> automaton;
public AccumulationProductSimpleRegular(M originalModel) {
super(originalModel);
public AccumulationProductSimpleRegular(M originalModel, boolean singleTrack) {
super(originalModel, singleTrack);
}
@SuppressWarnings("unchecked")
public static <T extends Model, R extends Rewards> AccumulationProductSimpleRegular<T> generate(final Model graph, final ExpressionAccumulation accexp, final Vector<R> rewards, final ProbModelChecker mc, BitSet statesOfInterest) throws PrismException {
public static <T extends Model, R extends Rewards> AccumulationProductSimpleRegular<T> generate(final Model graph, final ExpressionAccumulation accexp, final Vector<R> rewards, final boolean singleTrack, final ProbModelChecker mc, BitSet statesOfInterest) throws PrismException {
switch(graph.getModelType()) {
case DTMC:
return (AccumulationProductSimpleRegular<T>)generate((DTMC) graph, accexp, (Vector<MCRewards>) rewards, mc, statesOfInterest);
return (AccumulationProductSimpleRegular<T>)generate((DTMC) graph, accexp, (Vector<MCRewards>) rewards, singleTrack, mc, statesOfInterest);
case MDP:
return (AccumulationProductSimpleRegular<T>)generate((MDP) graph, accexp, (Vector<MDPRewards>) rewards, mc, statesOfInterest);
return (AccumulationProductSimpleRegular<T>)generate((MDP) graph, accexp, (Vector<MDPRewards>) rewards, singleTrack, mc, statesOfInterest);
default:
throw new PrismException("Can't handle accumulation product for " + graph.getModelType());
}
}
public static AccumulationProductSimpleRegular<DTMC> generate(final DTMC graph, final ExpressionAccumulation accexp, final Vector<MCRewards> rewards, final ProbModelChecker mc, BitSet statesOfInterest) throws PrismException {
final AccumulationProductSimpleRegular<DTMC> result = new AccumulationProductSimpleRegular<DTMC>(graph);
public static AccumulationProductSimpleRegular<DTMC> generate(final DTMC graph, final ExpressionAccumulation accexp, final Vector<MCRewards> rewards, final boolean singleTrack, final ProbModelChecker mc, BitSet statesOfInterest) throws PrismException {
final AccumulationProductSimpleRegular<DTMC> result = new AccumulationProductSimpleRegular<DTMC>(graph, singleTrack);
// Create auxiliary data
result.createAuxData(graph, accexp, rewards, mc);
@ -105,9 +105,9 @@ public class AccumulationProductSimpleRegular<M extends Model> extends Accumulat
return result;
}
public static AccumulationProductSimpleRegular<MDP> generate(final MDP graph, final ExpressionAccumulation accexp, final Vector<MDPRewards> rewards, final ProbModelChecker mc, BitSet statesOfInterest) throws PrismException {
public static AccumulationProductSimpleRegular<MDP> generate(final MDP graph, final ExpressionAccumulation accexp, final Vector<MDPRewards> rewards, final boolean singleTrack, final ProbModelChecker mc, BitSet statesOfInterest) throws PrismException {
// This is basically the same thing as for DTMCs
final AccumulationProductSimpleRegular<MDP> result = new AccumulationProductSimpleRegular<MDP>(graph);
final AccumulationProductSimpleRegular<MDP> result = new AccumulationProductSimpleRegular<MDP>(graph, singleTrack);
// Create auxiliary data
result.createAuxData(graph, accexp, rewards, mc);

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

@ -78,8 +78,15 @@ public class AccumulationTransformation<M extends ModelExplicit> implements Mode
// TODO: WHILE getFirstAccumulationExpression
// Get the first ExpressionAccumulation
ExpressionAccumulation accexp = transformedExpression.getFirstAccumulationExpression();
boolean singleTrack = true;
ExpressionAccumulation accexp = transformedExpression.getFirstAccumulationExpressionWithoutTemporal();
if(accexp == null) {
singleTrack = false;
accexp = transformedExpression.getFirstAccumulationExpression();
}
mc.getLog().println(" [AT] for " + accexp);
mc.getLog().println(" ... single track? " + singleTrack);
// Rewrite it, if it is a BOX
if (accexp.getSymbol().isBox()) {
@ -114,24 +121,24 @@ public class AccumulationTransformation<M extends ModelExplicit> implements Mode
if(isComplex || forceComplex) {
mc.getLog().println(" ... using complex!");
doTransformationComplex(accexp, rewards);
doTransformationComplex(accexp, rewards, singleTrack);
} else {
mc.getLog().println(" ... using simple!");
doTransformationSimple(accexp, rewards);
doTransformationSimple(accexp, rewards, singleTrack);
}
}
@SuppressWarnings("unchecked")
protected void doTransformationComplex(ExpressionAccumulation accexp, Vector<Rewards> rewards) throws PrismException {
protected void doTransformationComplex(ExpressionAccumulation accexp, Vector<Rewards> rewards, boolean singleTrack) throws PrismException {
StopWatch clock = new StopWatch(mc.getLog());
// Build the product
clock.start("accumulation product construction");
if(accexp.hasRegularExpression()) {
product = (AccumulationProductComplexRegular<M>) AccumulationProductComplexRegular.generate(originalModel, accexp, rewards, mc, statesOfInterest);
product = (AccumulationProductComplexRegular<M>) AccumulationProductComplexRegular.generate(originalModel, accexp, rewards, singleTrack, mc, statesOfInterest);
} else if (accexp.hasBoundExpression()) {
product = (AccumulationProductComplexCounting<M>) AccumulationProductComplexCounting.generate(originalModel, accexp, rewards, mc, statesOfInterest);
product = (AccumulationProductComplexCounting<M>) AccumulationProductComplexCounting.generate(originalModel, accexp, rewards, singleTrack, mc, statesOfInterest);
} else {
throw new PrismException("Accumulation Expression has no valid monitor!");
}
@ -176,7 +183,7 @@ public class AccumulationTransformation<M extends ModelExplicit> implements Mode
}
@SuppressWarnings("unchecked")
protected void doTransformationSimple(ExpressionAccumulation accexp, Vector<Rewards> rewards) throws PrismException {
protected void doTransformationSimple(ExpressionAccumulation accexp, Vector<Rewards> rewards, boolean singleTrack) throws PrismException {
StopWatch clock = new StopWatch(mc.getLog());
// Build the product
@ -184,9 +191,9 @@ public class AccumulationTransformation<M extends ModelExplicit> implements Mode
if(accexp.hasRegularExpression()) {
//throw new PrismException("I don't know how to do regular things...");
product = (AccumulationProductSimpleRegular<M>) AccumulationProductSimpleRegular.generate(originalModel, accexp, rewards, mc, statesOfInterest);
product = (AccumulationProductSimpleRegular<M>) AccumulationProductSimpleRegular.generate(originalModel, accexp, rewards, singleTrack, mc, statesOfInterest);
} else if (accexp.hasBoundExpression()) {
product = (AccumulationProductSimpleCounting<M>) AccumulationProductSimpleCounting.generate(originalModel, accexp, rewards, mc, statesOfInterest);
product = (AccumulationProductSimpleCounting<M>) AccumulationProductSimpleCounting.generate(originalModel, accexp, rewards, singleTrack, mc, statesOfInterest);
} else {
throw new PrismException("Accumulation Expression has no valid monitor!");
}

25
prism/src/parser/ast/Expression.java
View File

@ -1006,6 +1006,31 @@ public abstract class Expression extends ASTElement
return null;
}
/**
* Get the first Accumulation Subexpression that is not in a Temporal Operator
*/
public ExpressionAccumulation getFirstAccumulationExpressionWithoutTemporal()
{
try {
ASTTraverse astt = new ASTTraverse()
{
public Object visit(ExpressionTemporal expr)
{
return null;
}
public Object visit(ExpressionAccumulation accexp) throws PrismLangException
{
throw new PrismLangException("Found accumulation here!", accexp);
}
};
this.accept(astt);
} catch (PrismLangException e) {
return (ExpressionAccumulation)e.getASTElement();
}
return null;
}
/**
* Test if an expression is an LTL formula and is in positive normal form,
* i.e. where negation only occurs at the level of state formulae.

Write Preview
Loading…
Cancel
Save