Browse Source

param.ValueComputer: extends PrismComponent

Provides access to log and settings.
master
Joachim Klein 8 years ago
committed by Dave Parker
parent
commit
d212b33f2b
  1. 2
      prism/src/param/ParamModelChecker.java
  2. 8
      prism/src/param/ValueComputer.java

2
prism/src/param/ParamModelChecker.java

@ -220,7 +220,7 @@ final public class ParamModelChecker extends PrismComponent
constraintChecker = new ConstraintChecker(numRandomPoints);
regionFactory = new BoxRegionFactory(functionFactory, constraintChecker, precision,
model.getNumStates(), model.getFirstInitialState(), simplifyRegions, splitMethod);
valueComputer = new ValueComputer(paramModel, regionFactory, precision, eliminationOrder, bisimType);
valueComputer = new ValueComputer(this, paramModel, regionFactory, precision, eliminationOrder, bisimType);
long timer = 0;

8
prism/src/param/ValueComputer.java

@ -32,12 +32,15 @@ import java.util.HashMap;
import java.util.HashSet;
import java.util.Map.Entry;
import prism.PrismComponent;
/**
* Computes values for properties of a parametric Markov model.
*
* @author Ernst Moritz Hahn <emhahn@cs.ox.ac.uk> (University of Oxford)
*/
final class ValueComputer
final class ValueComputer extends PrismComponent
{
private enum PropType {
REACH,
@ -230,7 +233,8 @@ final class ValueComputer
private StateEliminator.EliminationOrder eliminationOrder;
private Lumper.BisimType bisimType;
ValueComputer(ParamModel model, RegionFactory regionFactory, BigRational precision, StateEliminator.EliminationOrder eliminationOrder, Lumper.BisimType bisimType) {
ValueComputer(PrismComponent parent, ParamModel model, RegionFactory regionFactory, BigRational precision, StateEliminator.EliminationOrder eliminationOrder, Lumper.BisimType bisimType) {
super(parent);
this.model = model;
this.regionFactory = regionFactory;
this.functionFactory = regionFactory.getFunctionFactory();

Loading…
Cancel
Save