From ecade3f8578e415c345702bda2664c145700b132 Mon Sep 17 00:00:00 2001 From: dehnert Date: Mon, 28 Aug 2017 20:02:23 +0200 Subject: [PATCH 1/9] fixes issue #9 raised by Joachim Klein --- src/storm/storage/prism/Program.cpp | 5 +++++ 1 file changed, 5 insertions(+) diff --git a/src/storm/storage/prism/Program.cpp b/src/storm/storage/prism/Program.cpp index a87ea5888..387423066 100644 --- a/src/storm/storage/prism/Program.cpp +++ b/src/storm/storage/prism/Program.cpp @@ -492,6 +492,11 @@ namespace storm { } } + // If there are no variables, there is no restriction on the initial states. + if (!result.isInitialized()) { + result = manager->boolean(true); + } + return result; } } From 2d30108b499003e90b9ec48ead2bf59dc5ebe4d4 Mon Sep 17 00:00:00 2001 From: dehnert Date: Mon, 28 Aug 2017 20:23:09 +0200 Subject: [PATCH 2/9] fixes issue #10 raised by Joachim Klein --- src/storm/logic/VariableSubstitutionVisitor.cpp | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/src/storm/logic/VariableSubstitutionVisitor.cpp b/src/storm/logic/VariableSubstitutionVisitor.cpp index 00eee1e01..2a84a0c10 100644 --- a/src/storm/logic/VariableSubstitutionVisitor.cpp +++ b/src/storm/logic/VariableSubstitutionVisitor.cpp @@ -53,7 +53,7 @@ namespace storm { if (f.hasUpperBound(i)) { upperBounds.push_back(TimeBound(f.isUpperBoundStrict(i), f.getUpperBound(i).substitute(substitution))); } else { - lowerBounds.push_back(boost::none); + upperBounds.push_back(boost::none); } tbReferences.push_back(f.getTimeBoundReference(i)); } From beb80cc5af32290747844c365f9ecb0d9a0b4b3a Mon Sep 17 00:00:00 2001 From: dehnert Date: Mon, 28 Aug 2017 22:40:46 +0200 Subject: [PATCH 3/9] fixes issue #11 raised by Joachim Klein --- src/storm/modelchecker/CheckTask.h | 1 + 1 file changed, 1 insertion(+) diff --git a/src/storm/modelchecker/CheckTask.h b/src/storm/modelchecker/CheckTask.h index 4440f1ba3..828f85215 100644 --- a/src/storm/modelchecker/CheckTask.h +++ b/src/storm/modelchecker/CheckTask.h @@ -52,6 +52,7 @@ namespace storm { template CheckTask substituteFormula(NewFormulaType const& newFormula) const { CheckTask result(newFormula, this->optimizationDirection, this->rewardModel, this->onlyInitialStatesRelevant, this->bound, this->qualitative, this->produceSchedulers, this->hint); + result.updateOperatorInformation(); return result; } From 2d2cc9577403deaa49e9b55968bcbe924decdf06 Mon Sep 17 00:00:00 2001 From: TimQu Date: Tue, 29 Aug 2017 10:01:07 +0200 Subject: [PATCH 4/9] fixed issue #12 raised by Joachim Klein --- src/storm/utility/graph.cpp | 5 +++-- 1 file changed, 3 insertions(+), 2 deletions(-) diff --git a/src/storm/utility/graph.cpp b/src/storm/utility/graph.cpp index 13065000a..c341cdc22 100644 --- a/src/storm/utility/graph.cpp +++ b/src/storm/utility/graph.cpp @@ -165,7 +165,7 @@ namespace storm { } candidateStates = storm::utility::graph::getReachableStates(transitionMatrix, choiceTargets, candidateStates, storm::storage::BitVector(candidateStates.size(), false)); - // At this point we know that every candidate state can reach a choice at least once without leaving the set of candidate states. + // At this point we know that every candidate state can reach a state with a choice without leaving the set of candidate states. // We now compute the states that can reach a choice at least twice, three times, four times, ... until a fixpoint is reached. while (!candidateStates.empty()) { // Update the states with a choice that stays within the set of candidates @@ -193,11 +193,12 @@ namespace storm { // Update the candidates storm::storage::BitVector newCandidates = storm::utility::graph::performProb1E(transitionMatrix, transitionMatrix.getRowGroupIndices(), backwardTransitions, candidateStates, statesWithChoice); - // Check if conferged + // Check if converged if (newCandidates == candidateStates) { assert(!candidateStates.empty()); return true; } + candidateStates = std::move(newCandidates); } return false; } From 06ec288296862ce8222a54dbda6bbfa3d3eabf35 Mon Sep 17 00:00:00 2001 From: TimQu Date: Tue, 29 Aug 2017 10:01:44 +0200 Subject: [PATCH 5/9] enabled pcaa test that uses rational numbers --- .../SparseMaPcaaMultiObjectiveModelCheckerTest.cpp | 10 +++------- 1 file changed, 3 insertions(+), 7 deletions(-) diff --git a/src/test/storm/modelchecker/SparseMaPcaaMultiObjectiveModelCheckerTest.cpp b/src/test/storm/modelchecker/SparseMaPcaaMultiObjectiveModelCheckerTest.cpp index b78eead1b..ad9699e46 100644 --- a/src/test/storm/modelchecker/SparseMaPcaaMultiObjectiveModelCheckerTest.cpp +++ b/src/test/storm/modelchecker/SparseMaPcaaMultiObjectiveModelCheckerTest.cpp @@ -16,23 +16,19 @@ #include "storm/api/storm.h" -/* Rationals for MAs not supported at this point TEST(SparseMaPcaaMultiObjectiveModelCheckerTest, serverRationalNumbers) { std::string programFile = STORM_TEST_RESOURCES_DIR "/ma/server.ma"; std::string formulasAsString = "multi(Tmax=? [ F \"error\" ], Pmax=? [ F \"processB\" ]) "; // pareto - // formulasAsString += "; \n multi(..)"; // programm, model, formula storm::prism::Program program = storm::api::parseProgram(programFile); program.checkValidity(); - std::vector> formulas = storm::api::extractFormulasFromProperties(parseFormulasForProgram(formulasAsString, program)); + std::vector> formulas = storm::api::extractFormulasFromProperties(storm::api::parsePropertiesForPrismProgram(formulasAsString, program)); storm::generator::NextStateGeneratorOptions options(formulas); std::shared_ptr> ma = storm::builder::ExplicitModelBuilder(program, options).build()->as>(); - storm::modelchecker::SparseMarkovAutomatonCslModelChecker> checker(*ma); - - std::unique_ptr result = checker.check(storm::modelchecker::CheckTask(*formulas[0], true)); + std::unique_ptr result = storm::modelchecker::multiobjective::performMultiObjectiveModelChecking(*ma, formulas[0]->asMultiObjectiveFormula(), storm::modelchecker::multiobjective::MultiObjectiveMethodSelection::Pcaa); ASSERT_TRUE(result->isExplicitParetoCurveCheckResult()); storm::RationalNumber p1 = storm::utility::convertNumber(11.0); p1 /= storm::utility::convertNumber(6.0); @@ -45,7 +41,7 @@ TEST(SparseMaPcaaMultiObjectiveModelCheckerTest, serverRationalNumbers) { EXPECT_TRUE(expectedAchievableValues->contains(result->asExplicitParetoCurveCheckResult().getUnderApproximation())); EXPECT_TRUE(result->asExplicitParetoCurveCheckResult().getOverApproximation()->contains(expectedAchievableValues)); -}*/ +} TEST(SparseMaPcaaMultiObjectiveModelCheckerTest, server) { From 5bb656407822a18ad03bad00a78efa6369e2866b Mon Sep 17 00:00:00 2001 From: dehnert Date: Tue, 29 Aug 2017 10:57:24 +0200 Subject: [PATCH 6/9] remove debug output --- src/storm/logic/VariableSubstitutionVisitor.cpp | 1 - 1 file changed, 1 deletion(-) diff --git a/src/storm/logic/VariableSubstitutionVisitor.cpp b/src/storm/logic/VariableSubstitutionVisitor.cpp index 2a84a0c10..bc5c43ed9 100644 --- a/src/storm/logic/VariableSubstitutionVisitor.cpp +++ b/src/storm/logic/VariableSubstitutionVisitor.cpp @@ -43,7 +43,6 @@ namespace storm { std::vector tbReferences; for (unsigned i = 0; i < f.getDimension(); ++i) { - std::cout << f.hasLowerBound(i) << std::endl; if (f.hasLowerBound(i)) { lowerBounds.push_back(TimeBound(f.isLowerBoundStrict(i), f.getLowerBound(i).substitute(substitution))); } else { From 0c5aa1645d577c32864bbd68657f603b41505c5d Mon Sep 17 00:00:00 2001 From: dehnert Date: Tue, 29 Aug 2017 13:33:53 +0200 Subject: [PATCH 7/9] fix reward model generation in JIT builder --- src/storm/builder/jit/ExplicitJitJaniModelBuilder.cpp | 5 +++-- 1 file changed, 3 insertions(+), 2 deletions(-) diff --git a/src/storm/builder/jit/ExplicitJitJaniModelBuilder.cpp b/src/storm/builder/jit/ExplicitJitJaniModelBuilder.cpp index 8f23d14ce..a550ee130 100644 --- a/src/storm/builder/jit/ExplicitJitJaniModelBuilder.cpp +++ b/src/storm/builder/jit/ExplicitJitJaniModelBuilder.cpp @@ -1088,6 +1088,7 @@ namespace storm { std::stringstream tmp; indent(tmp, indentLevel + 1) << "{% for reward in destination_rewards %}choice.addReward({$reward.index}, probability * transientOut.{$reward.variable});" << std::endl; indent(tmp, indentLevel + 1) << "{% endfor %}" << std::endl; + vectorSource << cpptempl::parse(tmp.str(), modelData); indent(vectorSource, indentLevel) << "}" << std::endl << std::endl; indent(vectorSource, indentLevel) << "void performSynchronizedDestinations_" << synchronizationVectorIndex << "(StateType const& in, StateBehaviour& behaviour, StateSet& statesToExplore, "; @@ -2309,8 +2310,8 @@ namespace storm { {% if dontFixDeadlocks %} if (behaviour.empty() && behaviour.isExpanded() ) { - std::cout << currentState << std::endl; - throw storm::exceptions::WrongFormatException("Error while creating sparse matrix from JANI model: found deadlock state and fixing deadlocks was explicitly disabled."); + std::cout << "found deadlock state: " << currentState << std::endl; + throw storm::exceptions::WrongFormatException("Error while creating sparse matrix from JANI model: found deadlock state and fixing deadlocks was explicitly disabled."); } {% endif %} From 3c8f9a2ecf1f87569cc262d6d374c11377acc886 Mon Sep 17 00:00:00 2001 From: Matthias Volk Date: Wed, 30 Aug 2017 14:46:02 +0200 Subject: [PATCH 8/9] Added 5th build stage --- .travis.yml | 51 +++++++++++++++++++++++++++++++++++++++ travis/build-helper.sh | 4 +-- travis/build.sh | 4 +-- travis/generate_travis.py | 1 + 4 files changed, 56 insertions(+), 4 deletions(-) diff --git a/.travis.yml b/.travis.yml index c824cddf6..2b5f50657 100644 --- a/.travis.yml +++ b/.travis.yml @@ -243,6 +243,57 @@ jobs: after_failure: - find build -iname '*err*.log' -type f -print -exec cat {} \; + ### + # Stage: Build (5th run) + ### + + # osx + - stage: Build (5th run) + os: osx + compiler: clang + env: CONFIG=DefaultDebug COMPILER=clang-4.0 STL=libc++ + install: + - travis/install_osx.sh + script: + - travis/build.sh BuildLast + after_failure: + - find build -iname '*err*.log' -type f -print -exec cat {} \; + - stage: Build (5th run) + os: osx + compiler: clang + env: CONFIG=DefaultRelease COMPILER=clang-4.0 STL=libc++ + install: + - travis/install_osx.sh + script: + - travis/build.sh BuildLast + after_failure: + - find build -iname '*err*.log' -type f -print -exec cat {} \; + # ubuntu-16.10 + - stage: Build (5th run) + os: linux + compiler: gcc + env: CONFIG=DefaultDebug LINUX=ubuntu-16.10 COMPILER=gcc-6 + install: + - travis/install_linux.sh + script: + - travis/build.sh BuildLast + before_cache: + - docker cp storm:/storm/. . + after_failure: + - find build -iname '*err*.log' -type f -print -exec cat {} \; + - stage: Build (5th run) + os: linux + compiler: gcc + env: CONFIG=DefaultRelease LINUX=ubuntu-16.10 COMPILER=gcc-6 + install: + - travis/install_linux.sh + script: + - travis/build.sh BuildLast + before_cache: + - docker cp storm:/storm/. . + after_failure: + - find build -iname '*err*.log' -type f -print -exec cat {} \; + ### # Stage: Test all ### diff --git a/travis/build-helper.sh b/travis/build-helper.sh index c6f2dff60..8d73c87e7 100755 --- a/travis/build-helper.sh +++ b/travis/build-helper.sh @@ -13,7 +13,7 @@ travis_fold() { # Helper for distinguishing between different runs run() { case "$1" in - Build1 | Build2 | Build3 | Build4) + Build*) if [[ "$1" == "Build1" ]] then # CMake @@ -38,7 +38,7 @@ run() { make -j$N_JOBS travis_fold end make # Set skip-file - if [[ "$1" != "Build4" ]] + if [[ "$1" != "BuildLast" ]] then touch skip.txt else diff --git a/travis/build.sh b/travis/build.sh index 0b7900e70..668e4f18e 100755 --- a/travis/build.sh +++ b/travis/build.sh @@ -13,7 +13,7 @@ EXITCODE=42 if [ -f build/skip.txt ] then # Remove flag s.t. tests will be executed - if [[ "$1" == "Build4" ]] + if [[ "$1" == "BuildLast" ]] then rm build/skip.txt fi @@ -63,7 +63,7 @@ osx) exit 1 esac -if [[ $EXITCODE == 124 ]] && [[ "$1" == Build* ]] && [[ "$1" != "Build4" ]] +if [[ $EXITCODE == 124 ]] && [[ "$1" == Build* ]] && [[ "$1" != "BuildLast" ]] then exit 0 else diff --git a/travis/generate_travis.py b/travis/generate_travis.py index c47afac0c..14e058a85 100644 --- a/travis/generate_travis.py +++ b/travis/generate_travis.py @@ -24,6 +24,7 @@ stages = [ ("Build (2nd run)", "Build2"), ("Build (3rd run)", "Build3"), ("Build (4th run)", "Build4"), + ("Build (5th run)", "BuildLast"), ("Test all", "TestAll"), ] From f7c803827b5d6d8870b5fd28b0a7afedd4972897 Mon Sep 17 00:00:00 2001 From: dehnert Date: Wed, 30 Aug 2017 21:00:15 +0200 Subject: [PATCH 9/9] remove debug output --- resources/3rdparty/sylvan/src/storm_wrapper.cpp | 2 -- 1 file changed, 2 deletions(-) diff --git a/resources/3rdparty/sylvan/src/storm_wrapper.cpp b/resources/3rdparty/sylvan/src/storm_wrapper.cpp index 09fb51ccf..fb92720d0 100644 --- a/resources/3rdparty/sylvan/src/storm_wrapper.cpp +++ b/resources/3rdparty/sylvan/src/storm_wrapper.cpp @@ -125,8 +125,6 @@ int storm_rational_number_is_zero(storm_rational_number_ptr a) { std::lock_guard lock(rationalNumberMutex); #endif - std::cout << "got ptr for eq check " << a << std::endl; - return storm::utility::isZero(*(storm::RationalNumber const*)a) ? 1 : 0; }