Browse Source

storm-pars compiles now

tempestpy_adaptions
TimQu 7 years ago
parent
commit
45279f9914
  1. 2
      src/storm-pars/modelchecker/region/SparseDtmcParameterLiftingModelChecker.cpp
  2. 9
      src/storm-pars/modelchecker/region/SparseMdpParameterLiftingModelChecker.cpp

2
src/storm-pars/modelchecker/region/SparseDtmcParameterLiftingModelChecker.cpp

@ -288,7 +288,7 @@ namespace storm {
if (stepBound) {
assert(*stepBound > 0);
x = std::vector<ConstantType>(maybeStates.getNumberOfSetBits(), storm::utility::zero<ConstantType>());
solver->repeatedMultiply(dirForParameters, x, &parameterLifter->getVector(), *stepBound);
solver->repeatedMultiply(env, dirForParameters, x, &parameterLifter->getVector(), *stepBound);
} else {
x.resize(maybeStates.getNumberOfSetBits(), storm::utility::zero<ConstantType>());
solver->solveEquations(env, dirForParameters, x, parameterLifter->getVector());

9
src/storm-pars/modelchecker/region/SparseMdpParameterLiftingModelChecker.cpp

@ -248,14 +248,7 @@ namespace storm {
parameterLifter->specifyRegion(region, dirForParameters);
// Set up the solver
auto solver = solverFactory->create(player1Matrix, parameterLifter->getMatrix());
if (storm::NumberTraits<ConstantType>::IsExact && dynamic_cast<storm::solver::StandardGameSolver<ConstantType>*>(solver.get())) {
STORM_LOG_INFO("Parameter Lifting: Setting solution method for exact Game Solver to policy iteration");
auto* standardSolver = dynamic_cast<storm::solver::StandardGameSolver<ConstantType>*>(solver.get());
auto settings = standardSolver->getSettings();
settings.setSolutionMethod(storm::solver::StandardGameSolverSettings<ConstantType>::SolutionMethod::PolicyIteration);
standardSolver->setSettings(settings);
}
auto solver = solverFactory->create(env, player1Matrix, parameterLifter->getMatrix());
if (lowerResultBound) solver->setLowerBound(lowerResultBound.get());
if (upperResultBound) solver->setUpperBound(upperResultBound.get());
if (applyPreviousResultAsHint) {

Loading…
Cancel
Save