diff --git a/src/adapters/CarlAdapter.h b/src/adapters/CarlAdapter.h index 856ca1504..c0191701a 100644 --- a/src/adapters/CarlAdapter.h +++ b/src/adapters/CarlAdapter.h @@ -12,8 +12,8 @@ #include #include #include -#include -#include +#include +#include namespace carl { // Define hash values for all polynomials and rational function. @@ -48,8 +48,10 @@ namespace storm { typedef carl::MultivariatePolynomial RawPolynomial; typedef carl::FactorizedPolynomial Polynomial; typedef carl::Relation CompareRelation; + typedef carl::RationalFunction RationalFunction; typedef carl::Interval Interval; + template using ArithConstraint = carl::SimpleConstraint; } #endif diff --git a/src/models/sparse/Dtmc.cpp b/src/models/sparse/Dtmc.cpp index f1248af39..b5dbaa40c 100644 --- a/src/models/sparse/Dtmc.cpp +++ b/src/models/sparse/Dtmc.cpp @@ -189,12 +189,12 @@ namespace storm { } template - std::unordered_set> const& Dtmc::ConstraintCollector::getWellformedConstraints() const { + std::unordered_set> const& Dtmc::ConstraintCollector::getWellformedConstraints() const { return this->wellformedConstraintSet; } template - std::unordered_set> const& Dtmc::ConstraintCollector::getGraphPreservingConstraints() const { + std::unordered_set> const& Dtmc::ConstraintCollector::getGraphPreservingConstraints() const { return this->graphPreservingConstraintSet; } @@ -207,7 +207,7 @@ namespace storm { 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); + graphPreservingConstraintSet.emplace(transition.getValue(), storm::CompareRelation::GREATER); } } STORM_LOG_ASSERT(!comparator.isConstant(sum) || comparator.isOne(sum), "If the sum is a constant, it must be equal to 1."); diff --git a/src/models/sparse/Dtmc.h b/src/models/sparse/Dtmc.h index af1d2ad3f..0bf0cfce1 100644 --- a/src/models/sparse/Dtmc.h +++ b/src/models/sparse/Dtmc.h @@ -63,11 +63,11 @@ namespace storm { class ConstraintCollector { private: // A set of constraints that says that the DTMC actually has valid probability distributions in all states. - std::unordered_set> wellformedConstraintSet; + 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; + std::unordered_set> graphPreservingConstraintSet; // A comparator that is used for storm::utility::ConstantsComparator comparator; @@ -86,14 +86,14 @@ namespace storm { * * @return The set of wellformed-ness constraints. */ - std::unordered_set> const& getWellformedConstraints() const; + 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; + std::unordered_set> const& getGraphPreservingConstraints() const; /*! * Constructs the constraints for the given DTMC. diff --git a/src/utility/cli.cpp b/src/utility/cli.cpp index 7e7a99080..40e8c4693 100644 --- a/src/utility/cli.cpp +++ b/src/utility/cli.cpp @@ -113,7 +113,6 @@ namespace storm { std::cout << "Command line arguments: " << commandStream.str() << std::endl; std::cout << "Current working directory: " << getCurrentWorkingDirectory() << std::endl << std::endl; } - } void printUsage() { diff --git a/src/utility/cli.h b/src/utility/cli.h index 82044200b..3e1b820e4 100644 --- a/src/utility/cli.h +++ b/src/utility/cli.h @@ -251,7 +251,7 @@ namespace storm { } #ifdef STORM_HAVE_CARL - 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::models::sparse::Dtmc::ConstraintCollector const& constraintCollector, std::string const& path) { std::ofstream filestream; filestream.open(path); // TODO: add checks. @@ -261,9 +261,9 @@ namespace storm { 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::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")); + std::copy(constraintCollector.getGraphPreservingConstraints().begin(), constraintCollector.getGraphPreservingConstraints().end(), std::ostream_iterator>(filestream, "\n")); filestream.close(); }