Browse Source

fixed invocation of instantiation checkers

main
TimQu 8 years ago
parent
commit
ed550e6255
  1. 1
      src/storm-pars/modelchecker/region/SparseDtmcParameterLiftingModelChecker.cpp
  2. 2
      src/storm-pars/modelchecker/region/SparseMdpParameterLiftingModelChecker.cpp

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

@ -207,6 +207,7 @@ namespace storm {
if (!instantiationChecker) { if (!instantiationChecker) {
instantiationChecker = std::make_unique<storm::modelchecker::SparseDtmcInstantiationModelChecker<SparseModelType, ConstantType>>(*this->parametricModel); instantiationChecker = std::make_unique<storm::modelchecker::SparseDtmcInstantiationModelChecker<SparseModelType, ConstantType>>(*this->parametricModel);
instantiationChecker->specifyFormula(this->currentCheckTask->template convertValueType<typename SparseModelType::ValueType>()); instantiationChecker->specifyFormula(this->currentCheckTask->template convertValueType<typename SparseModelType::ValueType>());
instantiationChecker->setInstantiationsAreGraphPreserving(true);
} }
return *instantiationChecker; return *instantiationChecker;
} }

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

@ -233,6 +233,7 @@ namespace storm {
if (!instantiationChecker) { if (!instantiationChecker) {
instantiationChecker = std::make_unique<storm::modelchecker::SparseMdpInstantiationModelChecker<SparseModelType, ConstantType>>(*this->parametricModel); instantiationChecker = std::make_unique<storm::modelchecker::SparseMdpInstantiationModelChecker<SparseModelType, ConstantType>>(*this->parametricModel);
instantiationChecker->specifyFormula(this->currentCheckTask->template convertValueType<typename SparseModelType::ValueType>()); instantiationChecker->specifyFormula(this->currentCheckTask->template convertValueType<typename SparseModelType::ValueType>());
instantiationChecker->setInstantiationsAreGraphPreserving(true);
} }
return *instantiationChecker; return *instantiationChecker;
} }
@ -302,6 +303,7 @@ namespace storm {
result[maybeState] = *maybeStateResIt; result[maybeState] = *maybeStateResIt;
++maybeStateResIt; ++maybeStateResIt;
} }
return std::make_unique<storm::modelchecker::ExplicitQuantitativeCheckResult<ConstantType>>(std::move(result)); return std::make_unique<storm::modelchecker::ExplicitQuantitativeCheckResult<ConstantType>>(std::move(result));
} }

Loading…
Cancel
Save