From f2ad4781fec01fe12333d71622e91c5a3469243a Mon Sep 17 00:00:00 2001 From: Mavo Date: Fri, 13 May 2016 14:20:37 +0200 Subject: [PATCH] Distincting between supportsParameters and hasParameters Former-commit-id: a5d961f47089cc6aceef1105eb5e82e9d621d38f --- src/models/ModelBase.cpp | 12 +++++++-- src/models/ModelBase.h | 20 +++++++++++++-- src/models/sparse/Model.cpp | 25 ++++++++++++++++-- src/models/sparse/Model.h | 12 ++++++++- stormpy/lib/stormpy/__init__.py | 32 ++++++++++-------------- stormpy/src/core/model.cpp | 4 ++- stormpy/tests/core/test_bisimulation.py | 8 +++--- stormpy/tests/core/test_model.py | 21 +++++++++++++--- stormpy/tests/core/test_modelchecking.py | 2 +- 9 files changed, 100 insertions(+), 36 deletions(-) diff --git a/src/models/ModelBase.cpp b/src/models/ModelBase.cpp index 00a566b9b..92a2bb560 100644 --- a/src/models/ModelBase.cpp +++ b/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; } } -} \ No newline at end of file +} diff --git a/src/models/ModelBase.h b/src/models/ModelBase.h index 9fd80171a..eaa3c2b65 100644 --- a/src/models/ModelBase.h +++ b/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. diff --git a/src/models/sparse/Model.cpp b/src/models/sparse/Model.cpp index f0cf38e1c..265f0d8b0 100644 --- a/src/models/sparse/Model.cpp +++ b/src/models/sparse/Model.cpp @@ -311,10 +311,31 @@ namespace storm { } template - bool Model::isParametric() const { + bool Model::supportsParameters() const { return std::is_same::value; } + template + bool Model::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 + bool Model::isExact() const { + // TODO: change when dedicated data-structure for exact values is present + return this->supportsParameters(); + } + template std::unordered_map& Model::getRewardModels() { return this->rewardModels; @@ -342,4 +363,4 @@ namespace storm { } } -} \ No newline at end of file +} diff --git a/src/models/sparse/Model.h b/src/models/sparse/Model.h index a458bdff7..a73b10c8f 100644 --- a/src/models/sparse/Model.h +++ b/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); diff --git a/stormpy/lib/stormpy/__init__.py b/stormpy/lib/stormpy/__init__.py index 325d23a6f..ebcff7e99 100644 --- a/stormpy/lib/stormpy/__init__.py +++ b/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) diff --git a/stormpy/src/core/model.cpp b/stormpy/src/core/model.cpp index fe618618e..79f9dca4e 100644 --- a/stormpy/src/core/model.cpp +++ b/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>, "Get model as DTMC") .def("as_pdtmc", &storm::models::ModelBase::as>, "Get model as pDTMC") .def("as_mdp", &storm::models::ModelBase::as>, "Get model as MDP") diff --git a/stormpy/tests/core/test_bisimulation.py b/stormpy/tests/core/test_bisimulation.py index 2bd9bd974..5d74a2953 100644 --- a/stormpy/tests/core/test_bisimulation.py +++ b/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() diff --git a/stormpy/tests/core/test_model.py b/stormpy/tests/core/test_model.py index 843b4ff88..cd91abccc 100644 --- a/stormpy/tests/core/test_model.py +++ b/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 diff --git a/stormpy/tests/core/test_modelchecking.py b/stormpy/tests/core/test_modelchecking.py index 4bcb9a4e7..2c9b8caab 100644 --- a/stormpy/tests/core/test_modelchecking.py +++ b/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))