From 5c7d3db7437a2d488b8fd5df678251c6d7eeb8d3 Mon Sep 17 00:00:00 2001 From: Sebastian Junges Date: Mon, 15 May 2017 21:42:16 +0200 Subject: [PATCH] towards proper side constraints for parametetric systems --- src/storm/adapters/CarlAdapter.h | 1 + src/storm/analysis/GraphConditions.cpp | 63 ++++++++++++++++++++++ src/storm/analysis/GraphConditions.h | 75 ++++++++++++++++++++++++++ src/storm/cli/entrypoints.h | 8 ++- src/storm/models/sparse/Dtmc.cpp | 42 +-------------- src/storm/models/sparse/Dtmc.h | 54 +------------------ src/storm/utility/storm.h | 14 +++-- 7 files changed, 154 insertions(+), 103 deletions(-) create mode 100644 src/storm/analysis/GraphConditions.cpp create mode 100644 src/storm/analysis/GraphConditions.h diff --git a/src/storm/adapters/CarlAdapter.h b/src/storm/adapters/CarlAdapter.h index 27aa37960..642822b68 100644 --- a/src/storm/adapters/CarlAdapter.h +++ b/src/storm/adapters/CarlAdapter.h @@ -9,6 +9,7 @@ #include #include #include +#include namespace carl { // Define hash values for all polynomials and rational function. diff --git a/src/storm/analysis/GraphConditions.cpp b/src/storm/analysis/GraphConditions.cpp new file mode 100644 index 000000000..063c963b1 --- /dev/null +++ b/src/storm/analysis/GraphConditions.cpp @@ -0,0 +1,63 @@ + +#include "GraphConditions.h" +#include "storm/utility/constants.h" +#include "storm/exceptions/NotImplementedException.h" + +namespace storm { + namespace analysis { + template + ConstraintCollector::ConstraintCollector(storm::models::sparse::Dtmc const& dtmc) { + process(dtmc); + } + + template + std::unordered_set::val> const& ConstraintCollector::getWellformedConstraints() const { + return this->wellformedConstraintSet; + } + + template + std::unordered_set::val> const& ConstraintCollector::getGraphPreservingConstraints() const { + return this->graphPreservingConstraintSet; + } + + template + void ConstraintCollector::process(storm::models::sparse::Dtmc const& dtmc) { + for(uint_fast64_t state = 0; state < dtmc.getNumberOfStates(); ++state) { + ValueType sum = storm::utility::zero(); + for (auto const& transition : dtmc.getRows(state)) { + sum += transition.getValue(); + if (!storm::utility::isConstant(transition.getValue())) { + if (transition.getValue().denominator().isConstant()) { + if (transition.getValue().denominatorAsNumber() > 0) { + wellformedConstraintSet.emplace((transition.getValue().nominator() - transition.getValue().denominator()).polynomial(), storm::CompareRelation::LEQ); + wellformedConstraintSet.emplace(transition.getValue().nominator().polynomial(), storm::CompareRelation::GEQ); + } else if (transition.getValue().denominatorAsNumber() < 0) { + wellformedConstraintSet.emplace((transition.getValue().nominator() - transition.getValue().denominator()).polynomial(), storm::CompareRelation::GEQ); + wellformedConstraintSet.emplace(transition.getValue().nominator().polynomial(), storm::CompareRelation::LEQ); + } else { + assert(false); // Should fail before. + } + } else { + wellformedConstraintSet.emplace(transition.getValue().denominator().polynomial(), storm::CompareRelation::NEQ); + STORM_LOG_THROW(false, storm::exceptions::NotImplementedException, "Rational functions at edges not yet supported."); + } + graphPreservingConstraintSet.emplace(transition.getValue().nominator().polynomial(), storm::CompareRelation::NEQ); + } + } + STORM_LOG_ASSERT(!storm::utility::isConstant(sum) || storm::utility::isOne(sum), "If the sum is a constant, it must be equal to 1."); + if(!storm::utility::isConstant(sum)) { + wellformedConstraintSet.emplace((sum.nominator() - sum.denominator()).polynomial(), storm::CompareRelation::EQ); + } + + } + } + + template + void ConstraintCollector::operator()(storm::models::sparse::Dtmc const& dtmc) { + process(dtmc); + } + + + template class ConstraintCollector; + } +} \ No newline at end of file diff --git a/src/storm/analysis/GraphConditions.h b/src/storm/analysis/GraphConditions.h new file mode 100644 index 000000000..14bdd994f --- /dev/null +++ b/src/storm/analysis/GraphConditions.h @@ -0,0 +1,75 @@ +#pragma once + +#include +#include +#include "storm/adapters/CarlAdapter.h" +#include "storm/models/sparse/Dtmc.h" + +namespace storm { + namespace analysis { + +template +struct ConstraintType { + typedef storm::ArithConstraint val; +}; + +template +struct ConstraintType::value>::type> { + typedef carl::Formula val; +}; + +/** + * Class to collect constraints on parametric Markov chains. + */ +template +class ConstraintCollector { +private: + // A set of constraints that says that the DTMC actually has valid probability distributions in all states. + std::unordered_set::val> wellformedConstraintSet; + + // A set of constraints that makes sure that the underlying graph of the model does not change depending + // on the parameter values. + std::unordered_set::val> graphPreservingConstraintSet; + +public: + /*! + * Constructs the a constraint collector for the given DTMC. The constraints are built and ready for + * retrieval after the construction. + * + * @param dtmc The DTMC for which to create the constraints. + */ + ConstraintCollector(storm::models::sparse::Dtmc const& dtmc); + + /*! + * Returns the set of wellformed-ness constraints. + * + * @return The set of wellformed-ness constraints. + */ + std::unordered_set::val> const& getWellformedConstraints() const; + + /*! + * Returns the set of graph-preserving constraints. + * + * @return The set of graph-preserving constraints. + */ + std::unordered_set::val> const& getGraphPreservingConstraints() const; + + /*! + * Constructs the constraints for the given DTMC. + * + * @param dtmc The DTMC for which to create the constraints. + */ + void process(storm::models::sparse::Dtmc const& dtmc); + + /*! + * Constructs the constraints for the given DTMC by calling the process method. + * + * @param dtmc The DTMC for which to create the constraints. + */ + void operator()(storm::models::sparse::Dtmc const& dtmc); + +}; + + + } +} \ No newline at end of file diff --git a/src/storm/cli/entrypoints.h b/src/storm/cli/entrypoints.h index c5baa8287..b43db8bd9 100644 --- a/src/storm/cli/entrypoints.h +++ b/src/storm/cli/entrypoints.h @@ -1,10 +1,10 @@ -#ifndef STORM_ENTRYPOINTS_H_H -#define STORM_ENTRYPOINTS_H_H +#pragma once #include #include "storm/utility/storm.h" +#include "storm/analysis/GraphConditions.h" #include "storm/storage/SymbolicModelDescription.h" #include "storm/utility/DirectEncodingExporter.h" #include "storm/utility/Stopwatch.h" @@ -112,7 +112,7 @@ namespace storm { } if (storm::settings::getModule().exportResultToFile()) { - exportParametricResultToFile(result->asExplicitQuantitativeCheckResult()[*model->getInitialStates().begin()], storm::models::sparse::Dtmc::ConstraintCollector(*(model->template as>())), storm::settings::getModule().exportResultPath()); + exportParametricResultToFile(result->asExplicitQuantitativeCheckResult()[*model->getInitialStates().begin()], storm::analysis::ConstraintCollector(*(model->template as>())), storm::settings::getModule().exportResultPath()); } } } @@ -469,5 +469,3 @@ namespace storm { } } - -#endif //STORM_ENTRYPOINTS_H_H diff --git a/src/storm/models/sparse/Dtmc.cpp b/src/storm/models/sparse/Dtmc.cpp index c61afdaf9..319a06ee9 100644 --- a/src/storm/models/sparse/Dtmc.cpp +++ b/src/storm/models/sparse/Dtmc.cpp @@ -25,47 +25,7 @@ namespace storm { STORM_LOG_THROW(probabilityMatrix.isProbabilistic(), storm::exceptions::InvalidArgumentException, "The probability matrix is invalid."); } -#ifdef STORM_HAVE_CARL - template - Dtmc::ConstraintCollector::ConstraintCollector(Dtmc const& dtmc) { - process(dtmc); - } - - template - std::unordered_set> const& Dtmc::ConstraintCollector::getWellformedConstraints() const { - return this->wellformedConstraintSet; - } - - template - std::unordered_set> const& Dtmc::ConstraintCollector::getGraphPreservingConstraints() const { - return this->graphPreservingConstraintSet; - } - - template - void Dtmc::ConstraintCollector::process(storm::models::sparse::Dtmc const& dtmc) { - for(uint_fast64_t state = 0; state < dtmc.getNumberOfStates(); ++state) { - ValueType sum = storm::utility::zero(); - for (auto const& transition : dtmc.getRows(state)) { - sum += transition.getValue(); - if (!storm::utility::isConstant(transition.getValue())) { - wellformedConstraintSet.emplace(transition.getValue() - 1, storm::CompareRelation::LEQ); - wellformedConstraintSet.emplace(transition.getValue(), storm::CompareRelation::GEQ); - graphPreservingConstraintSet.emplace(transition.getValue(), storm::CompareRelation::GREATER); - } - } - STORM_LOG_ASSERT(!storm::utility::isConstant(sum) || storm::utility::isOne(sum), "If the sum is a constant, it must be equal to 1."); - if(!storm::utility::isConstant(sum)) { - wellformedConstraintSet.emplace(sum - 1, storm::CompareRelation::EQ); - } - - } - } - - template - void Dtmc::ConstraintCollector::operator()(storm::models::sparse::Dtmc const& dtmc) { - process(dtmc); - } -#endif + template class Dtmc; template class Dtmc; diff --git a/src/storm/models/sparse/Dtmc.h b/src/storm/models/sparse/Dtmc.h index 25002856c..4f2d0dfb1 100644 --- a/src/storm/models/sparse/Dtmc.h +++ b/src/storm/models/sparse/Dtmc.h @@ -1,10 +1,7 @@ #ifndef STORM_MODELS_SPARSE_DTMC_H_ #define STORM_MODELS_SPARSE_DTMC_H_ -#include #include "storm/models/sparse/DeterministicModel.h" -#include "storm/utility/OsDetection.h" -#include "storm/adapters/CarlAdapter.h" namespace storm { namespace models { @@ -47,56 +44,7 @@ namespace storm { Dtmc(Dtmc&& dtmc) = default; Dtmc& operator=(Dtmc&& dtmc) = default; - -#ifdef STORM_HAVE_CARL - class ConstraintCollector { - private: - // A set of constraints that says that the DTMC actually has valid probability distributions in all states. - std::unordered_set> wellformedConstraintSet; - - // A set of constraints that makes sure that the underlying graph of the model does not change depending - // on the parameter values. - std::unordered_set> graphPreservingConstraintSet; - - public: - /*! - * Constructs the a constraint collector for the given DTMC. The constraints are built and ready for - * retrieval after the construction. - * - * @param dtmc The DTMC for which to create the constraints. - */ - ConstraintCollector(storm::models::sparse::Dtmc const& dtmc); - - /*! - * Returns the set of wellformed-ness constraints. - * - * @return The set of wellformed-ness constraints. - */ - std::unordered_set> const& getWellformedConstraints() const; - - /*! - * Returns the set of graph-preserving constraints. - * - * @return The set of graph-preserving constraints. - */ - std::unordered_set> const& getGraphPreservingConstraints() const; - - /*! - * Constructs the constraints for the given DTMC. - * - * @param dtmc The DTMC for which to create the constraints. - */ - void process(storm::models::sparse::Dtmc const& dtmc); - - /*! - * Constructs the constraints for the given DTMC by calling the process method. - * - * @param dtmc The DTMC for which to create the constraints. - */ - void operator()(storm::models::sparse::Dtmc const& dtmc); - - }; -#endif + }; } // namespace sparse diff --git a/src/storm/utility/storm.h b/src/storm/utility/storm.h index c2230c87c..0600c36d2 100644 --- a/src/storm/utility/storm.h +++ b/src/storm/utility/storm.h @@ -93,6 +93,9 @@ #include "storm/generator/PrismNextStateGenerator.h" #include "storm/generator/JaniNextStateGenerator.h" +#include "storm/analysis/GraphConditions.h" + + // Headers related to exception handling. #include "storm/exceptions/InvalidStateException.h" #include "storm/exceptions/InvalidArgumentException.h" @@ -580,19 +583,22 @@ namespace storm { return result; } - inline void exportParametricResultToFile(storm::RationalFunction const& result, storm::models::sparse::Dtmc::ConstraintCollector const& constraintCollector, std::string const& path) { + inline void exportParametricResultToFile(storm::RationalFunction const& result, storm::analysis::ConstraintCollector const& constraintCollector, std::string const& path) { std::ofstream filestream; storm::utility::openFile(path, filestream); - // TODO: add checks. filestream << "!Parameters: "; std::set vars = result.gatherVariables(); std::copy(vars.begin(), vars.end(), std::ostream_iterator(filestream, "; ")); filestream << std::endl; filestream << "!Result: " << result << std::endl; filestream << "!Well-formed Constraints: " << std::endl; - std::copy(constraintCollector.getWellformedConstraints().begin(), constraintCollector.getWellformedConstraints().end(), std::ostream_iterator>(filestream, "\n")); + std::vector stringConstraints; + std::transform(constraintCollector.getWellformedConstraints().begin(), constraintCollector.getWellformedConstraints().end(), std::back_inserter(stringConstraints), [](carl::Formula const& c) -> std::string { return c.toString();}); + std::copy(stringConstraints.begin(), stringConstraints.end(), std::ostream_iterator(filestream, "\n")); filestream << "!Graph-preserving Constraints: " << std::endl; - std::copy(constraintCollector.getGraphPreservingConstraints().begin(), constraintCollector.getGraphPreservingConstraints().end(), std::ostream_iterator>(filestream, "\n")); + stringConstraints.clear(); + std::transform(constraintCollector.getGraphPreservingConstraints().begin(), constraintCollector.getGraphPreservingConstraints().end(), std::back_inserter(stringConstraints), [](carl::Formula const& c) -> std::string { return c.toString();}); + std::copy(stringConstraints.begin(), stringConstraints.end(), std::ostream_iterator(filestream, "\n")); storm::utility::closeFile(filestream); }