diff --git a/src/storm-pars/modelchecker/region/SparseDtmcParameterLiftingModelChecker.cpp b/src/storm-pars/modelchecker/region/SparseDtmcParameterLiftingModelChecker.cpp index ff8f29577..5f32c8386 100644 --- a/src/storm-pars/modelchecker/region/SparseDtmcParameterLiftingModelChecker.cpp +++ b/src/storm-pars/modelchecker/region/SparseDtmcParameterLiftingModelChecker.cpp @@ -207,6 +207,7 @@ namespace storm { if (!instantiationChecker) { instantiationChecker = std::make_unique>(*this->parametricModel); instantiationChecker->specifyFormula(this->currentCheckTask->template convertValueType()); + instantiationChecker->setInstantiationsAreGraphPreserving(true); } return *instantiationChecker; } diff --git a/src/storm-pars/modelchecker/region/SparseMdpParameterLiftingModelChecker.cpp b/src/storm-pars/modelchecker/region/SparseMdpParameterLiftingModelChecker.cpp index 32f8ca809..723ab4910 100644 --- a/src/storm-pars/modelchecker/region/SparseMdpParameterLiftingModelChecker.cpp +++ b/src/storm-pars/modelchecker/region/SparseMdpParameterLiftingModelChecker.cpp @@ -233,6 +233,7 @@ namespace storm { if (!instantiationChecker) { instantiationChecker = std::make_unique>(*this->parametricModel); instantiationChecker->specifyFormula(this->currentCheckTask->template convertValueType()); + instantiationChecker->setInstantiationsAreGraphPreserving(true); } return *instantiationChecker; } @@ -302,6 +303,7 @@ namespace storm { result[maybeState] = *maybeStateResIt; ++maybeStateResIt; } + return std::make_unique>(std::move(result)); }