Distincting between supportsParameters and hasParameters

Former-commit-id: a5d961f470

src/models/ModelBase.cpp

@@ -18,8 +18,16 @@ namespace storm {
             return this->getType() == modelType;
         }
         
-        bool ModelBase::isParametric() const { 
+        bool ModelBase::supportsParameters() const {
+            return false;
+        }
+
+        bool ModelBase::hasParameters() const {
+            return false;
+        }
+
+        bool ModelBase::isExact() const {
             return false;
         }
     }
-}
+}

src/models/ModelBase.h

@@ -98,9 +98,25 @@ namespace storm {
             bool isOfType(storm::models::ModelType const& modelType) const;
             
             /*!
-             * Checks whether the model is parametric
+             * Checks whether the model supports parameters.
+             *
+             * @return True iff the model supports parameters.
+             */
+            virtual bool supportsParameters() const;
+            
+            /*!
+             * Checks whether the model has parameters.
+             *
+             * @return True iff the model has parameters.
+             */
+            virtual bool hasParameters() const;
+            
+            /*!
+             * Checks whether the model is exact.
+             *
+             * @return True iff the model is exact.
              */
-            virtual bool isParametric() const;
+            virtual bool isExact() const;
             
         private:
             // The type of the model.

src/models/sparse/Model.cpp

@@ -311,10 +311,31 @@ namespace storm {
             }
             
             template<typename ValueType, typename RewardModelType>
-            bool Model<ValueType, RewardModelType>::isParametric() const {
+            bool Model<ValueType, RewardModelType>::supportsParameters() const {
                 return std::is_same<ValueType, storm::RationalFunction>::value;
             }
             
+            template<typename ValueType, typename RewardModelType>
+            bool Model<ValueType, RewardModelType>::hasParameters() const {
+                if (!this->supportsParameters()) {
+                    return false;
+                }
+                // Check for parameters
+                for (auto const& entry : this->getTransitionMatrix()) {
+                    if (!storm::utility::isConstant(entry.getValue())) {
+                        return true;
+                    }
+                }
+                // Only constant values present
+                return false;
+            }
+            
+            template<typename ValueType, typename RewardModelType>
+            bool Model<ValueType, RewardModelType>::isExact() const {
+                // TODO: change when dedicated data-structure for exact values is present
+                return this->supportsParameters();
+            }
+            
             template<typename ValueType, typename RewardModelType>
             std::unordered_map<std::string, RewardModelType>& Model<ValueType, RewardModelType>::getRewardModels() {
                 return this->rewardModels;
@@ -342,4 +363,4 @@ namespace storm {
             
         }
     }
-}
+}

src/models/sparse/Model.h

@@ -293,7 +293,17 @@ namespace storm {
                 
                 virtual bool isSparseModel() const override;
                 
-                virtual bool isParametric() const override;
+                virtual bool supportsParameters() const override;
+                
+                /*!
+                 * Checks whether the model has parameters.
+                 * Performance warning: the worst-case complexity is linear in the number of transitions.
+                 *
+                 * @return True iff the model has parameters.
+                 */
+                virtual bool hasParameters() const override;
+                
+                virtual bool isExact() const override;
             protected:
 
                 RewardModelType & rewardModel(std::string const& rewardModelName);

stormpy/lib/stormpy/__init__.py

@@ -5,32 +5,26 @@ core.set_up("")
 
 def build_model(program, formulae):
     intermediate = core._build_model(program, formulae)
-    
-    if intermediate.parametric():
-         raise RuntimeError("Model should be non-parametric")
+    assert not intermediate.supports_parameters()
+    if intermediate.model_type() == ModelType.DTMC:
+        return intermediate.as_dtmc()
+    elif intermediate.model_type() == ModelType.MDP:
+        return intermediate.as_mdp()
     else:
-         if intermediate.model_type() == ModelType.DTMC:
-             return intermediate.as_dtmc()
-         elif intermediate.model_type() == ModelType.MDP:
-             return intermediate.as_mdp()
-         else:
-             raise RuntimeError("Not supported non-parametric model constructed")
+        raise RuntimeError("Not supported non-parametric model constructed")
 
 def build_parametric_model(program, formulae):
     intermediate = core._build_parametric_model(program, formulae)
-    
-    if intermediate.parametric():
-         if intermediate.model_type() == ModelType.DTMC:
-             return intermediate.as_pdtmc()
-         elif intermediate.model_type() == ModelType.MDP:
-             return intermediate.as_pmdp()
-         else:
-             raise RuntimeError("Not supported parametric model constructed")
+    assert intermediate.supports_parameters()
+    if intermediate.model_type() == ModelType.DTMC:
+        return intermediate.as_pdtmc()
+    elif intermediate.model_type() == ModelType.MDP:
+        return intermediate.as_pmdp()
     else:
-        raise RuntimeError("Model should be parametric")
+        raise RuntimeError("Not supported parametric model constructed")
 
 def perform_bisimulation(model, formula, bisimulation_type):
-    if model.parametric():
+    if model.supports_parameters():
         return core._perform_parametric_bisimulation(model, formula, bisimulation_type)
     else:
         return core._perform_bisimulation(model, formula, bisimulation_type)

stormpy/src/core/model.cpp

@@ -28,7 +28,9 @@ void define_model(py::module& m) {
         .def("nr_states", &storm::models::ModelBase::getNumberOfStates, "Get number of states")
         .def("nr_transitions", &storm::models::ModelBase::getNumberOfTransitions, "Get number of transitions")
         .def("model_type", &storm::models::ModelBase::getType, "Get model type")
-        .def("parametric", &storm::models::ModelBase::isParametric, "Check if model is parametric")
+        .def("supports_parameters", &storm::models::ModelBase::supportsParameters, "Check if model supports parameters")
+        .def("has_parameters", &storm::models::ModelBase::hasParameters, "Check if model has parameters")
+        .def("is_exact", &storm::models::ModelBase::isExact, "Check if model is exact")
         .def("as_dtmc", &storm::models::ModelBase::as<storm::models::sparse::Dtmc<double>>, "Get model as DTMC")
         .def("as_pdtmc", &storm::models::ModelBase::as<storm::models::sparse::Dtmc<storm::RationalFunction>>, "Get model as pDTMC")
         .def("as_mdp", &storm::models::ModelBase::as<storm::models::sparse::Mdp<double>>, "Get model as MDP")

stormpy/tests/core/test_bisimulation.py

@@ -13,12 +13,12 @@ class TestBisimulation:
         assert model.nr_states() == 7403
         assert model.nr_transitions() == 13041
         assert model.model_type() == stormpy.ModelType.DTMC
-        assert not model.parametric()
+        assert not model.supports_parameters()
         model_bisim = stormpy.perform_bisimulation(model, formulas[0], stormpy.BisimulationType.STRONG)
         assert model_bisim.nr_states() == 64
         assert model_bisim.nr_transitions() == 104
         assert model_bisim.model_type() == stormpy.ModelType.DTMC
-        assert not model_bisim.parametric()
+        assert not model_bisim.supports_parameters()
     
     def test_parametric_bisimulation(self):
         program = stormpy.parse_program("../examples/pdtmc/crowds/crowds_3-5.pm")
@@ -32,9 +32,9 @@ class TestBisimulation:
         assert model.nr_states() == 1367
         assert model.nr_transitions() == 2027
         assert model.model_type() == stormpy.ModelType.DTMC
-        assert model.parametric()
+        assert model.has_parameters()
         model_bisim = stormpy.perform_bisimulation(model, formulas[0], stormpy.BisimulationType.STRONG)
         assert model_bisim.nr_states() == 80
         assert model_bisim.nr_transitions() == 120
         assert model_bisim.model_type() == stormpy.ModelType.DTMC
-        assert model_bisim.parametric()
+        assert model_bisim.has_parameters()

stormpy/tests/core/test_model.py

@@ -12,7 +12,7 @@ class TestModel:
         assert model.nr_states() == 13
         assert model.nr_transitions() == 20
         assert model.model_type() == stormpy.ModelType.DTMC
-        assert not model.parametric()
+        assert not model.supports_parameters()
         assert type(model) is stormpy.SparseDtmc
  
     def test_build_parametric_dtmc_from_prism_program(self):
@@ -27,7 +27,8 @@ class TestModel:
         assert model.nr_states() == 613
         assert model.nr_transitions() == 803
         assert model.model_type() == stormpy.ModelType.DTMC
-        assert model.parametric()
+        assert model.supports_parameters()
+        assert model.has_parameters()
         assert type(model) is stormpy.SparseParametricDtmc
     
     def test_build_dtmc(self):
@@ -37,7 +38,7 @@ class TestModel:
         assert model.nr_states() == 13
         assert model.nr_transitions() == 20
         assert model.model_type() == stormpy.ModelType.DTMC
-        assert not model.parametric()
+        assert not model.supports_parameters()
         assert type(model) is stormpy.SparseDtmc
     
     def test_build_parametric_dtmc(self):
@@ -47,5 +48,17 @@ class TestModel:
         assert model.nr_states() == 613
         assert model.nr_transitions() == 803
         assert model.model_type() == stormpy.ModelType.DTMC
-        assert model.parametric()
+        assert model.supports_parameters()
+        assert model.has_parameters()
+        assert type(model) is stormpy.SparseParametricDtmc
+    
+    def test_build_dtmc_supporting_parameters(self):
+        program = stormpy.parse_program("../examples/dtmc/die/die.pm")
+        formulas = stormpy.parse_formulas_for_program("P=? [ F \"one\" ]", program)
+        model = stormpy.build_parametric_model(program, formulas[0])
+        assert model.nr_states() == 13
+        assert model.nr_transitions() == 20
+        assert model.model_type() == stormpy.ModelType.DTMC
+        assert model.supports_parameters()
+        assert not model.has_parameters()
         assert type(model) is stormpy.SparseParametricDtmc

stormpy/tests/core/test_modelchecking.py

@@ -13,7 +13,7 @@ class TestModelChecking:
         assert model.nr_states() == 613
         assert model.nr_transitions() == 803
         assert model.model_type() == stormpy.ModelType.DTMC
-        assert model.parametric()
+        assert model.has_parameters()
         result = stormpy.perform_state_elimination(model, formulas[0])
         func = result.result_function
         one = pycarl.FactorizedPolynomial(pycarl.Rational(1))