From ed550e6255aa5554f7df432a40664616d767497e Mon Sep 17 00:00:00 2001
From: TimQu <tim.quatmann@cs.rwth-aachen.de>
Date: Tue, 27 Jun 2017 18:13:05 +0200
Subject: [PATCH] fixed invocation of instantiation checkers

---
 .../region/SparseDtmcParameterLiftingModelChecker.cpp           | 1 +
 .../region/SparseMdpParameterLiftingModelChecker.cpp            | 2 ++
 2 files changed, 3 insertions(+)

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