WIP

moves-rwth · Jun 20, 2024 · 22b586a · 22b586a
1 parent 7de29ca
commit 22b586a
Show file tree

Hide file tree

Showing 18 changed files with 298 additions and 209 deletions.
diff --git a/src/storm-pars/modelchecker/instantiation/SparseCtmcInstantiationModelChecker.cpp b/src/storm-pars/modelchecker/instantiation/SparseCtmcInstantiationModelChecker.cpp
@@ -23,6 +23,12 @@ std::unique_ptr<CheckResult> SparseCtmcInstantiationModelChecker<SparseModelType
     return modelChecker.check(env, *this->currentCheckTask);
 }
 
+template<typename SparseModelType, typename ConstantType>
+bool SparseCtmcInstantiationModelChecker<SparseModelType, ConstantType>::isProbabilistic(storm::utility::parametric::Valuation<typename SparseModelType::ValueType> const& valuation) {
+    auto const& instantiatedModel = modelInstantiator.instantiate(valuation);
+    return instantiatedModel.getTransitionMatrix().isProbabilistic();
+}
+
 template class SparseCtmcInstantiationModelChecker<storm::models::sparse::Ctmc<storm::RationalFunction>, double>;
 template class SparseCtmcInstantiationModelChecker<storm::models::sparse::Ctmc<storm::RationalFunction>, storm::RationalNumber>;
 }  // namespace modelchecker

diff --git a/src/storm-pars/modelchecker/instantiation/SparseCtmcInstantiationModelChecker.h b/src/storm-pars/modelchecker/instantiation/SparseCtmcInstantiationModelChecker.h
@@ -23,6 +23,8 @@ class SparseCtmcInstantiationModelChecker : public SparseInstantiationModelCheck
     virtual std::unique_ptr<CheckResult> check(Environment const& env,
                                                storm::utility::parametric::Valuation<typename SparseModelType::ValueType> const& valuation) override;
 
+    virtual bool isProbabilistic(storm::utility::parametric::Valuation<typename SparseModelType::ValueType> const& valuation) override;
+
     storm::utility::ModelInstantiator<SparseModelType, storm::models::sparse::Ctmc<ConstantType>> modelInstantiator;
 };
 }  // namespace modelchecker

diff --git a/src/storm-pars/modelchecker/instantiation/SparseDtmcInstantiationModelChecker.cpp b/src/storm-pars/modelchecker/instantiation/SparseDtmcInstantiationModelChecker.cpp
@@ -194,6 +194,12 @@ std::unique_ptr<CheckResult> SparseDtmcInstantiationModelChecker<SparseModelType
     return result;
 }
 
+template<typename SparseModelType, typename ConstantType>
+bool SparseDtmcInstantiationModelChecker<SparseModelType, ConstantType>::isProbabilistic(storm::utility::parametric::Valuation<typename SparseModelType::ValueType> const& valuation) {
+    auto const& instantiatedModel = modelInstantiator.instantiate(valuation);
+    return instantiatedModel.getTransitionMatrix().isProbabilistic();
+}
+
 template class SparseDtmcInstantiationModelChecker<storm::models::sparse::Dtmc<storm::RationalFunction>, double>;
 template class SparseDtmcInstantiationModelChecker<storm::models::sparse::Dtmc<storm::RationalFunction>, storm::RationalNumber>;
 

diff --git a/src/storm-pars/modelchecker/instantiation/SparseDtmcInstantiationModelChecker.h b/src/storm-pars/modelchecker/instantiation/SparseDtmcInstantiationModelChecker.h
@@ -23,6 +23,8 @@ class SparseDtmcInstantiationModelChecker : public SparseInstantiationModelCheck
     virtual std::unique_ptr<CheckResult> check(Environment const& env,
                                                storm::utility::parametric::Valuation<typename SparseModelType::ValueType> const& valuation) override;
 
+    virtual bool isProbabilistic(storm::utility::parametric::Valuation<typename SparseModelType::ValueType> const& valuation) override;
+
    protected:
     // Optimizations for the different formula types
     std::unique_ptr<CheckResult> checkReachabilityProbabilityFormula(

diff --git a/src/storm-pars/modelchecker/instantiation/SparseInstantiationModelChecker.h b/src/storm-pars/modelchecker/instantiation/SparseInstantiationModelChecker.h
@@ -25,6 +25,8 @@ class SparseInstantiationModelChecker {
 
     virtual std::unique_ptr<CheckResult> check(Environment const& env,
                                                storm::utility::parametric::Valuation<typename SparseModelType::ValueType> const& valuation) = 0;
+
+    virtual bool isProbabilistic(storm::utility::parametric::Valuation<typename SparseModelType::ValueType> const& valuation) = 0;
 
     // If set, it is assumed that all considered model instantiations have the same underlying graph structure.
     // This bypasses the graph analysis for the different instantiations.

diff --git a/src/storm-pars/modelchecker/instantiation/SparseMdpInstantiationModelChecker.cpp b/src/storm-pars/modelchecker/instantiation/SparseMdpInstantiationModelChecker.cpp
@@ -232,6 +232,12 @@ std::unique_ptr<CheckResult> SparseMdpInstantiationModelChecker<SparseModelType,
     return result;
 }
 
+template<typename SparseModelType, typename ConstantType>
+bool SparseMdpInstantiationModelChecker<SparseModelType, ConstantType>::isProbabilistic(storm::utility::parametric::Valuation<typename SparseModelType::ValueType> const& valuation) {
+    auto const& instantiatedModel = modelInstantiator.instantiate(valuation);
+    return instantiatedModel.getTransitionMatrix().isProbabilistic();
+}
+
 template class SparseMdpInstantiationModelChecker<storm::models::sparse::Mdp<storm::RationalFunction>, double>;
 template class SparseMdpInstantiationModelChecker<storm::models::sparse::Mdp<storm::RationalFunction>, storm::RationalNumber>;
 

diff --git a/src/storm-pars/modelchecker/instantiation/SparseMdpInstantiationModelChecker.h b/src/storm-pars/modelchecker/instantiation/SparseMdpInstantiationModelChecker.h
@@ -23,6 +23,8 @@ class SparseMdpInstantiationModelChecker : public SparseInstantiationModelChecke
     virtual std::unique_ptr<CheckResult> check(Environment const& env,
                                                storm::utility::parametric::Valuation<typename SparseModelType::ValueType> const& valuation) override;
 
+    virtual bool isProbabilistic(storm::utility::parametric::Valuation<typename SparseModelType::ValueType> const& valuation) override;
+
    protected:
     // Optimizations for the different formula types
     std::unique_ptr<CheckResult> checkReachabilityProbabilityFormula(

diff --git a/src/storm-pars/modelchecker/region/RegionRefinementChecker.cpp b/src/storm-pars/modelchecker/region/RegionRefinementChecker.cpp
@@ -89,6 +89,10 @@ class PartitioningProgress {
         fractionOfAllViolatedArea += addDiscoveredArea(area);
     }
 
+    void addAllIllDefinedArea(T const& area) {
+        fractionOfAllIllDefinedArea += addDiscoveredArea(area);
+    }
+
    private:
     static uint64_t asPercentage(T const& value) {
         return storm::utility::convertNumber<uint64_t>(storm::utility::round<T>(value * storm::utility::convertNumber<T, uint64_t>(100u)));
@@ -99,6 +103,7 @@ class PartitioningProgress {
     T fractionOfUndiscoveredArea;
     T fractionOfAllSatArea;
     T fractionOfAllViolatedArea;
+    T fractionOfAllIllDefinedArea;
     storm::utility::ProgressMeasurement progress;
 };
 
@@ -145,12 +150,12 @@ std::unique_ptr<storm::modelchecker::RegionRefinementCheckResult<ParametricType>
 
         currentRegion.result = regionChecker->analyzeRegion(env, currentRegion, hypothesis);
 
-        std::cout << currentRegion.result << std::endl;
-
         if (currentRegion.result == RegionResult::AllSat) {
             progress.addAllSatArea(currentRegion.region.area());
         } else if (currentRegion.result == RegionResult::AllViolated) {
             progress.addAllViolatedArea(currentRegion.region.area());
+        } else if (currentRegion.result == RegionResult::AllIllDefined) {
+            progress.addAllIllDefinedArea(currentRegion.region.area());
         } else {
             // Split the region as long as the desired refinement depth is not reached.
             if (!depthThreshold || currentRegion.refinementDepth < depthThreshold.value()) {

diff --git a/src/storm-pars/modelchecker/region/RegionSplitEstimateKind.h b/src/storm-pars/modelchecker/region/RegionSplitEstimateKind.h
@@ -1,5 +1,5 @@
 #pragma once
 
 namespace storm::modelchecker {
-enum class RegionSplitEstimateKind { Distance, StateValueDelta, MinMaxDelta, MinMaxDeltaWeighted, Derivative };
+enum class RegionSplitEstimateKind { Distance, StateValueDelta, StateValueDeltaWeighted, Derivative };
 }