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

CHANGELOG.md

@@ -6,6 +6,12 @@ The releases of major and minor versions contain an overview of changes since th
 
 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)
 

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/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

@@ -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);
             
         };