From 7170fea7ce239b9fabe1c7104675e1b61b2f2a77 Mon Sep 17 00:00:00 2001 From: Sebastian Junges Date: Wed, 19 Apr 2017 11:28:46 +0200 Subject: [PATCH 1/5] Jit Fix for LTS support --- src/storm/builder/jit/ModelComponentsBuilder.cpp | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/src/storm/builder/jit/ModelComponentsBuilder.cpp b/src/storm/builder/jit/ModelComponentsBuilder.cpp index 6c51840ad..6f61feb19 100644 --- a/src/storm/builder/jit/ModelComponentsBuilder.cpp +++ b/src/storm/builder/jit/ModelComponentsBuilder.cpp @@ -129,7 +129,7 @@ namespace storm { return new storm::models::sparse::Dtmc>(std::move(transitionMatrix), std::move(stateLabeling), std::move(rewardModels)); } else if (modelType == storm::jani::ModelType::CTMC) { return new storm::models::sparse::Ctmc>(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>(std::move(transitionMatrix), std::move(stateLabeling), std::move(rewardModels)); } else if (modelType == storm::jani::ModelType::MA) { std::vector exitRates(transitionMatrix.getRowGroupCount(), storm::utility::zero()); From a21995052c5fe00b58f47b17e1d7e7e11738bb30 Mon Sep 17 00:00:00 2001 From: Sebastian Junges Date: Wed, 19 Apr 2017 13:44:47 +0200 Subject: [PATCH 2/5] fix for probabilistic reachability formulae --- src/storm/parser/JaniParser.cpp | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/src/storm/parser/JaniParser.cpp b/src/storm/parser/JaniParser.cpp index 08df6b605..ecb3ed0ff 100644 --- a/src/storm/parser/JaniParser.cpp +++ b/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(args[1], storm::logic::FormulaContext::Reward); + return std::make_shared(args[1], formulaContext); } else { return std::make_shared(args[0], args[1]); } From 38eadad17db56c287a16ed9da72c1667e6c8bb8a Mon Sep 17 00:00:00 2001 From: Sebastian Junges Date: Wed, 19 Apr 2017 13:46:44 +0200 Subject: [PATCH 3/5] Jit: Expression labels which occur twice in list of formulae now supported --- .../builder/jit/ExplicitJitJaniModelBuilder.cpp | 13 +++++++++---- 1 file changed, 9 insertions(+), 4 deletions(-) diff --git a/src/storm/builder/jit/ExplicitJitJaniModelBuilder.cpp b/src/storm/builder/jit/ExplicitJitJaniModelBuilder.cpp index 9844a64af..6df0210e9 100644 --- a/src/storm/builder/jit/ExplicitJitJaniModelBuilder.cpp +++ b/src/storm/builder/jit/ExplicitJitJaniModelBuilder.cpp @@ -1531,12 +1531,17 @@ namespace storm { } } } - + + std::set 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); From 8c6b22bebcc8b89a287388dc6d7cc04407b50072 Mon Sep 17 00:00:00 2001 From: TimQu Date: Thu, 13 Apr 2017 09:37:54 +0200 Subject: [PATCH 4/5] Incremented minimal z3 version required for the z3LpSolver to 4.5.0 as the optimizer in 4.4.1 yielded wrong results in the tests --- resources/3rdparty/CMakeLists.txt | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/resources/3rdparty/CMakeLists.txt b/resources/3rdparty/CMakeLists.txt index 80f9e787a..e917be668 100644 --- a/resources/3rdparty/CMakeLists.txt +++ b/resources/3rdparty/CMakeLists.txt @@ -141,7 +141,7 @@ if(Z3_FOUND) OUTPUT_STRIP_TRAILING_WHITESPACE) if (z3_version_output MATCHES "([0-9]*\\.[0-9]*\\.[0-9]*)") set(Z3_VERSION "${CMAKE_MATCH_1}") - if(NOT "${Z3_VERSION}" VERSION_LESS "4.4.1") + if(NOT "${Z3_VERSION}" VERSION_LESS "4.5.0") set(STORM_HAVE_Z3_OPTIMIZE ON) endif() endif() From 5f83f4451db5c17de022d87b5db593da46ae23aa Mon Sep 17 00:00:00 2001 From: TimQu Date: Wed, 19 Apr 2017 15:23:56 +0200 Subject: [PATCH 5/5] added a few virtual destructors to prevent memory leaks. --- .../multiobjective/pcaa/SparseMaPcaaWeightVectorChecker.h | 2 ++ .../multiobjective/pcaa/SparseMdpPcaaWeightVectorChecker.h | 4 +++- .../multiobjective/pcaa/SparsePcaaAchievabilityQuery.h | 3 ++- .../modelchecker/multiobjective/pcaa/SparsePcaaParetoQuery.h | 2 ++ .../multiobjective/pcaa/SparsePcaaQuantitativeQuery.h | 3 ++- src/storm/modelchecker/multiobjective/pcaa/SparsePcaaQuery.h | 2 ++ .../multiobjective/pcaa/SparsePcaaWeightVectorChecker.h | 2 ++ 7 files changed, 15 insertions(+), 3 deletions(-) diff --git a/src/storm/modelchecker/multiobjective/pcaa/SparseMaPcaaWeightVectorChecker.h b/src/storm/modelchecker/multiobjective/pcaa/SparseMaPcaaWeightVectorChecker.h index 1ac363c4d..827f1701e 100644 --- a/src/storm/modelchecker/multiobjective/pcaa/SparseMaPcaaWeightVectorChecker.h +++ b/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: /* diff --git a/src/storm/modelchecker/multiobjective/pcaa/SparseMdpPcaaWeightVectorChecker.h b/src/storm/modelchecker/multiobjective/pcaa/SparseMdpPcaaWeightVectorChecker.h index aa0425c4f..8b56386c9 100644 --- a/src/storm/modelchecker/multiobjective/pcaa/SparseMdpPcaaWeightVectorChecker.h +++ b/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: /*! diff --git a/src/storm/modelchecker/multiobjective/pcaa/SparsePcaaAchievabilityQuery.h b/src/storm/modelchecker/multiobjective/pcaa/SparsePcaaAchievabilityQuery.h index d4f3ea32b..c250f257b 100644 --- a/src/storm/modelchecker/multiobjective/pcaa/SparsePcaaAchievabilityQuery.h +++ b/src/storm/modelchecker/multiobjective/pcaa/SparsePcaaAchievabilityQuery.h @@ -25,7 +25,8 @@ namespace storm { */ SparsePcaaAchievabilityQuery(SparsePcaaPreprocessorReturnType& preprocessorResult); - + virtual ~SparsePcaaAchievabilityQuery() = default; + /* * Invokes the computation and retrieves the result */ diff --git a/src/storm/modelchecker/multiobjective/pcaa/SparsePcaaParetoQuery.h b/src/storm/modelchecker/multiobjective/pcaa/SparsePcaaParetoQuery.h index 08256f3c7..b6361faff 100644 --- a/src/storm/modelchecker/multiobjective/pcaa/SparsePcaaParetoQuery.h +++ b/src/storm/modelchecker/multiobjective/pcaa/SparsePcaaParetoQuery.h @@ -25,6 +25,8 @@ namespace storm { */ SparsePcaaParetoQuery(SparsePcaaPreprocessorReturnType& preprocessorResult); + virtual ~SparsePcaaParetoQuery() = default; + /* * Invokes the computation and retrieves the result diff --git a/src/storm/modelchecker/multiobjective/pcaa/SparsePcaaQuantitativeQuery.h b/src/storm/modelchecker/multiobjective/pcaa/SparsePcaaQuantitativeQuery.h index 3e72763f1..ca2d8c81a 100644 --- a/src/storm/modelchecker/multiobjective/pcaa/SparsePcaaQuantitativeQuery.h +++ b/src/storm/modelchecker/multiobjective/pcaa/SparsePcaaQuantitativeQuery.h @@ -25,7 +25,8 @@ namespace storm { */ SparsePcaaQuantitativeQuery(SparsePcaaPreprocessorReturnType& preprocessorResult); - + virtual ~SparsePcaaQuantitativeQuery() = default; + /* * Invokes the computation and retrieves the result */ diff --git a/src/storm/modelchecker/multiobjective/pcaa/SparsePcaaQuery.h b/src/storm/modelchecker/multiobjective/pcaa/SparsePcaaQuery.h index c0a891a13..e6404c9ac 100644 --- a/src/storm/modelchecker/multiobjective/pcaa/SparsePcaaQuery.h +++ b/src/storm/modelchecker/multiobjective/pcaa/SparsePcaaQuery.h @@ -22,6 +22,8 @@ namespace storm { typedef std::vector Point; typedef std::vector WeightVector; + virtual ~SparsePcaaQuery() = default; + /* * Invokes the computation and retrieves the result */ diff --git a/src/storm/modelchecker/multiobjective/pcaa/SparsePcaaWeightVectorChecker.h b/src/storm/modelchecker/multiobjective/pcaa/SparsePcaaWeightVectorChecker.h index 452f30189..d80eb4931 100644 --- a/src/storm/modelchecker/multiobjective/pcaa/SparsePcaaWeightVectorChecker.h +++ b/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