sp
/
tempest
1
0
Fork 0
Code Issues Pull Requests Projects Releases Wiki Activity
Browse Source

unification of some constructs in carl propagated to storm 

Former-commit-id: 34ba08debf
main
sjunges 10 years ago
parent
613724fa9f
commit
2e0c9c1244
5 changed files with 14 additions and 13 deletions
Whitespace
Show all changes Ignore whitespace when comparing lines Ignore changes in amount of whitespace Ignore changes in whitespace at EOL
Unified View
Diff Options
Show Stats Download Patch File Download Diff File
  1. 6
      src/adapters/CarlAdapter.h
  2. 6
      src/models/sparse/Dtmc.cpp
  3. 8
      src/models/sparse/Dtmc.h
  4. 1
      src/utility/cli.cpp
  5. 6
      src/utility/cli.h

6
src/adapters/CarlAdapter.h
View File

@ -12,8 +12,8 @@
#include <carl/core/RationalFunction.h> #include <carl/core/RationalFunction.h>
#include <carl/core/VariablePool.h> #include <carl/core/VariablePool.h>
#include <carl/core/FactorizedPolynomial.h> #include <carl/core/FactorizedPolynomial.h>
#include <carl/formula/Relation.h>
#include <carl/formula/Formula.h>
#include <carl/core/Relation.h>
#include <carl/core/SimpleConstraint.h>
namespace carl { namespace carl {
// Define hash values for all polynomials and rational function. // Define hash values for all polynomials and rational function.
@ -48,8 +48,10 @@ namespace storm {
typedef carl::MultivariatePolynomial<RationalNumber> RawPolynomial; typedef carl::MultivariatePolynomial<RationalNumber> RawPolynomial;
typedef carl::FactorizedPolynomial<RawPolynomial> Polynomial; typedef carl::FactorizedPolynomial<RawPolynomial> Polynomial;
typedef carl::Relation CompareRelation; typedef carl::Relation CompareRelation;
typedef carl::RationalFunction<Polynomial> RationalFunction; typedef carl::RationalFunction<Polynomial> RationalFunction;
typedef carl::Interval<double> Interval; typedef carl::Interval<double> Interval;
template<typename T> using ArithConstraint = carl::SimpleConstraint<T>;
} }
#endif #endif

6
src/models/sparse/Dtmc.cpp
View File

@ -189,12 +189,12 @@ namespace storm {
} }
template<typename ValueType> template<typename ValueType>
std::unordered_set<carl::Constraint<ValueType>> const& Dtmc<ValueType>::ConstraintCollector::getWellformedConstraints() const {
std::unordered_set<storm::ArithConstraint<ValueType>> const& Dtmc<ValueType>::ConstraintCollector::getWellformedConstraints() const {
return this->wellformedConstraintSet; return this->wellformedConstraintSet;
} }
template<typename ValueType> template<typename ValueType>
std::unordered_set<carl::Constraint<ValueType>> const& Dtmc<ValueType>::ConstraintCollector::getGraphPreservingConstraints() const {
std::unordered_set<storm::ArithConstraint<ValueType>> const& Dtmc<ValueType>::ConstraintCollector::getGraphPreservingConstraints() const {
return this->graphPreservingConstraintSet; return this->graphPreservingConstraintSet;
} }
@ -207,7 +207,7 @@ namespace storm {
if (!comparator.isConstant(transition.getValue())) { if (!comparator.isConstant(transition.getValue())) {
wellformedConstraintSet.emplace(transition.getValue() - 1, storm::CompareRelation::LEQ); wellformedConstraintSet.emplace(transition.getValue() - 1, storm::CompareRelation::LEQ);
wellformedConstraintSet.emplace(transition.getValue(), storm::CompareRelation::GEQ); 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."); STORM_LOG_ASSERT(!comparator.isConstant(sum) || comparator.isOne(sum), "If the sum is a constant, it must be equal to 1.");

8
src/models/sparse/Dtmc.h
View File

@ -63,11 +63,11 @@ namespace storm {
class ConstraintCollector { class ConstraintCollector {
private: private:
// A set of constraints that says that the DTMC actually has valid probability distributions in all states. // A set of constraints that says that the DTMC actually has valid probability distributions in all states.
std::unordered_set<carl::Constraint<ValueType>> wellformedConstraintSet;
std::unordered_set<storm::ArithConstraint<ValueType>> wellformedConstraintSet;
// A set of constraints that makes sure that the underlying graph of the model does not change depending // A set of constraints that makes sure that the underlying graph of the model does not change depending
// on the parameter values. // on the parameter values.
std::unordered_set<carl::Constraint<ValueType>> graphPreservingConstraintSet;
std::unordered_set<storm::ArithConstraint<ValueType>> graphPreservingConstraintSet;
// A comparator that is used for // A comparator that is used for
storm::utility::ConstantsComparator<ValueType> comparator; storm::utility::ConstantsComparator<ValueType> comparator;
@ -86,14 +86,14 @@ namespace storm {
* *
* @return The set of wellformed-ness constraints. * @return The set of wellformed-ness constraints.
*/ */
std::unordered_set<carl::Constraint<ValueType>> const& getWellformedConstraints() const;
std::unordered_set<storm::ArithConstraint<ValueType>> const& getWellformedConstraints() const;
/*! /*!
* Returns the set of graph-preserving constraints. * Returns the set of graph-preserving constraints.
* *
* @return The set of graph-preserving constraints. * @return The set of graph-preserving constraints.
*/ */
std::unordered_set<carl::Constraint<ValueType>> const& getGraphPreservingConstraints() const;
std::unordered_set<storm::ArithConstraint<ValueType>> const& getGraphPreservingConstraints() const;
/*! /*!
* Constructs the constraints for the given DTMC. * Constructs the constraints for the given DTMC.

1
src/utility/cli.cpp
View File

@ -113,7 +113,6 @@ namespace storm {
std::cout << "Command line arguments: " << commandStream.str() << std::endl; std::cout << "Command line arguments: " << commandStream.str() << std::endl;
std::cout << "Current working directory: " << getCurrentWorkingDirectory() << std::endl << std::endl; std::cout << "Current working directory: " << getCurrentWorkingDirectory() << std::endl << std::endl;
} }
}
void printUsage() { void printUsage() {

6
src/utility/cli.h
View File

@ -251,7 +251,7 @@ namespace storm {
} }
#ifdef STORM_HAVE_CARL #ifdef STORM_HAVE_CARL
void exportParametricResultToFile(storm::RationalFunction const& result, storm::models::sparse::Dtmc<storm::RationalFunction>::ConstraintCollector const& constraintCollector, std::string const& path) {
inline void exportParametricResultToFile(storm::RationalFunction const& result, storm::models::sparse::Dtmc<storm::RationalFunction>::ConstraintCollector const& constraintCollector, std::string const& path) {
std::ofstream filestream; std::ofstream filestream;
filestream.open(path); filestream.open(path);
// TODO: add checks. // TODO: add checks.
@ -261,9 +261,9 @@ namespace storm {
filestream << std::endl; filestream << std::endl;
filestream << "!Result: " << result << std::endl; filestream << "!Result: " << result << std::endl;
filestream << "!Well-formed Constraints: " << std::endl; filestream << "!Well-formed Constraints: " << std::endl;
std::copy(constraintCollector.getWellformedConstraints().begin(), constraintCollector.getWellformedConstraints().end(), std::ostream_iterator<carl::Constraint<storm::RationalFunction>>(filestream, "\n"));
std::copy(constraintCollector.getWellformedConstraints().begin(), constraintCollector.getWellformedConstraints().end(), std::ostream_iterator<storm::ArithConstraint<storm::RationalFunction>>(filestream, "\n"));
filestream << "!Graph-preserving Constraints: " << std::endl; filestream << "!Graph-preserving Constraints: " << std::endl;
std::copy(constraintCollector.getGraphPreservingConstraints().begin(), constraintCollector.getGraphPreservingConstraints().end(), std::ostream_iterator<carl::Constraint<storm::RationalFunction>>(filestream, "\n"));
std::copy(constraintCollector.getGraphPreservingConstraints().begin(), constraintCollector.getGraphPreservingConstraints().end(), std::ostream_iterator<storm::ArithConstraint<storm::RationalFunction>>(filestream, "\n"));
filestream.close(); filestream.close();
} }

Write Preview
Loading…
Cancel
Save