Merge remote-tracking branch 'origin/master' into reward-bounded-multi-objective

.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
     ###

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<std::mutex> lock(rationalNumberMutex);
 #endif
     
-    std::cout << "got ptr for eq check " << a << std::endl;
-    
     return storm::utility::isZero(*(storm::RationalNumber const*)a) ? 1 : 0;
 }
 

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<IndexType, ValueType>& behaviour, StateSet<StateType>& statesToExplore, ";
@@ -2309,7 +2310,7 @@ namespace storm {
 
                                         {% if dontFixDeadlocks %}
                                         if (behaviour.empty() && behaviour.isExpanded() ) {
-                                            std::cout << currentState << std::endl;
+                                            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 %}

src/storm/logic/VariableSubstitutionVisitor.cpp

@@ -43,7 +43,6 @@ namespace storm {
             std::vector<storm::logic::TimeBoundReference> 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 {
@@ -53,7 +52,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));
             }

src/storm/modelchecker/CheckTask.h

@@ -52,6 +52,7 @@ namespace storm {
             template<typename NewFormulaType>
             CheckTask<NewFormulaType, ValueType> substituteFormula(NewFormulaType const& newFormula) const {
                 CheckTask<NewFormulaType, ValueType> result(newFormula, this->optimizationDirection, this->rewardModel, this->onlyInitialStatesRelevant, this->bound, this->qualitative, this->produceSchedulers, this->hint);
+                result.updateOperatorInformation();
                 return result;
             }
             

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;
             }
         }

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;
             }

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<std::shared_ptr<storm::logic::Formula const>> formulas = storm::api::extractFormulasFromProperties(parseFormulasForProgram(formulasAsString, program));
+    std::vector<std::shared_ptr<storm::logic::Formula const>> formulas = storm::api::extractFormulasFromProperties(storm::api::parsePropertiesForPrismProgram(formulasAsString, program));
     storm::generator::NextStateGeneratorOptions options(formulas);
     std::shared_ptr<storm::models::sparse::MarkovAutomaton<storm::RationalNumber>> ma = storm::builder::ExplicitModelBuilder<storm::RationalNumber>(program, options).build()->as<storm::models::sparse::MarkovAutomaton<storm::RationalNumber>>();
     
-    storm::modelchecker::SparseMarkovAutomatonCslModelChecker<storm::models::sparse::MarkovAutomaton<storm::RationalNumber>> checker(*ma);
-    
-    std::unique_ptr<storm::modelchecker::CheckResult> result = checker.check(storm::modelchecker::CheckTask<storm::logic::Formula>(*formulas[0], true));
+    std::unique_ptr<storm::modelchecker::CheckResult> result = storm::modelchecker::multiobjective::performMultiObjectiveModelChecking(*ma, formulas[0]->asMultiObjectiveFormula(), storm::modelchecker::multiobjective::MultiObjectiveMethodSelection::Pcaa);
     ASSERT_TRUE(result->isExplicitParetoCurveCheckResult());
     
     storm::RationalNumber p1 = storm::utility::convertNumber<storm::RationalNumber>(11.0); p1 /= storm::utility::convertNumber<storm::RationalNumber>(6.0);
@@ -45,7 +41,7 @@ TEST(SparseMaPcaaMultiObjectiveModelCheckerTest, serverRationalNumbers) {
     EXPECT_TRUE(expectedAchievableValues->contains(result->asExplicitParetoCurveCheckResult<storm::RationalNumber>().getUnderApproximation()));
     EXPECT_TRUE(result->asExplicitParetoCurveCheckResult<storm::RationalNumber>().getOverApproximation()->contains(expectedAchievableValues));
     
-}*/
+}
 
 
 TEST(SparseMaPcaaMultiObjectiveModelCheckerTest, server) {

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

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

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"),
 ]