Merge branch 'master' of https://srv-i2.informatik.rwth-aachen.de/scm/git/storm

CHANGELOG.md

@@ -8,6 +8,11 @@ Version 1.1.x
 -------------
 Long run average computation via ValueIteration, LP based MDP model checking, parametric model checking has an own binary
 
+### Version 1.1.1
+- c++ api changes: Building model takes BuilderOptions instead of extended list of Booleans, does not depend on settings anymore.
+- storm-cli-utilities now contains cli related stuff, instead of storm-lib
+- storm-pars: support for welldefinedness constraints in mdps.
+
 ### Version 1.1.0 (2017/8)
 
 - Support for long-run average rewards on MDPs and Markov automata using a value-iteration based approach.

src/storm-pars-cli/storm-pars.cpp

@@ -306,15 +306,8 @@ namespace storm {
 
             if (parSettings.onlyObtainConstraints()) {
                 STORM_LOG_THROW(parSettings.exportResultToFile(), storm::exceptions::InvalidSettingsException, "When computing constraints, export path has to be specified.");
-                if (model->isOfType(storm::models::ModelType::Dtmc)) {
-                    auto dtmc = model->template as<storm::models::sparse::Dtmc<ValueType>>();
-                    storm::api::exportParametricResultToFile<ValueType>(boost::none, storm::analysis::ConstraintCollector<ValueType>(*dtmc),parSettings.exportResultPath());
-                    return;
-                } else {
-                    STORM_LOG_THROW(parSettings.exportResultToFile(), storm::exceptions::NotImplementedException, "Constraints for MDPs and CTMCs not implemented.");
-
-                }
-
+                storm::api::exportParametricResultToFile<ValueType>(boost::none, storm::analysis::ConstraintCollector<ValueType>(*(model->as<storm::models::sparse::Model<ValueType>>())), parSettings.exportResultPath());
+                return;
             }
 
             if (model) {

src/storm/adapters/RationalFunctionAdapter.h

@@ -7,7 +7,6 @@
 #include <carl/core/VariablePool.h>
 #include <carl/core/FactorizedPolynomial.h>
 #include <carl/core/Relation.h>
-#include <carl/core/SimpleConstraint.h>
 #include <carl/util/stringparser.h>
 
 namespace carl {
@@ -58,5 +57,5 @@ namespace storm {
     
     typedef carl::RationalFunction<Polynomial, true> RationalFunction;
     typedef carl::Interval<double> Interval;
-    template<typename T> using ArithConstraint = carl::SimpleConstraint<T>;
 }
+

src/storm/adapters/Smt2ExpressionAdapter.h

@@ -38,8 +38,7 @@ namespace storm {
             std::string translateExpression(storm::expressions::Expression const& ) {
                 STORM_LOG_THROW(false, storm::exceptions::NotImplementedException, "functionality not (yet) implemented");
             }
-            
-#ifdef STORM_HAVE_CARL              
+
             /*!
              * Translates the given constraint "leftHandSide relation rightHandSide" to an equivalent expression for Smt2.
 			 
@@ -60,6 +59,7 @@ namespace storm {
                             ") " +
                         ")";
             }
+
             
             /*!
              * Translates the given constraint "leftHandSide relation 0" to an equivalent expression for Smt2.
@@ -67,31 +67,16 @@ namespace storm {
              * @param constraint
              * @return An equivalent expression for Smt2.
              */
-            std::string translateExpression(storm::ArithConstraint<storm::RawPolynomial> const& constraint) {
-                std::stringstream ss;
-                ss << "(" << constraint.rel() << " " << 
-                        constraint.lhs().toString(false, useReadableVarNames) << " " << 
-                            "0 " <<
-                        ")";
-                return ss.str();
-            }
-            
-            /*!
-             * Translates the given constraint "leftHandSide relation 0" to an equivalent expression for Smt2.
-			 
-             * @param constraint
-             * @return An equivalent expression for Smt2.
-             */
-            std::string translateExpression(storm::ArithConstraint<storm::Polynomial> const& constraint) {
+            std::string translateExpression(storm::RationalFunction const& leftHandSide, storm::CompareRelation const& relation) {
                                 
                 std::stringstream ss;
-                ss << "(" << constraint.rel() << " " << 
-                        constraint.lhs().toString(false, useReadableVarNames) << " " << 
+                ss << "(" << relation << " " <<
+                        leftHandSide.toString(false, useReadableVarNames) << " " <<
                             "0 " <<
                         ")";
                 return ss.str();
             }
-#endif
+
             /*!
              * Translates the given variable to an equivalent expression for Smt2.
              *
@@ -126,7 +111,7 @@ namespace storm {
             }
             
             
-#ifdef STORM_HAVE_CARL
+
             /*! Checks whether the variables in the given set are already declared and creates them if necessary
              *  @param variables the set of variables to check
              */
@@ -167,7 +152,6 @@ namespace storm {
                 }
                 return result;
             }
-#endif
             
         private:
             // The manager that can be used to build expressions.

src/storm/analysis/GraphConditions.cpp

@@ -1,4 +1,6 @@
 
+#include "storm/models/sparse/MarkovAutomaton.h"
+#include "storm/models/sparse/Ctmc.h"
 #include "GraphConditions.h"
 #include "storm/utility/constants.h"
 #include "storm/exceptions/NotImplementedException.h"
@@ -9,8 +11,8 @@ namespace storm {
 
 
         template <typename ValueType>
-        ConstraintCollector<ValueType>::ConstraintCollector(storm::models::sparse::Dtmc<ValueType> const& dtmc) {
-            process(dtmc);
+        ConstraintCollector<ValueType>::ConstraintCollector(storm::models::sparse::Model<ValueType> const& model) {
+            process(model);
         }
 
         template <typename ValueType>
@@ -50,10 +52,13 @@ namespace storm {
         }
 
         template <typename ValueType>
-        void ConstraintCollector<ValueType>::process(storm::models::sparse::Dtmc<ValueType> const& dtmc) {
-            for(uint_fast64_t state = 0; state < dtmc.getNumberOfStates(); ++state) {
+        void ConstraintCollector<ValueType>::process(storm::models::sparse::Model<ValueType> const& model) {
+            for(uint_fast64_t action = 0; action < model.getTransitionMatrix().getRowCount(); ++action) {
                 ValueType sum = storm::utility::zero<ValueType>();
-                for (auto const& transition : dtmc.getRows(state)) {
+
+                for (auto transitionIt = model.getTransitionMatrix().begin(action); transitionIt != model.getTransitionMatrix().end(action); ++transitionIt) {
+                    auto const& transition = *transitionIt;
+                    std::cout << transition.getValue() << std::endl;
                     sum += transition.getValue();
                     if (!storm::utility::isConstant(transition.getValue())) {
                         auto const& transitionVars = transition.getValue().gatherVariables();
@@ -90,9 +95,17 @@ namespace storm {
                     // Assert: sum == 1
                     wellformedConstraintSet.emplace((sum.nominator() - sum.denominator()).polynomialWithCoefficient(), storm::CompareRelation::EQ);
                 }
+            }
 
+            if (model.getType() == storm::models::ModelType::Ctmc) {
+                auto const& exitRateVector = static_cast<storm::models::sparse::Ctmc<ValueType> const&>(model).getExitRateVector();
+                wellformedRequiresNonNegativeEntries(exitRateVector);
+            } else if (model.getType() == storm::models::ModelType::MarkovAutomaton) {
+                auto const& exitRateVector = static_cast<storm::models::sparse::MarkovAutomaton<ValueType> const&>(model).getExitRates();
+                wellformedRequiresNonNegativeEntries(exitRateVector);
             }
-            for(auto const& rewModelEntry : dtmc.getRewardModels()) {
+
+            for(auto const& rewModelEntry : model.getRewardModels()) {
                 if (rewModelEntry.second.hasStateRewards()) {
                     wellformedRequiresNonNegativeEntries(rewModelEntry.second.getStateRewardVector());
                 }
@@ -117,13 +130,13 @@ namespace storm {
                         }
                     }
                 }
-
             }
+
         }
 
         template <typename ValueType>
-        void ConstraintCollector<ValueType>::operator()(storm::models::sparse::Dtmc<ValueType> const& dtmc) {
-            process(dtmc);
+        void ConstraintCollector<ValueType>::operator()(storm::models::sparse::Model<ValueType> const& model) {
+            process(model);
         }
 
         template class ConstraintCollector<storm::RationalFunction>;

src/storm/analysis/GraphConditions.h

@@ -8,12 +8,12 @@
 
 namespace storm {
     namespace analysis {
-        
+
         template <typename ValueType, typename Enable=void>
         struct ConstraintType {
-            typedef storm::ArithConstraint<ValueType> val;
+            typedef void* val;
         };
-        
+
         template<typename ValueType>
         struct ConstraintType<ValueType, typename std::enable_if<std::is_same<storm::RationalFunction, ValueType>::value>::type> {
             typedef carl::Formula<typename ValueType::PolyType::PolyType> val;
@@ -38,12 +38,12 @@ namespace storm {
             void wellformedRequiresNonNegativeEntries(std::vector<ValueType> const&);
         public:
             /*!
-             * Constructs a constraint collector for the given DTMC. The constraints are built and ready for
+             * Constructs a constraint collector for the given Model. The constraints are built and ready for
              * retrieval after the construction.
              *
-             * @param dtmc The DTMC for which to create the constraints.
+             * @param model The Model for which to create the constraints.
              */
-            ConstraintCollector(storm::models::sparse::Dtmc<ValueType> const& dtmc);
+            ConstraintCollector(storm::models::sparse::Model<ValueType> const& model);
             
             /*!
              * Returns the set of wellformed-ness constraints.
@@ -66,18 +66,18 @@ namespace storm {
             std::set<storm::RationalFunctionVariable> const& getVariables() const;
             
             /*!
-             * Constructs the constraints for the given DTMC.
+             * Constructs the constraints for the given Model.
              *
-             * @param dtmc The DTMC for which to create the constraints.
+             * @param model The DTMC for which to create the constraints.
              */
-            void process(storm::models::sparse::Dtmc<ValueType> const& dtmc);
+            void process(storm::models::sparse::Model<ValueType> const& model);
             
             /*!
-             * Constructs the constraints for the given DTMC by calling the process method.
+             * Constructs the constraints for the given Model by calling the process method.
              *
-             * @param dtmc The DTMC for which to create the constraints.
+             * @param model The Model for which to create the constraints.
              */
-            void operator()(storm::models::sparse::Dtmc<ValueType> const& dtmc);
+            void operator()(storm::models::sparse::Model<ValueType> const& model);
             
         };
         

src/storm/solver/SmtlibSmtSolver.cpp

@@ -102,33 +102,6 @@ namespace storm {
             writeCommand("( assert " + expressionAdapter->translateExpression(leftHandSide, relation, rightHandSide) + " )", true);
         }
         
-        void SmtlibSmtSolver::add(storm::ArithConstraint<storm::RationalFunction> const& constraint) {
-            add(constraint.lhs(), constraint.rel());
-        }
-        
-        void SmtlibSmtSolver::add(storm::ArithConstraint<storm::RawPolynomial> const& constraint) {
-            //if some of the occurring variables are not declared yet, we will have to.
-            std::set<storm::RationalFunctionVariable> variables = constraint.lhs().gatherVariables();
-            std::vector<std::string> const varDeclarations = expressionAdapter->checkForUndeclaredVariables(variables);
-            for (auto declaration : varDeclarations){
-                writeCommand(declaration, true);
-            }
-            writeCommand("( assert " + expressionAdapter->translateExpression(constraint) + " )", true);
-        }
-        
-        void SmtlibSmtSolver::add(storm::RationalFunctionVariable const& guard, typename storm::ArithConstraint<storm::Polynomial> const& constraint){
-            STORM_LOG_THROW((guard.getType()==carl::VariableType::VT_BOOL), storm::exceptions::IllegalArgumentException, "Tried to add a guarded constraint, but the guard is not of type bool.");
-            //if some of the occurring variables are not declared yet, we will have to (including the guard!).
-            std::set<storm::RationalFunctionVariable> variables = constraint.lhs().gatherVariables();
-            variables.insert(guard);
-            std::vector<std::string> const varDeclarations = expressionAdapter->checkForUndeclaredVariables(variables);
-            for (auto declaration : varDeclarations){
-                writeCommand(declaration, true);
-            }
-            std::string guardName= carl::VariablePool::getInstance().getName(guard, this->useReadableVarNames);
-            writeCommand("( assert (=> " + guardName + " " + expressionAdapter->translateExpression(constraint) + " ) )", true);
-        }
-        
         void SmtlibSmtSolver::add(const storm::RationalFunctionVariable& variable, bool value){
             STORM_LOG_THROW((variable.getType()==carl::VariableType::VT_BOOL), storm::exceptions::IllegalArgumentException, "Tried to add a constraint that consists of a non-boolean variable.");
             std::set<storm::RationalFunctionVariable> variableSet;

src/storm/solver/SmtlibSmtSolver.h

@@ -51,12 +51,7 @@ namespace storm {
             //adds the constraint "leftHandSide relation rightHandSide"
             virtual void add(storm::RationalFunction const& leftHandSide, storm::CompareRelation const& relation, storm::RationalFunction const& rightHandSide=storm::RationalFunction(0));
             
-            //adds the given carl constraint
-            void add(typename storm::ArithConstraint<storm::RationalFunction> const& constraint);
-            void add(typename storm::ArithConstraint<storm::RawPolynomial> const& constraint);
-            
-            // adds the given carl constraint that is guarded by the given guard. The guard should have type 'bool'
-            void add(storm::RationalFunctionVariable const& guard, typename storm::ArithConstraint<storm::Polynomial> const& constraint);
+          
             
             // asserts that the given variable has the given value. The variable should have type 'bool'
             void add(storm::RationalFunctionVariable const& variable, bool value);
@@ -65,10 +60,9 @@ namespace storm {
             virtual CheckResult check() override;
 
             virtual CheckResult checkWithAssumptions(std::set<storm::expressions::Expression> const& assumptions) override;
-#ifndef WINDOWS
+
             virtual CheckResult checkWithAssumptions(std::initializer_list<storm::expressions::Expression> const& assumptions) override;
-#endif
-            
+
             bool isNeedsRestart() const;
             
             //Todo: some of these might be added in the future