Merge branch 'master' into reward-bounded-multi-objective

7 years ago · b97f75698b
14 changed files with 55 additions and 215 deletions
--- a/.travis.yml
+++ b/.travis.yml
@ -7,6 +7,7 @@ branches:
  only:
  - master
  - stable
+sudo: required
 dist: trusty
 language: cpp

@ -20,7 +21,6 @@ cache:
 # Enable docker support
 services:
 - docker
-sudo: required

 notifications:
  email:
@ -43,7 +43,7 @@ jobs:
    - stage: Build (1st run)
      os: osx
      compiler: clang
-      env: CONFIG=DefaultDebug COMPILER=clang-4.0 STL=libc++
+      env: CONFIG=DefaultDebug COMPILER=clang STL=libc++
      install:
        - rm -rf build
        - travis/install_osx.sh
@ -54,7 +54,7 @@ jobs:
    - stage: Build (1st run)
      os: osx
      compiler: clang
-      env: CONFIG=DefaultRelease COMPILER=clang-4.0 STL=libc++
+      env: CONFIG=DefaultRelease COMPILER=clang STL=libc++
      install:
        - rm -rf build
        - travis/install_osx.sh
@ -66,7 +66,7 @@ jobs:
    - stage: Build (1st run)
      os: linux
      compiler: gcc
-      env: CONFIG=DefaultDebug LINUX=ubuntu-16.10 COMPILER=gcc-6
+      env: CONFIG=DefaultDebug LINUX=ubuntu-16.10 COMPILER=gcc
      install:
        - rm -rf build
        - travis/install_linux.sh
@ -79,7 +79,7 @@ jobs:
    - stage: Build (1st run)
      os: linux
      compiler: gcc
-      env: CONFIG=DefaultRelease LINUX=ubuntu-16.10 COMPILER=gcc-6
+      env: CONFIG=DefaultRelease LINUX=ubuntu-16.10 COMPILER=gcc
      install:
        - rm -rf build
        - travis/install_linux.sh
@ -98,7 +98,7 @@ jobs:
    - stage: Build (2nd run)
      os: osx
      compiler: clang
-      env: CONFIG=DefaultDebug COMPILER=clang-4.0 STL=libc++
+      env: CONFIG=DefaultDebug COMPILER=clang STL=libc++
      install:
        - travis/install_osx.sh
      script:
@ -108,7 +108,7 @@ jobs:
    - stage: Build (2nd run)
      os: osx
      compiler: clang
-      env: CONFIG=DefaultRelease COMPILER=clang-4.0 STL=libc++
+      env: CONFIG=DefaultRelease COMPILER=clang STL=libc++
      install:
        - travis/install_osx.sh
      script:
@ -119,7 +119,7 @@ jobs:
    - stage: Build (2nd run)
      os: linux
      compiler: gcc
-      env: CONFIG=DefaultDebug LINUX=ubuntu-16.10 COMPILER=gcc-6
+      env: CONFIG=DefaultDebug LINUX=ubuntu-16.10 COMPILER=gcc
      install:
        - travis/install_linux.sh
      script:
@ -131,7 +131,7 @@ jobs:
    - stage: Build (2nd run)
      os: linux
      compiler: gcc
-      env: CONFIG=DefaultRelease LINUX=ubuntu-16.10 COMPILER=gcc-6
+      env: CONFIG=DefaultRelease LINUX=ubuntu-16.10 COMPILER=gcc
      install:
        - travis/install_linux.sh
      script:
@ -149,7 +149,7 @@ jobs:
    - stage: Build (3rd run)
      os: osx
      compiler: clang
-      env: CONFIG=DefaultDebug COMPILER=clang-4.0 STL=libc++
+      env: CONFIG=DefaultDebug COMPILER=clang STL=libc++
      install:
        - travis/install_osx.sh
      script:
@ -159,7 +159,7 @@ jobs:
    - stage: Build (3rd run)
      os: osx
      compiler: clang
-      env: CONFIG=DefaultRelease COMPILER=clang-4.0 STL=libc++
+      env: CONFIG=DefaultRelease COMPILER=clang STL=libc++
      install:
        - travis/install_osx.sh
      script:
@ -170,7 +170,7 @@ jobs:
    - stage: Build (3rd run)
      os: linux
      compiler: gcc
-      env: CONFIG=DefaultDebug LINUX=ubuntu-16.10 COMPILER=gcc-6
+      env: CONFIG=DefaultDebug LINUX=ubuntu-16.10 COMPILER=gcc
      install:
        - travis/install_linux.sh
      script:
@ -182,7 +182,7 @@ jobs:
    - stage: Build (3rd run)
      os: linux
      compiler: gcc
-      env: CONFIG=DefaultRelease LINUX=ubuntu-16.10 COMPILER=gcc-6
+      env: CONFIG=DefaultRelease LINUX=ubuntu-16.10 COMPILER=gcc
      install:
        - travis/install_linux.sh
      script:
@ -200,68 +200,17 @@ jobs:
    - stage: Build (4th run)
      os: osx
      compiler: clang
-      env: CONFIG=DefaultDebug COMPILER=clang-4.0 STL=libc++
-      install:
-        - travis/install_osx.sh
-      script:
-        - travis/build.sh Build4
-      after_failure:
-        - find build -iname '*err*.log' -type f -print -exec cat {} \;
-    - stage: Build (4th run)
-      os: osx
-      compiler: clang
-      env: CONFIG=DefaultRelease COMPILER=clang-4.0 STL=libc++
-      install:
-        - travis/install_osx.sh
-      script:
-        - travis/build.sh Build4
-      after_failure:
-        - find build -iname '*err*.log' -type f -print -exec cat {} \;
-    # ubuntu-16.10
-    - stage: Build (4th run)
-      os: linux
-      compiler: gcc
-      env: CONFIG=DefaultDebug LINUX=ubuntu-16.10 COMPILER=gcc-6
-      install:
-        - travis/install_linux.sh
-      script:
-        - travis/build.sh Build4
-      before_cache:
-        - docker cp storm:/storm/. .
-      after_failure:
-        - find build -iname '*err*.log' -type f -print -exec cat {} \;
-    - stage: Build (4th run)
-      os: linux
-      compiler: gcc
-      env: CONFIG=DefaultRelease LINUX=ubuntu-16.10 COMPILER=gcc-6
-      install:
-        - travis/install_linux.sh
-      script:
-        - travis/build.sh Build4
-      before_cache:
-        - docker cp storm:/storm/. .
-      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++
+      env: CONFIG=DefaultDebug COMPILER=clang 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)
+    - stage: Build (4th run)
      os: osx
      compiler: clang
-      env: CONFIG=DefaultRelease COMPILER=clang-4.0 STL=libc++
+      env: CONFIG=DefaultRelease COMPILER=clang STL=libc++
      install:
        - travis/install_osx.sh
      script:
@ -269,10 +218,10 @@ jobs:
      after_failure:
        - find build -iname '*err*.log' -type f -print -exec cat {} \;
    # ubuntu-16.10
-    - stage: Build (5th run)
+    - stage: Build (4th run)
      os: linux
      compiler: gcc
-      env: CONFIG=DefaultDebug LINUX=ubuntu-16.10 COMPILER=gcc-6
+      env: CONFIG=DefaultDebug LINUX=ubuntu-16.10 COMPILER=gcc
      install:
        - travis/install_linux.sh
      script:
@ -281,10 +230,10 @@ jobs:
        - docker cp storm:/storm/. .
      after_failure:
        - find build -iname '*err*.log' -type f -print -exec cat {} \;
-    - stage: Build (5th run)
+    - stage: Build (4th run)
      os: linux
      compiler: gcc
-      env: CONFIG=DefaultRelease LINUX=ubuntu-16.10 COMPILER=gcc-6
+      env: CONFIG=DefaultRelease LINUX=ubuntu-16.10 COMPILER=gcc
      install:
        - travis/install_linux.sh
      script:
@ -302,7 +251,7 @@ jobs:
    - stage: Test all
      os: osx
      compiler: clang
-      env: CONFIG=DefaultDebug COMPILER=clang-4.0 STL=libc++
+      env: CONFIG=DefaultDebug COMPILER=clang STL=libc++
      install:
        - travis/install_osx.sh
      script:
@ -312,7 +261,7 @@ jobs:
    - stage: Test all
      os: osx
      compiler: clang
-      env: CONFIG=DefaultRelease COMPILER=clang-4.0 STL=libc++
+      env: CONFIG=DefaultRelease COMPILER=clang STL=libc++
      install:
        - travis/install_osx.sh
      script:
@ -323,7 +272,7 @@ jobs:
    - stage: Test all
      os: linux
      compiler: gcc
-      env: CONFIG=DefaultDebug LINUX=ubuntu-16.10 COMPILER=gcc-6
+      env: CONFIG=DefaultDebug LINUX=ubuntu-16.10 COMPILER=gcc
      install:
        - travis/install_linux.sh
      script:
@ -335,7 +284,7 @@ jobs:
    - stage: Test all
      os: linux
      compiler: gcc
-      env: CONFIG=DefaultRelease LINUX=ubuntu-16.10 COMPILER=gcc-6
+      env: CONFIG=DefaultRelease LINUX=ubuntu-16.10 COMPILER=gcc
      install:
        - travis/install_linux.sh
      script:
--- a/resources/3rdparty/CMakeLists.txt
+++ b/resources/3rdparty/CMakeLists.txt
@ -395,9 +395,9 @@ endif()
 set(STORM_HAVE_MSAT ${ENABLE_MSAT})
 if (ENABLE_MSAT)
    message (STATUS "Storm - Linking with MathSAT.")
-    link_directories("${MSAT_ROOT}/lib")
-    include_directories("${MSAT_ROOT}/include")
-    list(APPEND STORM_LINK_LIBRARIES "mathsat")
+    find_library(MSAT_LIB mathsat PATHS "${MSAT_ROOT}/lib")
+    add_imported_library(msat SHARED ${MSAT_LIB} "${MSAT_ROOT}/include")
+    list(APPEND STORM_DEP_TARGETS msat_SHARED)
 endif(ENABLE_MSAT)

 #############################################################
--- a/src/storm/builder/jit/ExplicitJitJaniModelBuilder.cpp
+++ b/src/storm/builder/jit/ExplicitJitJaniModelBuilder.cpp
@ -3,6 +3,7 @@
 #include <iostream>
 #include <cstdio>
 #include <chrono>
+#include <errno.h>

 #include "storm/solver/SmtSolver.h"

@ -163,7 +164,7 @@ namespace storm {
                STORM_LOG_TRACE("Executing command: " << command);
                
                std::unique_ptr<FILE> pipe(popen(command.c_str(), "r"));
-                STORM_LOG_THROW(pipe, storm::exceptions::InvalidStateException, "Call to popen failed.");
+                STORM_LOG_THROW(pipe, storm::exceptions::InvalidStateException, "Call to popen failed: " << strerror(errno));
                
                while (!feof(pipe.get())) {
                    if (fgets(buffer, 128, pipe.get()) != nullptr)
--- a/src/storm/storage/SparseMatrix.cpp
+++ b/src/storm/storage/SparseMatrix.cpp
@ -1493,8 +1493,9 @@ namespace storm {
            typename std::vector<ValueType>::iterator resultIterator = x.end() - 1;
            typename std::vector<ValueType>::iterator resultIteratorEnd = x.begin() - 1;
            
-            index_type currentRow = 0;
+            index_type currentRow = getRowCount();
            for (; resultIterator != resultIteratorEnd; --rowIterator, --resultIterator, --bIt) {
+                --currentRow;
                ValueType tmpValue = storm::utility::zero<ValueType>();
                ValueType diagonalElement = storm::utility::zero<ValueType>();
                
@ -1505,9 +1506,8 @@ namespace storm {
                        diagonalElement += it->getValue();
                    }
                }
-                
+                assert(!storm::utility::isZero(diagonalElement));
                *resultIterator = ((storm::utility::one<ValueType>() - omega) * *resultIterator) + (omega / diagonalElement) * (*bIt - tmpValue);
-                ++currentRow;
            }
        }
        
--- a/travis/build-helper.sh
+++ b/travis/build-helper.sh
@ -50,7 +50,13 @@ run() {
    # Test all
    travis_fold start test_all
    cd build
-    ctest test --output-on-failure
+    # Hack to avoid memout problem with jit and sylvan
+    # 1. Run other tests without builder tests
+    ctest test --output-on-failure -E run-test-builder
+    # 2. Run builder tests without sylvan tests
+    ./bin/test-builder --gtest_filter=-"DdJaniModelBuilderTest_Sylvan.*"
+    # 3. Just run sylvan tests
+    ./bin/test-builder --gtest_filter="DdJaniModelBuilderTest_Sylvan.*"
    travis_fold end test_all
    ;;

@ -66,57 +72,17 @@ run() {
 export PATH="/usr/local/opt/coreutils/libexec/gnubin:$PATH"

 case $COMPILER in
-gcc-4.8)
-    export CC=gcc-4.8
-    export CXX=g++-4.8
-    ;;
-
-gcc-4.9)
-    export CC=gcc-4.9
-    export CXX=g++-4.9
-    ;;
-
-gcc-5)
-    export CC=gcc-5
-    export CXX=g++-5
-    ;;
-
 gcc-6)
    export CC=gcc-6
    export CXX=g++-6
    ;;

-gcc-default)
+gcc)
    export CC=gcc
    export CXX=g++
    ;;

-clang-3.5)
-    export CC=clang-3.5
-    export CXX=clang++-3.5
-    ;;
-
-clang-3.6)
-    export CC=clang-3.6
-    export CXX=clang++-3.6
-    ;;
-
-clang-3.7)
-    export CC=clang-3.7
-    export CXX=clang++-3.7
-    ;;
-
-clang-3.8)
-    export CC=clang-3.8
-    export CXX=clang++-3.8
-    ;;
-
-clang-3.9)
-    export CC=clang-3.9
-    export CXX=clang++-3.9
-    ;;
-
-clang-4.0)
+clang-4)
    case "$OS" in
    linux)
        export CC=clang-4.0
@ -130,7 +96,7 @@ clang-4.0)
    esac
    ;;

-clang-default)
+clang)
    export CC=clang
    export CXX=clang++
    ;;
--- a/travis/dockerfiles/Dockerfile.debian-9
+++ b/travis/dockerfiles/Dockerfile.debian-9
@ -1,16 +0,0 @@
-FROM debian:9
-MAINTAINER Matthias Volk <matthias.volk@cs.rwth-aachen.de>
-
-RUN apt-get update -qq && apt-get install -y --no-install-recommends \
-    build-essential \
-    ruby \
-    git \
-    cmake \
-    libboost-all-dev \
-    libcln-dev \
-    libeigen3-dev \
-    libgmp-dev \
-    libginac-dev \
-    automake \
-    libglpk-dev \
-    libz3-dev
--- a/travis/dockerfiles/Dockerfile.storm
+++ b/travis/dockerfiles/Dockerfile.storm
@ -1,8 +0,0 @@
-FROM mvolk/storm-basesystem:ubuntu-16.10
-MAINTAINER Matthias Volk <matthias.volk@cs.rwth-aachen.de>
-
-COPY build_carl.sh /opt
-RUN cd opt && ./build_carl.sh
-
-COPY build_storm.sh /opt
-RUN cd opt && ./build_storm.sh
--- a/travis/dockerfiles/Dockerfile.ubuntu-16.10
+++ b/travis/dockerfiles/Dockerfile.ubuntu-16.10
@ -1,17 +0,0 @@
-FROM ubuntu:16.10
-MAINTAINER Matthias Volk <matthias.volk@cs.rwth-aachen.de>
-
-RUN apt-get update -qq && apt-get install -y --no-install-recommends \
-    build-essential \
-    ruby \
-    git \
-    cmake \
-    libboost-all-dev \
-    libcln-dev \
-    libeigen3-dev \
-    libgmp-dev \
-    libginac-dev \
-    automake \
-    libglpk-dev \
-    libhwloc-dev \
-    libz3-dev
--- a/travis/dockerfiles/build_carl.sh
+++ b/travis/dockerfiles/build_carl.sh
@ -1,9 +0,0 @@
-#!/bin/bash
-echo "Building Carl..."
-git clone https://github.com/smtrat/carl.git
-cd carl
-mkdir build
-cd build
-cmake .. -DCMAKE_BUILD_TYPE=Release -DUSE_CLN_NUMBERS=ON -DUSE_GINAC=ON
-make lib_carl -j2
-echo "Building Carl finished"
--- a/travis/dockerfiles/build_docker.sh
+++ b/travis/dockerfiles/build_docker.sh
@ -1,9 +0,0 @@
-#!/bin/bash
-
-# Build Ubuntu 16.10 "Yakkety Yak"
-docker build -t mvolk/storm-basesystem:ubuntu-16.10 -f Dockerfile.ubuntu-16.10 .
-docker push mvolk/storm-basesystem:ubuntu-16.10
-
-# Build Debian 9 "Stretch"
-docker build -t mvolk/storm-basesystem:debian-9 -f Dockerfile.debian-9 .
-docker push mvolk/storm-basesystem:debian-9
--- a/travis/dockerfiles/build_storm.sh
+++ b/travis/dockerfiles/build_storm.sh
@ -1,9 +0,0 @@
-#!/bin/bash
-echo "Building Storm..."
-git clone https://github.com/moves-rwth/storm.git
-cd storm
-mkdir build
-cd build
-cmake .. -DCMAKE_BUILD_TYPE=Release
-make storm storm-dft storm-pars -j1
-echo "Building Storm finished"
--- a/travis/generate_travis.py
+++ b/travis/generate_travis.py
@ -2,14 +2,14 @@
 # Configuration for Linux
 configs_linux = [
    # OS, compiler
-    ("ubuntu-16.10", "gcc", "-6"),
+    ("ubuntu-16.10", "gcc", ""),
    #("debian-9", "gcc", "-6"),
 ]

 # Configurations for Mac
 configs_mac = [
    # OS, compiler
-    ("osx", "clang", "-4.0"),
+    ("osx", "clang", ""),
 ]

 # Build types
@ -23,8 +23,7 @@ stages = [
    ("Build (1st run)", "Build1"),
    ("Build (2nd run)", "Build2"),
    ("Build (3rd run)", "Build3"),
-    ("Build (4th run)", "Build4"),
-    ("Build (5th run)", "BuildLast"),
+    ("Build (4th run)", "BuildLast"),
    ("Test all", "TestAll"),
 ]

@ -41,6 +40,7 @@ if __name__ == "__main__":
    s += "  only:\n"
    s += "  - master\n"
    s += "  - stable\n"
+    s += "sudo: required\n"
    s += "dist: trusty\n"
    s += "language: cpp\n"
    s += "\n"
@ -54,7 +54,6 @@ if __name__ == "__main__":
    s += "# Enable docker support\n"
    s += "services:\n"
    s += "- docker\n"
-    s += "sudo: required\n"
    s += "\n"

    s += "notifications:\n"
--- a/travis/install_linux.sh
+++ b/travis/install_linux.sh
@ -8,4 +8,4 @@ then
  exit 0
 fi

-sudo apt-get install -qq -y docker
+#sudo apt-get install -qq -y docker
--- a/travis/install_osx.sh
+++ b/travis/install_osx.sh
@ -18,8 +18,7 @@ install_brew_package() {
    brew outdated "$1" || brew upgrade "$@"
  else
    # Package not installed yet, install.
-    # If there are conflicts, try overwriting the files (these are in /usr/local anyway so it should be ok).
-    brew install "$@" || brew link --overwrite gcc49
+    brew install "$@" || brew link --overwrite "$@"
  fi
 }

@ -40,19 +39,14 @@ install_brew_package md5sha1sum
 # For `timeout'
 install_brew_package coreutils

-which cmake &>/dev/null || install_brew_package cmake
+install_brew_package cmake

 # Install compiler
 case "${COMPILER}" in
-gcc-4.8)       install_brew_package gcc@4.8 ;;
-gcc-4.9)       install_brew_package gcc@4.9 ;;
-gcc-5)         install_brew_package gcc@5 ;;
-gcc-6)         install_brew_package gcc@6 ;;
-clang-default) ;;
-clang-3.7)     install_brew_package llvm@3.7 --with-clang --with-libcxx;;
-clang-3.8)     install_brew_package llvm@3.8 --with-clang --with-libcxx;;
-clang-3.9)     install_brew_package llvm@3.9 --with-clang --with-libcxx;;
-clang-4.0)     install_brew_package llvm     --with-clang --with-libcxx;;
+gcc)         install_brew_package gcc ;;
+gcc-6)       install_brew_package gcc@6 ;;
+clang)       ;;
+clang-4)     install_brew_package llvm@4 --with-clang --with-libcxx;;
 *) echo "Compiler not supported: ${COMPILER}. See travis/install_osx.sh"; exit 1 ;;
 esac
 travis_fold end brew_install_util
@ -66,8 +60,7 @@ install_brew_package ginac
 install_brew_package doxygen
 install_brew_package boost --c++11
 install_brew_package z3 # optional
-brew tap homebrew/science
-install_brew_package homebrew/science/glpk
-install_brew_package homebrew/science/hwloc
+install_brew_package glpk
+install_brew_package hwloc
 install_brew_package eigen
 travis_fold end brew_install_dependencies