Merge branch 'master' into refactor_pla

src/storm/builder/jit/ExplicitJitJaniModelBuilder.cpp

@@ -1531,12 +1531,17 @@ namespace storm {
                         }
                     }
                 }
-                    
+
+                std::set<std::string> expressionLabelStrings;
                 for (auto const& expression : this->options.getExpressionLabels()) {
                     cpptempl::data_map label;
-                    label["name"] = expression.toString();
-                    label["predicate"] = expressionTranslator.translate(shiftVariablesWrtLowerBound(expression), storm::expressions::ToCppTranslationOptions(variablePrefixes, variableToName, storm::expressions::ToCppTranslationMode::CastDouble));
-                    labels.push_back(label);
+                    std::string expressionLabelString = expression.toString();
+                    if(expressionLabelStrings.count(expressionLabelString) == 0) {
+                        label["name"] = expression.toString();
+                        label["predicate"] = expressionTranslator.translate(shiftVariablesWrtLowerBound(expression), storm::expressions::ToCppTranslationOptions(variablePrefixes, variableToName, storm::expressions::ToCppTranslationMode::CastDouble));
+                        labels.push_back(label);
+                        expressionLabelStrings.insert(expressionLabelString);
+                    }
                 }
                     
                 modelData["labels"] = cpptempl::make_data(labels);

src/storm/builder/jit/ModelComponentsBuilder.cpp

@@ -129,7 +129,7 @@ namespace storm {
                     return new storm::models::sparse::Dtmc<ValueType, storm::models::sparse::StandardRewardModel<ValueType>>(std::move(transitionMatrix), std::move(stateLabeling), std::move(rewardModels));
                 } else if (modelType == storm::jani::ModelType::CTMC) {
                     return new storm::models::sparse::Ctmc<ValueType, storm::models::sparse::StandardRewardModel<ValueType>>(std::move(transitionMatrix), std::move(stateLabeling), std::move(rewardModels));
-                } else if (modelType == storm::jani::ModelType::MDP) {
+                } else if (modelType == storm::jani::ModelType::MDP || modelType == storm::jani::ModelType::LTS) {
                     return new storm::models::sparse::Mdp<ValueType, storm::models::sparse::StandardRewardModel<ValueType>>(std::move(transitionMatrix), std::move(stateLabeling), std::move(rewardModels));
                 } else if (modelType == storm::jani::ModelType::MA) {
                     std::vector<ValueType> exitRates(transitionMatrix.getRowGroupCount(), storm::utility::zero<ValueType>());

src/storm/modelchecker/multiobjective/pcaa/SparseMaPcaaWeightVectorChecker.h

@@ -31,6 +31,8 @@ namespace storm {
                                                           storm::storage::BitVector const& ecActions,
                                                           storm::storage::BitVector const& possiblyRecurrentStates);
                 
+                virtual ~SparseMaPcaaWeightVectorChecker() = default;
+
             private:
                 
                 /*

src/storm/modelchecker/multiobjective/pcaa/SparseMdpPcaaWeightVectorChecker.h

@@ -25,7 +25,9 @@ namespace storm {
                                                  storm::storage::BitVector const& actionsWithNegativeReward,
                                                  storm::storage::BitVector const& ecActions,
                                                  storm::storage::BitVector const& possiblyRecurrentStates);
-                
+
+                virtual ~SparseMdpPcaaWeightVectorChecker() = default;
+
             private:
                 
                 /*!

src/storm/modelchecker/multiobjective/pcaa/SparsePcaaAchievabilityQuery.h

@@ -25,7 +25,8 @@ namespace storm {
                  */
                 SparsePcaaAchievabilityQuery(SparsePcaaPreprocessorReturnType<SparseModelType>& preprocessorResult);
                 
-                
+                virtual ~SparsePcaaAchievabilityQuery() = default;
+
                 /*
                  * Invokes the computation and retrieves the result
                  */

src/storm/modelchecker/multiobjective/pcaa/SparsePcaaParetoQuery.h

@@ -25,6 +25,8 @@ namespace storm {
                  */
                 SparsePcaaParetoQuery(SparsePcaaPreprocessorReturnType<SparseModelType>& preprocessorResult);
                 
+                virtual ~SparsePcaaParetoQuery() = default;
+
                 
                 /*
                  * Invokes the computation and retrieves the result

src/storm/modelchecker/multiobjective/pcaa/SparsePcaaQuantitativeQuery.h

@@ -25,7 +25,8 @@ namespace storm {
                  */
                 SparsePcaaQuantitativeQuery(SparsePcaaPreprocessorReturnType<SparseModelType>& preprocessorResult);
                 
-                
+                virtual ~SparsePcaaQuantitativeQuery() = default;
+
                 /*
                  * Invokes the computation and retrieves the result
                  */

src/storm/modelchecker/multiobjective/pcaa/SparsePcaaQuery.h

@@ -22,6 +22,8 @@ namespace storm {
                 typedef std::vector<GeometryValueType> Point;
                 typedef std::vector<GeometryValueType> WeightVector;
                 
+                virtual ~SparsePcaaQuery() = default;
+                
                 /*
                  * Invokes the computation and retrieves the result
                  */

src/storm/modelchecker/multiobjective/pcaa/SparsePcaaWeightVectorChecker.h

@@ -40,6 +40,8 @@ namespace storm {
                                                         storm::storage::BitVector const& ecActions,
                                                         storm::storage::BitVector const& possiblyRecurrentStates);
                 
+                virtual ~SparsePcaaWeightVectorChecker() = default;
+                
                 /*!
                  * - computes the maximal expected reward w.r.t. the weighted sum of the rewards of the individual objectives
                  * - extracts the scheduler that induces this maximum

src/storm/parser/JaniParser.cpp

@@ -370,7 +370,7 @@ namespace storm {
                         STORM_LOG_THROW(false, storm::exceptions::NotSupportedException, "Reward bounded properties are not supported by storm");
                     }
                     if (args[0]->isTrueFormula()) {
-                        return std::make_shared<storm::logic::EventuallyFormula const>(args[1], storm::logic::FormulaContext::Reward);
+                        return std::make_shared<storm::logic::EventuallyFormula const>(args[1], formulaContext);
                     } else {
                         return std::make_shared<storm::logic::UntilFormula const>(args[0], args[1]);
                     }