From ef09fab7168987a377c91b6da9794b52cf7de0a0 Mon Sep 17 00:00:00 2001 From: Matthias Volk Date: Tue, 8 Jan 2019 17:12:45 +0100 Subject: [PATCH 01/11] Better check if element name is already used --- src/storm-dft/builder/DFTBuilder.cpp | 7 +++--- src/storm-dft/builder/DFTBuilder.h | 36 ++++++++++++++++++---------- 2 files changed, 28 insertions(+), 15 deletions(-) diff --git a/src/storm-dft/builder/DFTBuilder.cpp b/src/storm-dft/builder/DFTBuilder.cpp index d3e635636..87bd5f407 100644 --- a/src/storm-dft/builder/DFTBuilder.cpp +++ b/src/storm-dft/builder/DFTBuilder.cpp @@ -140,7 +140,8 @@ namespace storm { if (children.size() <= 1) { STORM_LOG_ERROR("Sequence enforcers require at least two children"); } - if (mElements.count(name) != 0) { + if (nameInUse(name)) { + STORM_LOG_ERROR("Element with name '" << name << "' already exists."); return false; } DFTRestrictionPointer restr; @@ -166,8 +167,8 @@ namespace storm { template bool DFTBuilder::addStandardGate(std::string const& name, std::vector const& children, storm::storage::DFTElementType tp) { STORM_LOG_ASSERT(children.size() > 0, "No child for " << name); - if(mElements.count(name) != 0) { - // Element with that name already exists. + if (nameInUse(name)) { + STORM_LOG_ERROR("Element with name '" << name << "' already exists."); return false; } DFTElementPointer element; diff --git a/src/storm-dft/builder/DFTBuilder.h b/src/storm-dft/builder/DFTBuilder.h index 4d9f2652f..479db529c 100644 --- a/src/storm-dft/builder/DFTBuilder.h +++ b/src/storm-dft/builder/DFTBuilder.h @@ -93,8 +93,8 @@ namespace storm { if(children.size() <= 1) { STORM_LOG_ERROR("Dependencies require at least two children"); } - if(mElements.count(name) != 0) { - // Element with that name already exists. + if (nameInUse(name)) { + STORM_LOG_ERROR("Element with name '" << name << "' already exists."); return false; } @@ -122,13 +122,11 @@ namespace storm { if(binaryDependencies) { for (size_t i = 1; i < children.size(); ++i) { std::string nameDep = name + "_" + std::to_string(i); - if (mElements.count(nameDep) != 0) { - // Element with that name already exists. - STORM_LOG_ERROR("Element with name: " << nameDep << " already exists."); + if (nameInUse(nameDep)) { + STORM_LOG_ERROR("Element with name '" << name << "' already exists."); return false; } - STORM_LOG_ASSERT(storm::utility::isOne(probability) || children.size() == 2, - "PDep with multiple children supported."); + STORM_LOG_ASSERT(storm::utility::isOne(probability) || children.size() == 2, "PDep with multiple children supported."); DFTDependencyPointer element = std::make_shared>(mNextId++, nameDep, probability); mElements[element->name()] = element; mDependencyChildNames[element] = {trigger, children[i]}; @@ -146,8 +144,8 @@ namespace storm { bool addVotElement(std::string const& name, unsigned threshold, std::vector const& children) { STORM_LOG_ASSERT(children.size() > 0, "Has no child."); - if(mElements.count(name) != 0) { - STORM_LOG_ERROR("Element with name: " << name << " already exists."); + if (nameInUse(name)) { + STORM_LOG_ERROR("Element with name '" << name << "' already exists."); return false; } // It is an and-gate @@ -174,19 +172,33 @@ namespace storm { //TODO Matthias: collect constraints for SMT solving //failureRate > 0 //0 <= dormancyFactor <= 1 - STORM_LOG_ASSERT(mElements.find(name) == mElements.end(), "Element '" << name << "' already exists."); + if (nameInUse(name)) { + STORM_LOG_ERROR("Element with name '" << name << "' already exists."); + return false; + } mElements[name] = std::make_shared>(mNextId++, name, failureRate, dormancyFactor, transient); return true; } void addLayoutInfo(std::string const& name, double x, double y) { - STORM_LOG_ASSERT(mElements.count(name) > 0, "Element '" << name << "' not found."); + if (!nameInUse(name)) { + STORM_LOG_ERROR("Element with name '" << name << "' not found."); + } mLayoutInfo[name] = storm::storage::DFTLayoutInfo(x, y); } bool setTopLevel(std::string const& tle) { mTopLevelIdentifier = tle; - return mElements.count(tle) > 0; + return nameInUse(tle); + } + + /** + * Check whether the name is already used. + * @param name Element name. + * @return True iff name is already in use. + */ + bool nameInUse(std::string const& name) { + return mElements.find(name) != mElements.end(); } std::string getUniqueName(std::string name); From 32f757e4b4f26e18e4bee75c066dac59baafbc7d Mon Sep 17 00:00:00 2001 From: Matthias Volk Date: Tue, 8 Jan 2019 17:13:09 +0100 Subject: [PATCH 02/11] Fixed json export for FDEPs --- src/storm-dft/storage/dft/DftJsonExporter.cpp | 2 ++ 1 file changed, 2 insertions(+) diff --git a/src/storm-dft/storage/dft/DftJsonExporter.cpp b/src/storm-dft/storage/dft/DftJsonExporter.cpp index 4fa2a8937..6dd3d2299 100644 --- a/src/storm-dft/storage/dft/DftJsonExporter.cpp +++ b/src/storm-dft/storage/dft/DftJsonExporter.cpp @@ -80,6 +80,8 @@ namespace storm { std::stringstream stream; stream << dependency->probability(); nodeData["probability"] = stream.str(); + } else { + nodeData["type"] = "fdep"; } } else if (element->isBasicElement()) { // Set BE specific data From 09a5c44c6e55f16b7ecdb9d3a99920811d70bbe8 Mon Sep 17 00:00:00 2001 From: Matthias Volk Date: Thu, 24 Jan 2019 13:58:47 +0100 Subject: [PATCH 03/11] Fixed usage of denominatorAsNumber --- src/storm/analysis/GraphConditions.cpp | 10 ++++++---- 1 file changed, 6 insertions(+), 4 deletions(-) diff --git a/src/storm/analysis/GraphConditions.cpp b/src/storm/analysis/GraphConditions.cpp index 663bf2b52..c11fccb0b 100644 --- a/src/storm/analysis/GraphConditions.cpp +++ b/src/storm/analysis/GraphConditions.cpp @@ -38,9 +38,10 @@ namespace storm { auto const& transitionVars = entry.gatherVariables(); variableSet.insert(transitionVars.begin(), transitionVars.end()); if (entry.denominator().isConstant()) { - if (entry.denominatorAsNumber() > 0) { + assert(entry.denominator().constantPart() != 0); + if (entry.denominator().constantPart() > 0) { wellformedConstraintSet.emplace(entry.nominator().polynomialWithCoefficient(), storm::CompareRelation::GEQ); - } else if (entry.denominatorAsNumber() < 0) { + } else if (entry.denominator().constantPart() < 0) { wellformedConstraintSet.emplace(entry.nominator().polynomialWithCoefficient(), storm::CompareRelation::LEQ); } else { assert(false); // Should fail before. @@ -117,9 +118,10 @@ namespace storm { for (auto const& entry : rewModelEntry.second.getTransitionRewardMatrix()) { if(!entry.getValue().isConstant()) { if (entry.getValue().denominator().isConstant()) { - if (entry.getValue().denominatorAsNumber() > 0) { + assert(entry.getValue().denominator().constantPart() != 0); + if (entry.getValue().denominator().constantPart() > 0) { wellformedConstraintSet.emplace(entry.getValue().nominator().polynomialWithCoefficient(), storm::CompareRelation::GEQ); - } else if (entry.getValue().denominatorAsNumber() < 0) { + } else if (entry.getValue().denominator().constantPart() < 0) { wellformedConstraintSet.emplace(entry.getValue().nominator().polynomialWithCoefficient(), storm::CompareRelation::LEQ); } else { assert(false); // Should fail before. From 66ab97ba4f2c635162d43ef97cc189fdbb60ba03 Mon Sep 17 00:00:00 2001 From: TimQu Date: Tue, 29 Jan 2019 18:09:42 +0100 Subject: [PATCH 04/11] transformer: Added functionality to also translate expected time formulas to expected rewards. --- src/storm/api/transformation.h | 30 +++++++++++-------- .../ExpectedTimeToExpectedRewardVisitor.cpp | 28 +++++++++++++++++ .../ExpectedTimeToExpectedRewardVisitor.h | 25 ++++++++++++++++ ...ntinuousToDiscreteTimeModelTransformer.cpp | 19 ++++++++++-- ...ContinuousToDiscreteTimeModelTransformer.h | 8 ++++- 5 files changed, 95 insertions(+), 15 deletions(-) create mode 100644 src/storm/logic/ExpectedTimeToExpectedRewardVisitor.cpp create mode 100644 src/storm/logic/ExpectedTimeToExpectedRewardVisitor.h diff --git a/src/storm/api/transformation.h b/src/storm/api/transformation.h index c501c10cf..4c51e1fa4 100644 --- a/src/storm/api/transformation.h +++ b/src/storm/api/transformation.h @@ -13,21 +13,24 @@ namespace storm { /*! * Transforms the given continuous model to a discrete time model. - * If such a transformation does not preserve one of the given formulas, an error is issued. + * If such a transformation does not preserve one of the given formulas, a warning is issued. */ template - std::shared_ptr> transformContinuousToDiscreteTimeSparseModel(std::shared_ptr> const& model, std::vector> const& formulas) { + std::pair>, std::vector>> transformContinuousToDiscreteTimeSparseModel(std::shared_ptr> const& model, std::vector> const& formulas) { storm::transformer::ContinuousToDiscreteTimeModelTransformer transformer; - for (auto const& formula : formulas) { - STORM_LOG_THROW(transformer.preservesFormula(*formula), storm::exceptions::InvalidOperationException, "Transformation to discrete time model does not preserve formula " << *formula << "."); + std::string timeRewardName = "_time"; + while(model->hasRewardModel(timeRewardName)) { + timeRewardName += "_"; } + auto newFormulas = transformer.checkAndTransformFormulas(formulas, timeRewardName) + STORM_LOG_WARN_COND(newFormulas.size() == formulas.size(), "Transformation of a " << model->getType() << " to a discrete time model does not preserve all properties."); if (model->isOfType(storm::models::ModelType::Ctmc)) { - return transformer.transform(*model->template as>()); + return std::make_pair(transformer.transform(*model->template as>()), newFormulas); } else if (model->isOfType(storm::models::ModelType::MarkovAutomaton)) { - return transformer.transform(*model->template as>()); + return std::make_pair(transformer.transform(*model->template as>()), newFormulas); } else { STORM_LOG_THROW(false, storm::exceptions::NotSupportedException, "Transformation of a " << model->getType() << " to a discrete time model is not supported"); } @@ -40,18 +43,21 @@ namespace storm { * If such a transformation does not preserve one of the given formulas, an error is issued. */ template - std::shared_ptr> transformContinuousToDiscreteTimeSparseModel(storm::models::sparse::Model&& model, std::vector> const& formulas) { + std::pair>, std::vector>> transformContinuousToDiscreteTimeSparseModel(storm::models::sparse::Model&& model, std::vector> const& formulas) { storm::transformer::ContinuousToDiscreteTimeModelTransformer transformer; - for (auto const& formula : formulas) { - STORM_LOG_THROW(transformer.preservesFormula(*formula), storm::exceptions::InvalidOperationException, "Transformation to discrete time model does not preserve formula " << *formula << "."); + std::string timeRewardName = "_time"; + while(model.hasRewardModel(timeRewardName)) { + timeRewardName += "_"; } - + auto newFormulas = transformer.checkAndTransformFormulas(formulas, timeRewardName) + STORM_LOG_WARN_COND(newFormulas.size() == formulas.size(), "Transformation of a " << model->getType() << " to a discrete time model does not preserve all properties."); + if (model.isOfType(storm::models::ModelType::Ctmc)) { - return transformer.transform(std::move(*model.template as>())); + return std::make_pair(transformer.transform(std::move(*model.template as>())), newFormulas); } else if (model.isOfType(storm::models::ModelType::MarkovAutomaton)) { - return transformer.transform(std::move(*model.template as>())); + return std::make_pair(transformer.transform(std::move(*model.template as>())), newFormulas); } else { STORM_LOG_THROW(false, storm::exceptions::NotSupportedException, "Transformation of a " << model.getType() << " to a discrete time model is not supported."); } diff --git a/src/storm/logic/ExpectedTimeToExpectedRewardVisitor.cpp b/src/storm/logic/ExpectedTimeToExpectedRewardVisitor.cpp new file mode 100644 index 000000000..d240446a6 --- /dev/null +++ b/src/storm/logic/ExpectedTimeToExpectedRewardVisitor.cpp @@ -0,0 +1,28 @@ +#include "storm/logic/ExpectedTimeToExpectedRewardVisitor.h" +#include "storm/logic/Formulas.h" + +#include "storm/utility/macros.h" + +#include "storm/exceptions/InvalidPropertyException.h" + +namespace storm { + namespace logic { + + ExpectedTimeToExpectedRewardVisitor::ExpectedTimeToExpectedRewardVisitor(std::string const& timeRewardModelName) : timeRewardModelName(timeRewardModelName) { + // Intentionally left empty + } + + std::shared_ptr ExpectedTimeToExpectedRewardVisitor::substitute(Formula const& f) const { + boost::any result = f.accept(*this, boost::any()); + return boost::any_cast>(result); + } + + boost::any ExpectedTimeToExpectedRewardVisitor::visit(TimeOperatorFormula const& f, boost::any const& data) const { + STORM_LOG_THROW(f.getSubformula().isEventuallyFormula(), storm::exceptions::InvalidPropertyException, "Expected eventually formula within time operator. Got " << f << " instead."); + std::shared_ptr subsubformula = boost::any_cast>(f.getSubformula().asEventuallyFormula().getSubformula().accept(*this, data)); + STORM_LOG_THROW(f.getSubformula().isReachabilityTimeFormula(), storm::exceptions::InvalidPropertyException, "Expected time path formula within time operator. Got " << f << " instead."); + std::shared_ptr subformula = std::make_shared(subsubformula, storm::logic::FormulaContext::Reward); + return std::static_pointer_cast(std::make_shared(subformula, timeRewardModelName, f.getOperatorInformation())); + } + } +} diff --git a/src/storm/logic/ExpectedTimeToExpectedRewardVisitor.h b/src/storm/logic/ExpectedTimeToExpectedRewardVisitor.h new file mode 100644 index 000000000..b182a8520 --- /dev/null +++ b/src/storm/logic/ExpectedTimeToExpectedRewardVisitor.h @@ -0,0 +1,25 @@ +#pragma once + +#include + +#include "storm/logic/CloneVisitor.h" + +#include "storm/storage/expressions/Expression.h" + +namespace storm { + namespace logic { + + class ExpectedTimeToExpectedRewardVisitor : public CloneVisitor { + public: + ExpectedTimeToExpectedRewardVisitor(std::string const& timeRewardModelName); + + std::shared_ptr substitute(Formula const& f) const; + + virtual boost::any visit(TimeOperatorFormula const& f, boost::any const& data) const override; + + private: + std::string const& timeRewardModelName; + }; + + } +} diff --git a/src/storm/transformer/ContinuousToDiscreteTimeModelTransformer.cpp b/src/storm/transformer/ContinuousToDiscreteTimeModelTransformer.cpp index 20357f400..411c60821 100644 --- a/src/storm/transformer/ContinuousToDiscreteTimeModelTransformer.cpp +++ b/src/storm/transformer/ContinuousToDiscreteTimeModelTransformer.cpp @@ -5,7 +5,7 @@ #include "storm/models/sparse/StandardRewardModel.h" #include "storm/logic/Formulas.h" #include "storm/logic/FragmentSpecification.h" -#include "storm/logic/CloneVisitor.h" +#include "storm/logic/ExpectedTimeToExpectedRewardVisitor.h" #include "storm/utility/macros.h" #include "storm/utility/vector.h" @@ -93,7 +93,22 @@ namespace storm { fragment.setReachabilityRewardFormulasAllowed(true); return formula.isInFragment(fragment); } - + + template + std::vector> ContinuousToDiscreteTimeModelTransformer::checkAndTransformFormulas(std::vector> const& formulas, std::string const& timeRewardName) { + std::vector> result; + storm::logic::ExpectedTimeToExpectedRewardVisitor v(timeRewardName); + for (auto const& f : formulas) { + // Translate expected time formulas + auto newF = v.substitute(*f); + if(preservesFormula(*newF)) { + result.push_back(newF); + } else { + STORM_LOG_INFO("Continuous to discrete time transformation does not preserve formula " << *f); + } + } + return result; + } template std::shared_ptr> ContinuousToDiscreteTimeModelTransformer::transform(storm::models::sparse::MarkovAutomaton const& ma, boost::optional const& timeRewardModelName) { diff --git a/src/storm/transformer/ContinuousToDiscreteTimeModelTransformer.h b/src/storm/transformer/ContinuousToDiscreteTimeModelTransformer.h index d26b96c1f..b9e1d699a 100644 --- a/src/storm/transformer/ContinuousToDiscreteTimeModelTransformer.h +++ b/src/storm/transformer/ContinuousToDiscreteTimeModelTransformer.h @@ -18,7 +18,13 @@ namespace storm { // If this method returns true, the given formula is preserced by the transformation static bool preservesFormula(storm::logic::Formula const& formula); - + + // Checks whether the given formulas are preserved. + // Expected time formulas are translated to expected reward formulas. + // The returned vector only contains formulas that are preserved by the transformation. + static std::vector> checkAndTransformFormulas(std::vector> const& formulas, std::string const& timeRewardName); + + // Transforms the given CTMC to its underlying (aka embedded) DTMC. // A reward model for time is added if a corresponding reward model name is given static std::shared_ptr> transform(storm::models::sparse::Ctmc const& ctmc, boost::optional const& timeRewardModelName = boost::none); From dfd1fec8c591b8e7e85fc0e2268046aa7ef71920 Mon Sep 17 00:00:00 2001 From: Matthias Volk Date: Tue, 29 Jan 2019 20:46:27 +0100 Subject: [PATCH 05/11] Fixed compile issues --- src/storm-pars-cli/storm-pars.cpp | 2 +- src/storm-pars/api/region.h | 4 ++-- src/storm/api/transformation.h | 10 +++++----- 3 files changed, 8 insertions(+), 8 deletions(-) diff --git a/src/storm-pars-cli/storm-pars.cpp b/src/storm-pars-cli/storm-pars.cpp index 4495f26c1..bf3ac8f38 100644 --- a/src/storm-pars-cli/storm-pars.cpp +++ b/src/storm-pars-cli/storm-pars.cpp @@ -145,7 +145,7 @@ namespace storm { } if (parametricSettings.transformContinuousModel() && (result.first->isOfType(storm::models::ModelType::Ctmc) || result.first->isOfType(storm::models::ModelType::MarkovAutomaton))) { - result.first = storm::api::transformContinuousToDiscreteTimeSparseModel(std::move(*result.first->template as>()), storm::api::extractFormulasFromProperties(input.properties)); + result.first = storm::api::transformContinuousToDiscreteTimeSparseModel(std::move(*result.first->template as>()), storm::api::extractFormulasFromProperties(input.properties)).first; result.second = true; } diff --git a/src/storm-pars/api/region.h b/src/storm-pars/api/region.h index ee8d44bff..c032426e5 100644 --- a/src/storm-pars/api/region.h +++ b/src/storm-pars/api/region.h @@ -91,7 +91,7 @@ namespace storm { if (consideredModel->isOfType(storm::models::ModelType::Ctmc) || consideredModel->isOfType(storm::models::ModelType::MarkovAutomaton)) { STORM_LOG_WARN("Parameter lifting not supported for continuous time models. Transforming continuous model to discrete model..."); std::vector> taskFormulaAsVector { task.getFormula().asSharedPointer() }; - consideredModel = storm::api::transformContinuousToDiscreteTimeSparseModel(consideredModel, taskFormulaAsVector); + consideredModel = storm::api::transformContinuousToDiscreteTimeSparseModel(consideredModel, taskFormulaAsVector).first; STORM_LOG_THROW(consideredModel->isOfType(storm::models::ModelType::Dtmc) || consideredModel->isOfType(storm::models::ModelType::Mdp), storm::exceptions::UnexpectedException, "Transformation to discrete time model has failed."); } @@ -121,7 +121,7 @@ namespace storm { if (consideredModel->isOfType(storm::models::ModelType::Ctmc) || consideredModel->isOfType(storm::models::ModelType::MarkovAutomaton)) { STORM_LOG_WARN("Parameter lifting not supported for continuous time models. Transforming continuous model to discrete model..."); std::vector> taskFormulaAsVector { task.getFormula().asSharedPointer() }; - consideredModel = storm::api::transformContinuousToDiscreteTimeSparseModel(consideredModel, taskFormulaAsVector); + consideredModel = storm::api::transformContinuousToDiscreteTimeSparseModel(consideredModel, taskFormulaAsVector).first; STORM_LOG_THROW(consideredModel->isOfType(storm::models::ModelType::Dtmc) || consideredModel->isOfType(storm::models::ModelType::Mdp), storm::exceptions::UnexpectedException, "Transformation to discrete time model has failed."); } diff --git a/src/storm/api/transformation.h b/src/storm/api/transformation.h index 4c51e1fa4..d2a84d9f7 100644 --- a/src/storm/api/transformation.h +++ b/src/storm/api/transformation.h @@ -24,7 +24,7 @@ namespace storm { while(model->hasRewardModel(timeRewardName)) { timeRewardName += "_"; } - auto newFormulas = transformer.checkAndTransformFormulas(formulas, timeRewardName) + auto newFormulas = transformer.checkAndTransformFormulas(formulas, timeRewardName); STORM_LOG_WARN_COND(newFormulas.size() == formulas.size(), "Transformation of a " << model->getType() << " to a discrete time model does not preserve all properties."); if (model->isOfType(storm::models::ModelType::Ctmc)) { @@ -34,7 +34,7 @@ namespace storm { } else { STORM_LOG_THROW(false, storm::exceptions::NotSupportedException, "Transformation of a " << model->getType() << " to a discrete time model is not supported"); } - return nullptr; + return std::make_pair(nullptr, newFormulas);; } /*! @@ -51,8 +51,8 @@ namespace storm { while(model.hasRewardModel(timeRewardName)) { timeRewardName += "_"; } - auto newFormulas = transformer.checkAndTransformFormulas(formulas, timeRewardName) - STORM_LOG_WARN_COND(newFormulas.size() == formulas.size(), "Transformation of a " << model->getType() << " to a discrete time model does not preserve all properties."); + auto newFormulas = transformer.checkAndTransformFormulas(formulas, timeRewardName); + STORM_LOG_WARN_COND(newFormulas.size() == formulas.size(), "Transformation of a " << model.getType() << " to a discrete time model does not preserve all properties."); if (model.isOfType(storm::models::ModelType::Ctmc)) { return std::make_pair(transformer.transform(std::move(*model.template as>())), newFormulas); @@ -61,7 +61,7 @@ namespace storm { } else { STORM_LOG_THROW(false, storm::exceptions::NotSupportedException, "Transformation of a " << model.getType() << " to a discrete time model is not supported."); } - return nullptr; + return std::make_pair(nullptr, newFormulas);; } From 267efd692afa08cf710161311735a5f9e9aeffea Mon Sep 17 00:00:00 2001 From: Matthias Volk Date: Tue, 29 Jan 2019 21:12:24 +0100 Subject: [PATCH 06/11] Construct time reward model --- src/storm/api/transformation.h | 8 ++++---- 1 file changed, 4 insertions(+), 4 deletions(-) diff --git a/src/storm/api/transformation.h b/src/storm/api/transformation.h index d2a84d9f7..0fb25b2f2 100644 --- a/src/storm/api/transformation.h +++ b/src/storm/api/transformation.h @@ -28,9 +28,9 @@ namespace storm { STORM_LOG_WARN_COND(newFormulas.size() == formulas.size(), "Transformation of a " << model->getType() << " to a discrete time model does not preserve all properties."); if (model->isOfType(storm::models::ModelType::Ctmc)) { - return std::make_pair(transformer.transform(*model->template as>()), newFormulas); + return std::make_pair(transformer.transform(*model->template as>(), timeRewardName), newFormulas); } else if (model->isOfType(storm::models::ModelType::MarkovAutomaton)) { - return std::make_pair(transformer.transform(*model->template as>()), newFormulas); + return std::make_pair(transformer.transform(*model->template as>(), timeRewardName), newFormulas); } else { STORM_LOG_THROW(false, storm::exceptions::NotSupportedException, "Transformation of a " << model->getType() << " to a discrete time model is not supported"); } @@ -55,9 +55,9 @@ namespace storm { STORM_LOG_WARN_COND(newFormulas.size() == formulas.size(), "Transformation of a " << model.getType() << " to a discrete time model does not preserve all properties."); if (model.isOfType(storm::models::ModelType::Ctmc)) { - return std::make_pair(transformer.transform(std::move(*model.template as>())), newFormulas); + return std::make_pair(transformer.transform(std::move(*model.template as>()), timeRewardName), newFormulas); } else if (model.isOfType(storm::models::ModelType::MarkovAutomaton)) { - return std::make_pair(transformer.transform(std::move(*model.template as>())), newFormulas); + return std::make_pair(transformer.transform(std::move(*model.template as>()), timeRewardName), newFormulas); } else { STORM_LOG_THROW(false, storm::exceptions::NotSupportedException, "Transformation of a " << model.getType() << " to a discrete time model is not supported."); } From 399c0610863a56511bee4a1c0079b14f67194cfd Mon Sep 17 00:00:00 2001 From: Matthias Volk Date: Tue, 29 Jan 2019 21:12:34 +0100 Subject: [PATCH 07/11] Typos --- src/storm-parsers/parser/DirectEncodingParser.cpp | 4 ++-- .../transformer/ContinuousToDiscreteTimeModelTransformer.h | 2 +- 2 files changed, 3 insertions(+), 3 deletions(-) diff --git a/src/storm-parsers/parser/DirectEncodingParser.cpp b/src/storm-parsers/parser/DirectEncodingParser.cpp index 160ada212..5e4eee7ab 100644 --- a/src/storm-parsers/parser/DirectEncodingParser.cpp +++ b/src/storm-parsers/parser/DirectEncodingParser.cpp @@ -106,13 +106,13 @@ namespace storm { // Initialize auto modelComponents = std::make_shared>(); bool nonDeterministic = (type == storm::models::ModelType::Mdp || type == storm::models::ModelType::MarkovAutomaton || type == storm::models::ModelType::Pomdp); - bool continousTime = (type == storm::models::ModelType::Ctmc || type == storm::models::ModelType::MarkovAutomaton); + bool continuousTime = (type == storm::models::ModelType::Ctmc || type == storm::models::ModelType::MarkovAutomaton); storm::storage::SparseMatrixBuilder builder = storm::storage::SparseMatrixBuilder(0, 0, 0, false, nonDeterministic, 0); modelComponents->stateLabeling = storm::models::sparse::StateLabeling(stateSize); modelComponents->observabilityClasses = std::vector(); modelComponents->observabilityClasses->resize(stateSize); std::vector> stateRewards; - if (continousTime) { + if (continuousTime) { modelComponents->exitRates = std::vector(stateSize); if (type == storm::models::ModelType::MarkovAutomaton) { modelComponents->markovianStates = storm::storage::BitVector(stateSize); diff --git a/src/storm/transformer/ContinuousToDiscreteTimeModelTransformer.h b/src/storm/transformer/ContinuousToDiscreteTimeModelTransformer.h index b9e1d699a..26a95fdd8 100644 --- a/src/storm/transformer/ContinuousToDiscreteTimeModelTransformer.h +++ b/src/storm/transformer/ContinuousToDiscreteTimeModelTransformer.h @@ -16,7 +16,7 @@ namespace storm { class ContinuousToDiscreteTimeModelTransformer { public: - // If this method returns true, the given formula is preserced by the transformation + // If this method returns true, the given formula is preserved by the transformation static bool preservesFormula(storm::logic::Formula const& formula); // Checks whether the given formulas are preserved. From a1c5aa946c9d078aa328f18e0a16ddb70aed61f9 Mon Sep 17 00:00:00 2001 From: Matthias Volk Date: Wed, 30 Jan 2019 12:49:39 +0100 Subject: [PATCH 08/11] Integrated symbolic verification of parametric systems into storm-pars --- src/storm-pars-cli/storm-pars.cpp | 59 +++++++++++++++++++++++++++---- 1 file changed, 52 insertions(+), 7 deletions(-) diff --git a/src/storm-pars-cli/storm-pars.cpp b/src/storm-pars-cli/storm-pars.cpp index bf3ac8f38..f9de0c8d4 100644 --- a/src/storm-pars-cli/storm-pars.cpp +++ b/src/storm-pars-cli/storm-pars.cpp @@ -154,12 +154,14 @@ namespace storm { template std::pair, bool> preprocessDdModel(std::shared_ptr> const& model, SymbolicInput const& input) { - - std::pair, bool> result = std::make_pair(model, false); - auto coreSettings = storm::settings::getModule(); + auto generalSettings = storm::settings::getModule(); + auto bisimulationSettings = storm::settings::getModule(); + + std::pair, bool> result = std::make_pair(model, false); + if (coreSettings.getEngine() == storm::settings::modules::CoreSettings::Engine::Hybrid) { - // Currently, hybrid engine for parametric models just referrs to building the model symbolically. + // Currently, hybrid engine for parametric models just refers to building the model symbolically. STORM_LOG_INFO("Translating symbolic model to sparse model..."); result.first = storm::api::transformSymbolicToSparseModel(model); result.second = true; @@ -168,6 +170,13 @@ namespace storm { if (sparsePreprocessingResult.second) { result.first = sparsePreprocessingResult.first; } + } else { + STORM_LOG_ASSERT(coreSettings.getEngine() == storm::settings::modules::CoreSettings::Engine::Dd, "Expected Dd engine."); + if (generalSettings.isBisimulationSet()) { + STORM_LOG_THROW(false, storm::exceptions::NotSupportedException, "Bisimulation is not supported for symbolic parametric models."); + //result.first = storm::cli::preprocessDdModelBisimulation(result.first->template as>(), input, bisimulationSettings); + //result.second = true; + } } return result; } @@ -461,11 +470,47 @@ namespace storm { } } } - + + template + void verifyPropertiesWithSymbolicEngine(std::shared_ptr> const& model, SymbolicInput const& input, SampleInformation const& samples) { + if (samples.empty()) { + verifyProperties(input.properties, + [&model] (std::shared_ptr const& formula) { + std::unique_ptr result = storm::api::verifyWithDdEngine(model, storm::api::createTask(formula, true)); + if (result) { + result->filter(storm::modelchecker::SymbolicQualitativeCheckResult(model->getReachableStates(), model->getInitialStates())); + } + return result; + }, + [&model] (std::unique_ptr const& result) { + auto parametricSettings = storm::settings::getModule(); + if (parametricSettings.exportResultToFile() && model->isOfType(storm::models::ModelType::Dtmc)) { + //auto dtmc = model->template as>(); + //boost::optional rationalFunction = result->asSymbolicQuantitativeCheckResult().sum(); + //storm::api::exportParametricResultToFile(rationalFunction, storm::analysis::ConstraintCollector(*dtmc), parametricSettings.exportResultPath()); + } + }); + } else { + STORM_LOG_THROW(false, storm::exceptions::NotSupportedException, "Sampling is not supported in the symbolic engine."); + } + } + + template + void verifyWithDdEngine(std::shared_ptr> const& model, SymbolicInput const& input, std::vector> const& regions, SampleInformation const& samples) { + if (regions.empty()) { + storm::pars::verifyPropertiesWithSymbolicEngine(model, input, samples); + } else { + STORM_LOG_THROW(false, storm::exceptions::NotSupportedException, "Region verification is not supported in the symbolic engine."); + } + } + template void verifyParametricModel(std::shared_ptr const& model, SymbolicInput const& input, std::vector> const& regions, SampleInformation const& samples) { - STORM_LOG_ASSERT(model->isSparseModel(), "Unexpected model type."); - storm::pars::verifyWithSparseEngine(model->as>(), input, regions, samples); + if (model->isSparseModel()) { + storm::pars::verifyWithSparseEngine(model->as>(), input, regions, samples); + } else { + storm::pars::verifyWithDdEngine(model->as>(), input, regions, samples); + } } template From b2ea3993ef168d5c9766ae583c7c54aa0dccc3e2 Mon Sep 17 00:00:00 2001 From: Matthias Volk Date: Wed, 30 Jan 2019 22:04:58 +0100 Subject: [PATCH 09/11] Fixed assertion in symbolic bisimulation --- src/storm/storage/dd/bisimulation/QuotientExtractor.cpp | 2 ++ 1 file changed, 2 insertions(+) diff --git a/src/storm/storage/dd/bisimulation/QuotientExtractor.cpp b/src/storm/storage/dd/bisimulation/QuotientExtractor.cpp index 1ba224331..36f7f1fe3 100644 --- a/src/storm/storage/dd/bisimulation/QuotientExtractor.cpp +++ b/src/storm/storage/dd/bisimulation/QuotientExtractor.cpp @@ -998,6 +998,8 @@ namespace storm { // Check quotient matrix for sanity. if (std::is_same::value) { STORM_LOG_ASSERT(quotientTransitionMatrix.greater(storm::utility::one()).isZero(), "Illegal entries in quotient matrix."); + } else if (std::is_same::value) { + // No comparison for rational functions } else { STORM_LOG_ASSERT(quotientTransitionMatrix.greater(storm::utility::one() + storm::utility::convertNumber(1e-6)).isZero(), "Illegal entries in quotient matrix."); } From 374071670a4e5f4d87f2ceb67af0a143ea69f3b1 Mon Sep 17 00:00:00 2001 From: Matthias Volk Date: Wed, 30 Jan 2019 22:05:20 +0100 Subject: [PATCH 10/11] Activated symbolic bisimulation for parametric models --- src/storm-pars-cli/storm-pars.cpp | 5 ++--- 1 file changed, 2 insertions(+), 3 deletions(-) diff --git a/src/storm-pars-cli/storm-pars.cpp b/src/storm-pars-cli/storm-pars.cpp index f9de0c8d4..e522f0baf 100644 --- a/src/storm-pars-cli/storm-pars.cpp +++ b/src/storm-pars-cli/storm-pars.cpp @@ -173,9 +173,8 @@ namespace storm { } else { STORM_LOG_ASSERT(coreSettings.getEngine() == storm::settings::modules::CoreSettings::Engine::Dd, "Expected Dd engine."); if (generalSettings.isBisimulationSet()) { - STORM_LOG_THROW(false, storm::exceptions::NotSupportedException, "Bisimulation is not supported for symbolic parametric models."); - //result.first = storm::cli::preprocessDdModelBisimulation(result.first->template as>(), input, bisimulationSettings); - //result.second = true; + result.first = storm::cli::preprocessDdModelBisimulation(result.first->template as>(), input, bisimulationSettings); + result.second = true; } } return result; From bcde728c3c87abe2a2bfa15ca2c23b6356f75cd2 Mon Sep 17 00:00:00 2001 From: Matthias Volk Date: Wed, 30 Jan 2019 22:14:42 +0100 Subject: [PATCH 11/11] Transform formulas to deterministic-time as well --- src/storm-pars-cli/storm-pars.cpp | 80 ++++++++++++++++++++----------- 1 file changed, 53 insertions(+), 27 deletions(-) diff --git a/src/storm-pars-cli/storm-pars.cpp b/src/storm-pars-cli/storm-pars.cpp index e522f0baf..b001381b7 100644 --- a/src/storm-pars-cli/storm-pars.cpp +++ b/src/storm-pars-cli/storm-pars.cpp @@ -45,6 +45,16 @@ namespace storm { bool graphPreserving; bool exact; }; + + struct PreprocessResult { + PreprocessResult(std::shared_ptr const& model, bool changed) : changed(changed), model(model) { + // Intentionally left empty. + } + + bool changed; + std::shared_ptr model; + boost::optional>> formulas; + }; template std::vector> parseRegions(std::shared_ptr const& model) { @@ -127,72 +137,76 @@ namespace storm { } template - std::pair, bool> preprocessSparseModel(std::shared_ptr> const& model, SymbolicInput const& input) { + PreprocessResult preprocessSparseModel(std::shared_ptr> const& model, SymbolicInput const& input) { auto generalSettings = storm::settings::getModule(); auto bisimulationSettings = storm::settings::getModule(); auto parametricSettings = storm::settings::getModule(); - std::pair, bool> result = std::make_pair(model, false); + PreprocessResult result(model, false); - if (result.first->isOfType(storm::models::ModelType::MarkovAutomaton)) { - result.first = storm::cli::preprocessSparseMarkovAutomaton(result.first->template as>()); - result.second = true; + if (result.model->isOfType(storm::models::ModelType::MarkovAutomaton)) { + result.model = storm::cli::preprocessSparseMarkovAutomaton(result.model->template as>()); + result.changed = true; } if (generalSettings.isBisimulationSet()) { - result.first = storm::cli::preprocessSparseModelBisimulation(result.first->template as>(), input, bisimulationSettings); - result.second = true; + result.model = storm::cli::preprocessSparseModelBisimulation(result.model->template as>(), input, bisimulationSettings); + result.changed = true; } - if (parametricSettings.transformContinuousModel() && (result.first->isOfType(storm::models::ModelType::Ctmc) || result.first->isOfType(storm::models::ModelType::MarkovAutomaton))) { - result.first = storm::api::transformContinuousToDiscreteTimeSparseModel(std::move(*result.first->template as>()), storm::api::extractFormulasFromProperties(input.properties)).first; - result.second = true; + if (parametricSettings.transformContinuousModel() && (model->isOfType(storm::models::ModelType::Ctmc) || model->isOfType(storm::models::ModelType::MarkovAutomaton))) { + auto transformResult = storm::api::transformContinuousToDiscreteTimeSparseModel(std::move(*model->template as>()), storm::api::extractFormulasFromProperties(input.properties)); + result.model = transformResult.first; + // Set transformed properties as new properties in input + result.formulas = transformResult.second; + result.changed = true; } return result; } template - std::pair, bool> preprocessDdModel(std::shared_ptr> const& model, SymbolicInput const& input) { + PreprocessResult preprocessDdModel(std::shared_ptr> const& model, SymbolicInput const& input) { auto coreSettings = storm::settings::getModule(); auto generalSettings = storm::settings::getModule(); auto bisimulationSettings = storm::settings::getModule(); - std::pair, bool> result = std::make_pair(model, false); + PreprocessResult result(model, false); if (coreSettings.getEngine() == storm::settings::modules::CoreSettings::Engine::Hybrid) { // Currently, hybrid engine for parametric models just refers to building the model symbolically. STORM_LOG_INFO("Translating symbolic model to sparse model..."); - result.first = storm::api::transformSymbolicToSparseModel(model); - result.second = true; + result.model = storm::api::transformSymbolicToSparseModel(model); + result.changed = true; // Invoke preprocessing on the sparse model - auto sparsePreprocessingResult = storm::pars::preprocessSparseModel(result.first->as>(), input); - if (sparsePreprocessingResult.second) { - result.first = sparsePreprocessingResult.first; + PreprocessResult sparsePreprocessingResult = storm::pars::preprocessSparseModel(result.model->as>(), input); + if (sparsePreprocessingResult.changed) { + result.model = sparsePreprocessingResult.model; + result.formulas = sparsePreprocessingResult.formulas; } } else { STORM_LOG_ASSERT(coreSettings.getEngine() == storm::settings::modules::CoreSettings::Engine::Dd, "Expected Dd engine."); if (generalSettings.isBisimulationSet()) { - result.first = storm::cli::preprocessDdModelBisimulation(result.first->template as>(), input, bisimulationSettings); - result.second = true; + result.model = storm::cli::preprocessDdModelBisimulation(result.model->template as>(), input, bisimulationSettings); + result.changed = true; } } return result; } template - std::pair, bool> preprocessModel(std::shared_ptr const& model, SymbolicInput const& input) { + PreprocessResult preprocessModel(std::shared_ptr const& model, SymbolicInput const& input) { storm::utility::Stopwatch preprocessingWatch(true); - - std::pair, bool> result = std::make_pair(model, false); + + PreprocessResult result(model, false); if (model->isSparseModel()) { - result = storm::pars::preprocessSparseModel(result.first->as>(), input); + result = storm::pars::preprocessSparseModel(result.model->as>(), input); } else { STORM_LOG_ASSERT(model->isSymbolicModel(), "Unexpected model type."); - result = storm::pars::preprocessDdModel(result.first->as>(), input); + result = storm::pars::preprocessDdModel(result.model->as>(), input); } - if (result.second) { + if (result.changed) { STORM_PRINT_AND_LOG(std::endl << "Time for model preprocessing: " << preprocessingWatch << "." << std::endl << std::endl); } return result; @@ -536,8 +550,20 @@ namespace storm { if (model) { auto preprocessingResult = storm::pars::preprocessModel(model, input); - if (preprocessingResult.second) { - model = preprocessingResult.first; + if (preprocessingResult.changed) { + model = preprocessingResult.model; + + if (preprocessingResult.formulas) { + std::vector newProperties; + for (size_t i = 0; i < preprocessingResult.formulas.get().size(); ++i) { + auto formula = preprocessingResult.formulas.get().at(i); + STORM_LOG_ASSERT(i < input.properties.size(), "Index " << i << " greater than number of properties."); + storm::jani::Property property = input.properties.at(i); + newProperties.push_back(storm::jani::Property(property.getName(), formula, property.getUndefinedConstants(), property.getComment())); + } + input.properties = newProperties; + } + model->printModelInformationToStream(std::cout); } }