From 4dbbe3c561a3a2a4ea2345ca6ac17b1555590188 Mon Sep 17 00:00:00 2001 From: dehnert Date: Thu, 23 Jul 2015 11:12:21 -0700 Subject: [PATCH] moved constraint collection to DTMC class Former-commit-id: 5471a20bec2428ae930bacb8467f21e80fa7c89c --- .../reachability/CollectConstraints.h | 63 --------------- .../reachability/DirectEncoding.h | 80 ------------------- src/models/sparse/Dtmc.cpp | 40 ++++++++++ src/models/sparse/Dtmc.h | 51 ++++++++++++ src/utility/cli.h | 23 +++++- 5 files changed, 113 insertions(+), 144 deletions(-) delete mode 100644 src/modelchecker/reachability/CollectConstraints.h delete mode 100644 src/modelchecker/reachability/DirectEncoding.h diff --git a/src/modelchecker/reachability/CollectConstraints.h b/src/modelchecker/reachability/CollectConstraints.h deleted file mode 100644 index d77273770..000000000 --- a/src/modelchecker/reachability/CollectConstraints.h +++ /dev/null @@ -1,63 +0,0 @@ -/** - * @file: CollectConstraints.h - * @author: Sebastian Junges - * - * @since October 8, 2014 - */ - -#pragma once -#include "src/models/Dtmc.h" - -namespace storm { -namespace modelchecker { - namespace reachability { - template - class CollectConstraints - { - private: - std::unordered_set> wellformedConstraintSet; - std::unordered_set> graphPreservingConstraintSet; - storm::utility::ConstantsComparator comparator; - - public: - std::unordered_set> const& wellformedConstraints() const { - return this->wellformedConstraintSet; - } - - std::unordered_set> const& graphPreservingConstraints() const { - return this->graphPreservingConstraintSet; - } - - void process(storm::models::Dtmc const& dtmc) - { - for(uint_fast64_t state = 0; state < dtmc.getNumberOfStates(); ++state) - { - ValueType sum; - assert(comparator.isZero(sum)); - for(auto const& transition : dtmc.getRows(state)) - { - sum += transition.getValue(); - if(!transition.getValue().isConstant()) - { - wellformedConstraintSet.emplace(transition.getValue() - 1, storm::CompareRelation::LEQ); - wellformedConstraintSet.emplace(transition.getValue(), storm::CompareRelation::GEQ); - graphPreservingConstraintSet.emplace(transition.getValue(), storm::CompareRelation::GT); - } - } - assert(!comparator.isConstant(sum) || comparator.isOne(sum)); - if(!sum.isConstant()) { - wellformedConstraintSet.emplace(sum - 1, storm::CompareRelation::EQ); - } - - } - } - - void operator()(storm::models::Dtmc const& dtmc) - { - process(dtmc); - } - - }; - } -} -} diff --git a/src/modelchecker/reachability/DirectEncoding.h b/src/modelchecker/reachability/DirectEncoding.h deleted file mode 100644 index 69ddeeb28..000000000 --- a/src/modelchecker/reachability/DirectEncoding.h +++ /dev/null @@ -1,80 +0,0 @@ -/** - * @file: DirectEncoding.h - * @author: Sebastian Junges - * - * @since April 8, 2014 - */ - -#pragma once - -#ifdef STORM_HAVE_CARL -#include - -namespace storm -{ - namespace modelchecker - { - namespace reachability - { - class DirectEncoding - { - public: - template - std::string encodeAsSmt2(storm::storage::SparseMatrix const& transitionMatrix, std::vector const& oneStepProbabilities, std::set const& parameters, storm::storage::BitVector const& initialStates, typename T::CoeffType const& threshold, bool lessequal = false) { - - carl::io::WriteTosmt2Stream smt2; - uint_fast64_t numberOfStates = transitionMatrix.getRowCount(); - carl::VariablePool& vpool = carl::VariablePool::getInstance(); - std::vector stateVars; - for (carl::Variable const& p : parameters) { - smt2 << ("parameter_bound_" + vpool.getName(p)); - smt2 << carl::io::smt2node::AND; - smt2 << carl::Constraint(Polynomial::PolyType(p), carl::CompareRelation::GT); - smt2 << carl::Constraint(Polynomial::PolyType(p) - Polynomial::PolyType(1), carl::CompareRelation::LT); - smt2 << carl::io::smt2node::CLOSENODE; - } - - for (uint_fast64_t state = 0; state < numberOfStates; ++state) { - carl::Variable stateVar = vpool.getFreshVariable("s_" + std::to_string(state)); - stateVars.push_back(stateVar); - smt2 << ("state_bound_" + std::to_string(state)); - smt2 << carl::io::smt2node::AND; - smt2 << carl::Constraint(Polynomial::PolyType(stateVar), carl::CompareRelation::GT); - smt2 << carl::Constraint(Polynomial::PolyType(stateVar) - Polynomial::PolyType(1), carl::CompareRelation::LT); - smt2 << carl::io::smt2node::CLOSENODE; - } - - smt2.setAutomaticLineBreaks(true); - Polynomial::PolyType initStateReachSum; - for (uint_fast64_t state = 0; state < numberOfStates; ++state) { - T reachpropPol; - for (auto const& transition : transitionMatrix.getRow(state)) { -// reachpropPol += transition.getValue() * stateVars[transition.getColumn()]; - } - reachpropPol += oneStepProbabilities[state]; - smt2 << ("transition_" + std::to_string(state)); -// smt2 << carl::Constraint(reachpropPol - stateVars[state], carl::CompareRelation::EQ); - } - - smt2 << ("reachability"); - - carl::CompareRelation thresholdRelation = lessequal ? carl::CompareRelation::LEQ : carl::CompareRelation::GEQ; - smt2 << carl::io::smt2node::OR; - for (uint_fast64_t state : initialStates) { - smt2 << carl::Constraint(Polynomial::PolyType(stateVars[state]) - threshold, thresholdRelation); - } - smt2 << carl::io::smt2node::CLOSENODE; - - smt2 << carl::io::smt2flag::CHECKSAT; - smt2 << carl::io::smt2flag::MODEL; - smt2 << carl::io::smt2flag::UNSAT_CORE; - std::stringstream strm; - strm << smt2; - return strm.str(); - } - }; - } - } -} - -#endif \ No newline at end of file diff --git a/src/models/sparse/Dtmc.cpp b/src/models/sparse/Dtmc.cpp index 05a67daf9..f2f197428 100644 --- a/src/models/sparse/Dtmc.cpp +++ b/src/models/sparse/Dtmc.cpp @@ -182,6 +182,46 @@ namespace storm { // return storm::models::Dtmc(newMatBuilder.build(), newLabeling, newStateRewards, std::move(newTransitionRewards), newChoiceLabels); } + 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 (!comparator.isConstant(transition.getValue())) { + wellformedConstraintSet.emplace(transition.getValue() - 1, storm::CompareRelation::LEQ); + wellformedConstraintSet.emplace(transition.getValue(), storm::CompareRelation::GEQ); + graphPreservingConstraintSet.emplace(transition.getValue(), storm::CompareRelation::GT); + } + } + STORM_LOG_ASSERT(!comparator.isConstant(sum) || comparator.isOne(sum), "If the sum is a constant, it must be equal to 1."); + if(!comparator.isConstant(sum)) { + wellformedConstraintSet.emplace(sum - 1, storm::CompareRelation::EQ); + } + + } + } + + template + void Dtmc::ConstraintCollector::operator()(storm::models::sparse::Dtmc const& dtmc) { + process(dtmc); + } + template bool Dtmc::checkValidityOfProbabilityMatrix() const { if (this->getTransitionMatrix().getRowCount() != this->getTransitionMatrix().getColumnCount()) { diff --git a/src/models/sparse/Dtmc.h b/src/models/sparse/Dtmc.h index eb37c9432..37095f05e 100644 --- a/src/models/sparse/Dtmc.h +++ b/src/models/sparse/Dtmc.h @@ -59,6 +59,57 @@ namespace storm { */ Dtmc getSubDtmc(storm::storage::BitVector const& states) const; + 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; + + // A comparator that is used for + storm::utility::ConstantsComparator comparator; + + 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); + + }; + private: /*! * Checks the probability matrix for validity. diff --git a/src/utility/cli.h b/src/utility/cli.h index 351584e78..73cb2d2e3 100644 --- a/src/utility/cli.h +++ b/src/utility/cli.h @@ -145,7 +145,7 @@ namespace storm { std::cout << "--------" << std::endl << std::endl; - // std::cout << storm::utility::StormVersion::longVersionString() << std::endl; + std::cout << storm::utility::StormVersion::longVersionString() << std::endl; #ifdef STORM_HAVE_INTELTBB std::cout << "Linked with Intel Threading Building Blocks v" << TBB_VERSION_MAJOR << "." << TBB_VERSION_MINOR << " (Interface version " << TBB_INTERFACE_VERSION << ")." << std::endl; #endif @@ -473,6 +473,22 @@ namespace storm { } #ifdef STORM_HAVE_CARL + void exportParametricResultToFile(storm::RationalFunction const& result, storm::models::sparse::Dtmc::ConstraintCollector const& constraintCollector, std::string const& path) { + std::ofstream filestream; + filestream.open(path); + // 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")); + filestream << "!Graph-preserving Constraints: " << std::endl; + std::copy(constraintCollector.getGraphPreservingConstraints().begin(), constraintCollector.getGraphPreservingConstraints().end(), std::ostream_iterator>(filestream, "\n")); + filestream.close(); + } + template<> void verifySparseModel(boost::optional const& program, std::shared_ptr> model, std::shared_ptr formula) { storm::settings::modules::GeneralSettings const& settings = storm::settings::generalSettings(); @@ -498,6 +514,11 @@ namespace storm { } else { std::cout << " skipped, because the modelling formalism is currently unsupported." << std::endl; } + + storm::settings::modules::ParametricSettings const& parametricSettings = storm::settings::parametricSettings(); + if (parametricSettings.exportResultToFile()) { + exportParametricResultToFile(result->asExplicitQuantitativeCheckResult()[*dtmc->getInitialStates().begin()], storm::models::sparse::Dtmc::ConstraintCollector(*dtmc), parametricSettings.exportResultPath()); + } } #endif