Merge branch 'master' into TimParamSysAndSMT

Former-commit-id: 6ef9d0524d

src/builder/DdPrismModelBuilder.cpp

@@ -190,18 +190,18 @@ namespace storm {
             };
             
         template <storm::dd::DdType Type>
-        DdPrismModelBuilder<Type>::Options::Options() : buildAllRewardModels(true), rewardModelsToBuild(), constantDefinitions(), buildAllLabels(true), labelsToBuild(), expressionLabels(), terminalStates() {
+        DdPrismModelBuilder<Type>::Options::Options() : buildAllRewardModels(true), rewardModelsToBuild(), constantDefinitions(), buildAllLabels(true), labelsToBuild(), expressionLabels(), terminalStates(), negatedTerminalStates() {
             // Intentionally left empty.
         }
         
         template <storm::dd::DdType Type>
-        DdPrismModelBuilder<Type>::Options::Options(storm::logic::Formula const& formula) : buildAllRewardModels(false), rewardModelsToBuild(), constantDefinitions(), buildAllLabels(false), labelsToBuild(std::set<std::string>()), expressionLabels(std::vector<storm::expressions::Expression>()), terminalStates() {
+        DdPrismModelBuilder<Type>::Options::Options(storm::logic::Formula const& formula) : buildAllRewardModels(false), rewardModelsToBuild(), constantDefinitions(), buildAllLabels(false), labelsToBuild(std::set<std::string>()), expressionLabels(std::vector<storm::expressions::Expression>()), terminalStates(), negatedTerminalStates() {
             this->preserveFormula(formula);
             this->setTerminalStatesFromFormula(formula);
         }
         
         template <storm::dd::DdType Type>
-        DdPrismModelBuilder<Type>::Options::Options(std::vector<std::shared_ptr<storm::logic::Formula>> const& formulas) : buildAllRewardModels(false), rewardModelsToBuild(), constantDefinitions(), buildAllLabels(false), labelsToBuild(), expressionLabels(), terminalStates() {
+        DdPrismModelBuilder<Type>::Options::Options(std::vector<std::shared_ptr<storm::logic::Formula>> const& formulas) : buildAllRewardModels(false), rewardModelsToBuild(), constantDefinitions(), buildAllLabels(false), labelsToBuild(), expressionLabels(), terminalStates(), negatedTerminalStates() {
             if (formulas.empty()) {
                 this->buildAllRewardModels = true;
                 this->buildAllLabels = true;
@@ -221,6 +221,9 @@ namespace storm {
             if (terminalStates) {
                 terminalStates.reset();
             }
+            if (negatedTerminalStates) {
+                negatedTerminalStates.reset();
+            }
 
             // If we are not required to build all reward models, we determine the reward models we need to build.
             if (!buildAllRewardModels) {
@@ -261,10 +264,16 @@ namespace storm {
                     this->setTerminalStatesFromFormula(sub);
                 }
             } else if (formula.isUntilFormula()) {
-                storm::logic::Formula const& right = formula.asUntilFormula().getLeftSubformula();
+                storm::logic::Formula const& right = formula.asUntilFormula().getRightSubformula();
                 if (right.isAtomicExpressionFormula() || right.isAtomicLabelFormula()) {
                     this->setTerminalStatesFromFormula(right);
                 }
+                storm::logic::Formula const& left = formula.asUntilFormula().getLeftSubformula();
+                if (left.isAtomicExpressionFormula()) {
+                    negatedTerminalStates = left.asAtomicExpressionFormula().getExpression();
+                } else if (left.isAtomicLabelFormula()) {
+                    negatedTerminalStates = left.asAtomicLabelFormula().getLabel();
+                }
             } else if (formula.isProbabilityOperatorFormula()) {
                 storm::logic::Formula const& sub = formula.asProbabilityOperatorFormula().getSubformula();
                 if (sub.isEventuallyFormula() || sub.isUntilFormula()) {
@@ -1023,16 +1032,33 @@ namespace storm {
             storm::dd::Add<Type> stateActionDd = system.stateActionDd;
             
             // If we were asked to treat some states as terminal states, we cut away their transitions now.
-            if (options.terminalStates) {
-                storm::expressions::Expression terminalExpression;
-                if (options.terminalStates.get().type() == typeid(storm::expressions::Expression)) {
-                    terminalExpression = boost::get<storm::expressions::Expression>(options.terminalStates.get());
-                } else {
-                    std::string const& labelName = boost::get<std::string>(options.terminalStates.get());
-                    terminalExpression = preparedProgram.getLabelExpression(labelName);
+            if (options.terminalStates || options.negatedTerminalStates) {
+                storm::dd::Add<Type> terminalStatesAdd = generationInfo.manager->getAddZero();
+                if (options.terminalStates) {
+                    storm::expressions::Expression terminalExpression;
+                    if (options.terminalStates.get().type() == typeid(storm::expressions::Expression)) {
+                        terminalExpression = boost::get<storm::expressions::Expression>(options.terminalStates.get());
+                    } else {
+                        std::string const& labelName = boost::get<std::string>(options.terminalStates.get());
+                        terminalExpression = preparedProgram.getLabelExpression(labelName);
+                    }
+                
+                    STORM_LOG_TRACE("Making the states satisfying " << terminalExpression << " terminal.");
+                    terminalStatesAdd = generationInfo.rowExpressionAdapter->translateExpression(terminalExpression);
                 }
-                STORM_LOG_TRACE("Making the states satisfying " << terminalExpression << " terminal.");
-                storm::dd::Add<Type> terminalStatesAdd = generationInfo.rowExpressionAdapter->translateExpression(terminalExpression);
+                if (options.negatedTerminalStates) {
+                    storm::expressions::Expression nonTerminalExpression;
+                    if (options.negatedTerminalStates.get().type() == typeid(storm::expressions::Expression)) {
+                        nonTerminalExpression = boost::get<storm::expressions::Expression>(options.negatedTerminalStates.get());
+                    } else {
+                        std::string const& labelName = boost::get<std::string>(options.terminalStates.get());
+                        nonTerminalExpression = preparedProgram.getLabelExpression(labelName);
+                    }
+                    
+                    STORM_LOG_TRACE("Making the states *not* satisfying " << nonTerminalExpression << " terminal.");
+                    terminalStatesAdd |= !generationInfo.rowExpressionAdapter->translateExpression(nonTerminalExpression);
+                }
+                
                 transitionMatrix *= !terminalStatesAdd;
             }
             

src/builder/DdPrismModelBuilder.h

@@ -99,9 +99,13 @@ namespace storm {
                 // An optional set of expressions for which labels need to be built.
                 boost::optional<std::vector<storm::expressions::Expression>> expressionLabels;
                 
-                // An optional expression or label that characterizes the terminal states of the model. If this is set,
-                // the outgoing transitions of these states are replaced with a self-loop.
+                // An optional expression or label that (a subset of) characterizes the terminal states of the model.
+                // If this is set, the outgoing transitions of these states are replaced with a self-loop.
                 boost::optional<boost::variant<storm::expressions::Expression, std::string>> terminalStates;
+                
+                // An optional expression or label whose negation characterizes (a subset of) the terminal states of the
+                // model. If this is set, the outgoing transitions of these states are replaced with a self-loop.
+                boost::optional<boost::variant<storm::expressions::Expression, std::string>> negatedTerminalStates;
             };
             
             /*!

src/builder/ExplicitPrismModelBuilder.cpp

@@ -106,17 +106,17 @@ namespace storm {
         }
 
         template <typename ValueType, typename IndexType>
-        ExplicitPrismModelBuilder<ValueType, IndexType>::Options::Options() : buildCommandLabels(false), buildAllRewardModels(true), rewardModelsToBuild(), constantDefinitions(), buildAllLabels(true), labelsToBuild(), expressionLabels(), terminalStates() {
+        ExplicitPrismModelBuilder<ValueType, IndexType>::Options::Options() : buildCommandLabels(false), buildAllRewardModels(true), rewardModelsToBuild(), constantDefinitions(), buildAllLabels(true), labelsToBuild(), expressionLabels(), terminalStates(), negatedTerminalStates() {
             // Intentionally left empty.
         }
         
         template <typename ValueType, typename IndexType>
-        ExplicitPrismModelBuilder<ValueType, IndexType>::Options::Options(storm::logic::Formula const& formula) : buildCommandLabels(false), buildAllRewardModels(false), rewardModelsToBuild(), constantDefinitions(), buildAllLabels(false), labelsToBuild(std::set<std::string>()), expressionLabels(std::vector<storm::expressions::Expression>()), terminalStates() {
+        ExplicitPrismModelBuilder<ValueType, IndexType>::Options::Options(storm::logic::Formula const& formula) : buildCommandLabels(false), buildAllRewardModels(false), rewardModelsToBuild(), constantDefinitions(), buildAllLabels(false), labelsToBuild(std::set<std::string>()), expressionLabels(std::vector<storm::expressions::Expression>()), terminalStates(), negatedTerminalStates() {
             this->preserveFormula(formula);
         }
         
         template <typename ValueType, typename IndexType>
-        ExplicitPrismModelBuilder<ValueType, IndexType>::Options::Options(std::vector<std::shared_ptr<storm::logic::Formula>> const& formulas) : buildCommandLabels(false), buildAllRewardModels(false), rewardModelsToBuild(), constantDefinitions(), buildAllLabels(false), labelsToBuild(), expressionLabels(), terminalStates() {
+        ExplicitPrismModelBuilder<ValueType, IndexType>::Options::Options(std::vector<std::shared_ptr<storm::logic::Formula>> const& formulas) : buildCommandLabels(false), buildAllRewardModels(false), rewardModelsToBuild(), constantDefinitions(), buildAllLabels(false), labelsToBuild(), expressionLabels(), terminalStates(), negatedTerminalStates() {
             if (formulas.empty()) {
                 this->buildAllRewardModels = true;
                 this->buildAllLabels = true;
@@ -142,10 +142,16 @@ namespace storm {
                     this->setTerminalStatesFromFormula(sub);
                 }
             } else if (formula.isUntilFormula()) {
-                storm::logic::Formula const& right = formula.asUntilFormula().getLeftSubformula();
+                storm::logic::Formula const& right = formula.asUntilFormula().getRightSubformula();
                 if (right.isAtomicExpressionFormula() || right.isAtomicLabelFormula()) {
                     this->setTerminalStatesFromFormula(right);
                 }
+                storm::logic::Formula const& left = formula.asUntilFormula().getLeftSubformula();
+                if (left.isAtomicExpressionFormula()) {
+                    negatedTerminalStates = left.asAtomicExpressionFormula().getExpression();
+                } else if (left.isAtomicLabelFormula()) {
+                    negatedTerminalStates = left.asAtomicLabelFormula().getLabel();
+                }
             } else if (formula.isProbabilityOperatorFormula()) {
                 storm::logic::Formula const& sub = formula.asProbabilityOperatorFormula().getSubformula();
                 if (sub.isEventuallyFormula() || sub.isUntilFormula()) {
@@ -160,6 +166,9 @@ namespace storm {
             if (terminalStates) {
                 terminalStates.reset();
             }
+            if (negatedTerminalStates) {
+                negatedTerminalStates.reset();
+            }
             
             // If we are not required to build all reward models, we determine the reward models we need to build.
             if (!buildAllRewardModels) {
@@ -934,7 +943,8 @@ namespace storm {
                 rewardModelBuilders.emplace_back(deterministicModel, rewardModel.get().hasStateRewards(), rewardModel.get().hasStateActionRewards(), rewardModel.get().hasTransitionRewards());
             }
             
-            // If we were asked to treat some states as terminal states, we cut away their transitions now.
+            // If we were asked to treat some states as terminal states, we determine an expression characterizing the
+            // terminal states of the model that we pass on to the matrix building routine.
             boost::optional<storm::expressions::Expression> terminalExpression;
             if (options.terminalStates) {
                 if (options.terminalStates.get().type() == typeid(storm::expressions::Expression)) {
@@ -944,9 +954,27 @@ namespace storm {
                     terminalExpression = program.getLabelExpression(labelName);
                 }
             }
+            if (options.negatedTerminalStates) {
+                if (options.negatedTerminalStates.get().type() == typeid(storm::expressions::Expression)) {
+                    if (terminalExpression) {
+                        terminalExpression = terminalExpression.get() || !boost::get<storm::expressions::Expression>(options.negatedTerminalStates.get());
+                    } else {
+                        terminalExpression = !boost::get<storm::expressions::Expression>(options.negatedTerminalStates.get());
+                    }
+                } else {
+                    std::string const& labelName = boost::get<std::string>(options.negatedTerminalStates.get());
+                    if (terminalExpression) {
+                        terminalExpression = terminalExpression.get() || !program.getLabelExpression(labelName);
+                    } else {
+                        terminalExpression = !program.getLabelExpression(labelName);
+                    }
+                }
+            }
+            if (terminalExpression) {
+                STORM_LOG_TRACE("Making the states satisfying " << terminalExpression.get() << " terminal.");
+            }
             
             modelComponents.choiceLabeling = buildMatrices(program, variableInformation, selectedRewardModels, stateInformation, options.buildCommandLabels, deterministicModel, discreteTimeModel, transitionMatrixBuilder, rewardModelBuilders, terminalExpression);
-            
             modelComponents.transitionMatrix = transitionMatrixBuilder.build();
             
             // Now finalize all reward models.

src/builder/ExplicitPrismModelBuilder.h

@@ -193,9 +193,13 @@ namespace storm {
                 // An optional set of expressions for which labels need to be built.
                 boost::optional<std::vector<storm::expressions::Expression>> expressionLabels;
                 
-                // An optional expression or label that characterizes the terminal states of the model. If this is set,
-                // the outgoing transitions of these states are replaced with a self-loop.
+                // An optional expression or label that characterizes (a subset of) the terminal states of the model. If
+                // this is set, the outgoing transitions of these states are replaced with a self-loop.
                 boost::optional<boost::variant<storm::expressions::Expression, std::string>> terminalStates;
+                
+                // An optional expression or label whose negation characterizes (a subset of) the terminal states of the
+                // model. If this is set, the outgoing transitions of these states are replaced with a self-loop.
+                boost::optional<boost::variant<storm::expressions::Expression, std::string>> negatedTerminalStates;
             };
             
             /*!

src/modelchecker/results/CheckResult.h

@@ -21,6 +21,8 @@ namespace storm {
         // The base class of all check results.
         class CheckResult {
         public:
+            virtual ~CheckResult() = default;
+            
             /*!
              * Filters the current result wrt. to the filter, i.e. only keeps the entries that are selected by the filter.
              * This means that the filter must be a qualitative result of proper type (symbolic/explicit).

src/modelchecker/results/ExplicitQualitativeCheckResult.h

@@ -18,6 +18,7 @@ namespace storm {
             typedef std::map<storm::storage::sparse::state_type, bool> map_type;
             
             ExplicitQualitativeCheckResult();
+            virtual ~ExplicitQualitativeCheckResult() = default;
             ExplicitQualitativeCheckResult(map_type const& map);
             ExplicitQualitativeCheckResult(map_type&& map);
             ExplicitQualitativeCheckResult(storm::storage::sparse::state_type state, bool value);

src/modelchecker/results/ExplicitQuantitativeCheckResult.h

@@ -30,6 +30,7 @@ namespace storm {
             ExplicitQuantitativeCheckResult(ExplicitQuantitativeCheckResult&& other) = default;
             ExplicitQuantitativeCheckResult& operator=(ExplicitQuantitativeCheckResult&& other) = default;
 #endif
+            virtual ~ExplicitQuantitativeCheckResult() = default;
             
             ValueType& operator[](storm::storage::sparse::state_type state);
             ValueType const& operator[](storm::storage::sparse::state_type state) const;

src/modelchecker/results/QualitativeCheckResult.h

@@ -7,6 +7,7 @@ namespace storm {
     namespace modelchecker {
         class QualitativeCheckResult : public CheckResult {
         public:
+            virtual ~QualitativeCheckResult() = default;
             virtual QualitativeCheckResult& operator&=(QualitativeCheckResult const& other);
             virtual QualitativeCheckResult& operator|=(QualitativeCheckResult const& other);
             virtual void complement();

src/modelchecker/results/QuantitativeCheckResult.h

@@ -7,6 +7,9 @@ namespace storm {
     namespace modelchecker {
         class QuantitativeCheckResult : public CheckResult {
         public:
+            
+            virtual ~QuantitativeCheckResult() = default;
+            
             virtual std::unique_ptr<CheckResult> compareAgainstBound(storm::logic::ComparisonType comparisonType, double bound) const;
             
             virtual bool isQuantitative() const override;