Merge branch 'master' into solver_requirements

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

CHANGELOG.md

@@ -13,6 +13,7 @@ Long run average computation via ValueIteration, LP based MDP model checking, pa
 - storm-cli-utilities now contains cli related stuff, instead of storm-lib
 - storm-pars: support for welldefinedness constraints in mdps.
 - symbolic (MT/BDD) bisimulation 
+- Fixed issue related to variable names that can not be used in Exprtk.
 
 ### Version 1.1.0 (2017/8)
 

src/storm/storage/dd/BisimulationDecomposition.cpp

@@ -9,6 +9,9 @@
 #include "storm/models/symbolic/Mdp.h"
 #include "storm/models/symbolic/StandardRewardModel.h"
 
+#include "storm/settings/SettingsManager.h"
+#include "storm/settings/modules/IOSettings.h"
+
 #include "storm/utility/macros.h"
 #include "storm/exceptions/InvalidOperationException.h"
 #include "storm/exceptions/NotSupportedException.h"
@@ -29,16 +32,25 @@ namespace storm {
         
         template <storm::dd::DdType DdType, typename ValueType>
         BisimulationDecomposition<DdType, ValueType>::BisimulationDecomposition(storm::models::symbolic::Model<DdType, ValueType> const& model, storm::storage::BisimulationType const& bisimulationType) : model(model), preservationInformation(model, bisimulationType), refiner(createRefiner(model, Partition<DdType, ValueType>::create(model, bisimulationType, preservationInformation))) {
+            auto const& ioSettings = storm::settings::getModule<storm::settings::modules::IOSettings>();
+            showProgress = ioSettings.isExplorationShowProgressSet();
+            showProgressDelay = ioSettings.getExplorationShowProgressDelay();
             this->refineWrtRewardModels();
         }
         
         template <storm::dd::DdType DdType, typename ValueType>
         BisimulationDecomposition<DdType, ValueType>::BisimulationDecomposition(storm::models::symbolic::Model<DdType, ValueType> const& model, std::vector<std::shared_ptr<storm::logic::Formula const>> const& formulas, storm::storage::BisimulationType const& bisimulationType) : model(model), preservationInformation(model, formulas, bisimulationType), refiner(createRefiner(model, Partition<DdType, ValueType>::create(model, bisimulationType, preservationInformation))) {
+            auto const& ioSettings = storm::settings::getModule<storm::settings::modules::IOSettings>();
+            showProgress = ioSettings.isExplorationShowProgressSet();
+            showProgressDelay = ioSettings.getExplorationShowProgressDelay();
             this->refineWrtRewardModels();
         }
         
         template <storm::dd::DdType DdType, typename ValueType>
         BisimulationDecomposition<DdType, ValueType>::BisimulationDecomposition(storm::models::symbolic::Model<DdType, ValueType> const& model, Partition<DdType, ValueType> const& initialPartition, bisimulation::PreservationInformation<DdType, ValueType> const& preservationInformation) : model(model), preservationInformation(preservationInformation), refiner(createRefiner(model, initialPartition)) {
+            auto const& ioSettings = storm::settings::getModule<storm::settings::modules::IOSettings>();
+            showProgress = ioSettings.isExplorationShowProgressSet();
+            showProgressDelay = ioSettings.getExplorationShowProgressDelay();
             this->refineWrtRewardModels();
         }
         
@@ -55,12 +67,24 @@ namespace storm {
 #endif
 
             auto start = std::chrono::high_resolution_clock::now();
+            auto timeOfLastMessage = start;
             uint64_t iterations = 0;
             bool refined = true;
             while (refined) {
                 refined = refiner->refine(mode);
+
                 ++iterations;
                 STORM_LOG_TRACE("After iteration " << iterations << " partition has " << refiner->getStatePartition().getNumberOfBlocks() << " blocks.");
+                
+                if (showProgress) {
+                    auto now = std::chrono::high_resolution_clock::now();
+                    auto durationSinceLastMessage = std::chrono::duration_cast<std::chrono::seconds>(now - timeOfLastMessage).count();
+                    if (static_cast<uint64_t>(durationSinceLastMessage) >= showProgressDelay) {
+                        auto durationSinceStart = std::chrono::duration_cast<std::chrono::seconds>(now - start).count();
+                        std::cout << "State partition after " << iterations << " iterations (" << durationSinceStart << "ms) has " << refiner->getStatePartition().getNumberOfBlocks() << " blocks." << std::endl;
+                        timeOfLastMessage = std::chrono::high_resolution_clock::now();
+                    }
+                }
             }
             auto end = std::chrono::high_resolution_clock::now();
             

src/storm/storage/dd/BisimulationDecomposition.h

@@ -60,6 +60,12 @@ namespace storm {
             
             // The refiner to use.
             std::unique_ptr<bisimulation::PartitionRefiner<DdType, ValueType>> refiner;
+            
+            // A flag indicating whether progress is reported.
+            bool showProgress;
+            
+            // The delay between progress reports.
+            uint64_t showProgressDelay;
         };
         
     }

src/storm/storage/expressions/ExprtkExpressionEvaluator.cpp

@@ -1,3 +1,5 @@
+#include <string>
+
 #include "storm/storage/expressions/ExprtkExpressionEvaluator.h"
 #include "storm/storage/expressions/ExpressionManager.h"
 
@@ -13,11 +15,11 @@ namespace storm {
 
             for (auto const& variableTypePair : manager) {
                 if (variableTypePair.second.isBooleanType()) {
-                    symbolTable->add_variable(variableTypePair.first.getName(), this->booleanValues[variableTypePair.first.getOffset()]);
+                    symbolTable->add_variable("v" + std::to_string(variableTypePair.first.getIndex()), this->booleanValues[variableTypePair.first.getOffset()]);
                 } else if (variableTypePair.second.isIntegerType()) {
-                    symbolTable->add_variable(variableTypePair.first.getName(), this->integerValues[variableTypePair.first.getOffset()]);
+                    symbolTable->add_variable("v" + std::to_string(variableTypePair.first.getIndex()), this->integerValues[variableTypePair.first.getOffset()]);
                 } else if (variableTypePair.second.isRationalType()) {
-                    symbolTable->add_variable(variableTypePair.first.getName(), this->rationalValues[variableTypePair.first.getOffset()]);
+                    symbolTable->add_variable("v" + std::to_string(variableTypePair.first.getIndex()), this->rationalValues[variableTypePair.first.getOffset()]);
                 }
             }
         }

src/storm/storage/expressions/ToExprtkStringVisitor.cpp

@@ -167,7 +167,7 @@ namespace storm {
         }
         
         boost::any ToExprtkStringVisitor::visit(VariableExpression const& expression, boost::any const&) {
-            stream << expression.getVariableName();
+            stream << "v" + std::to_string(expression.getVariable().getIndex());
             return boost::any();
         }
         

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