Merge remote-tracking branch 'origin/master' into quantiles

CHANGELOG.md

@@ -7,6 +7,8 @@ The releases of major and minor versions contain an overview of changes since th
 Version 1.3.x
 -------------
 
+### Version 1.3.1 (under development)
+- Fixed sparse bisimulation of MDPs (which failed if all non-absorbing states in the quotient are initial)
 
 ### Version 1.3.0 (2018/12)
 - Slightly improved scheduler extraction

src/storm-cli-utilities/model-handling.h

@@ -579,7 +579,7 @@ namespace storm {
                     STORM_PRINT("Time for model checking: " << *watch << "." << std::endl);
                 }
             } else {
-                STORM_PRINT(" failed, property is unsupported by selected engine/settings." << std::endl);
+                STORM_LOG_ERROR("Property is unsupported by selected engine/settings." << std::endl);
             }
         }
         

src/storm-counterexamples/CMakeLists.txt

@@ -8,7 +8,7 @@ file(GLOB_RECURSE STORM_CEX_SOURCES ${PROJECT_SOURCE_DIR}/src/storm-counterexamp
 file(GLOB_RECURSE STORM_CEX_HEADERS ${PROJECT_SOURCE_DIR}/src/storm-counterexamples/*/*.h)
 
 
-# Create storm-dft.
+# Create storm-counterexamples.
 add_library(storm-counterexamples SHARED ${STORM_CEX_SOURCES} ${STORM_CEX_HEADERS})
 
 # Remove define symbol for shared libstorm.

src/storm-dft/builder/DFTBuilder.cpp

@@ -140,7 +140,8 @@ namespace storm {
             if (children.size() <= 1) {
                 STORM_LOG_ERROR("Sequence enforcers require at least two children");
             }
-            if (mElements.count(name) != 0) {
+            if (nameInUse(name)) {
+                STORM_LOG_ERROR("Element with name '" << name << "' already exists.");
                 return false;
             }
             DFTRestrictionPointer restr;
@@ -166,8 +167,8 @@ namespace storm {
         template<typename ValueType>
         bool DFTBuilder<ValueType>::addStandardGate(std::string const& name, std::vector<std::string> const& children, storm::storage::DFTElementType tp) {
             STORM_LOG_ASSERT(children.size() > 0, "No child for " << name);
-            if(mElements.count(name) != 0) {
-                // Element with that name already exists.
+            if (nameInUse(name)) {
+                STORM_LOG_ERROR("Element with name '" << name << "' already exists.");
                 return false;
             }
             DFTElementPointer element;

src/storm-dft/builder/DFTBuilder.h

@@ -93,8 +93,8 @@ namespace storm {
                 if(children.size() <= 1) {
                     STORM_LOG_ERROR("Dependencies require at least two children");
                 }
-                if(mElements.count(name) != 0) {
-                    // Element with that name already exists.
+                if (nameInUse(name)) {
+                    STORM_LOG_ERROR("Element with name '" << name << "' already exists.");
                     return false;
                 }
 
@@ -122,13 +122,11 @@ namespace storm {
                     if(binaryDependencies) {
                         for (size_t i = 1; i < children.size(); ++i) {
                             std::string nameDep = name + "_" + std::to_string(i);
-                            if (mElements.count(nameDep) != 0) {
-                                // Element with that name already exists.
-                                STORM_LOG_ERROR("Element with name: " << nameDep << " already exists.");
+                            if (nameInUse(nameDep)) {
+                                STORM_LOG_ERROR("Element with name '" << name << "' already exists.");
                                 return false;
                             }
-                            STORM_LOG_ASSERT(storm::utility::isOne(probability) || children.size() == 2,
-                                             "PDep with multiple children supported.");
+                            STORM_LOG_ASSERT(storm::utility::isOne(probability) || children.size() == 2, "PDep with multiple children supported.");
                             DFTDependencyPointer element = std::make_shared<storm::storage::DFTDependency<ValueType>>(mNextId++, nameDep, probability);
                             mElements[element->name()] = element;
                             mDependencyChildNames[element] = {trigger, children[i]};
@@ -146,8 +144,8 @@ namespace storm {
 
             bool addVotElement(std::string const& name, unsigned threshold, std::vector<std::string> const& children) {
                 STORM_LOG_ASSERT(children.size() > 0, "Has no child.");
-                if(mElements.count(name) != 0) {
-                    STORM_LOG_ERROR("Element with name: " << name << " already exists.");
+                if (nameInUse(name)) {
+                    STORM_LOG_ERROR("Element with name '" << name << "' already exists.");
                     return false;
                 }
                 // It is an and-gate
@@ -174,19 +172,33 @@ namespace storm {
                 //TODO Matthias: collect constraints for SMT solving
                 //failureRate > 0
                 //0 <= dormancyFactor <= 1
-                STORM_LOG_ASSERT(mElements.find(name) == mElements.end(), "Element '" << name << "' already exists.");
+                if (nameInUse(name)) {
+                    STORM_LOG_ERROR("Element with name '" << name << "' already exists.");
+                    return false;
+                }
                 mElements[name] = std::make_shared<storm::storage::DFTBE<ValueType>>(mNextId++, name, failureRate, dormancyFactor, transient);
                 return true;
             }
 
             void addLayoutInfo(std::string const& name, double x, double y) {
-                STORM_LOG_ASSERT(mElements.count(name) > 0, "Element '" << name << "' not found.");
+                if (!nameInUse(name)) {
+                    STORM_LOG_ERROR("Element with name '" << name << "' not found.");
+                }
                 mLayoutInfo[name] = storm::storage::DFTLayoutInfo(x, y);
             }
             
             bool setTopLevel(std::string const& tle) {
                 mTopLevelIdentifier = tle;
-                return mElements.count(tle) > 0;
+                return nameInUse(tle);
+            }
+
+            /**
+             * Check whether the name is already used.
+             * @param name Element name.
+             * @return True iff name is already in use.
+             */
+            bool nameInUse(std::string const& name) {
+                return mElements.find(name) != mElements.end();
             }
             
             std::string getUniqueName(std::string name);

src/storm-dft/storage/dft/DFTIsomorphism.h

@@ -255,6 +255,7 @@ namespace storage {
         void colourize(std::shared_ptr<const DFTGate<ValueType>> const& gate) {
              STORM_LOG_TRACE("Colour " << gate->id() << ": "  << gate->type() << " " << gate->nrChildren() << " " << gate->rank() << ".");
              gateColour[gate->id()] = gateColourizer(gate->type(), gate->nrChildren(), gate->nrParents(), 0, gate->rank());
+             STORM_LOG_TRACE("Coloured " << gate->id() << " with " << gateColour[gate->id()] << ".");
         }
         
         void colourize(std::shared_ptr<const DFTDependency<ValueType>> const& dep) {

src/storm-dft/storage/dft/DftJsonExporter.cpp

@@ -80,6 +80,8 @@ namespace storm {
                     std::stringstream stream;
                     stream << dependency->probability();
                     nodeData["probability"] = stream.str();
+                } else {
+                    nodeData["type"] = "fdep";
                 }
             } else if (element->isBasicElement()) {
                 // Set BE specific data

src/storm-dft/storage/dft/SymmetricUnits.h

@@ -108,7 +108,7 @@ namespace storm {
                 }
                 // Sort by length of symmetry or (if equal) by lower first element
                 std::sort(sortedGroups.begin(), sortedGroups.end(), [&](const size_t left, const size_t right) {
-                    return groups.at(left).size() < groups.at(right).size() || (groups.at(left).size() == groups.at(right).size() && groups.at(left).front().front() < groups.at(left).front().front());
+                    return groups.at(left).size() < groups.at(right).size() || (groups.at(left).size() == groups.at(right).size() && groups.at(left).front().front() < groups.at(right).front().front());
                 });
                 
                 // Sort hierarchical

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

@@ -45,6 +45,16 @@ namespace storm {
             bool graphPreserving;
             bool exact;
         };
+
+        struct PreprocessResult {
+            PreprocessResult(std::shared_ptr<storm::models::ModelBase> const& model, bool changed) : changed(changed), model(model) {
+                // Intentionally left empty.
+            }
+
+            bool changed;
+            std::shared_ptr<storm::models::ModelBase> model;
+            boost::optional<std::vector<std::shared_ptr<storm::logic::Formula const>>> formulas;
+        };
         
         template <typename ValueType>
         std::vector<storm::storage::ParameterRegion<ValueType>> parseRegions(std::shared_ptr<storm::models::ModelBase> const& model) {
@@ -127,64 +137,76 @@ namespace storm {
         }
         
         template <typename ValueType>
-        std::pair<std::shared_ptr<storm::models::ModelBase>, bool> preprocessSparseModel(std::shared_ptr<storm::models::sparse::Model<ValueType>> const& model, SymbolicInput const& input) {
+        PreprocessResult preprocessSparseModel(std::shared_ptr<storm::models::sparse::Model<ValueType>> const& model, SymbolicInput const& input) {
             auto generalSettings = storm::settings::getModule<storm::settings::modules::GeneralSettings>();
             auto bisimulationSettings = storm::settings::getModule<storm::settings::modules::BisimulationSettings>();
             auto parametricSettings = storm::settings::getModule<storm::settings::modules::ParametricSettings>();
             
-            std::pair<std::shared_ptr<storm::models::ModelBase>, bool> result = std::make_pair(model, false);
+            PreprocessResult result(model, false);
             
-            if (result.first->isOfType(storm::models::ModelType::MarkovAutomaton)) {
-                result.first = storm::cli::preprocessSparseMarkovAutomaton(result.first->template as<storm::models::sparse::MarkovAutomaton<ValueType>>());
-                result.second = true;
+            if (result.model->isOfType(storm::models::ModelType::MarkovAutomaton)) {
+                result.model = storm::cli::preprocessSparseMarkovAutomaton(result.model->template as<storm::models::sparse::MarkovAutomaton<ValueType>>());
+                result.changed = true;
             }
             
             if (generalSettings.isBisimulationSet()) {
-                result.first = storm::cli::preprocessSparseModelBisimulation(result.first->template as<storm::models::sparse::Model<ValueType>>(), input, bisimulationSettings);
-                result.second = true;
+                result.model = storm::cli::preprocessSparseModelBisimulation(result.model->template as<storm::models::sparse::Model<ValueType>>(), input, bisimulationSettings);
+                result.changed = true;
             }
             
-            if (parametricSettings.transformContinuousModel() && (result.first->isOfType(storm::models::ModelType::Ctmc) || result.first->isOfType(storm::models::ModelType::MarkovAutomaton))) {
-                result.first = storm::api::transformContinuousToDiscreteTimeSparseModel(std::move(*result.first->template as<storm::models::sparse::Model<ValueType>>()), storm::api::extractFormulasFromProperties(input.properties));
-                result.second = true;
+            if (parametricSettings.transformContinuousModel() && (model->isOfType(storm::models::ModelType::Ctmc) || model->isOfType(storm::models::ModelType::MarkovAutomaton))) {
+                auto transformResult = storm::api::transformContinuousToDiscreteTimeSparseModel(std::move(*model->template as<storm::models::sparse::Model<ValueType>>()), storm::api::extractFormulasFromProperties(input.properties));
+                result.model = transformResult.first;
+                // Set transformed properties as new properties in input
+                result.formulas = transformResult.second;
+                result.changed = true;
             }
             
             return result;
         }
         
         template <storm::dd::DdType DdType, typename ValueType>
-        std::pair<std::shared_ptr<storm::models::ModelBase>, bool> preprocessDdModel(std::shared_ptr<storm::models::symbolic::Model<DdType, ValueType>> const& model, SymbolicInput const& input) {
-            
-            std::pair<std::shared_ptr<storm::models::ModelBase>, bool> result = std::make_pair(model, false);
-        
+        PreprocessResult preprocessDdModel(std::shared_ptr<storm::models::symbolic::Model<DdType, ValueType>> const& model, SymbolicInput const& input) {
             auto coreSettings = storm::settings::getModule<storm::settings::modules::CoreSettings>();
+            auto generalSettings = storm::settings::getModule<storm::settings::modules::GeneralSettings>();
+            auto bisimulationSettings = storm::settings::getModule<storm::settings::modules::BisimulationSettings>();
+
+            PreprocessResult result(model, false);
+
             if (coreSettings.getEngine() == storm::settings::modules::CoreSettings::Engine::Hybrid) {
-                // Currently, hybrid engine for parametric models just referrs to building the model symbolically.
+                // Currently, hybrid engine for parametric models just refers to building the model symbolically.
                 STORM_LOG_INFO("Translating symbolic model to sparse model...");
-                result.first = storm::api::transformSymbolicToSparseModel(model);
-                result.second = true;
+                result.model = storm::api::transformSymbolicToSparseModel(model);
+                result.changed = true;
                 // Invoke preprocessing on the sparse model
-                auto sparsePreprocessingResult = storm::pars::preprocessSparseModel<ValueType>(result.first->as<storm::models::sparse::Model<ValueType>>(), input);
-                if (sparsePreprocessingResult.second) {
-                    result.first = sparsePreprocessingResult.first;
+                PreprocessResult sparsePreprocessingResult = storm::pars::preprocessSparseModel<ValueType>(result.model->as<storm::models::sparse::Model<ValueType>>(), input);
+                if (sparsePreprocessingResult.changed) {
+                    result.model = sparsePreprocessingResult.model;
+                    result.formulas = sparsePreprocessingResult.formulas;
+                }
+            } else {
+                STORM_LOG_ASSERT(coreSettings.getEngine() == storm::settings::modules::CoreSettings::Engine::Dd, "Expected Dd engine.");
+                if (generalSettings.isBisimulationSet()) {
+                    result.model = storm::cli::preprocessDdModelBisimulation(result.model->template as<storm::models::symbolic::Model<DdType, ValueType>>(), input, bisimulationSettings);
+                    result.changed = true;
                 }
             }
             return result;
         }
         
         template <storm::dd::DdType DdType, typename ValueType>
-        std::pair<std::shared_ptr<storm::models::ModelBase>, bool> preprocessModel(std::shared_ptr<storm::models::ModelBase> const& model, SymbolicInput const& input) {
+        PreprocessResult preprocessModel(std::shared_ptr<storm::models::ModelBase> const& model, SymbolicInput const& input) {
             storm::utility::Stopwatch preprocessingWatch(true);
-            
-            std::pair<std::shared_ptr<storm::models::ModelBase>, bool> result = std::make_pair(model, false);
+
+            PreprocessResult result(model, false);
             if (model->isSparseModel()) {
-                result = storm::pars::preprocessSparseModel<ValueType>(result.first->as<storm::models::sparse::Model<ValueType>>(), input);
+                result = storm::pars::preprocessSparseModel<ValueType>(result.model->as<storm::models::sparse::Model<ValueType>>(), input);
             } else {
                 STORM_LOG_ASSERT(model->isSymbolicModel(), "Unexpected model type.");
-                result = storm::pars::preprocessDdModel<DdType, ValueType>(result.first->as<storm::models::symbolic::Model<DdType, ValueType>>(), input);
+                result = storm::pars::preprocessDdModel<DdType, ValueType>(result.model->as<storm::models::symbolic::Model<DdType, ValueType>>(), input);
             }
             
-            if (result.second) {
+            if (result.changed) {
                 STORM_PRINT_AND_LOG(std::endl << "Time for model preprocessing: " << preprocessingWatch << "." << std::endl << std::endl);
             }
             return result;
@@ -235,7 +257,7 @@ namespace storm {
                     STORM_PRINT_AND_LOG("Time for model checking: " << *watch << "." << std::endl << std::endl);
                 }
             } else {
-                STORM_PRINT_AND_LOG(" failed, property is unsupported by selected engine/settings." << std::endl);
+                STORM_LOG_ERROR("Property is unsupported by selected engine/settings." << std::endl);
             }
         }
         
@@ -353,6 +375,11 @@ namespace storm {
                                                     boost::optional<ValueType> rationalFunction = result->asExplicitQuantitativeCheckResult<ValueType>()[*model->getInitialStates().begin()];
                                                     storm::api::exportParametricResultToFile(rationalFunction, storm::analysis::ConstraintCollector<ValueType>(*dtmc), parametricSettings.exportResultPath());
                                                 }
+                                                else if (parametricSettings.exportResultToFile() && model->isOfType(storm::models::ModelType::Ctmc)) {
+                                                    auto ctmc = model->template as<storm::models::sparse::Ctmc<ValueType>>();
+                                                    boost::optional<ValueType> rationalFunction = result->asExplicitQuantitativeCheckResult<ValueType>()[*model->getInitialStates().begin()];
+                                                    storm::api::exportParametricResultToFile(rationalFunction, storm::analysis::ConstraintCollector<ValueType>(*ctmc), parametricSettings.exportResultPath());
+                                                }
                                             });
             } else {
                 STORM_LOG_TRACE("Sampling the model at given points.");
@@ -461,11 +488,47 @@ namespace storm {
                 }
             }
         }
-        
+
+        template <storm::dd::DdType DdType, typename ValueType>
+        void verifyPropertiesWithSymbolicEngine(std::shared_ptr<storm::models::symbolic::Model<DdType, ValueType>> const& model, SymbolicInput const& input, SampleInformation<ValueType> const& samples) {
+            if (samples.empty()) {
+                verifyProperties<ValueType>(input.properties,
+                                            [&model] (std::shared_ptr<storm::logic::Formula const> const& formula) {
+                                                std::unique_ptr<storm::modelchecker::CheckResult> result = storm::api::verifyWithDdEngine<DdType, ValueType>(model, storm::api::createTask<ValueType>(formula, true));
+                                                if (result) {
+                                                    result->filter(storm::modelchecker::SymbolicQualitativeCheckResult<DdType>(model->getReachableStates(), model->getInitialStates()));
+                                                }
+                                                return result;
+                                            },
+                                            [&model] (std::unique_ptr<storm::modelchecker::CheckResult> const& result) {
+                                                auto parametricSettings = storm::settings::getModule<storm::settings::modules::ParametricSettings>();
+                                                if (parametricSettings.exportResultToFile() && model->isOfType(storm::models::ModelType::Dtmc)) {
+                                                    //auto dtmc = model->template as<storm::models::symbolic::Dtmc<DdType, ValueType>>();
+                                                    //boost::optional<ValueType> rationalFunction = result->asSymbolicQuantitativeCheckResult<DdType, ValueType>().sum();
+                                                    //storm::api::exportParametricResultToFile(rationalFunction, storm::analysis::ConstraintCollector<ValueType>(*dtmc), parametricSettings.exportResultPath());
+                                                }
+                                            });
+            } else {
+                STORM_LOG_THROW(false, storm::exceptions::NotSupportedException, "Sampling is not supported in the symbolic engine.");
+            }
+        }
+
+        template <storm::dd::DdType DdType, typename ValueType>
+        void verifyWithDdEngine(std::shared_ptr<storm::models::symbolic::Model<DdType, ValueType>> const& model, SymbolicInput const& input, std::vector<storm::storage::ParameterRegion<ValueType>> const& regions, SampleInformation<ValueType> const& samples) {
+            if (regions.empty()) {
+                storm::pars::verifyPropertiesWithSymbolicEngine(model, input, samples);
+            } else {
+                STORM_LOG_THROW(false, storm::exceptions::NotSupportedException, "Region verification is not supported in the symbolic engine.");
+            }
+        }
+
         template <storm::dd::DdType DdType, typename ValueType>
         void verifyParametricModel(std::shared_ptr<storm::models::ModelBase> const& model, SymbolicInput const& input, std::vector<storm::storage::ParameterRegion<ValueType>> const& regions, SampleInformation<ValueType> const& samples) {
-            STORM_LOG_ASSERT(model->isSparseModel(), "Unexpected model type.");
-            storm::pars::verifyWithSparseEngine<ValueType>(model->as<storm::models::sparse::Model<ValueType>>(), input, regions, samples);
+            if (model->isSparseModel()) {
+                storm::pars::verifyWithSparseEngine<ValueType>(model->as<storm::models::sparse::Model<ValueType>>(), input, regions, samples);
+            } else {
+                storm::pars::verifyWithDdEngine<DdType, ValueType>(model->as<storm::models::symbolic::Model<DdType, ValueType>>(), input, regions, samples);
+            }
         }
         
         template <storm::dd::DdType DdType, typename ValueType>
@@ -492,8 +555,20 @@ namespace storm {
             
             if (model) {
                 auto preprocessingResult = storm::pars::preprocessModel<DdType, ValueType>(model, input);
-                if (preprocessingResult.second) {
-                    model = preprocessingResult.first;
+                if (preprocessingResult.changed) {
+                    model = preprocessingResult.model;
+
+                    if (preprocessingResult.formulas) {
+                        std::vector<storm::jani::Property> newProperties;
+                        for (size_t i = 0; i < preprocessingResult.formulas.get().size(); ++i) {
+                            auto formula = preprocessingResult.formulas.get().at(i);
+                            STORM_LOG_ASSERT(i < input.properties.size(), "Index " << i << " greater than number of properties.");
+                            storm::jani::Property property = input.properties.at(i);
+                            newProperties.push_back(storm::jani::Property(property.getName(), formula, property.getUndefinedConstants(), property.getComment()));
+                        }
+                        input.properties = newProperties;
+                    }
+
                     model->printModelInformationToStream(std::cout);
                 }
             }

src/storm-pars/api/region.h

@@ -91,7 +91,7 @@ namespace storm {
             if (consideredModel->isOfType(storm::models::ModelType::Ctmc) || consideredModel->isOfType(storm::models::ModelType::MarkovAutomaton)) {
                     STORM_LOG_WARN("Parameter lifting not supported for continuous time models. Transforming continuous model to discrete model...");
                     std::vector<std::shared_ptr<storm::logic::Formula const>> taskFormulaAsVector { task.getFormula().asSharedPointer() };
-                    consideredModel = storm::api::transformContinuousToDiscreteTimeSparseModel(consideredModel, taskFormulaAsVector);
+                    consideredModel = storm::api::transformContinuousToDiscreteTimeSparseModel(consideredModel, taskFormulaAsVector).first;
                     STORM_LOG_THROW(consideredModel->isOfType(storm::models::ModelType::Dtmc) || consideredModel->isOfType(storm::models::ModelType::Mdp), storm::exceptions::UnexpectedException, "Transformation to discrete time model has failed.");
             }
             
@@ -121,7 +121,7 @@ namespace storm {
             if (consideredModel->isOfType(storm::models::ModelType::Ctmc) || consideredModel->isOfType(storm::models::ModelType::MarkovAutomaton)) {
                     STORM_LOG_WARN("Parameter lifting not supported for continuous time models. Transforming continuous model to discrete model...");
                     std::vector<std::shared_ptr<storm::logic::Formula const>> taskFormulaAsVector { task.getFormula().asSharedPointer() };
-                    consideredModel = storm::api::transformContinuousToDiscreteTimeSparseModel(consideredModel, taskFormulaAsVector);
+                    consideredModel = storm::api::transformContinuousToDiscreteTimeSparseModel(consideredModel, taskFormulaAsVector).first;
                     STORM_LOG_THROW(consideredModel->isOfType(storm::models::ModelType::Dtmc) || consideredModel->isOfType(storm::models::ModelType::Mdp), storm::exceptions::UnexpectedException, "Transformation to discrete time model has failed.");
             }
             

src/storm-pars/parser/ParameterRegionParser.cpp

@@ -1,3 +1,4 @@
+#include <storm/exceptions/WrongFormatException.h>
 #include "storm-pars/parser/ParameterRegionParser.h"
 
 #include "storm/utility/macros.h"
@@ -10,13 +11,13 @@ namespace storm {
 
         template<typename ParametricType>
         void ParameterRegionParser<ParametricType>::parseParameterBoundaries(Valuation& lowerBoundaries, Valuation& upperBoundaries, std::string const& parameterBoundariesString, std::set<VariableType> const& consideredVariables) {
-            
             std::string::size_type positionOfFirstRelation = parameterBoundariesString.find("<=");
             STORM_LOG_THROW(positionOfFirstRelation!=std::string::npos, storm::exceptions::InvalidArgumentException, "When parsing the region" << parameterBoundariesString << " I could not find  a '<=' after the first number");
             std::string::size_type positionOfSecondRelation = parameterBoundariesString.find("<=", positionOfFirstRelation+2);
             STORM_LOG_THROW(positionOfSecondRelation!=std::string::npos, storm::exceptions::InvalidArgumentException, "When parsing the region" << parameterBoundariesString << " I could not find  a '<=' after the parameter");
 
             std::string parameter = parameterBoundariesString.substr(positionOfFirstRelation+2,positionOfSecondRelation-(positionOfFirstRelation+2));
+
             //removes all whitespaces from the parameter string:
             parameter.erase(std::remove_if (parameter.begin(), parameter.end(), ::isspace), parameter.end());
             STORM_LOG_THROW(parameter.length()>0, storm::exceptions::InvalidArgumentException, "When parsing the region" << parameterBoundariesString << " I could not find a parameter");
@@ -25,17 +26,19 @@ namespace storm {
             for (auto const& v : consideredVariables) {
                 std::stringstream stream;
                 stream << v;
-                std::string vAsString = stream.str();
                 if (parameter == stream.str()) {
                     var = std::make_unique<VariableType>(v);
+                    break;
                 }
             }
-            STORM_LOG_ASSERT(var, "Could not find parameter " << parameter << " in the set of considered variables");
-            
-            CoefficientType lb = storm::utility::convertNumber<CoefficientType>(parameterBoundariesString.substr(0,positionOfFirstRelation));
-            CoefficientType ub = storm::utility::convertNumber<CoefficientType>(parameterBoundariesString.substr(positionOfSecondRelation+2));
-            lowerBoundaries.emplace(std::make_pair(*var, lb));
-            upperBoundaries.emplace(std::make_pair(*var, ub));
+            if (var) {
+                CoefficientType lb = storm::utility::convertNumber<CoefficientType>(parameterBoundariesString.substr(0,positionOfFirstRelation));
+                CoefficientType ub = storm::utility::convertNumber<CoefficientType>(parameterBoundariesString.substr(positionOfSecondRelation+2));
+                lowerBoundaries.emplace(std::make_pair(*var, lb));
+                upperBoundaries.emplace(std::make_pair(*var, ub));
+            } else {
+                STORM_LOG_WARN("Could not find parameter " << parameter << " in the set of considered variables. Ignoring this parameter.");
+            }
         }
 
         template<typename ParametricType>
@@ -49,6 +52,12 @@ namespace storm {
                     parseParameterBoundaries(lowerBoundaries, upperBoundaries, parameterBoundary, consideredVariables);
                 }
             }
+
+            // Check that all considered variables are bounded
+            for (auto const& v : consideredVariables) {
+                STORM_LOG_THROW(lowerBoundaries.count(v) > 0, storm::exceptions::WrongFormatException, "Variable " << v << " was not defined in region string.");
+                STORM_LOG_ASSERT(upperBoundaries.count(v) > 0, "Variable " << v << " has a lower but not an upper bound.");
+            }
             return storm::storage::ParameterRegion<ParametricType>(std::move(lowerBoundaries), std::move(upperBoundaries));
         }
 

src/storm-parsers/parser/DirectEncodingParser.cpp

@@ -106,13 +106,13 @@ namespace storm {
             // Initialize
             auto modelComponents = std::make_shared<storm::storage::sparse::ModelComponents<ValueType, RewardModelType>>();
             bool nonDeterministic = (type == storm::models::ModelType::Mdp || type == storm::models::ModelType::MarkovAutomaton || type == storm::models::ModelType::Pomdp);
-            bool continousTime = (type == storm::models::ModelType::Ctmc || type == storm::models::ModelType::MarkovAutomaton);
+            bool continuousTime = (type == storm::models::ModelType::Ctmc || type == storm::models::ModelType::MarkovAutomaton);
             storm::storage::SparseMatrixBuilder<ValueType> builder = storm::storage::SparseMatrixBuilder<ValueType>(0, 0, 0, false, nonDeterministic, 0);
             modelComponents->stateLabeling = storm::models::sparse::StateLabeling(stateSize);
             modelComponents->observabilityClasses = std::vector<uint32_t>();
             modelComponents->observabilityClasses->resize(stateSize);
             std::vector<std::vector<ValueType>> stateRewards;
-            if (continousTime) {
+            if (continuousTime) {
                 modelComponents->exitRates = std::vector<ValueType>(stateSize);
                 if (type == storm::models::ModelType::MarkovAutomaton) {
                     modelComponents->markovianStates = storm::storage::BitVector(stateSize);

src/storm-pomdp-cli/settings/modules/POMDPSettings.h

@@ -4,20 +4,18 @@
 #include "storm/settings/modules/ModuleSettings.h"
 #include "storm-pomdp/storage/PomdpMemory.h"
 
-#include "storm-dft/builder/DftExplorationHeuristic.h"
-
 namespace storm {
     namespace settings {
         namespace modules {
 
             /*!
-             * This class represents the settings for DFT model checking.
+             * This class represents the settings for POMDP model checking.
              */
             class POMDPSettings : public ModuleSettings {
             public:
 
                 /*!
-                 * Creates a new set of DFT settings.
+                 * Creates a new set of POMDP settings.
                  */
                 POMDPSettings();
 

src/storm/analysis/GraphConditions.cpp

@@ -38,16 +38,17 @@ namespace storm {
                     auto const& transitionVars = entry.gatherVariables();
                     variableSet.insert(transitionVars.begin(), transitionVars.end());
                     if (entry.denominator().isConstant()) {
-                        if (entry.denominatorAsNumber() > 0) {
+                        assert(entry.denominator().constantPart() != 0);
+                        if (entry.denominator().constantPart() > 0) {
                             wellformedConstraintSet.emplace(entry.nominator().polynomialWithCoefficient(), storm::CompareRelation::GEQ);
-                        } else if (entry.denominatorAsNumber() < 0) {
+                        } else if (entry.denominator().constantPart() < 0) {
                             wellformedConstraintSet.emplace(entry.nominator().polynomialWithCoefficient(), storm::CompareRelation::LEQ);
                         } else {
                             assert(false); // Should fail before.
                         }
                     } else {
                         wellformedConstraintSet.emplace(entry.denominator().polynomialWithCoefficient(), storm::CompareRelation::NEQ);
-                        STORM_LOG_THROW(false, storm::exceptions::NotImplementedException, "Rational functions at state rewards not yet supported.");
+                        wellformedConstraintSet.emplace(carl::FormulaType::ITE, typename ConstraintType<ValueType>::val(entry.denominator().polynomialWithCoefficient(), storm::CompareRelation::GREATER), typename ConstraintType<ValueType>::val(entry.nominator().polynomialWithCoefficient(), storm::CompareRelation::GEQ), typename ConstraintType<ValueType>::val(entry.nominator().polynomialWithCoefficient(), storm::CompareRelation::LEQ));
                     }
                 }
             }
@@ -55,47 +56,70 @@ namespace storm {
 
         template <typename ValueType>
         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 transitionIt = model.getTransitionMatrix().begin(action); transitionIt != model.getTransitionMatrix().end(action); ++transitionIt) {
-                    auto const& transition = *transitionIt;
-                    sum += transition.getValue();
-                    if (!storm::utility::isConstant(transition.getValue())) {
-                        auto const& transitionVars = transition.getValue().gatherVariables();
-                        variableSet.insert(transitionVars.begin(), transitionVars.end());
-                        // Assert: 0 <= transition <= 1
+
+            if (model.getType() != storm::models::ModelType::Ctmc) {
+
+                for(uint_fast64_t action = 0; action < model.getTransitionMatrix().getRowCount(); ++action) {
+                    ValueType sum = storm::utility::zero<ValueType>();
+
+                    for (auto transitionIt = model.getTransitionMatrix().begin(action); transitionIt != model.getTransitionMatrix().end(action); ++transitionIt) {
+                        auto const& transition = *transitionIt;
+                        sum += transition.getValue();
+                        if (!storm::utility::isConstant(transition.getValue())) {
+                            auto const& transitionVars = transition.getValue().gatherVariables();
+                            variableSet.insert(transitionVars.begin(), transitionVars.end());
+                            // Assert: 0 <= transition <= 1
+                            if (transition.getValue().denominator().isConstant()) {
+                                assert(transition.getValue().denominator().constantPart() != 0);
+                                if (transition.getValue().denominator().constantPart() > 0) {
+                                    // Assert: nom <= denom
+                                    wellformedConstraintSet.emplace((transition.getValue().nominator() - transition.getValue().denominator()).polynomialWithCoefficient(), storm::CompareRelation::LEQ);
+                                    // Assert: nom >= 0
+                                    wellformedConstraintSet.emplace(transition.getValue().nominator().polynomialWithCoefficient(), storm::CompareRelation::GEQ);
+                                } else if (transition.getValue().denominator().constantPart() < 0) {
+                                    // Assert nom >= denom
+                                    wellformedConstraintSet.emplace((transition.getValue().nominator() - transition.getValue().denominator()).polynomialWithCoefficient(), storm::CompareRelation::GEQ);
+                                    // Assert: nom <= 0
+                                    wellformedConstraintSet.emplace(transition.getValue().nominator().polynomialWithCoefficient(), storm::CompareRelation::LEQ);
+                                } else {
+                                    STORM_LOG_ASSERT(false, "Denominator must not equal 0.");
+                                }
+                            } else {
+                                // Assert: denom != 0
+                                wellformedConstraintSet.emplace(transition.getValue().denominator().polynomialWithCoefficient(), storm::CompareRelation::NEQ);
+                                 // Assert: transition >= 0 <==> if denom > 0 then nom >= 0 else nom <= 0
+                                wellformedConstraintSet.emplace(carl::FormulaType::ITE, typename ConstraintType<ValueType>::val(transition.getValue().denominator().polynomialWithCoefficient(), storm::CompareRelation::GREATER), typename ConstraintType<ValueType>::val(transition.getValue().nominator().polynomialWithCoefficient(), storm::CompareRelation::GEQ), typename ConstraintType<ValueType>::val(transition.getValue().nominator().polynomialWithCoefficient(), storm::CompareRelation::LEQ));
+                                 // TODO: Assert: transition <= 1 <==> if denom > 0 then nom - denom <= 0 else nom - denom >= 0
+                            }
+                            // Assert: transition > 0
+                            graphPreservingConstraintSet.emplace(transition.getValue().nominator().polynomialWithCoefficient(), storm::CompareRelation::NEQ);
+                        }
+                    }
+                    STORM_LOG_ASSERT(!storm::utility::isConstant(sum) || storm::utility::isOne(sum), "If the sum is a constant, it must be equal to 1.");
+                    if(!storm::utility::isConstant(sum)) {
+                        // Assert: sum == 1
+                        wellformedConstraintSet.emplace((sum.nominator() - sum.denominator()).polynomialWithCoefficient(), storm::CompareRelation::EQ);
+                    }
+                }
+            } else {
+                for (auto const& transition : model.getTransitionMatrix()) {
+                    if(!transition.getValue().isConstant()) {
                         if (transition.getValue().denominator().isConstant()) {
                             assert(transition.getValue().denominator().constantPart() != 0);
                             if (transition.getValue().denominator().constantPart() > 0) {
-                                // Assert: nom <= denom
-                                wellformedConstraintSet.emplace((transition.getValue().nominator() - transition.getValue().denominator()).polynomialWithCoefficient(), storm::CompareRelation::LEQ);
-                                // Assert: nom >= 0
                                 wellformedConstraintSet.emplace(transition.getValue().nominator().polynomialWithCoefficient(), storm::CompareRelation::GEQ);
                             } else if (transition.getValue().denominator().constantPart() < 0) {
-                                // Assert nom >= denom
-                                wellformedConstraintSet.emplace((transition.getValue().nominator() - transition.getValue().denominator()).polynomialWithCoefficient(), storm::CompareRelation::GEQ);
-                                // Assert: nom <= 0
                                 wellformedConstraintSet.emplace(transition.getValue().nominator().polynomialWithCoefficient(), storm::CompareRelation::LEQ);
                             } else {
-                                STORM_LOG_ASSERT(false, "Denominator must not equal 0.");
+                                assert(false); // Should fail before.
                             }
                         } else {
-                            // Assert: denom != 0
                             wellformedConstraintSet.emplace(transition.getValue().denominator().polynomialWithCoefficient(), storm::CompareRelation::NEQ);
-                             // Assert: transition >= 0 <==> if denom > 0 then nom >= 0 else nom <= 0
                             wellformedConstraintSet.emplace(carl::FormulaType::ITE, typename ConstraintType<ValueType>::val(transition.getValue().denominator().polynomialWithCoefficient(), storm::CompareRelation::GREATER), typename ConstraintType<ValueType>::val(transition.getValue().nominator().polynomialWithCoefficient(), storm::CompareRelation::GEQ), typename ConstraintType<ValueType>::val(transition.getValue().nominator().polynomialWithCoefficient(), storm::CompareRelation::LEQ));
-                             // TODO: Assert: transition <= 1 <==> if denom > 0 then nom - denom <= 0 else nom - denom >= 0
                         }
-                        // Assert: transition > 0
                         graphPreservingConstraintSet.emplace(transition.getValue().nominator().polynomialWithCoefficient(), storm::CompareRelation::NEQ);
                     }
                 }
-                STORM_LOG_ASSERT(!storm::utility::isConstant(sum) || storm::utility::isOne(sum), "If the sum is a constant, it must be equal to 1.");
-                if(!storm::utility::isConstant(sum)) {
-                    // Assert: sum == 1
-                    wellformedConstraintSet.emplace((sum.nominator() - sum.denominator()).polynomialWithCoefficient(), storm::CompareRelation::EQ);
-                }
             }
 
             if (model.getType() == storm::models::ModelType::Ctmc) {
@@ -117,16 +141,17 @@ namespace storm {
                     for (auto const& entry : rewModelEntry.second.getTransitionRewardMatrix()) {
                         if(!entry.getValue().isConstant()) {
                             if (entry.getValue().denominator().isConstant()) {
-                                if (entry.getValue().denominatorAsNumber() > 0) {
+                                assert(entry.getValue().denominator().constantPart() != 0);
+                                if (entry.getValue().denominator().constantPart() > 0) {
                                     wellformedConstraintSet.emplace(entry.getValue().nominator().polynomialWithCoefficient(), storm::CompareRelation::GEQ);
-                                } else if (entry.getValue().denominatorAsNumber() < 0) {
+                                } else if (entry.getValue().denominator().constantPart() < 0) {
                                     wellformedConstraintSet.emplace(entry.getValue().nominator().polynomialWithCoefficient(), storm::CompareRelation::LEQ);
                                 } else {
                                     assert(false); // Should fail before.
                                 }
                             } else {
                                 wellformedConstraintSet.emplace(entry.getValue().denominator().polynomialWithCoefficient(), storm::CompareRelation::NEQ);
-                                STORM_LOG_THROW(false, storm::exceptions::NotImplementedException, "Rational functions at transition rewards are not yet supported.");
+                                wellformedConstraintSet.emplace(carl::FormulaType::ITE, typename ConstraintType<ValueType>::val(entry.getValue().denominator().polynomialWithCoefficient(), storm::CompareRelation::GREATER), typename ConstraintType<ValueType>::val(entry.getValue().nominator().polynomialWithCoefficient(), storm::CompareRelation::GEQ), typename ConstraintType<ValueType>::val(entry.getValue().nominator().polynomialWithCoefficient(), storm::CompareRelation::LEQ));
                             }
                         }
                     }

src/storm/api/transformation.h

@@ -13,25 +13,28 @@ namespace storm {
         
         /*!
          * Transforms the given continuous model to a discrete time model.
-         * If such a transformation does not preserve one of the given formulas, an error is issued.
+         * If such a transformation does not preserve one of the given formulas, a warning is issued.
          */
         template <typename ValueType>
-        std::shared_ptr<storm::models::sparse::Model<ValueType>> transformContinuousToDiscreteTimeSparseModel(std::shared_ptr<storm::models::sparse::Model<ValueType>> const& model, std::vector<std::shared_ptr<storm::logic::Formula const>> const& formulas) {
+        std::pair<std::shared_ptr<storm::models::sparse::Model<ValueType>>, std::vector<std::shared_ptr<storm::logic::Formula const>>>  transformContinuousToDiscreteTimeSparseModel(std::shared_ptr<storm::models::sparse::Model<ValueType>> const& model, std::vector<std::shared_ptr<storm::logic::Formula const>> const& formulas) {
             
             storm::transformer::ContinuousToDiscreteTimeModelTransformer<ValueType> transformer;
             
-            for (auto const& formula : formulas) {
-                STORM_LOG_THROW(transformer.preservesFormula(*formula), storm::exceptions::InvalidOperationException, "Transformation to discrete time model does not preserve formula " << *formula << ".");
+            std::string timeRewardName = "_time";
+            while(model->hasRewardModel(timeRewardName)) {
+                timeRewardName += "_";
             }
+            auto newFormulas = transformer.checkAndTransformFormulas(formulas, timeRewardName);
+            STORM_LOG_WARN_COND(newFormulas.size() == formulas.size(), "Transformation of a " << model->getType() << " to a discrete time model does not preserve all properties.");
             
             if (model->isOfType(storm::models::ModelType::Ctmc)) {
-                return transformer.transform(*model->template as<storm::models::sparse::Ctmc<ValueType>>());
+                return std::make_pair(transformer.transform(*model->template as<storm::models::sparse::Ctmc<ValueType>>(), timeRewardName), newFormulas);
             } else if (model->isOfType(storm::models::ModelType::MarkovAutomaton)) {
-                return transformer.transform(*model->template as<storm::models::sparse::MarkovAutomaton<ValueType>>());
+                return std::make_pair(transformer.transform(*model->template as<storm::models::sparse::MarkovAutomaton<ValueType>>(), timeRewardName), newFormulas);
             } else {
                 STORM_LOG_THROW(false, storm::exceptions::NotSupportedException, "Transformation of a " << model->getType() << " to a discrete time model is not supported");
             }
-            return nullptr;
+            return std::make_pair(nullptr, newFormulas);;
         }
 
         /*!
@@ -40,22 +43,25 @@ namespace storm {
          * If such a transformation does not preserve one of the given formulas, an error is issued.
          */
         template <typename ValueType>
-        std::shared_ptr<storm::models::sparse::Model<ValueType>> transformContinuousToDiscreteTimeSparseModel(storm::models::sparse::Model<ValueType>&& model, std::vector<std::shared_ptr<storm::logic::Formula const>> const& formulas) {
+        std::pair<std::shared_ptr<storm::models::sparse::Model<ValueType>>, std::vector<std::shared_ptr<storm::logic::Formula const>>> transformContinuousToDiscreteTimeSparseModel(storm::models::sparse::Model<ValueType>&& model, std::vector<std::shared_ptr<storm::logic::Formula const>> const& formulas) {
             
             storm::transformer::ContinuousToDiscreteTimeModelTransformer<ValueType> transformer;
             
-            for (auto const& formula : formulas) {
-                STORM_LOG_THROW(transformer.preservesFormula(*formula), storm::exceptions::InvalidOperationException, "Transformation to discrete time model does not preserve formula " << *formula << ".");
+             std::string timeRewardName = "_time";
+            while(model.hasRewardModel(timeRewardName)) {
+                timeRewardName += "_";
             }
-            
+            auto newFormulas = transformer.checkAndTransformFormulas(formulas, timeRewardName);
+            STORM_LOG_WARN_COND(newFormulas.size() == formulas.size(), "Transformation of a " << model.getType() << " to a discrete time model does not preserve all properties.");
+           
             if (model.isOfType(storm::models::ModelType::Ctmc)) {
-                return transformer.transform(std::move(*model.template as<storm::models::sparse::Ctmc<ValueType>>()));
+                return std::make_pair(transformer.transform(std::move(*model.template as<storm::models::sparse::Ctmc<ValueType>>()), timeRewardName), newFormulas);
             } else if (model.isOfType(storm::models::ModelType::MarkovAutomaton)) {
-                return transformer.transform(std::move(*model.template as<storm::models::sparse::MarkovAutomaton<ValueType>>()));
+                return std::make_pair(transformer.transform(std::move(*model.template as<storm::models::sparse::MarkovAutomaton<ValueType>>()), timeRewardName), newFormulas);
             } else {
                 STORM_LOG_THROW(false, storm::exceptions::NotSupportedException, "Transformation of a " << model.getType() << " to a discrete time model is not supported.");
             }
-            return nullptr;
+            return std::make_pair(nullptr, newFormulas);;
             
         }
         

src/storm/builder/ParallelCompositionBuilder.h

@@ -21,4 +21,4 @@ namespace storm {
     }
 }
 
-#endif	/* EXPLICITDFTMODELBUPARALLELCOMPOSITIONBUILDER_HILDERAPPROX_H */
+#endif	/* PARALLELCOMPOSITIONBUILDER_*/

src/storm/exceptions/BaseException.cpp

@@ -5,11 +5,11 @@ namespace storm {
         BaseException::BaseException() : exception() {
             // Intentionally left empty.
         }
-        
+
         BaseException::BaseException(BaseException const& other) : exception(other), stream(other.stream.str()) {
             // Intentionally left empty.
         }
-        
+
         BaseException::BaseException(char const* cstr) {
             stream << cstr;
         }
@@ -17,10 +17,21 @@ namespace storm {
 		BaseException::~BaseException() {
 			// Intentionally left empty.
 		}
-        
+
         const char* BaseException::what() const NOEXCEPT {
-            errorString = this->stream.str();
+            errorString = this->type() + ": " + this->stream.str();
+            if (!this->additionalInfo().empty()) {
+                errorString += " " + this->additionalInfo();
+            }
             return errorString.c_str();
         }
+
+        std::string BaseException::type() const {
+            return "BaseException";
+        }
+
+        std::string BaseException::additionalInfo() const {
+            return "";
+        }
     }
 }

src/storm/exceptions/BaseException.h

@@ -42,7 +42,17 @@ namespace storm {
              * @return The message associated with this exception.
              */
             virtual const char* what() const NOEXCEPT override;
-            
+
+            /*!
+             * Returns the type of the exception.
+             */
+            virtual std::string type() const;
+
+            /*!
+             * Returns additional information about the exception.
+             */
+            virtual std::string additionalInfo() const;
+
         protected:
             // This stream stores the message of this exception.
             std::stringstream stream;

src/storm/exceptions/ExceptionMacros.h

@@ -16,6 +16,9 @@ exception_name(exception_name const& cp) : BaseException(cp) { \
 } \
 ~exception_name() throw() { \
 } \
+virtual std::string type() const override { \
+    return #exception_name; \
+} \
 template<typename T> \
 exception_name& operator<<(T const& var) { \
     this->stream << var; \

src/storm/logic/ExpectedTimeToExpectedRewardVisitor.cpp

@@ -0,0 +1,28 @@
+#include "storm/logic/ExpectedTimeToExpectedRewardVisitor.h"
+#include "storm/logic/Formulas.h"
+
+#include "storm/utility/macros.h"
+
+#include "storm/exceptions/InvalidPropertyException.h"
+
+namespace storm {
+    namespace logic {
+
+        ExpectedTimeToExpectedRewardVisitor::ExpectedTimeToExpectedRewardVisitor(std::string const& timeRewardModelName) : timeRewardModelName(timeRewardModelName) {
+            // Intentionally left empty
+        }
+        
+        std::shared_ptr<Formula> ExpectedTimeToExpectedRewardVisitor::substitute(Formula const& f) const {
+            boost::any result = f.accept(*this, boost::any());
+            return boost::any_cast<std::shared_ptr<Formula>>(result);
+        }
+ 
+        boost::any ExpectedTimeToExpectedRewardVisitor::visit(TimeOperatorFormula const& f, boost::any const& data) const {
+            STORM_LOG_THROW(f.getSubformula().isEventuallyFormula(), storm::exceptions::InvalidPropertyException, "Expected eventually formula within time operator. Got " << f << " instead.");
+            std::shared_ptr<Formula> subsubformula = boost::any_cast<std::shared_ptr<Formula>>(f.getSubformula().asEventuallyFormula().getSubformula().accept(*this, data));
+            STORM_LOG_THROW(f.getSubformula().isReachabilityTimeFormula(), storm::exceptions::InvalidPropertyException, "Expected time path formula within time operator. Got " << f << " instead.");
+            std::shared_ptr<Formula> subformula = std::make_shared<EventuallyFormula>(subsubformula, storm::logic::FormulaContext::Reward);
+            return std::static_pointer_cast<Formula>(std::make_shared<RewardOperatorFormula>(subformula, timeRewardModelName, f.getOperatorInformation()));
+        }
+    }
+}

src/storm/logic/ExpectedTimeToExpectedRewardVisitor.h

@@ -0,0 +1,25 @@
+#pragma once
+
+#include <map>
+
+#include "storm/logic/CloneVisitor.h"
+
+#include "storm/storage/expressions/Expression.h"
+
+namespace storm {
+    namespace logic {
+        
+        class ExpectedTimeToExpectedRewardVisitor : public CloneVisitor {
+        public:
+            ExpectedTimeToExpectedRewardVisitor(std::string const& timeRewardModelName);
+            
+            std::shared_ptr<Formula> substitute(Formula const& f) const;
+            
+            virtual boost::any visit(TimeOperatorFormula const& f, boost::any const& data) const override;
+
+        private:
+            std::string const& timeRewardModelName;
+        };
+        
+    }
+}

src/storm/modelchecker/csl/SparseMarkovAutomatonCslModelChecker.cpp

@@ -70,7 +70,7 @@ namespace storm {
             std::unique_ptr<CheckResult> rightResultPointer = this->check(env, pathFormula.getRightSubformula());
             ExplicitQualitativeCheckResult const& rightResult = rightResultPointer->asExplicitQualitativeCheckResult();
 
-            STORM_LOG_THROW(pathFormula.getTimeBoundReference().isTimeBound(), storm::exceptions::NotImplementedException, "Currently step-bounded and reward=bpimded properties on MAs are not supported.");
+            STORM_LOG_THROW(pathFormula.getTimeBoundReference().isTimeBound(), storm::exceptions::NotImplementedException, "Currently step-bounded and reward-bounded properties on MAs are not supported.");
             double lowerBound = 0;
             double upperBound = 0;
             if (pathFormula.hasLowerBound()) {

src/storm/models/sparse/Model.cpp

@@ -40,9 +40,9 @@ namespace storm {
                 // general components for all model types.
                 STORM_LOG_THROW(this->getTransitionMatrix().getColumnCount() == stateCount, storm::exceptions::IllegalArgumentException, "Invalid column count of transition matrix.");
                 STORM_LOG_ASSERT(components.rateTransitions || this->hasParameters() || this->getTransitionMatrix().isProbabilistic(), "The matrix is not probabilistic.");
-                STORM_LOG_THROW(this->getStateLabeling().getNumberOfItems() == stateCount, storm::exceptions::IllegalArgumentException, "Invalid item count of state labeling.");
+                STORM_LOG_THROW(this->getStateLabeling().getNumberOfItems() == stateCount, storm::exceptions::IllegalArgumentException, "Invalid item count (" << this->getStateLabeling().getNumberOfItems() << ") of state labeling (states: " << stateCount << ").");
                 for (auto const& rewardModel : this->getRewardModels()) {
-                    STORM_LOG_THROW(!rewardModel.second.hasStateRewards() || rewardModel.second.getStateRewardVector().size() == stateCount, storm::exceptions::IllegalArgumentException, "Invalid size of state reward vector.");
+                    STORM_LOG_THROW(!rewardModel.second.hasStateRewards() || rewardModel.second.getStateRewardVector().size() == stateCount, storm::exceptions::IllegalArgumentException, "Invalid size (" << rewardModel.second.getStateRewardVector().size() << ") of state reward vector (states:" << stateCount  << ").");
                     STORM_LOG_THROW(!rewardModel.second.hasStateActionRewards() || rewardModel.second.getStateActionRewardVector().size() == choiceCount, storm::exceptions::IllegalArgumentException, "Invalid size of state reward vector.");
                     STORM_LOG_ASSERT(!rewardModel.second.hasTransitionRewards() || rewardModel.second.getTransitionRewardMatrix().isSubmatrixOf(this->getTransitionMatrix()), "The transition reward matrix is not a submatrix of the transition matrix, i.e. there are rewards for transitions that do not exist.");
                 }
@@ -473,8 +473,15 @@ namespace storm {
                 }
                 return result;
             }
+
+            std::set<storm::RationalFunctionVariable> getAllParameters(Model<storm::RationalFunction> const& model) {
+                std::set<storm::RationalFunctionVariable> parameters = getProbabilityParameters(model);
+                std::set<storm::RationalFunctionVariable> rewardParameters = getRewardParameters(model);
+                parameters.insert(rewardParameters.begin(), rewardParameters.end());
+                return parameters;
+            }
 #endif
-            
+
             template class Model<double>;
             template class Model<float>;
 

src/storm/models/sparse/Model.h

@@ -419,10 +419,28 @@ namespace storm {
                 boost::optional<std::shared_ptr<storm::storage::sparse::ChoiceOrigins>> choiceOrigins;
                 
             };
-            
+
 #ifdef STORM_HAVE_CARL
+            /*!
+             * Get all probability parameters occurring on transitions.
+             * @param model Model.
+             * @return Set of parameters.
+             */
             std::set<storm::RationalFunctionVariable> getProbabilityParameters(Model<storm::RationalFunction> const& model);
+
+            /*!
+             * Get all parameters occurring in rewards.
+             * @param model Model.
+             * @return Set of parameters.
+             */
             std::set<storm::RationalFunctionVariable> getRewardParameters(Model<storm::RationalFunction> const& model);
+
+            /*!
+             * Get all parameters (probability and rewards) occurring in the model.
+             * @param model Model.
+             * @return Set of parameters.
+             */
+            std::set<storm::RationalFunctionVariable> getAllParameters(Model<storm::RationalFunction> const& model);
 #endif
         } // namespace sparse
     } // namespace models

src/storm/storage/MaximalEndComponentDecomposition.cpp

@@ -74,10 +74,10 @@ namespace storm {
             if (states) {
                 endComponentStateSets.emplace_back(states->begin(), states->end(), true);
             } else {
-                std::vector<storm::storage::sparse::state_type> states;
-                states.resize(transitionMatrix.getRowGroupCount());
-                std::iota(states.begin(), states.end(), 0);
-                endComponentStateSets.emplace_back(states.begin(), states.end(), true);
+                std::vector<storm::storage::sparse::state_type> allStates;
+                allStates.resize(transitionMatrix.getRowGroupCount());
+                std::iota(allStates.begin(), allStates.end(), 0);
+                endComponentStateSets.emplace_back(allStates.begin(), allStates.end(), true);
             }
             storm::storage::BitVector statesToCheck(numberOfStates);
             storm::storage::BitVector includedChoices;

src/storm/storage/bisimulation/NondeterministicModelBisimulationDecomposition.cpp

@@ -211,7 +211,7 @@ namespace storm {
             }
             
             // Finally construct the quotient model.
-            this->quotient = std::make_shared<ModelType>(builder.build(), std::move(newLabeling), std::move(rewardModels));
+            this->quotient = std::make_shared<ModelType>(builder.build(0,this->size(), this->size()), std::move(newLabeling), std::move(rewardModels));
         }
         
         template<typename ModelType>

src/storm/storage/dd/bisimulation/QuotientExtractor.cpp

@@ -998,6 +998,8 @@ namespace storm {
                     // Check quotient matrix for sanity.
                     if (std::is_same<ValueType, storm::RationalNumber>::value) {
                         STORM_LOG_ASSERT(quotientTransitionMatrix.greater(storm::utility::one<ValueType>()).isZero(), "Illegal entries in quotient matrix.");
+                    } else if (std::is_same<ValueType, storm::RationalFunction>::value) {
+                        // No comparison for rational functions
                     } else {
                         STORM_LOG_ASSERT(quotientTransitionMatrix.greater(storm::utility::one<ValueType>() + storm::utility::convertNumber<ValueType>(1e-6)).isZero(), "Illegal entries in quotient matrix.");
                     }

src/storm/transformer/ContinuousToDiscreteTimeModelTransformer.cpp

@@ -5,7 +5,7 @@
 #include "storm/models/sparse/StandardRewardModel.h"
 #include "storm/logic/Formulas.h"
 #include "storm/logic/FragmentSpecification.h"
-#include "storm/logic/CloneVisitor.h"
+#include "storm/logic/ExpectedTimeToExpectedRewardVisitor.h"
 #include "storm/utility/macros.h"
 #include "storm/utility/vector.h"
 
@@ -93,7 +93,22 @@ namespace storm {
             fragment.setReachabilityRewardFormulasAllowed(true);
             return formula.isInFragment(fragment);
         }
-        
+  
+        template <typename ValueType, typename RewardModelType>
+        std::vector<std::shared_ptr<storm::logic::Formula const>> ContinuousToDiscreteTimeModelTransformer<ValueType, RewardModelType>::checkAndTransformFormulas(std::vector<std::shared_ptr<storm::logic::Formula const>> const& formulas, std::string const& timeRewardName) {
+            std::vector<std::shared_ptr<storm::logic::Formula const>> result;
+            storm::logic::ExpectedTimeToExpectedRewardVisitor v(timeRewardName);
+            for (auto const& f : formulas) {
+                // Translate expected time formulas
+                auto newF = v.substitute(*f);
+                if(preservesFormula(*newF)) {
+                    result.push_back(newF);
+                } else {
+                    STORM_LOG_INFO("Continuous to discrete time transformation does not preserve formula " << *f);
+                }
+            }
+            return result;
+        }
   
         template <typename ValueType, typename RewardModelType>
         std::shared_ptr<storm::models::sparse::Mdp<ValueType, RewardModelType>> ContinuousToDiscreteTimeModelTransformer<ValueType, RewardModelType>::transform(storm::models::sparse::MarkovAutomaton<ValueType, RewardModelType> const& ma, boost::optional<std::string> const& timeRewardModelName) {

src/storm/transformer/ContinuousToDiscreteTimeModelTransformer.h

@@ -16,9 +16,15 @@ namespace storm {
         class ContinuousToDiscreteTimeModelTransformer {
         public:
 
-            // If this method returns true, the given formula is preserced by the transformation
+            // If this method returns true, the given formula is preserved by the transformation
             static bool preservesFormula(storm::logic::Formula const& formula);
-        
+            
+            // Checks whether the given formulas are preserved.
+            // Expected time formulas are translated to expected reward formulas.
+            // The returned vector only contains formulas that are preserved by the transformation.
+            static std::vector<std::shared_ptr<storm::logic::Formula const>> checkAndTransformFormulas(std::vector<std::shared_ptr<storm::logic::Formula const>> const& formulas, std::string const& timeRewardName);
+            
+            
             // Transforms the given CTMC to its underlying (aka embedded) DTMC.
             // A reward model for time is added if a corresponding reward model name is given
             static std::shared_ptr<storm::models::sparse::Dtmc<ValueType, RewardModelType>> transform(storm::models::sparse::Ctmc<ValueType, RewardModelType> const& ctmc, boost::optional<std::string> const& timeRewardModelName = boost::none);