diff --git a/.gitmodules b/.gitmodules
deleted file mode 100644
index 92b35f18f..000000000
--- a/.gitmodules
+++ /dev/null
@@ -1,3 +0,0 @@
-[submodule "resources/3rdparty/cusplibrary"]
- path = resources/3rdparty/cusplibrary
- url = https://github.com/cusplibrary/cusplibrary.git
diff --git a/.travis.yml b/.travis.yml
index 2b5f50657..a9b1577af 100644
--- 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:
diff --git a/CHANGELOG.md b/CHANGELOG.md
index 5e971c46e..8e4c84799 100644
--- a/CHANGELOG.md
+++ b/CHANGELOG.md
@@ -19,6 +19,7 @@ Version 1.1.x
- 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.
+- DRN parser improved
### Version 1.1.0 (2017/8)
diff --git a/Jenkinsfile b/Jenkinsfile
deleted file mode 100644
index fd321e147..000000000
--- a/Jenkinsfile
+++ /dev/null
@@ -1,44 +0,0 @@
-node {
- def cmakeTool
- stage('Preparation') {
- // Get some code from a GitHub repository
- checkout scm
-
- cmakeTool = tool name: 'InSearchPath', type: 'hudson.plugins.cmake.CmakeTool'
-
- sh "rm -rf build"
- sh "mkdir -p build"
- }
- stage('Configure') {
- dir("build") {
- sh "${cmakeTool} .."
- }
-
- }
-
- stage('Build') {
- dir("build") {
- sh "make storm"
- }
-
- }
-
- stage('Build Tests') {
- dir("build") {
- sh "make -j 4 tests"
- }
-
- }
-
- stage('Test') {
- dir("build") {
- sh "make check-verbose"
- }
- }
-
- stage('Archive') {
- archiveArtifacts artifacts: 'build/bin/*', onlyIfSuccessful: true
- archiveArtifacts artifacts: 'build/lib/*', onlyIfSuccessful: true
- archiveArtifacts artifacts: 'build/include/*', onlyIfSuccessful: true
- }
-}
diff --git a/doc/build.md b/doc/build.md
deleted file mode 100644
index 725794034..000000000
--- a/doc/build.md
+++ /dev/null
@@ -1,37 +0,0 @@
-# Building Storm
-
-
-## Requirements
-CMake >= 3.2
- CMake is required as it is used to generate the Makefiles or Projects/Solutions required to build StoRM.
-
-### Compiler:
- A C++11 compliant compiler is required to build StoRM. It is tested and known to work with the following compilers:
- - GCC 5.3
- - Clang 3.5.0
-
- Other versions or compilers might work, but are not tested.
-
- The following Compilers are known NOT to work:
- - Microsoft Visual Studio versions older than 2013,
- - GCC versions 4.9.1 and older.
-
-Prerequisites:
- Boost >= 1.61
- Build using the Boost Build system, for x64 use "bjam address-model=64" or "bjam.exe address-model=64 --build-type=complete"
-
-## Instructions
-
-### General
-
-```bash
-mkdir build
-cd build
-```
-
-It is recommended to make an out-of-source build, meaning that the folder in which CMake generates its Cache, Makefiles and output files should not be the Project Root nor its Source Directory.
-A typical build layout is to create a folder "build" in the project root alongside the CMakeLists.txt file, change into this folder and execute "cmake .." as this will leave all source files untouched
-and makes cleaning up the build tree very easy.
-There are several options available for the CMake Script as to control behaviour and included components.
-If no error occured during the last CMake Configure round, press Generate.
-Now you can build StoRM using the generated project/makefiles in the Build folder you selected.
\ No newline at end of file
diff --git a/doc/dependencies.md b/doc/dependencies.md
deleted file mode 100644
index 34660fdc0..000000000
--- a/doc/dependencies.md
+++ /dev/null
@@ -1,37 +0,0 @@
-# Dependencies
-
-## Included Dependencies:
-- Carl 1.0
-- CUDD 3.0.0
- CUDD is included in the StoRM Sources under /resources/3rdparty/cudd-2.5.0 and builds automatically alongside StoRM.
- Its Sourced where heavily modified as to incorporate newer Versions of Boost, changes in C++ (TR1 to C++11) and
- to remove components only available under UNIX.
-- Eigen 3.3 beta1
- Eigen is included in the StoRM Sources under /resources/3rdparty/eigen and builds automatically alongside StoRM.
-
-
-- GTest 1.7.0
- GTest is included in the StoRM Sources under /resources/3rdparty/gtest-1.7.0 and builds automatically alongside StoRM
-- GMM >= 4.2
- GMM is included in the StoRM Sources under /resources/3rdparty/gmm-4.2 and builds automatically alongside StoRM.
-
-## Optional:
-- Gurobi >= 5.6.2
- Specify the path to the gurobi root dir using -DGUROBI_ROOT=/your/path/to/gurobi
-- Z3 >= 4.3.2
- Specify the path to the z3 root dir using -DZ3_ROOT=/your/path/to/z3
-- MathSAT >= 5.2.11
- Specify the path to the mathsat root dir using -DMSAT_ROOT=/your/path/to/mathsat
-- MPIR >= 2.7.0
- MSVC only and only if linked with MathSAT
- Specify the path to the gmp-include directory -DGMP_INCLUDE_DIR=/your/path/to/mathsat
- Specify the path to the mpir.lib directory -DGMP_MPIR_LIBRARY=/your/path/to/mpir.lib
- Specify the path to the mpirxx.lib directory -DGMP_MPIRXX_LIBRARY=/your/path/to/mpirxx.lib
-- GMP
- clang and gcc only
-- CUDA Toolkit >= 6.5
- Specify the path to the cuda toolkit root dir using -DCUDA_ROOT=/your/path/to/cuda
-- CUSP >= 0.4.0
- Only of built with CUDA Toolkit
- CUSP is included in the StoRM Sources as a git-submodule unter /resources/3rdparty/cusplibrary
-
diff --git a/doc/getting-started.md b/doc/getting-started.md
deleted file mode 100644
index 8b1378917..000000000
--- a/doc/getting-started.md
+++ /dev/null
@@ -1 +0,0 @@
-
diff --git a/install.sh b/install.sh
deleted file mode 100755
index 384bbb2e9..000000000
--- a/install.sh
+++ /dev/null
@@ -1,2 +0,0 @@
-#!/bin/bash
-pip install -ve stormpy
diff --git a/resources/3rdparty/CMakeLists.txt b/resources/3rdparty/CMakeLists.txt
index 34e38bbf7..cb7e064ec 100644
--- a/resources/3rdparty/CMakeLists.txt
+++ b/resources/3rdparty/CMakeLists.txt
@@ -227,6 +227,10 @@ if(carl_FOUND AND NOT STORM_FORCE_SHIPPED_CARL)
else()
message(SEND_ERROR "File ${carlLOCATION} does not exist, did you build carl?")
endif()
+ if("${carl_MINORYEARVERSION}" STREQUAL "" OR "${carl_MINORMONTHVERSION}" STREQUAL "" OR "${carl_MAINTENANCEVERSION}" STREQUAL "")
+ # don't have detailed version information, probably an old version of carl
+ message(FATAL_ERROR "Carl at ${carlLOCATION} outdated, require ${CARL_MINYEAR}.${CARL_MINMONTH}.${CARL_MINPATCH}, have ${carl_VERSION}")
+ endif()
if(${carl_MINORYEARVERSION} LESS ${CARL_MINYEAR})
message(SEND_ERROR "Carl outdated, require ${CARL_MINYEAR}.${CARL_MINMONTH}.${CARL_MINPATCH}, have ${carl_VERSION}")
elseif(${carl_MINORYEARVERSION} EQUAL ${CARL_MINYEAR})
@@ -391,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)
#############################################################
diff --git a/resources/3rdparty/sylvan/src/lace.c b/resources/3rdparty/sylvan/src/lace.c
index 08e9f8843..64443e23b 100755
--- a/resources/3rdparty/sylvan/src/lace.c
+++ b/resources/3rdparty/sylvan/src/lace.c
@@ -1088,6 +1088,12 @@ void lace_exit()
lace_resume();
lace_barrier();
+ // Free the memory of the workers.
+ for (unsigned int i=0; i<n_workers; i++) munmap(workers_memory[i], workers_memory_size);
+ free(workers_memory);
+ free(workers);
+ free(workers_p);
+
// finally, destroy the barriers
lace_barrier_destroy();
pthread_barrier_destroy(&suspend_barrier);
diff --git a/src/storm-cli-utilities/cli.cpp b/src/storm-cli-utilities/cli.cpp
index cb33c3205..3ff4d4593 100644
--- a/src/storm-cli-utilities/cli.cpp
+++ b/src/storm-cli-utilities/cli.cpp
@@ -64,7 +64,7 @@ namespace storm {
}
- void printHeader(std::string const& name, const int argc, const char* argv[]) {
+ void printHeader(std::string const& name, const int argc, const char** argv) {
STORM_PRINT(name << " " << storm::utility::StormVersion::shortVersionString() << std::endl << std::endl);
// "Compute" the command line argument string with which storm was invoked.
diff --git a/src/storm-cli-utilities/cli.h b/src/storm-cli-utilities/cli.h
index 4decbb02c..e8d8601e9 100644
--- a/src/storm-cli-utilities/cli.h
+++ b/src/storm-cli-utilities/cli.h
@@ -11,7 +11,7 @@ namespace storm {
*/
int64_t process(const int argc, const char** argv);
- void printHeader(std::string const& name, const int argc, const char* argv[]);
+ void printHeader(std::string const& name, const int argc, const char** argv);
void printVersion(std::string const& name);
@@ -27,7 +27,8 @@ namespace storm {
bool parseOptions(const int argc, const char* argv[]);
void processOptions();
-
+
+ void setUrgentOptions();
}
}
diff --git a/src/storm-cli-utilities/model-handling.h b/src/storm-cli-utilities/model-handling.h
index f702667b7..d91d84479 100644
--- a/src/storm-cli-utilities/model-handling.h
+++ b/src/storm-cli-utilities/model-handling.h
@@ -232,7 +232,9 @@ namespace storm {
std::shared_ptr<storm::models::sparse::Model<ValueType>> result = model;
model->close();
if (model->hasOnlyTrivialNondeterminism()) {
- result = model->convertToCTMC();
+ STORM_LOG_WARN_COND(false, "Non-deterministic choices in MA seem to be unnecessary. Consider using a CTMC instead.");
+ // Activate again if transformation is correct
+ //result = model->convertToCTMC();
}
return result;
}
diff --git a/src/storm-dft-cli/CMakeLists.txt b/src/storm-dft-cli/CMakeLists.txt
index b8cdbbd27..4780eef4d 100644
--- a/src/storm-dft-cli/CMakeLists.txt
+++ b/src/storm-dft-cli/CMakeLists.txt
@@ -1,9 +1,9 @@
# Create storm-dft.
-add_executable(storm-dft-cli ${PROJECT_SOURCE_DIR}/src/storm-dft-cli/storm-dyftee.cpp)
+add_executable(storm-dft-cli ${PROJECT_SOURCE_DIR}/src/storm-dft-cli/storm-dft.cpp)
target_link_libraries(storm-dft-cli storm-dft storm-cli-utilities) # Adding headers for xcode
set_target_properties(storm-dft-cli PROPERTIES OUTPUT_NAME "storm-dft")
add_dependencies(binaries storm-dft-cli)
# installation
-install(TARGETS storm-dft-cli RUNTIME DESTINATION bin LIBRARY DESTINATION lib OPTIONAL)
\ No newline at end of file
+install(TARGETS storm-dft-cli RUNTIME DESTINATION bin LIBRARY DESTINATION lib OPTIONAL)
diff --git a/src/storm-dft-cli/storm-dyftee.cpp b/src/storm-dft-cli/storm-dft.cpp
similarity index 64%
rename from src/storm-dft-cli/storm-dyftee.cpp
rename to src/storm-dft-cli/storm-dft.cpp
index 8eef6f0b5..3e69fb217 100644
--- a/src/storm-dft-cli/storm-dyftee.cpp
+++ b/src/storm-dft-cli/storm-dft.cpp
@@ -1,20 +1,14 @@
-#include "storm/logic/Formula.h"
-#include "storm/utility/initialize.h"
-#include "storm/api/storm.h"
-#include "storm-cli-utilities/cli.h"
-#include "storm/exceptions/BaseException.h"
-
-#include "storm/logic/Formula.h"
+#include "storm-dft/settings/DftSettings.h"
+#include "storm-dft/settings/modules/DftIOSettings.h"
+#include "storm-dft/settings/modules/FaultTreeSettings.h"
#include "storm/settings/modules/IOSettings.h"
-#include "storm/settings/modules/CoreSettings.h"
-#include "storm/settings/modules/DebugSettings.h"
-#include "storm/settings/modules/GmmxxEquationSolverSettings.h"
-#include "storm/settings/modules/MinMaxEquationSolverSettings.h"
-#include "storm/settings/modules/NativeEquationSolverSettings.h"
-#include "storm/settings/modules/EliminationSettings.h"
#include "storm/settings/modules/ResourceSettings.h"
+#include "storm/utility/initialize.h"
+#include "storm/api/storm.h"
+#include "storm-cli-utilities/cli.h"
+
#include "storm-dft/parser/DFTGalileoParser.h"
#include "storm-dft/parser/DFTJsonParser.h"
#include "storm-dft/modelchecker/dft/DFTModelChecker.h"
@@ -22,13 +16,8 @@
#include "storm-dft/transformations/DftToGspnTransformator.h"
#include "storm-dft/storage/dft/DftJsonExporter.h"
-#include "storm-dft/settings/modules/DFTSettings.h"
-
#include "storm-gspn/storage/gspn/GSPN.h"
#include "storm-gspn/storm-gspn.h"
-#include "storm/settings/modules/GSPNSettings.h"
-#include "storm/settings/modules/GSPNExportSettings.h"
-
#include <boost/lexical_cast.hpp>
#include <memory>
@@ -45,18 +34,18 @@
*/
template <typename ValueType>
void analyzeDFT(std::vector<std::string> const& properties, bool symred, bool allowModularisation, bool enableDC, double approximationError) {
- storm::settings::modules::DFTSettings const& dftSettings = storm::settings::getModule<storm::settings::modules::DFTSettings>();
+ storm::settings::modules::DftIOSettings const& dftIOSettings = storm::settings::getModule<storm::settings::modules::DftIOSettings>();
std::shared_ptr<storm::storage::DFT<ValueType>> dft;
// Build DFT from given file.
- if (dftSettings.isDftJsonFileSet()) {
+ if (dftIOSettings.isDftJsonFileSet()) {
storm::parser::DFTJsonParser<ValueType> parser;
- std::cout << "Loading DFT from file " << dftSettings.getDftJsonFilename() << std::endl;
- dft = std::make_shared<storm::storage::DFT<ValueType>>(parser.parseJson(dftSettings.getDftJsonFilename()));
+ std::cout << "Loading DFT from file " << dftIOSettings.getDftJsonFilename() << std::endl;
+ dft = std::make_shared<storm::storage::DFT<ValueType>>(parser.parseJson(dftIOSettings.getDftJsonFilename()));
} else {
storm::parser::DFTGalileoParser<ValueType> parser;
- std::cout << "Loading DFT from file " << dftSettings.getDftFilename() << std::endl;
- dft = std::make_shared<storm::storage::DFT<ValueType>>(parser.parseDFT(dftSettings.getDftFilename()));
+ std::cout << "Loading DFT from file " << dftIOSettings.getDftFilename() << std::endl;
+ dft = std::make_shared<storm::storage::DFT<ValueType>>(parser.parseDFT(dftIOSettings.getDftFilename()));
}
// Build properties
@@ -92,83 +81,39 @@ void analyzeWithSMT(std::string filename) {
//std::cout << "SMT result: " << sat << std::endl;
}
+void processOptions() {
+ // Start by setting some urgent options (log levels, resources, etc.)
+ storm::cli::setUrgentOptions();
-/*!
- * Initialize the settings manager.
- */
-void initializeSettings() {
- storm::settings::mutableManager().setName("Storm-DyFTeE", "storm-dft");
-
- // Register all known settings modules.
- storm::settings::addModule<storm::settings::modules::GeneralSettings>();
- storm::settings::addModule<storm::settings::modules::DFTSettings>();
- storm::settings::addModule<storm::settings::modules::CoreSettings>();
- storm::settings::addModule<storm::settings::modules::DebugSettings>();
- storm::settings::addModule<storm::settings::modules::IOSettings>();
- //storm::settings::addModule<storm::settings::modules::CounterexampleGeneratorSettings>();
- //storm::settings::addModule<storm::settings::modules::CuddSettings>();
- //storm::settings::addModule<storm::settings::modules::SylvanSettings>();
- storm::settings::addModule<storm::settings::modules::GmmxxEquationSolverSettings>();
- storm::settings::addModule<storm::settings::modules::MinMaxEquationSolverSettings>();
- storm::settings::addModule<storm::settings::modules::NativeEquationSolverSettings>();
- //storm::settings::addModule<storm::settings::modules::BisimulationSettings>();
- //storm::settings::addModule<storm::settings::modules::GlpkSettings>();
- //storm::settings::addModule<storm::settings::modules::GurobiSettings>();
- //storm::settings::addModule<storm::settings::modules::TopologicalValueIterationEquationSolverSettings>();
- //storm::settings::addModule<storm::settings::modules::ParametricSettings>();
- storm::settings::addModule<storm::settings::modules::EliminationSettings>();
- storm::settings::addModule<storm::settings::modules::ResourceSettings>();
-
- // For translation into JANI via GSPN.
- storm::settings::addModule<storm::settings::modules::GSPNSettings>();
- storm::settings::addModule<storm::settings::modules::GSPNExportSettings>();
- storm::settings::addModule<storm::settings::modules::JaniExportSettings>();
-}
-
-/*!
- * Entry point for the DyFTeE backend.
- *
- * @param argc The argc argument of main().
- * @param argv The argv argument of main().
- * @return Return code, 0 if successfull, not 0 otherwise.
- */
-int main(const int argc, const char** argv) {
- try {
- storm::utility::setUp();
- storm::cli::printHeader("Storm-DyFTeE", argc, argv);
- initializeSettings();
+ storm::cli::processOptions();
- bool optionsCorrect = storm::cli::parseOptions(argc, argv);
- if (!optionsCorrect) {
- return -1;
- }
-
- storm::settings::modules::DFTSettings const& dftSettings = storm::settings::getModule<storm::settings::modules::DFTSettings>();
+ storm::settings::modules::DftIOSettings const& dftIOSettings = storm::settings::getModule<storm::settings::modules::DftIOSettings>();
+ storm::settings::modules::FaultTreeSettings const& faultTreeSettings = storm::settings::getModule<storm::settings::modules::FaultTreeSettings>();
storm::settings::modules::GeneralSettings const& generalSettings = storm::settings::getModule<storm::settings::modules::GeneralSettings>();
storm::settings::modules::IOSettings const& ioSettings = storm::settings::getModule<storm::settings::modules::IOSettings>();
- if (!dftSettings.isDftFileSet() && !dftSettings.isDftJsonFileSet()) {
+ if (!dftIOSettings.isDftFileSet() && !dftIOSettings.isDftJsonFileSet()) {
STORM_LOG_THROW(false, storm::exceptions::InvalidSettingsException, "No input model.");
}
- if (dftSettings.isExportToJson()) {
- STORM_LOG_THROW(dftSettings.isDftFileSet(), storm::exceptions::InvalidSettingsException, "No input model in Galileo format given.");
+ if (dftIOSettings.isExportToJson()) {
+ STORM_LOG_THROW(dftIOSettings.isDftFileSet(), storm::exceptions::InvalidSettingsException, "No input model in Galileo format given.");
storm::parser::DFTGalileoParser<double> parser;
- storm::storage::DFT<double> dft = parser.parseDFT(dftSettings.getDftFilename());
+ storm::storage::DFT<double> dft = parser.parseDFT(dftIOSettings.getDftFilename());
// Export to json
- storm::storage::DftJsonExporter<double>::toFile(dft, dftSettings.getExportJsonFilename());
+ storm::storage::DftJsonExporter<double>::toFile(dft, dftIOSettings.getExportJsonFilename());
storm::utility::cleanUp();
- return 0;
+ return;
}
- if (dftSettings.isTransformToGspn()) {
+ if (dftIOSettings.isTransformToGspn()) {
std::shared_ptr<storm::storage::DFT<double>> dft;
- if (dftSettings.isDftJsonFileSet()) {
+ if (dftIOSettings.isDftJsonFileSet()) {
storm::parser::DFTJsonParser<double> parser;
- dft = std::make_shared<storm::storage::DFT<double>>(parser.parseJson(dftSettings.getDftJsonFilename()));
+ dft = std::make_shared<storm::storage::DFT<double>>(parser.parseJson(dftIOSettings.getDftJsonFilename()));
} else {
storm::parser::DFTGalileoParser<double> parser(true, false);
- dft = std::make_shared<storm::storage::DFT<double>>(parser.parseDFT(dftSettings.getDftFilename()));
+ dft = std::make_shared<storm::storage::DFT<double>>(parser.parseDFT(dftIOSettings.getDftFilename()));
}
storm::transformations::dft::DftToGspnTransformator<double> gspnTransformator(*dft);
gspnTransformator.transform();
@@ -199,7 +144,7 @@ int main(const int argc, const char** argv) {
delete model;
delete gspn;
storm::utility::cleanUp();
- return 0;
+ return;
}
bool parametric = false;
@@ -208,22 +153,22 @@ int main(const int argc, const char** argv) {
#endif
#ifdef STORM_HAVE_Z3
- if (dftSettings.solveWithSMT()) {
+ if (faultTreeSettings.solveWithSMT()) {
// Solve with SMT
if (parametric) {
// analyzeWithSMT<storm::RationalFunction>(dftSettings.getDftFilename());
} else {
- analyzeWithSMT<double>(dftSettings.getDftFilename());
+ analyzeWithSMT<double>(dftIOSettings.getDftFilename());
}
storm::utility::cleanUp();
- return 0;
+ return;
}
#endif
// Set min or max
std::string optimizationDirection = "min";
- if (dftSettings.isComputeMaximalValue()) {
- STORM_LOG_THROW(!dftSettings.isComputeMinimalValue(), storm::exceptions::InvalidSettingsException, "Cannot compute minimal and maximal values at the same time.");
+ if (dftIOSettings.isComputeMaximalValue()) {
+ STORM_LOG_THROW(!dftIOSettings.isComputeMinimalValue(), storm::exceptions::InvalidSettingsException, "Cannot compute minimal and maximal values at the same time.");
optimizationDirection = "max";
}
@@ -233,19 +178,19 @@ int main(const int argc, const char** argv) {
if (ioSettings.isPropertySet()) {
properties.push_back(ioSettings.getProperty());
}
- if (dftSettings.usePropExpectedTime()) {
+ if (dftIOSettings.usePropExpectedTime()) {
properties.push_back("T" + optimizationDirection + "=? [F \"failed\"]");
}
- if (dftSettings.usePropProbability()) {
+ if (dftIOSettings.usePropProbability()) {
properties.push_back("P" + optimizationDirection + "=? [F \"failed\"]");
}
- if (dftSettings.usePropTimebound()) {
+ if (dftIOSettings.usePropTimebound()) {
std::stringstream stream;
- stream << "P" << optimizationDirection << "=? [F<=" << dftSettings.getPropTimebound() << " \"failed\"]";
+ stream << "P" << optimizationDirection << "=? [F<=" << dftIOSettings.getPropTimebound() << " \"failed\"]";
properties.push_back(stream.str());
}
- if (dftSettings.usePropTimepoints()) {
- for (double timepoint : dftSettings.getPropTimepoints()) {
+ if (dftIOSettings.usePropTimepoints()) {
+ for (double timepoint : dftIOSettings.getPropTimepoints()) {
std::stringstream stream;
stream << "P" << optimizationDirection << "=? [F<=" << timepoint << " \"failed\"]";
properties.push_back(stream.str());
@@ -258,21 +203,51 @@ int main(const int argc, const char** argv) {
// Set possible approximation error
double approximationError = 0.0;
- if (dftSettings.isApproximationErrorSet()) {
- approximationError = dftSettings.getApproximationError();
+ if (faultTreeSettings.isApproximationErrorSet()) {
+ approximationError = faultTreeSettings.getApproximationError();
}
// From this point on we are ready to carry out the actual computations.
if (parametric) {
#ifdef STORM_HAVE_CARL
- analyzeDFT<storm::RationalFunction>(properties, dftSettings.useSymmetryReduction(), dftSettings.useModularisation(), !dftSettings.isDisableDC(), approximationError);
+ analyzeDFT<storm::RationalFunction>(properties, faultTreeSettings.useSymmetryReduction(), faultTreeSettings.useModularisation(), !faultTreeSettings.isDisableDC(), approximationError);
#else
STORM_LOG_THROW(false, storm::exceptions::NotSupportedException, "Parameters are not supported in this build.");
#endif
} else {
- analyzeDFT<double>(properties, dftSettings.useSymmetryReduction(), dftSettings.useModularisation(), !dftSettings.isDisableDC(), approximationError);
+ analyzeDFT<double>(properties, faultTreeSettings.useSymmetryReduction(), faultTreeSettings.useModularisation(), !faultTreeSettings.isDisableDC(), approximationError);
}
-
+}
+
+/*!
+ * Entry point for the DyFTeE backend.
+ *
+ * @param argc The argc argument of main().
+ * @param argv The argv argument of main().
+ * @return Return code, 0 if successfull, not 0 otherwise.
+ */
+/*!
+ * Main entry point of the executable storm-pars.
+ */
+int main(const int argc, const char** argv) {
+ try {
+ storm::utility::setUp();
+ storm::cli::printHeader("Storm-dft", argc, argv);
+ storm::settings::initializeDftSettings("Storm-dft", "storm-dft");
+
+ storm::utility::Stopwatch totalTimer(true);
+ if (!storm::cli::parseOptions(argc, argv)) {
+ return -1;
+ }
+
+ processOptions();
+ //storm::pars::processOptions();
+
+ totalTimer.stop();
+ if (storm::settings::getModule<storm::settings::modules::ResourceSettings>().isPrintTimeAndMemorySet()) {
+ storm::cli::printTimeAndMemoryStatistics(totalTimer.getTimeInMilliseconds());
+ }
+
// All operations have now been performed, so we clean up everything and terminate.
storm::utility::cleanUp();
return 0;
diff --git a/src/storm-dft/builder/ExplicitDFTModelBuilder.cpp b/src/storm-dft/builder/ExplicitDFTModelBuilder.cpp
index 4a29b0652..2b74432ad 100644
--- a/src/storm-dft/builder/ExplicitDFTModelBuilder.cpp
+++ b/src/storm-dft/builder/ExplicitDFTModelBuilder.cpp
@@ -6,456 +6,824 @@
#include "storm/models/sparse/Ctmc.h"
#include "storm/utility/constants.h"
#include "storm/utility/vector.h"
+#include "storm/utility/bitoperations.h"
#include "storm/exceptions/UnexpectedException.h"
#include "storm/settings/SettingsManager.h"
-
-#include "storm-dft/settings/modules/DFTSettings.h"
+#include "storm/logic/AtomicLabelFormula.h"
+#include "storm-dft/settings/modules/FaultTreeSettings.h"
namespace storm {
namespace builder {
- template <typename ValueType>
- ExplicitDFTModelBuilder<ValueType>::ModelComponents::ModelComponents() : transitionMatrix(), stateLabeling(), markovianStates(), exitRates(), choiceLabeling() {
+ template<typename ValueType, typename StateType>
+ ExplicitDFTModelBuilder<ValueType, StateType>::ModelComponents::ModelComponents() : transitionMatrix(), stateLabeling(), markovianStates(), exitRates(), choiceLabeling() {
// Intentionally left empty.
}
-
- template <typename ValueType>
- ExplicitDFTModelBuilder<ValueType>::ExplicitDFTModelBuilder(storm::storage::DFT<ValueType> const& dft, storm::storage::DFTIndependentSymmetries const& symmetries, bool enableDC) : mDft(dft), mStates(((mDft.stateVectorSize() / 64) + 1) * 64, INITIAL_BUCKETSIZE), enableDC(enableDC) {
- // stateVectorSize is bound for size of bitvector
- mStateGenerationInfo = std::make_shared<storm::storage::DFTStateGenerationInfo>(mDft.buildStateGenerationInfo(symmetries));
+ template<typename ValueType, typename StateType>
+ ExplicitDFTModelBuilder<ValueType, StateType>::MatrixBuilder::MatrixBuilder(bool canHaveNondeterminism) : mappingOffset(0), stateRemapping(), currentRowGroup(0), currentRow(0), canHaveNondeterminism((canHaveNondeterminism)) {
+ // Create matrix builder
+ builder = storm::storage::SparseMatrixBuilder<ValueType>(0, 0, 0, false, canHaveNondeterminism, 0);
}
+ template<typename ValueType, typename StateType>
+ ExplicitDFTModelBuilder<ValueType, StateType>::LabelOptions::LabelOptions(std::vector<std::shared_ptr<const storm::logic::Formula>> properties, bool buildAllLabels) : buildFailLabel(true), buildFailSafeLabel(false), buildAllLabels(buildAllLabels) {
+ // Get necessary labels from properties
+ std::vector<std::shared_ptr<storm::logic::AtomicLabelFormula const>> atomicLabels;
+ for (auto property : properties) {
+ property->gatherAtomicLabelFormulas(atomicLabels);
+ }
+ // Set usage of necessary labels
+ for (auto atomic : atomicLabels) {
+ std::string label = atomic->getLabel();
+ std::size_t foundIndex = label.find("_fail");
+ if (foundIndex != std::string::npos) {
+ elementLabels.insert(label.substr(0, foundIndex));
+ } else if (label.compare("failed") == 0) {
+ buildFailLabel = true;
+ } else if (label.compare("failsafe") == 0) {
+ buildFailSafeLabel = true;
+ } else {
+ STORM_LOG_WARN("Label '" << label << "' not known.");
+ }
+ }
+ }
+
+ template<typename ValueType, typename StateType>
+ ExplicitDFTModelBuilder<ValueType, StateType>::ExplicitDFTModelBuilder(storm::storage::DFT<ValueType> const& dft, storm::storage::DFTIndependentSymmetries const& symmetries, bool enableDC) :
+ dft(dft),
+ stateGenerationInfo(std::make_shared<storm::storage::DFTStateGenerationInfo>(dft.buildStateGenerationInfo(symmetries))),
+ enableDC(enableDC),
+ usedHeuristic(storm::settings::getModule<storm::settings::modules::FaultTreeSettings>().getApproximationHeuristic()),
+ generator(dft, *stateGenerationInfo, enableDC, mergeFailedStates),
+ matrixBuilder(!generator.isDeterministicModel()),
+ stateStorage(((dft.stateVectorSize() / 64) + 1) * 64),
+ // TODO Matthias: make choosable
+ //explorationQueue(dft.nrElements()+1, 0, 1)
+ explorationQueue(200, 0, 0.9)
+ {
+ // Intentionally left empty.
+ // TODO Matthias: remove again
+ usedHeuristic = storm::builder::ApproximationHeuristic::DEPTH;
+
+ // Compute independent subtrees
+ if (dft.topLevelType() == storm::storage::DFTElementType::OR) {
+ // We only support this for approximation with top level element OR
+ for (auto const& child : dft.getGate(dft.getTopLevelIndex())->children()) {
+ // Consider all children of the top level gate
+ std::vector<size_t> isubdft;
+ if (child->nrParents() > 1 || child->hasOutgoingDependencies()) {
+ STORM_LOG_TRACE("child " << child->name() << "does not allow modularisation.");
+ isubdft.clear();
+ } else if (dft.isGate(child->id())) {
+ isubdft = dft.getGate(child->id())->independentSubDft(false);
+ } else {
+ STORM_LOG_ASSERT(dft.isBasicElement(child->id()), "Child is no BE.");
+ if(dft.getBasicElement(child->id())->hasIngoingDependencies()) {
+ STORM_LOG_TRACE("child " << child->name() << "does not allow modularisation.");
+ isubdft.clear();
+ } else {
+ isubdft = {child->id()};
+ }
+ }
+ if(isubdft.empty()) {
+ subtreeBEs.clear();
+ break;
+ } else {
+ // Add new independent subtree
+ std::vector<size_t> subtree;
+ for (size_t id : isubdft) {
+ if (dft.isBasicElement(id)) {
+ subtree.push_back(id);
+ }
+ }
+ subtreeBEs.push_back(subtree);
+ }
+ }
+ }
+ if (subtreeBEs.empty()) {
+ // Consider complete tree
+ std::vector<size_t> subtree;
+ for (size_t id = 0; id < dft.nrElements(); ++id) {
+ if (dft.isBasicElement(id)) {
+ subtree.push_back(id);
+ }
+ }
+ subtreeBEs.push_back(subtree);
+ }
- template <typename ValueType>
- std::shared_ptr<storm::models::sparse::Model<ValueType>> ExplicitDFTModelBuilder<ValueType>::buildModel(LabelOptions const& labelOpts) {
- // Initialize
- bool deterministicModel = false;
- size_t rowOffset = 0;
- ModelComponents modelComponents;
- std::vector<uint_fast64_t> tmpMarkovianStates;
- storm::storage::SparseMatrixBuilder<ValueType> transitionMatrixBuilder(0, 0, 0, false, !deterministicModel, 0);
-
- if(mergeFailedStates) {
- // Introduce explicit fail state
- failedIndex = newIndex;
- newIndex++;
- transitionMatrixBuilder.newRowGroup(failedIndex);
- transitionMatrixBuilder.addNextValue(failedIndex, failedIndex, storm::utility::one<ValueType>());
- STORM_LOG_TRACE("Introduce fail state with id: " << failedIndex);
- modelComponents.exitRates.push_back(storm::utility::one<ValueType>());
- tmpMarkovianStates.push_back(failedIndex);
- }
-
- // Explore state space
- DFTStatePointer state = std::make_shared<storm::storage::DFTState<ValueType>>(mDft, *mStateGenerationInfo, newIndex);
- auto exploreResult = exploreStates(state, rowOffset, transitionMatrixBuilder, tmpMarkovianStates, modelComponents.exitRates);
- initialStateIndex = exploreResult.first;
- bool deterministic = exploreResult.second;
-
- // Before ending the exploration check for pseudo states which are not initialized yet
- for (auto & pseudoStatePair : mPseudoStatesMapping) {
- if (pseudoStatePair.first == 0) {
- // Create state from pseudo state and explore
- STORM_LOG_ASSERT(mStates.contains(pseudoStatePair.second), "Pseudo state not contained.");
- STORM_LOG_ASSERT(mStates.getValue(pseudoStatePair.second) >= OFFSET_PSEUDO_STATE, "State is no pseudo state.");
- STORM_LOG_TRACE("Create pseudo state from bit vector " << pseudoStatePair.second);
- DFTStatePointer pseudoState = std::make_shared<storm::storage::DFTState<ValueType>>(pseudoStatePair.second, mDft, *mStateGenerationInfo, newIndex);
- pseudoState->construct();
- STORM_LOG_ASSERT(pseudoStatePair.second == pseudoState->status(), "Pseudo states do not coincide.");
- STORM_LOG_TRACE("Explore pseudo state " << mDft.getStateString(pseudoState) << " with id " << pseudoState->getId());
- auto exploreResult = exploreStates(pseudoState, rowOffset, transitionMatrixBuilder, tmpMarkovianStates, modelComponents.exitRates);
- deterministic &= exploreResult.second;
- STORM_LOG_ASSERT(pseudoStatePair.first == pseudoState->getId(), "Pseudo state ids do not coincide");
- STORM_LOG_ASSERT(pseudoState->getId() == exploreResult.first, "Pseudo state ids do not coincide.");
+ for (auto tree : subtreeBEs) {
+ std::stringstream stream;
+ stream << "Subtree: ";
+ for (size_t id : tree) {
+ stream << id << ", ";
}
+ STORM_LOG_TRACE(stream.str());
}
-
- // Replace pseudo states in matrix
- std::vector<uint_fast64_t> pseudoStatesVector;
- for (auto const& pseudoStatePair : mPseudoStatesMapping) {
- pseudoStatesVector.push_back(pseudoStatePair.first);
- }
- STORM_LOG_ASSERT(std::find(pseudoStatesVector.begin(), pseudoStatesVector.end(), 0) == pseudoStatesVector.end(), "Unexplored pseudo state still contained.");
- transitionMatrixBuilder.replaceColumns(pseudoStatesVector, OFFSET_PSEUDO_STATE);
-
- STORM_LOG_DEBUG("Generated " << mStates.size() + (mergeFailedStates ? 1 : 0) << " states");
- STORM_LOG_DEBUG("Model is " << (deterministic ? "deterministic" : "non-deterministic"));
-
- size_t stateSize = mStates.size() + (mergeFailedStates ? 1 : 0);
- // Build Markov Automaton
- modelComponents.markovianStates = storm::storage::BitVector(stateSize, tmpMarkovianStates);
+ }
+
+ template<typename ValueType, typename StateType>
+ void ExplicitDFTModelBuilder<ValueType, StateType>::buildModel(LabelOptions const& labelOpts, size_t iteration, double approximationThreshold) {
+ STORM_LOG_TRACE("Generating DFT state space");
+
+ if (iteration < 1) {
+ // Initialize
+ modelComponents.markovianStates = storm::storage::BitVector(INITIAL_BITVECTOR_SIZE);
+
+ if(mergeFailedStates) {
+ // Introduce explicit fail state
+ storm::generator::StateBehavior<ValueType, StateType> behavior = generator.createMergeFailedState([this] (DFTStatePointer const& state) {
+ this->failedStateId = newIndex++;
+ matrixBuilder.stateRemapping.push_back(0);
+ return this->failedStateId;
+ } );
+
+ matrixBuilder.setRemapping(failedStateId);
+ STORM_LOG_ASSERT(!behavior.empty(), "Behavior is empty.");
+ matrixBuilder.newRowGroup();
+ setMarkovian(behavior.begin()->isMarkovian());
+
+ // Now add self loop.
+ // TODO Matthias: maybe use general method.
+ STORM_LOG_ASSERT(behavior.getNumberOfChoices() == 1, "Wrong number of choices for failed state.");
+ STORM_LOG_ASSERT(behavior.begin()->size() == 1, "Wrong number of transitions for failed state.");
+ std::pair<StateType, ValueType> stateProbabilityPair = *(behavior.begin()->begin());
+ STORM_LOG_ASSERT(stateProbabilityPair.first == failedStateId, "No self loop for failed state.");
+ STORM_LOG_ASSERT(storm::utility::isOne<ValueType>(stateProbabilityPair.second), "Probability for failed state != 1.");
+ matrixBuilder.addTransition(stateProbabilityPair.first, stateProbabilityPair.second);
+ matrixBuilder.finishRow();
+ }
+
+ // Build initial state
+ this->stateStorage.initialStateIndices = generator.getInitialStates(std::bind(&ExplicitDFTModelBuilder::getOrAddStateIndex, this, std::placeholders::_1));
+ STORM_LOG_ASSERT(stateStorage.initialStateIndices.size() == 1, "Only one initial state assumed.");
+ initialStateIndex = stateStorage.initialStateIndices[0];
+ STORM_LOG_TRACE("Initial state: " << initialStateIndex);
+ // Initialize heuristic values for inital state
+ STORM_LOG_ASSERT(!statesNotExplored.at(initialStateIndex).second, "Heuristic for initial state is already initialized");
+ ExplorationHeuristicPointer heuristic = std::make_shared<ExplorationHeuristic>(initialStateIndex);
+ heuristic->markExpand();
+ statesNotExplored[initialStateIndex].second = heuristic;
+ explorationQueue.push(heuristic);
+ } else {
+ initializeNextIteration();
+ }
+
+ if (approximationThreshold > 0) {
+ switch (usedHeuristic) {
+ case storm::builder::ApproximationHeuristic::NONE:
+ // Do not change anything
+ approximationThreshold = dft.nrElements()+10;
+ break;
+ case storm::builder::ApproximationHeuristic::DEPTH:
+ approximationThreshold = iteration + 1;
+ break;
+ case storm::builder::ApproximationHeuristic::PROBABILITY:
+ case storm::builder::ApproximationHeuristic::BOUNDDIFFERENCE:
+ approximationThreshold = 10 * std::pow(2, iteration);
+ break;
+ }
+ }
+ exploreStateSpace(approximationThreshold);
+
+ size_t stateSize = stateStorage.getNumberOfStates() + (mergeFailedStates ? 1 : 0);
+ modelComponents.markovianStates.resize(stateSize);
+ modelComponents.deterministicModel = generator.isDeterministicModel();
+
+ // Fix the entries in the transition matrix according to the mapping of ids to row group indices
+ STORM_LOG_ASSERT(matrixBuilder.getRemapping(initialStateIndex) == initialStateIndex, "Initial state should not be remapped.");
+ // TODO Matthias: do not consider all rows?
+ STORM_LOG_TRACE("Remap matrix: " << matrixBuilder.stateRemapping << ", offset: " << matrixBuilder.mappingOffset);
+ matrixBuilder.remap();
+
+ STORM_LOG_TRACE("State remapping: " << matrixBuilder.stateRemapping);
+ STORM_LOG_TRACE("Markovian states: " << modelComponents.markovianStates);
+ STORM_LOG_DEBUG("Model has " << stateSize << " states");
+ STORM_LOG_DEBUG("Model is " << (generator.isDeterministicModel() ? "deterministic" : "non-deterministic"));
+
// Build transition matrix
- modelComponents.transitionMatrix = transitionMatrixBuilder.build(stateSize, stateSize);
+ modelComponents.transitionMatrix = matrixBuilder.builder.build(stateSize, stateSize);
if (stateSize <= 15) {
STORM_LOG_TRACE("Transition matrix: " << std::endl << modelComponents.transitionMatrix);
} else {
STORM_LOG_TRACE("Transition matrix: too big to print");
}
- STORM_LOG_TRACE("Exit rates: " << storm::utility::vector::toString<ValueType>(modelComponents.exitRates));
- STORM_LOG_TRACE("Markovian states: " << modelComponents.markovianStates);
-
+
+ buildLabeling(labelOpts);
+ }
+
+ template<typename ValueType, typename StateType>
+ void ExplicitDFTModelBuilder<ValueType, StateType>::initializeNextIteration() {
+ STORM_LOG_TRACE("Refining DFT state space");
+
+ // TODO Matthias: should be easier now as skipped states all are at the end of the matrix
+ // Push skipped states to explore queue
+ // TODO Matthias: remove
+ for (auto const& skippedState : skippedStates) {
+ statesNotExplored[skippedState.second.first->getId()] = skippedState.second;
+ explorationQueue.push(skippedState.second.second);
+ }
+
+ // Initialize matrix builder again
+ // TODO Matthias: avoid copy
+ std::vector<uint_fast64_t> copyRemapping = matrixBuilder.stateRemapping;
+ matrixBuilder = MatrixBuilder(!generator.isDeterministicModel());
+ matrixBuilder.stateRemapping = copyRemapping;
+ StateType nrStates = modelComponents.transitionMatrix.getRowGroupCount();
+ STORM_LOG_ASSERT(nrStates == matrixBuilder.stateRemapping.size(), "No. of states does not coincide with mapping size.");
+
+ // Start by creating a remapping from the old indices to the new indices
+ std::vector<StateType> indexRemapping = std::vector<StateType>(nrStates, 0);
+ auto iterSkipped = skippedStates.begin();
+ size_t skippedBefore = 0;
+ for (size_t i = 0; i < indexRemapping.size(); ++i) {
+ while (iterSkipped != skippedStates.end() && iterSkipped->first <= i) {
+ STORM_LOG_ASSERT(iterSkipped->first < indexRemapping.size(), "Skipped is too high.");
+ ++skippedBefore;
+ ++iterSkipped;
+ }
+ indexRemapping[i] = i - skippedBefore;
+ }
+
+ // Set remapping
+ size_t nrExpandedStates = nrStates - skippedBefore;
+ matrixBuilder.mappingOffset = nrStates;
+ STORM_LOG_TRACE("# expanded states: " << nrExpandedStates);
+ StateType skippedIndex = nrExpandedStates;
+ std::map<StateType, std::pair<DFTStatePointer, ExplorationHeuristicPointer>> skippedStatesNew;
+ for (size_t id = 0; id < matrixBuilder.stateRemapping.size(); ++id) {
+ StateType index = matrixBuilder.getRemapping(id);
+ auto itFind = skippedStates.find(index);
+ if (itFind != skippedStates.end()) {
+ // Set new mapping for skipped state
+ matrixBuilder.stateRemapping[id] = skippedIndex;
+ skippedStatesNew[skippedIndex] = itFind->second;
+ indexRemapping[index] = skippedIndex;
+ ++skippedIndex;
+ } else {
+ // Set new mapping for expanded state
+ matrixBuilder.stateRemapping[id] = indexRemapping[index];
+ }
+ }
+ STORM_LOG_TRACE("New state remapping: " << matrixBuilder.stateRemapping);
+ std::stringstream ss;
+ ss << "Index remapping:" << std::endl;
+ for (auto tmp : indexRemapping) {
+ ss << tmp << " ";
+ }
+ STORM_LOG_TRACE(ss.str());
+
+ // Remap markovian states
+ storm::storage::BitVector markovianStatesNew = storm::storage::BitVector(modelComponents.markovianStates.size(), true);
+ // Iterate over all not set bits
+ modelComponents.markovianStates.complement();
+ size_t index = modelComponents.markovianStates.getNextSetIndex(0);
+ while (index < modelComponents.markovianStates.size()) {
+ markovianStatesNew.set(indexRemapping[index], false);
+ index = modelComponents.markovianStates.getNextSetIndex(index+1);
+ }
+ STORM_LOG_ASSERT(modelComponents.markovianStates.size() - modelComponents.markovianStates.getNumberOfSetBits() == markovianStatesNew.getNumberOfSetBits(), "Remapping of markovian states is wrong.");
+ STORM_LOG_ASSERT(markovianStatesNew.size() == nrStates, "No. of states does not coincide with markovian size.");
+ modelComponents.markovianStates = markovianStatesNew;
+
+ // Build submatrix for expanded states
+ // TODO Matthias: only use row groups when necessary
+ for (StateType oldRowGroup = 0; oldRowGroup < modelComponents.transitionMatrix.getRowGroupCount(); ++oldRowGroup) {
+ if (indexRemapping[oldRowGroup] < nrExpandedStates) {
+ // State is expanded -> copy to new matrix
+ matrixBuilder.newRowGroup();
+ for (StateType oldRow = modelComponents.transitionMatrix.getRowGroupIndices()[oldRowGroup]; oldRow < modelComponents.transitionMatrix.getRowGroupIndices()[oldRowGroup+1]; ++oldRow) {
+ for (typename storm::storage::SparseMatrix<ValueType>::const_iterator itEntry = modelComponents.transitionMatrix.begin(oldRow); itEntry != modelComponents.transitionMatrix.end(oldRow); ++itEntry) {
+ auto itFind = skippedStates.find(itEntry->getColumn());
+ if (itFind != skippedStates.end()) {
+ // Set id for skipped states as we remap it later
+ matrixBuilder.addTransition(matrixBuilder.mappingOffset + itFind->second.first->getId(), itEntry->getValue());
+ } else {
+ // Set newly remapped index for expanded states
+ matrixBuilder.addTransition(indexRemapping[itEntry->getColumn()], itEntry->getValue());
+ }
+ }
+ matrixBuilder.finishRow();
+ }
+ }
+ }
+
+ skippedStates = skippedStatesNew;
+
+ STORM_LOG_ASSERT(matrixBuilder.getCurrentRowGroup() == nrExpandedStates, "Row group size does not match.");
+ skippedStates.clear();
+ }
+
+ template<typename ValueType, typename StateType>
+ void ExplicitDFTModelBuilder<ValueType, StateType>::exploreStateSpace(double approximationThreshold) {
+ size_t nrExpandedStates = 0;
+ size_t nrSkippedStates = 0;
+ // TODO Matthias: do not empty queue every time but break before
+ while (!explorationQueue.empty()) {
+ // Get the first state in the queue
+ ExplorationHeuristicPointer currentExplorationHeuristic = explorationQueue.popTop();
+ StateType currentId = currentExplorationHeuristic->getId();
+ auto itFind = statesNotExplored.find(currentId);
+ STORM_LOG_ASSERT(itFind != statesNotExplored.end(), "Id " << currentId << " not found");
+ DFTStatePointer currentState = itFind->second.first;
+ STORM_LOG_ASSERT(currentExplorationHeuristic == itFind->second.second, "Exploration heuristics do not match");
+ STORM_LOG_ASSERT(currentState->getId() == currentId, "Ids do not match");
+ // Remove it from the list of not explored states
+ statesNotExplored.erase(itFind);
+ STORM_LOG_ASSERT(stateStorage.stateToId.contains(currentState->status()), "State is not contained in state storage.");
+ STORM_LOG_ASSERT(stateStorage.stateToId.getValue(currentState->status()) == currentId, "Ids of states do not coincide.");
+
+ // Get concrete state if necessary
+ if (currentState->isPseudoState()) {
+ // Create concrete state from pseudo state
+ currentState->construct();
+ }
+ STORM_LOG_ASSERT(!currentState->isPseudoState(), "State is pseudo state.");
+
+ // Remember that the current row group was actually filled with the transitions of a different state
+ matrixBuilder.setRemapping(currentId);
+
+ matrixBuilder.newRowGroup();
+
+ // Try to explore the next state
+ generator.load(currentState);
+
+ //if (approximationThreshold > 0.0 && nrExpandedStates > approximationThreshold && !currentExplorationHeuristic->isExpand()) {
+ if (approximationThreshold > 0.0 && currentExplorationHeuristic->isSkip(approximationThreshold)) {
+ // Skip the current state
+ ++nrSkippedStates;
+ STORM_LOG_TRACE("Skip expansion of state: " << dft.getStateString(currentState));
+ setMarkovian(true);
+ // Add transition to target state with temporary value 0
+ // TODO Matthias: what to do when there is no unique target state?
+ matrixBuilder.addTransition(failedStateId, storm::utility::zero<ValueType>());
+ // Remember skipped state
+ skippedStates[matrixBuilder.getCurrentRowGroup() - 1] = std::make_pair(currentState, currentExplorationHeuristic);
+ matrixBuilder.finishRow();
+ } else {
+ // Explore the current state
+ ++nrExpandedStates;
+ storm::generator::StateBehavior<ValueType, StateType> behavior = generator.expand(std::bind(&ExplicitDFTModelBuilder::getOrAddStateIndex, this, std::placeholders::_1));
+ STORM_LOG_ASSERT(!behavior.empty(), "Behavior is empty.");
+ setMarkovian(behavior.begin()->isMarkovian());
+
+ // Now add all choices.
+ for (auto const& choice : behavior) {
+ // Add the probabilistic behavior to the matrix.
+ for (auto const& stateProbabilityPair : choice) {
+ STORM_LOG_ASSERT(!storm::utility::isZero(stateProbabilityPair.second), "Probability zero.");
+ // Set transition to state id + offset. This helps in only remapping all previously skipped states.
+ matrixBuilder.addTransition(matrixBuilder.mappingOffset + stateProbabilityPair.first, stateProbabilityPair.second);
+ // Set heuristic values for reached states
+ auto iter = statesNotExplored.find(stateProbabilityPair.first);
+ if (iter != statesNotExplored.end()) {
+ // Update heuristic values
+ DFTStatePointer state = iter->second.first;
+ if (!iter->second.second) {
+ // Initialize heuristic values
+ ExplorationHeuristicPointer heuristic = std::make_shared<ExplorationHeuristic>(stateProbabilityPair.first, *currentExplorationHeuristic, stateProbabilityPair.second, choice.getTotalMass());
+ iter->second.second = heuristic;
+ if (state->hasFailed(dft.getTopLevelIndex()) || state->isFailsafe(dft.getTopLevelIndex()) || state->nrFailableDependencies() > 0 || (state->nrFailableDependencies() == 0 && state->nrFailableBEs() == 0)) {
+ // Do not skip absorbing state or if reached by dependencies
+ iter->second.second->markExpand();
+ }
+ if (usedHeuristic == storm::builder::ApproximationHeuristic::BOUNDDIFFERENCE) {
+ // Compute bounds for heuristic now
+ if (state->isPseudoState()) {
+ // Create concrete state from pseudo state
+ state->construct();
+ }
+ STORM_LOG_ASSERT(!currentState->isPseudoState(), "State is pseudo state.");
+
+ // Initialize bounds
+ // TODO Mathias: avoid hack
+ ValueType lowerBound = getLowerBound(state);
+ ValueType upperBound = getUpperBound(state);
+ heuristic->setBounds(lowerBound, upperBound);
+ }
+
+ explorationQueue.push(heuristic);
+ } else if (!iter->second.second->isExpand()) {
+ double oldPriority = iter->second.second->getPriority();
+ if (iter->second.second->updateHeuristicValues(*currentExplorationHeuristic, stateProbabilityPair.second, choice.getTotalMass())) {
+ // Update priority queue
+ explorationQueue.update(iter->second.second, oldPriority);
+ }
+ }
+ }
+ }
+ matrixBuilder.finishRow();
+ }
+ }
+ } // end exploration
+
+ STORM_LOG_INFO("Expanded " << nrExpandedStates << " states");
+ STORM_LOG_INFO("Skipped " << nrSkippedStates << " states");
+ STORM_LOG_ASSERT(nrSkippedStates == skippedStates.size(), "Nr skipped states is wrong");
+ }
+
+ template<typename ValueType, typename StateType>
+ void ExplicitDFTModelBuilder<ValueType, StateType>::buildLabeling(LabelOptions const& labelOpts) {
// Build state labeling
- modelComponents.stateLabeling = storm::models::sparse::StateLabeling(mStates.size() + (mergeFailedStates ? 1 : 0));
- // Initial state is always first state without any failure
+ modelComponents.stateLabeling = storm::models::sparse::StateLabeling(modelComponents.transitionMatrix.getRowGroupCount());
+ // Initial state
modelComponents.stateLabeling.addLabel("init");
+ STORM_LOG_ASSERT(matrixBuilder.getRemapping(initialStateIndex) == initialStateIndex, "Initial state should not be remapped.");
modelComponents.stateLabeling.addLabelToState("init", initialStateIndex);
// Label all states corresponding to their status (failed, failsafe, failed BE)
if(labelOpts.buildFailLabel) {
modelComponents.stateLabeling.addLabel("failed");
- }
+ }
if(labelOpts.buildFailSafeLabel) {
modelComponents.stateLabeling.addLabel("failsafe");
}
-
- // Collect labels for all BE
- std::vector<std::shared_ptr<storage::DFTBE<ValueType>>> basicElements = mDft.getBasicElements();
- for (std::shared_ptr<storage::DFTBE<ValueType>> elem : basicElements) {
- if(labelOpts.beLabels.count(elem->name()) > 0) {
- modelComponents.stateLabeling.addLabel(elem->name() + "_fail");
+
+ // Collect labels for all necessary elements
+ for (size_t id = 0; id < dft.nrElements(); ++id) {
+ std::shared_ptr<storage::DFTElement<ValueType> const> element = dft.getElement(id);
+ if (labelOpts.buildAllLabels || labelOpts.elementLabels.count(element->name()) > 0) {
+ modelComponents.stateLabeling.addLabel(element->name() + "_fail");
}
}
- if(mergeFailedStates) {
- modelComponents.stateLabeling.addLabelToState("failed", failedIndex);
+ // Set labels to states
+ if (mergeFailedStates) {
+ modelComponents.stateLabeling.addLabelToState("failed", failedStateId);
}
- for (auto const& stateIdPair : mStates) {
+ for (auto const& stateIdPair : stateStorage.stateToId) {
storm::storage::BitVector state = stateIdPair.first;
- size_t stateId = stateIdPair.second;
- if (!mergeFailedStates && labelOpts.buildFailLabel && mDft.hasFailed(state, *mStateGenerationInfo)) {
+ size_t stateId = matrixBuilder.getRemapping(stateIdPair.second);
+ if (!mergeFailedStates && labelOpts.buildFailLabel && dft.hasFailed(state, *stateGenerationInfo)) {
modelComponents.stateLabeling.addLabelToState("failed", stateId);
}
- if (labelOpts.buildFailSafeLabel && mDft.isFailsafe(state, *mStateGenerationInfo)) {
+ if (labelOpts.buildFailSafeLabel && dft.isFailsafe(state, *stateGenerationInfo)) {
modelComponents.stateLabeling.addLabelToState("failsafe", stateId);
- };
- // Set fail status for each BE
- for (std::shared_ptr<storage::DFTBE<ValueType>> elem : basicElements) {
- if (labelOpts.beLabels.count(elem->name()) > 0 && storm::storage::DFTState<ValueType>::hasFailed(state, mStateGenerationInfo->getStateIndex(elem->id())) ) {
- modelComponents.stateLabeling.addLabelToState(elem->name() + "_fail", stateId);
+ }
+ // Set fail status for each necessary element
+ for (size_t id = 0; id < dft.nrElements(); ++id) {
+ std::shared_ptr<storage::DFTElement<ValueType> const> element = dft.getElement(id);
+ if ((labelOpts.buildAllLabels || labelOpts.elementLabels.count(element->name()) > 0) && storm::storage::DFTState<ValueType>::hasFailed(state, stateGenerationInfo->getStateIndex(element->id()))) {
+ modelComponents.stateLabeling.addLabelToState(element->name() + "_fail", stateId);
+ }
+ }
+ }
+
+ STORM_LOG_TRACE(modelComponents.stateLabeling);
+ }
+
+ template<typename ValueType, typename StateType>
+ std::shared_ptr<storm::models::sparse::Model<ValueType>> ExplicitDFTModelBuilder<ValueType, StateType>::getModel() {
+ STORM_LOG_ASSERT(skippedStates.size() == 0, "Concrete model has skipped states");
+ return createModel(false);
+ }
+
+ template<typename ValueType, typename StateType>
+ std::shared_ptr<storm::models::sparse::Model<ValueType>> ExplicitDFTModelBuilder<ValueType, StateType>::getModelApproximation(bool lowerBound, bool expectedTime) {
+ if (expectedTime) {
+ // TODO Matthias: handle case with no skipped states
+ changeMatrixBound(modelComponents.transitionMatrix, lowerBound);
+ return createModel(true);
+ } else {
+ // Change model for probabilities
+ // TODO Matthias: make nicer
+ storm::storage::SparseMatrix<ValueType> matrix = modelComponents.transitionMatrix;
+ storm::models::sparse::StateLabeling labeling = modelComponents.stateLabeling;
+ if (lowerBound) {
+ // Set self loop for lower bound
+ for (auto it = skippedStates.begin(); it != skippedStates.end(); ++it) {
+ auto matrixEntry = matrix.getRow(it->first, 0).begin();
+ STORM_LOG_ASSERT(matrixEntry->getColumn() == failedStateId, "Transition has wrong target state.");
+ STORM_LOG_ASSERT(!it->second.first->isPseudoState(), "State is still pseudo state.");
+ matrixEntry->setValue(storm::utility::one<ValueType>());
+ matrixEntry->setColumn(it->first);
+ }
+ } else {
+ // Make skipped states failed states for upper bound
+ storm::storage::BitVector failedStates = modelComponents.stateLabeling.getStates("failed");
+ for (auto it = skippedStates.begin(); it != skippedStates.end(); ++it) {
+ failedStates.set(it->first);
}
+ labeling.setStates("failed", failedStates);
}
+
+ std::shared_ptr<storm::models::sparse::Model<ValueType>> model;
+ if (modelComponents.deterministicModel) {
+ model = std::make_shared<storm::models::sparse::Ctmc<ValueType>>(std::move(matrix), std::move(labeling));
+ } else {
+ // Build MA
+ // Compute exit rates
+ // TODO Matthias: avoid computing multiple times
+ modelComponents.exitRates = std::vector<ValueType>(modelComponents.markovianStates.size());
+ std::vector<typename storm::storage::SparseMatrix<ValueType>::index_type> indices = matrix.getRowGroupIndices();
+ for (StateType stateIndex = 0; stateIndex < modelComponents.markovianStates.size(); ++stateIndex) {
+ if (modelComponents.markovianStates[stateIndex]) {
+ modelComponents.exitRates[stateIndex] = matrix.getRowSum(indices[stateIndex]);
+ } else {
+ modelComponents.exitRates[stateIndex] = storm::utility::zero<ValueType>();
+ }
+ }
+ STORM_LOG_TRACE("Exit rates: " << modelComponents.exitRates);
+
+ storm::storage::sparse::ModelComponents<ValueType> maComponents(std::move(matrix), std::move(labeling));
+ maComponents.rateTransitions = true;
+ maComponents.markovianStates = modelComponents.markovianStates;
+ maComponents.exitRates = modelComponents.exitRates;
+ std::shared_ptr<storm::models::sparse::MarkovAutomaton<ValueType>> ma = std::make_shared<storm::models::sparse::MarkovAutomaton<ValueType>>(std::move(maComponents));
+ if (ma->hasOnlyTrivialNondeterminism()) {
+ // Markov automaton can be converted into CTMC
+ // TODO Matthias: change components which were not moved accordingly
+ model = ma->convertToCTMC();
+ } else {
+ model = ma;
+ }
+
+ }
+
+ if (model->getNumberOfStates() <= 15) {
+ STORM_LOG_TRACE("Transition matrix: " << std::endl << model->getTransitionMatrix());
+ } else {
+ STORM_LOG_TRACE("Transition matrix: too big to print");
+ }
+ return model;
}
+ }
+ template<typename ValueType, typename StateType>
+ std::shared_ptr<storm::models::sparse::Model<ValueType>> ExplicitDFTModelBuilder<ValueType, StateType>::createModel(bool copy) {
std::shared_ptr<storm::models::sparse::Model<ValueType>> model;
- storm::storage::sparse::ModelComponents<ValueType> components(std::move(modelComponents.transitionMatrix), std::move(modelComponents.stateLabeling));
- components.exitRates = std::move(modelComponents.exitRates);
- if (deterministic) {
- components.transitionMatrix.makeRowGroupingTrivial();
- model = std::make_shared<storm::models::sparse::Ctmc<ValueType>>(std::move(components));
+
+ if (modelComponents.deterministicModel) {
+ // Build CTMC
+ if (copy) {
+ model = std::make_shared<storm::models::sparse::Ctmc<ValueType>>(modelComponents.transitionMatrix, modelComponents.stateLabeling);
+ } else {
+ model = std::make_shared<storm::models::sparse::Ctmc<ValueType>>(std::move(modelComponents.transitionMatrix), std::move(modelComponents.stateLabeling));
+ }
} else {
- components.markovianStates = std::move(modelComponents.markovianStates);
- std::shared_ptr<storm::models::sparse::MarkovAutomaton<ValueType>> ma = std::make_shared<storm::models::sparse::MarkovAutomaton<ValueType>>(std::move(components));
+ // Build MA
+ // Compute exit rates
+ // TODO Matthias: avoid computing multiple times
+ modelComponents.exitRates = std::vector<ValueType>(modelComponents.markovianStates.size());
+ std::vector<typename storm::storage::SparseMatrix<ValueType>::index_type> indices = modelComponents.transitionMatrix.getRowGroupIndices();
+ for (StateType stateIndex = 0; stateIndex < modelComponents.markovianStates.size(); ++stateIndex) {
+ if (modelComponents.markovianStates[stateIndex]) {
+ modelComponents.exitRates[stateIndex] = modelComponents.transitionMatrix.getRowSum(indices[stateIndex]);
+ } else {
+ modelComponents.exitRates[stateIndex] = storm::utility::zero<ValueType>();
+ }
+ }
+ STORM_LOG_TRACE("Exit rates: " << modelComponents.exitRates);
+
+ std::shared_ptr<storm::models::sparse::MarkovAutomaton<ValueType>> ma;
+ if (copy) {
+ storm::storage::sparse::ModelComponents<ValueType> maComponents(modelComponents.transitionMatrix, modelComponents.stateLabeling);
+ maComponents.rateTransitions = true;
+ maComponents.markovianStates = modelComponents.markovianStates;
+ maComponents.exitRates = modelComponents.exitRates;
+ ma = std::make_shared<storm::models::sparse::MarkovAutomaton<ValueType>>(std::move(maComponents));
+ } else {
+ storm::storage::sparse::ModelComponents<ValueType> maComponents(std::move(modelComponents.transitionMatrix), std::move(modelComponents.stateLabeling));
+ maComponents.rateTransitions = true;
+ maComponents.markovianStates = std::move(modelComponents.markovianStates);
+ maComponents.exitRates = std::move(modelComponents.exitRates);
+ ma = std::make_shared<storm::models::sparse::MarkovAutomaton<ValueType>>(std::move(maComponents));
+ }
if (ma->hasOnlyTrivialNondeterminism()) {
// Markov automaton can be converted into CTMC
+ // TODO Matthias: change components which were not moved accordingly
model = ma->convertToCTMC();
} else {
model = ma;
}
}
-
+
+ if (model->getNumberOfStates() <= 15) {
+ STORM_LOG_TRACE("Transition matrix: " << std::endl << model->getTransitionMatrix());
+ } else {
+ STORM_LOG_TRACE("Transition matrix: too big to print");
+ }
return model;
}
-
- template <typename ValueType>
- std::pair<uint_fast64_t, bool> ExplicitDFTModelBuilder<ValueType>::exploreStates(DFTStatePointer const& state, size_t& rowOffset, storm::storage::SparseMatrixBuilder<ValueType>& transitionMatrixBuilder, std::vector<uint_fast64_t>& markovianStates, std::vector<ValueType>& exitRates) {
- STORM_LOG_TRACE("Explore state: " << mDft.getStateString(state));
-
- auto explorePair = checkForExploration(state);
- if (!explorePair.first) {
- // State does not need any exploration
- return std::make_pair(explorePair.second, true);
- }
-
-
- // Initialization
- // TODO Matthias: set Markovian states directly as bitvector?
- std::map<uint_fast64_t, ValueType> outgoingRates;
- std::vector<std::map<uint_fast64_t, ValueType>> outgoingProbabilities;
- bool hasDependencies = state->nrFailableDependencies() > 0;
- size_t failableCount = hasDependencies ? state->nrFailableDependencies() : state->nrFailableBEs();
- size_t smallest = 0;
- ValueType exitRate = storm::utility::zero<ValueType>();
- bool deterministic = !hasDependencies;
-
- // Absorbing state
- if (mDft.hasFailed(state) || mDft.isFailsafe(state) || state->nrFailableBEs() == 0) {
- uint_fast64_t stateId = addState(state);
- STORM_LOG_ASSERT(stateId == state->getId(), "Ids do not coincide.");
-
- // Add self loop
- transitionMatrixBuilder.newRowGroup(stateId + rowOffset);
- transitionMatrixBuilder.addNextValue(stateId + rowOffset, stateId, storm::utility::one<ValueType>());
- STORM_LOG_TRACE("Added self loop for " << stateId);
- exitRates.push_back(storm::utility::one<ValueType>());
- STORM_LOG_ASSERT(exitRates.size()-1 == stateId, "No. of considered states does not match state id.");
- markovianStates.push_back(stateId);
- // No further exploration required
- return std::make_pair(stateId, true);
- }
-
- // Let BE fail
- while (smallest < failableCount) {
- STORM_LOG_ASSERT(!mDft.hasFailed(state), "Dft has failed.");
-
- // Construct new state as copy from original one
- DFTStatePointer newState = std::make_shared<storm::storage::DFTState<ValueType>>(*state);
- std::pair<std::shared_ptr<storm::storage::DFTBE<ValueType> const>, bool> nextBEPair = newState->letNextBEFail(smallest++);
- std::shared_ptr<storm::storage::DFTBE<ValueType> const>& nextBE = nextBEPair.first;
- STORM_LOG_ASSERT(nextBE, "NextBE is null.");
- STORM_LOG_ASSERT(nextBEPair.second == hasDependencies, "Failure due to dependencies does not match.");
- STORM_LOG_TRACE("With the failure of: " << nextBE->name() << " [" << nextBE->id() << "] in " << mDft.getStateString(state));
-
- // Propagate failures
- storm::storage::DFTStateSpaceGenerationQueues<ValueType> queues;
-
- for (DFTGatePointer parent : nextBE->parents()) {
- if (newState->isOperational(parent->id())) {
- queues.propagateFailure(parent);
- }
- }
- for (DFTRestrictionPointer restr : nextBE->restrictions()) {
- queues.checkRestrictionLater(restr);
- }
- while (!queues.failurePropagationDone()) {
- DFTGatePointer next = queues.nextFailurePropagation();
- next->checkFails(*newState, queues);
- newState->updateFailableDependencies(next->id());
- }
-
- while(!queues.restrictionChecksDone()) {
- DFTRestrictionPointer next = queues.nextRestrictionCheck();
- next->checkFails(*newState, queues);
- newState->updateFailableDependencies(next->id());
- }
-
- if(newState->isInvalid()) {
- continue;
- }
- bool dftFailed = newState->hasFailed(mDft.getTopLevelIndex());
-
- while (!dftFailed && !queues.failsafePropagationDone()) {
- DFTGatePointer next = queues.nextFailsafePropagation();
- next->checkFailsafe(*newState, queues);
+ template<typename ValueType, typename StateType>
+ void ExplicitDFTModelBuilder<ValueType, StateType>::changeMatrixBound(storm::storage::SparseMatrix<ValueType> & matrix, bool lowerBound) const {
+ // Set lower bound for skipped states
+ for (auto it = skippedStates.begin(); it != skippedStates.end(); ++it) {
+ auto matrixEntry = matrix.getRow(it->first, 0).begin();
+ STORM_LOG_ASSERT(matrixEntry->getColumn() == failedStateId, "Transition has wrong target state.");
+ STORM_LOG_ASSERT(!it->second.first->isPseudoState(), "State is still pseudo state.");
+
+ ExplorationHeuristicPointer heuristic = it->second.second;
+ if (storm::utility::isZero(heuristic->getUpperBound())) {
+ // Initialize bounds
+ ValueType lowerBound = getLowerBound(it->second.first);
+ ValueType upperBound = getUpperBound(it->second.first);
+ heuristic->setBounds(lowerBound, upperBound);
}
- while (!dftFailed && enableDC && !queues.dontCarePropagationDone()) {
- DFTElementPointer next = queues.nextDontCarePropagation();
- next->checkDontCareAnymore(*newState, queues);
- }
-
- // Update failable dependencies
- if (!dftFailed) {
- newState->updateFailableDependencies(nextBE->id());
- newState->updateDontCareDependencies(nextBE->id());
- }
-
- uint_fast64_t newStateId;
- if(dftFailed && mergeFailedStates) {
- newStateId = failedIndex;
+ // Change bound
+ if (lowerBound) {
+ matrixEntry->setValue(it->second.second->getLowerBound());
} else {
- // Explore new state recursively
- auto explorePair = exploreStates(newState, rowOffset, transitionMatrixBuilder, markovianStates, exitRates);
- newStateId = explorePair.first;
- deterministic &= explorePair.second;
+ matrixEntry->setValue(it->second.second->getUpperBound());
}
+ }
+ }
- // Set transitions
- if (hasDependencies) {
- // Failure is due to dependency -> add non-deterministic choice
- std::map<uint_fast64_t, ValueType> choiceProbabilities;
- std::shared_ptr<storm::storage::DFTDependency<ValueType> const> dependency = mDft.getDependency(state->getDependencyId(smallest-1));
- choiceProbabilities.insert(std::make_pair(newStateId, dependency->probability()));
- STORM_LOG_TRACE("Added transition to " << newStateId << " with probability " << dependency->probability());
-
- if (!storm::utility::isOne(dependency->probability())) {
- // Add transition to state where dependency was unsuccessful
- DFTStatePointer unsuccessfulState = std::make_shared<storm::storage::DFTState<ValueType>>(*state);
- unsuccessfulState->letDependencyBeUnsuccessful(smallest-1);
- auto explorePair = exploreStates(unsuccessfulState, rowOffset, transitionMatrixBuilder, markovianStates, exitRates);
- uint_fast64_t unsuccessfulStateId = explorePair.first;
- deterministic &= explorePair.second;
- ValueType remainingProbability = storm::utility::one<ValueType>() - dependency->probability();
- choiceProbabilities.insert(std::make_pair(unsuccessfulStateId, remainingProbability));
- STORM_LOG_TRACE("Added transition to " << unsuccessfulStateId << " with remaining probability " << remainingProbability);
- }
- outgoingProbabilities.push_back(choiceProbabilities);
- } else {
- // Set failure rate according to activation
- bool isActive = true;
- if (mDft.hasRepresentant(nextBE->id())) {
- // Active must be checked for the state we are coming from as this state is responsible for the
- // rate and not the new state we are going to
- isActive = state->isActive(mDft.getRepresentant(nextBE->id()));
+ template<typename ValueType, typename StateType>
+ ValueType ExplicitDFTModelBuilder<ValueType, StateType>::getLowerBound(DFTStatePointer const& state) const {
+ // Get the lower bound by considering the failure of all possible BEs
+ ValueType lowerBound = storm::utility::zero<ValueType>();
+ for (size_t index = 0; index < state->nrFailableBEs(); ++index) {
+ lowerBound += state->getFailableBERate(index);
+ }
+ return lowerBound;
+ }
+
+ template<typename ValueType, typename StateType>
+ ValueType ExplicitDFTModelBuilder<ValueType, StateType>::getUpperBound(DFTStatePointer const& state) const {
+ if (state->hasFailed(dft.getTopLevelIndex())) {
+ return storm::utility::zero<ValueType>();
+ }
+
+ // Get the upper bound by considering the failure of all BEs
+ ValueType upperBound = storm::utility::one<ValueType>();
+ ValueType rateSum = storm::utility::zero<ValueType>();
+
+ // Compute for each independent subtree
+ for (std::vector<size_t> const& subtree : subtreeBEs) {
+ // Get all possible rates
+ std::vector<ValueType> rates;
+ storm::storage::BitVector coldBEs(subtree.size(), false);
+ for (size_t i = 0; i < subtree.size(); ++i) {
+ size_t id = subtree[i];
+ if (state->isOperational(id)) {
+ // Get BE rate
+ ValueType rate = state->getBERate(id);
+ if (storm::utility::isZero<ValueType>(rate)) {
+ // Get active failure rate for cold BE
+ rate = dft.getBasicElement(id)->activeFailureRate();
+ if (storm::utility::isZero<ValueType>(rate)) {
+ // Ignore BE which cannot fail
+ continue;
+ }
+ // Mark BE as cold
+ coldBEs.set(i, true);
+ }
+ rates.push_back(rate);
+ rateSum += rate;
}
- ValueType rate = isActive ? nextBE->activeFailureRate() : nextBE->passiveFailureRate();
- STORM_LOG_ASSERT(!storm::utility::isZero(rate), "Rate is 0.");
- auto resultFind = outgoingRates.find(newStateId);
- if (resultFind != outgoingRates.end()) {
- // Add to existing transition
- resultFind->second += rate;
- STORM_LOG_TRACE("Updated transition to " << resultFind->first << " with " << (isActive ? "active" : "passive") << " rate " << rate << " to new rate " << resultFind->second);
- } else {
- // Insert new transition
- outgoingRates.insert(std::make_pair(newStateId, rate));
- STORM_LOG_TRACE("Added transition to " << newStateId << " with " << (isActive ? "active" : "passive") << " rate " << rate);
+ }
+
+ STORM_LOG_ASSERT(rates.size() > 0, "No rates failable");
+
+ // Sort rates
+ std::sort(rates.begin(), rates.end());
+ std::vector<size_t> rateCount(rates.size(), 0);
+ size_t lastIndex = 0;
+ for (size_t i = 0; i < rates.size(); ++i) {
+ if (rates[lastIndex] != rates[i]) {
+ lastIndex = i;
}
- exitRate += rate;
+ ++rateCount[lastIndex];
}
- } // end while failing BE
-
- // Add state
- uint_fast64_t stateId = addState(state);
- STORM_LOG_ASSERT(stateId == state->getId(), "Ids do not match.");
- STORM_LOG_ASSERT(stateId == newIndex-1, "Id does not match no. of states.");
-
- if (hasDependencies) {
- // Add all probability transitions
- STORM_LOG_ASSERT(outgoingRates.empty(), "Outgoing transitions not empty.");
- transitionMatrixBuilder.newRowGroup(stateId + rowOffset);
- for (size_t i = 0; i < outgoingProbabilities.size(); ++i, ++rowOffset) {
- STORM_LOG_ASSERT(outgoingProbabilities[i].size() == 1 || outgoingProbabilities[i].size() == 2, "No. of outgoing transitions is not valid.");
- for (auto it = outgoingProbabilities[i].begin(); it != outgoingProbabilities[i].end(); ++it)
- {
- STORM_LOG_TRACE("Set transition from " << stateId << " to " << it->first << " with probability " << it->second);
- transitionMatrixBuilder.addNextValue(stateId + rowOffset, it->first, it->second);
+ for (size_t i = 0; i < rates.size(); ++i) {
+ // Cold BEs cannot fail in the first step
+ if (!coldBEs.get(i) && rateCount[i] > 0) {
+ std::iter_swap(rates.begin() + i, rates.end() - 1);
+ // Compute AND MTTF of subtree without current rate and scale with current rate
+ upperBound += rates.back() * rateCount[i] * computeMTTFAnd(rates, rates.size() - 1);
+ // Swap back
+ // TODO try to avoid swapping back
+ std::iter_swap(rates.begin() + i, rates.end() - 1);
}
}
- rowOffset--; // One increment too many
- } else {
- // Try to merge pseudo states with their instantiation
- // TODO Matthias: improve?
- for (auto it = outgoingRates.begin(); it != outgoingRates.end(); ) {
- if (it->first >= OFFSET_PSEUDO_STATE) {
- uint_fast64_t newId = it->first - OFFSET_PSEUDO_STATE;
- STORM_LOG_ASSERT(newId < mPseudoStatesMapping.size(), "Id is not valid.");
- if (mPseudoStatesMapping[newId].first > 0) {
- // State exists already
- newId = mPseudoStatesMapping[newId].first;
- auto itFind = outgoingRates.find(newId);
- if (itFind != outgoingRates.end()) {
- // Add probability from pseudo state to instantiation
- itFind->second += it->second;
- STORM_LOG_TRACE("Merged pseudo state " << newId << " adding rate " << it->second << " to total rate of " << itFind->second);
- } else {
- // Only change id
- outgoingRates.emplace(newId, it->second);
- STORM_LOG_TRACE("Instantiated pseudo state " << newId << " with rate " << it->second);
- }
- // Remove pseudo state
- it = outgoingRates.erase(it);
- } else {
- ++it;
+ }
+
+ STORM_LOG_TRACE("Upper bound is " << (rateSum / upperBound) << " for state " << state->getId());
+ STORM_LOG_ASSERT(!storm::utility::isZero(upperBound), "Upper bound is 0");
+ STORM_LOG_ASSERT(!storm::utility::isZero(rateSum), "State is absorbing");
+ return rateSum / upperBound;
+ }
+
+ template<typename ValueType, typename StateType>
+ ValueType ExplicitDFTModelBuilder<ValueType, StateType>::computeMTTFAnd(std::vector<ValueType> const& rates, size_t size) const {
+ ValueType result = storm::utility::zero<ValueType>();
+ if (size == 0) {
+ return result;
+ }
+
+ // TODO Matthias: works only for <64 BEs!
+ // WARNING: this code produces wrong results for more than 32 BEs
+ /*for (size_t i = 1; i < 4 && i <= rates.size(); ++i) {
+ size_t permutation = smallestIntWithNBitsSet(static_cast<size_t>(i));
+ ValueType sum = storm::utility::zero<ValueType>();
+ do {
+ ValueType permResult = storm::utility::zero<ValueType>();
+ for(size_t j = 0; j < rates.size(); ++j) {
+ if(permutation & static_cast<size_t>(1 << static_cast<size_t>(j))) {
+ // WARNING: if the first bit is set, it also recognizes the 32nd bit as set
+ // TODO: fix
+ permResult += rates[j];
}
- } else {
- ++it;
}
+ permutation = nextBitPermutation(permutation);
+ STORM_LOG_ASSERT(!storm::utility::isZero(permResult), "PermResult is 0");
+ sum += storm::utility::one<ValueType>() / permResult;
+ } while(permutation < (static_cast<size_t>(1) << rates.size()) && permutation != 0);
+ if (i % 2 == 0) {
+ result -= sum;
+ } else {
+ result += sum;
}
-
- // Add all rate transitions
- STORM_LOG_ASSERT(outgoingProbabilities.empty(), "Outgoing probabilities not empty.");
- transitionMatrixBuilder.newRowGroup(state->getId() + rowOffset);
- STORM_LOG_TRACE("Exit rate for " << state->getId() << ": " << exitRate);
- for (auto it = outgoingRates.begin(); it != outgoingRates.end(); ++it)
- {
- ValueType probability = it->second / exitRate; // Transform rate to probability
- STORM_LOG_TRACE("Set transition from " << state->getId() << " to " << it->first << " with rate " << it->second);
- transitionMatrixBuilder.addNextValue(state->getId() + rowOffset, it->first, probability);
+ }*/
+
+ // Compute result with permutations of size <= 3
+ ValueType one = storm::utility::one<ValueType>();
+ for (size_t i1 = 0; i1 < size; ++i1) {
+ // + 1/a
+ ValueType sum = rates[i1];
+ result += one / sum;
+ for (size_t i2 = 0; i2 < i1; ++i2) {
+ // - 1/(a+b)
+ ValueType sum2 = sum + rates[i2];
+ result -= one / sum2;
+ for (size_t i3 = 0; i3 < i2; ++i3) {
+ // + 1/(a+b+c)
+ result += one / (sum2 + rates[i3]);
+ }
}
-
- markovianStates.push_back(state->getId());
}
-
- STORM_LOG_TRACE("Finished exploring state: " << mDft.getStateString(state));
- exitRates.push_back(exitRate);
- STORM_LOG_ASSERT(exitRates.size()-1 == state->getId(), "Id does not match no. of states.");
- return std::make_pair(state->getId(), deterministic);
+
+ STORM_LOG_ASSERT(!storm::utility::isZero(result), "UpperBound is 0");
+ return result;
}
-
- template <typename ValueType>
- std::pair<bool, uint_fast64_t> ExplicitDFTModelBuilder<ValueType>::checkForExploration(DFTStatePointer const& state) {
+
+ template<typename ValueType, typename StateType>
+ StateType ExplicitDFTModelBuilder<ValueType, StateType>::getOrAddStateIndex(DFTStatePointer const& state) {
+ StateType stateId;
bool changed = false;
- if (mStateGenerationInfo->hasSymmetries()) {
+
+ if (stateGenerationInfo->hasSymmetries()) {
// Order state by symmetry
- STORM_LOG_TRACE("Check for symmetry: " << mDft.getStateString(state));
+ STORM_LOG_TRACE("Check for symmetry: " << dft.getStateString(state));
changed = state->orderBySymmetry();
- STORM_LOG_TRACE("State " << (changed ? "changed to " : "did not change") << (changed ? mDft.getStateString(state) : ""));
- }
-
- if (mStates.contains(state->status())) {
- // State already exists
- uint_fast64_t stateId = mStates.getValue(state->status());
- STORM_LOG_TRACE("State " << mDft.getStateString(state) << " with id " << stateId << " already exists");
-
- if (changed || stateId < OFFSET_PSEUDO_STATE) {
- // State is changed or an explored "normal" state
- return std::make_pair(false, stateId);
- }
-
- stateId -= OFFSET_PSEUDO_STATE;
- STORM_LOG_ASSERT(stateId < mPseudoStatesMapping.size(), "Id not valid.");
- if (mPseudoStatesMapping[stateId].first > 0) {
- // Pseudo state already explored
- return std::make_pair(false, mPseudoStatesMapping[stateId].first);
- }
-
- STORM_LOG_ASSERT(mPseudoStatesMapping[stateId].second == state->status(), "States do not coincide.");
- STORM_LOG_TRACE("Pseudo state " << mDft.getStateString(state) << " can be explored now");
- return std::make_pair(true, stateId);
- } else {
- // State does not exists
- if (changed) {
- // Remember state for later creation
- state->setId(mPseudoStatesMapping.size() + OFFSET_PSEUDO_STATE);
- mPseudoStatesMapping.push_back(std::make_pair(0, state->status()));
- mStates.findOrAdd(state->status(), state->getId());
- STORM_LOG_TRACE("Remember state for later creation: " << mDft.getStateString(state));
- return std::make_pair(false, state->getId());
- } else {
- // State needs exploration
- return std::make_pair(true, 0);
- }
+ STORM_LOG_TRACE("State " << (changed ? "changed to " : "did not change") << (changed ? dft.getStateString(state) : ""));
}
- }
- template <typename ValueType>
- uint_fast64_t ExplicitDFTModelBuilder<ValueType>::addState(DFTStatePointer const& state) {
- uint_fast64_t stateId;
- // TODO remove
- bool changed = state->orderBySymmetry();
- STORM_LOG_ASSERT(!changed, "State to add has changed by applying symmetry.");
-
- // Check if state already exists
- if (mStates.contains(state->status())) {
+ if (stateStorage.stateToId.contains(state->status())) {
// State already exists
- stateId = mStates.getValue(state->status());
- STORM_LOG_TRACE("State " << mDft.getStateString(state) << " with id " << stateId << " already exists");
-
- // Check if possible pseudo state can be created now
- STORM_LOG_ASSERT(stateId >= OFFSET_PSEUDO_STATE, "State is no pseudo state.");
- stateId -= OFFSET_PSEUDO_STATE;
- STORM_LOG_ASSERT(stateId < mPseudoStatesMapping.size(), "Pseudo state not known.");
- if (mPseudoStatesMapping[stateId].first == 0) {
- // Create pseudo state now
- STORM_LOG_ASSERT(mPseudoStatesMapping[stateId].second == state->status(), "Pseudo states do not coincide.");
- state->setId(newIndex++);
- mPseudoStatesMapping[stateId].first = state->getId();
- stateId = state->getId();
- mStates.setOrAdd(state->status(), stateId);
- STORM_LOG_TRACE("Now create state " << mDft.getStateString(state) << " with id " << stateId);
- return stateId;
- } else {
- STORM_LOG_ASSERT(false, "Pseudo state already created.");
- return 0;
+ stateId = stateStorage.stateToId.getValue(state->status());
+ STORM_LOG_TRACE("State " << dft.getStateString(state) << " with id " << stateId << " already exists");
+ if (!changed) {
+ // Check if state is pseudo state
+ // If state is explored already the possible pseudo state was already constructed
+ auto iter = statesNotExplored.find(stateId);
+ if (iter != statesNotExplored.end() && iter->second.first->isPseudoState()) {
+ // Create pseudo state now
+ STORM_LOG_ASSERT(iter->second.first->getId() == stateId, "Ids do not match.");
+ STORM_LOG_ASSERT(iter->second.first->status() == state->status(), "Pseudo states do not coincide.");
+ state->setId(stateId);
+ // Update mapping to map to concrete state now
+ // TODO Matthias: just change pointer?
+ statesNotExplored[stateId] = std::make_pair(state, iter->second.second);
+ // We do not push the new state on the exploration queue as the pseudo state was already pushed
+ STORM_LOG_TRACE("Created pseudo state " << dft.getStateString(state));
+ }
}
} else {
+ // State does not exist yet
+ STORM_LOG_ASSERT(state->isPseudoState() == changed, "State type (pseudo/concrete) wrong.");
// Create new state
state->setId(newIndex++);
- stateId = mStates.findOrAdd(state->status(), state->getId());
- STORM_LOG_TRACE("New state: " << mDft.getStateString(state));
- return stateId;
+ stateId = stateStorage.stateToId.findOrAdd(state->status(), state->getId());
+ STORM_LOG_ASSERT(stateId == state->getId(), "Ids do not match.");
+ // Insert state as not yet explored
+ ExplorationHeuristicPointer nullHeuristic;
+ statesNotExplored[stateId] = std::make_pair(state, nullHeuristic);
+ // Reserve one slot for the new state in the remapping
+ matrixBuilder.stateRemapping.push_back(0);
+ STORM_LOG_TRACE("New " << (state->isPseudoState() ? "pseudo" : "concrete") << " state: " << dft.getStateString(state));
+ }
+ return stateId;
+ }
+
+ template<typename ValueType, typename StateType>
+ void ExplicitDFTModelBuilder<ValueType, StateType>::setMarkovian(bool markovian) {
+ if (matrixBuilder.getCurrentRowGroup() > modelComponents.markovianStates.size()) {
+ // Resize BitVector
+ modelComponents.markovianStates.resize(modelComponents.markovianStates.size() + INITIAL_BITVECTOR_SIZE);
+ }
+ modelComponents.markovianStates.set(matrixBuilder.getCurrentRowGroup() - 1, markovian);
+ }
+
+ template<typename ValueType, typename StateType>
+ void ExplicitDFTModelBuilder<ValueType, StateType>::printNotExplored() const {
+ std::cout << "states not explored:" << std::endl;
+ for (auto it : statesNotExplored) {
+ std::cout << it.first << " -> " << dft.getStateString(it.second.first) << std::endl;
}
}
diff --git a/src/storm-dft/builder/ExplicitDFTModelBuilder.h b/src/storm-dft/builder/ExplicitDFTModelBuilder.h
index 2913a78fa..b96dea410 100644
--- a/src/storm-dft/builder/ExplicitDFTModelBuilder.h
+++ b/src/storm-dft/builder/ExplicitDFTModelBuilder.h
@@ -1,40 +1,42 @@
-#pragma once
+#pragma once
#include <boost/container/flat_set.hpp>
#include <boost/optional/optional.hpp>
#include <stack>
#include <unordered_set>
-
+#include <limits>
#include "storm/models/sparse/StateLabeling.h"
#include "storm/models/sparse/ChoiceLabeling.h"
#include "storm/models/sparse/StandardRewardModel.h"
#include "storm/models/sparse/Model.h"
#include "storm/storage/SparseMatrix.h"
-#include "storm/storage/BitVectorHashMap.h"
+#include "storm/storage/sparse/StateStorage.h"
+#include "storm-dft/builder/DftExplorationHeuristic.h"
+#include "storm-dft/generator/DftNextStateGenerator.h"
#include "storm-dft/storage/dft/DFT.h"
#include "storm-dft/storage/dft/SymmetricUnits.h"
-
-
-
-
+#include "storm-dft/storage/BucketPriorityQueue.h"
namespace storm {
namespace builder {
- template<typename ValueType>
+ /*!
+ * Build a Markov chain from DFT.
+ */
+ template<typename ValueType, typename StateType = uint32_t>
class ExplicitDFTModelBuilder {
- using DFTElementPointer = std::shared_ptr<storm::storage::DFTElement<ValueType>>;
- using DFTElementCPointer = std::shared_ptr<storm::storage::DFTElement<ValueType> const>;
- using DFTGatePointer = std::shared_ptr<storm::storage::DFTGate<ValueType>>;
using DFTStatePointer = std::shared_ptr<storm::storage::DFTState<ValueType>>;
- using DFTRestrictionPointer = std::shared_ptr<storm::storage::DFTRestriction<ValueType>>;
+ // TODO Matthias: make choosable
+ using ExplorationHeuristic = DFTExplorationHeuristicDepth<ValueType>;
+ using ExplorationHeuristicPointer = std::shared_ptr<ExplorationHeuristic>;
// A structure holding the individual components of a model.
struct ModelComponents {
+ // Constructor
ModelComponents();
// The transition matrix.
@@ -51,52 +53,310 @@ namespace storm {
// A vector that stores a labeling for each choice.
boost::optional<storm::models::sparse::ChoiceLabeling> choiceLabeling;
+
+ // A flag indicating if the model is deterministic.
+ bool deterministicModel;
+ };
+
+ // A class holding the information for building the transition matrix.
+ class MatrixBuilder {
+ public:
+ // Constructor
+ MatrixBuilder(bool canHaveNondeterminism);
+
+ /*!
+ * Set a mapping from a state id to the index in the matrix.
+ *
+ * @param id Id of the state.
+ */
+ void setRemapping(StateType id) {
+ STORM_LOG_ASSERT(id < stateRemapping.size(), "Invalid index for remapping.");
+ stateRemapping[id] = currentRowGroup;
+ }
+
+ /*!
+ * Create a new row group if the model is nondeterministic.
+ */
+ void newRowGroup() {
+ if (canHaveNondeterminism) {
+ builder.newRowGroup(currentRow);
+ }
+ ++currentRowGroup;
+ }
+
+ /*!
+ * Add a transition from the current row.
+ *
+ * @param index Target index
+ * @param value Value of transition
+ */
+ void addTransition(StateType index, ValueType value) {
+ builder.addNextValue(currentRow, index, value);
+ }
+
+ /*!
+ * Finish the current row.
+ */
+ void finishRow() {
+ ++currentRow;
+ }
+
+ /*!
+ * Remap the columns in the matrix.
+ */
+ void remap() {
+ builder.replaceColumns(stateRemapping, mappingOffset);
+ }
+
+ /*!
+ * Get the current row group.
+ *
+ * @return The current row group.
+ */
+ StateType getCurrentRowGroup() {
+ return currentRowGroup;
+ }
+
+ /*!
+ * Get the remapped state for the given id.
+ *
+ * @param id State.
+ *
+ * @return Remapped index.
+ */
+ StateType getRemapping(StateType id) {
+ STORM_LOG_ASSERT(id < stateRemapping.size(), "Invalid index for remapping.");
+ return stateRemapping[id];
+ }
+
+ // Matrix builder.
+ storm::storage::SparseMatrixBuilder<ValueType> builder;
+
+ // Offset to distinguish states which will not be remapped anymore and those which will.
+ size_t mappingOffset;
+
+ // A mapping from state ids to the row group indices in which they actually reside.
+ // TODO Matthias: avoid hack with fixed int type
+ std::vector<uint_fast64_t> stateRemapping;
+
+ private:
+
+ // Index of the current row group.
+ StateType currentRowGroup;
+
+ // Index of the current row.
+ StateType currentRow;
+
+ // Flag indicating if row groups are needed.
+ bool canHaveNondeterminism;
};
-
- const size_t INITIAL_BUCKETSIZE = 20000;
- const uint_fast64_t OFFSET_PSEUDO_STATE = UINT_FAST64_MAX / 2;
-
- storm::storage::DFT<ValueType> const& mDft;
- std::shared_ptr<storm::storage::DFTStateGenerationInfo> mStateGenerationInfo;
- storm::storage::BitVectorHashMap<uint_fast64_t> mStates;
- std::vector<std::pair<uint_fast64_t, storm::storage::BitVector>> mPseudoStatesMapping; // vector of (id to concrete state, bitvector)
- size_t newIndex = 0;
- bool mergeFailedStates = false;
- bool enableDC = true;
- size_t failedIndex = 0;
- size_t initialStateIndex = 0;
public:
+ // A structure holding the labeling options.
struct LabelOptions {
- bool buildFailLabel = true;
- bool buildFailSafeLabel = false;
- std::set<std::string> beLabels = {};
+ // Constructor
+ LabelOptions(std::vector<std::shared_ptr<storm::logic::Formula const>> properties, bool buildAllLabels = false);
+
+ // Flag indicating if the general fail label should be included.
+ bool buildFailLabel;
+
+ // Flag indicating if the general failsafe label should be included.
+ bool buildFailSafeLabel;
+
+ // Flag indicating if all possible labels should be included.
+ bool buildAllLabels;
+
+ // Set of element names whose fail label to include.
+ std::set<std::string> elementLabels;
};
-
+
+ /*!
+ * Constructor.
+ *
+ * @param dft DFT.
+ * @param symmetries Symmetries in the dft.
+ * @param enableDC Flag indicating if dont care propagation should be used.
+ */
ExplicitDFTModelBuilder(storm::storage::DFT<ValueType> const& dft, storm::storage::DFTIndependentSymmetries const& symmetries, bool enableDC);
- std::shared_ptr<storm::models::sparse::Model<ValueType>> buildModel(LabelOptions const& labelOpts);
+ /*!
+ * Build model from DFT.
+ *
+ * @param labelOpts Options for labeling.
+ * @param iteration Current number of iteration.
+ * @param approximationThreshold Threshold determining when to skip exploring states.
+ */
+ void buildModel(LabelOptions const& labelOpts, size_t iteration, double approximationThreshold = 0.0);
+
+ /*!
+ * Get the built model.
+ *
+ * @return The model built from the DFT.
+ */
+ std::shared_ptr<storm::models::sparse::Model<ValueType>> getModel();
+
+ /*!
+ * Get the built approximation model for either the lower or upper bound.
+ *
+ * @param lowerBound If true, the lower bound model is returned, else the upper bound model
+ * @param expectedTime If true, the bounds for expected time are computed, else the bounds for probabilities.
+ *
+ * @return The model built from the DFT.
+ */
+ std::shared_ptr<storm::models::sparse::Model<ValueType>> getModelApproximation(bool lowerBound, bool expectedTime);
private:
- std::pair<uint_fast64_t, bool> exploreStates(DFTStatePointer const& state, size_t& rowOffset, storm::storage::SparseMatrixBuilder<ValueType>& transitionMatrixBuilder, std::vector<uint_fast64_t>& markovianStates, std::vector<ValueType>& exitRates);
-
+
/*!
- * Adds a state to the explored states and handles pseudo states.
+ * Explore state space of DFT.
+ *
+ * @param approximationThreshold Threshold to determine when to skip states.
+ */
+ void exploreStateSpace(double approximationThreshold);
+
+ /*!
+ * Initialize the matrix for a refinement iteration.
+ */
+ void initializeNextIteration();
+
+ /*!
+ * Build the labeling.
+ *
+ * @param labelOpts Options for labeling.
+ */
+ void buildLabeling(LabelOptions const& labelOpts);
+
+ /*!
+ * Add a state to the explored states (if not already there). It also handles pseudo states.
*
* @param state The state to add.
- * @return Id of added state.
+ *
+ * @return Id of state.
+ */
+ StateType getOrAddStateIndex(DFTStatePointer const& state);
+
+ /*!
+ * Set markovian flag for the current state.
+ *
+ * @param markovian Flag indicating if the state is markovian.
+ */
+ void setMarkovian(bool markovian);
+
+ /**
+ * Change matrix to reflect the lower or upper approximation bound.
+ *
+ * @param matrix Matrix to change. The change are reflected here.
+ * @param lowerBound Flag indicating if the lower bound should be used. Otherwise the upper bound is used.
*/
- uint_fast64_t addState(DFTStatePointer const& state);
-
+ void changeMatrixBound(storm::storage::SparseMatrix<ValueType> & matrix, bool lowerBound) const;
+
/*!
- * Check if state needs an exploration and remember pseudo states for later creation.
+ * Get lower bound approximation for state.
+ *
+ * @param state The state.
+ *
+ * @return Lower bound approximation.
+ */
+ ValueType getLowerBound(DFTStatePointer const& state) const;
+
+ /*!
+ * Get upper bound approximation for state.
+ *
+ * @param state The state.
+ *
+ * @return Upper bound approximation.
+ */
+ ValueType getUpperBound(DFTStatePointer const& state) const;
+
+ /*!
+ * Compute the MTTF of an AND gate via a closed formula.
+ * The used formula is 1/( 1/a + 1/b + 1/c + ... - 1/(a+b) - 1/(a+c) - ... + 1/(a+b+c) + ... - ...)
+ *
+ * @param rates List of rates of children of AND.
+ * @param size Only indices < size are considered in the vector.
+ * @return MTTF.
+ */
+ ValueType computeMTTFAnd(std::vector<ValueType> const& rates, size_t size) const;
+
+ /*!
+ * Compares the priority of two states.
+ *
+ * @param idA Id of first state
+ * @param idB Id of second state
*
- * @param state State which might need exploration.
- * @return Pair of flag indicating whether the state needs exploration now and the state id if the state already
- * exists.
+ * @return True if the priority of the first state is greater then the priority of the second one.
*/
- std::pair<bool, uint_fast64_t> checkForExploration(DFTStatePointer const& state);
+ bool isPriorityGreater(StateType idA, StateType idB) const;
+ void printNotExplored() const;
+
+ /*!
+ * Create the model model from the model components.
+ *
+ * @param copy If true, all elements of the model component are copied (used for approximation). If false
+ * they are moved to reduce the memory overhead.
+ *
+ * @return The model built from the model components.
+ */
+ std::shared_ptr<storm::models::sparse::Model<ValueType>> createModel(bool copy);
+
+ // Initial size of the bitvector.
+ const size_t INITIAL_BITVECTOR_SIZE = 20000;
+ // Offset used for pseudo states.
+ const StateType OFFSET_PSEUDO_STATE = std::numeric_limits<StateType>::max() / 2;
+
+ // Dft
+ storm::storage::DFT<ValueType> const& dft;
+
+ // General information for state generation
+ // TODO Matthias: use const reference
+ std::shared_ptr<storm::storage::DFTStateGenerationInfo> stateGenerationInfo;
+
+ // Flag indication if dont care propagation should be used.
+ bool enableDC = true;
+
+ //TODO Matthias: make changeable
+ const bool mergeFailedStates = true;
+
+ // Heuristic used for approximation
+ storm::builder::ApproximationHeuristic usedHeuristic;
+
+ // Current id for new state
+ size_t newIndex = 0;
+
+ // Id of failed state
+ size_t failedStateId = 0;
+
+ // Id of initial state
+ size_t initialStateIndex = 0;
+
+ // Next state generator for exploring the state space
+ storm::generator::DftNextStateGenerator<ValueType, StateType> generator;
+
+ // Structure for the components of the model.
+ ModelComponents modelComponents;
+
+ // Structure for the transition matrix builder.
+ MatrixBuilder matrixBuilder;
+
+ // Internal information about the states that were explored.
+ storm::storage::sparse::StateStorage<StateType> stateStorage;
+
+ // A priority queue of states that still need to be explored.
+ storm::storage::BucketPriorityQueue<ValueType> explorationQueue;
+
+ // A mapping of not yet explored states from the id to the tuple (state object, heuristic values).
+ std::map<StateType, std::pair<DFTStatePointer, ExplorationHeuristicPointer>> statesNotExplored;
+
+ // Holds all skipped states which were not yet expanded. More concretely it is a mapping from matrix indices
+ // to the corresponding skipped states.
+ // Notice that we need an ordered map here to easily iterate in increasing order over state ids.
+ // TODO remove again
+ std::map<StateType, std::pair<DFTStatePointer, ExplorationHeuristicPointer>> skippedStates;
+
+ // List of independent subtrees and the BEs contained in them.
+ std::vector<std::vector<size_t>> subtreeBEs;
};
+
}
}
diff --git a/src/storm-dft/builder/ExplicitDFTModelBuilderApprox.cpp b/src/storm-dft/builder/ExplicitDFTModelBuilderApprox.cpp
deleted file mode 100644
index 0c7d69628..000000000
--- a/src/storm-dft/builder/ExplicitDFTModelBuilderApprox.cpp
+++ /dev/null
@@ -1,841 +0,0 @@
-#include "ExplicitDFTModelBuilderApprox.h"
-
-#include <map>
-
-#include "storm/models/sparse/MarkovAutomaton.h"
-#include "storm/models/sparse/Ctmc.h"
-#include "storm/utility/constants.h"
-#include "storm/utility/vector.h"
-#include "storm/utility/bitoperations.h"
-#include "storm/exceptions/UnexpectedException.h"
-#include "storm/settings/SettingsManager.h"
-#include "storm/logic/AtomicLabelFormula.h"
-#include "storm-dft/settings/modules/DFTSettings.h"
-
-
-namespace storm {
- namespace builder {
-
- template<typename ValueType, typename StateType>
- ExplicitDFTModelBuilderApprox<ValueType, StateType>::ModelComponents::ModelComponents() : transitionMatrix(), stateLabeling(), markovianStates(), exitRates(), choiceLabeling() {
- // Intentionally left empty.
- }
-
- template<typename ValueType, typename StateType>
- ExplicitDFTModelBuilderApprox<ValueType, StateType>::MatrixBuilder::MatrixBuilder(bool canHaveNondeterminism) : mappingOffset(0), stateRemapping(), currentRowGroup(0), currentRow(0), canHaveNondeterminism((canHaveNondeterminism)) {
- // Create matrix builder
- builder = storm::storage::SparseMatrixBuilder<ValueType>(0, 0, 0, false, canHaveNondeterminism, 0);
- }
-
- template<typename ValueType, typename StateType>
- ExplicitDFTModelBuilderApprox<ValueType, StateType>::LabelOptions::LabelOptions(std::vector<std::shared_ptr<const storm::logic::Formula>> properties, bool buildAllLabels) : buildFailLabel(true), buildFailSafeLabel(false), buildAllLabels(buildAllLabels) {
- // Get necessary labels from properties
- std::vector<std::shared_ptr<storm::logic::AtomicLabelFormula const>> atomicLabels;
- for (auto property : properties) {
- property->gatherAtomicLabelFormulas(atomicLabels);
- }
- // Set usage of necessary labels
- for (auto atomic : atomicLabels) {
- std::string label = atomic->getLabel();
- std::size_t foundIndex = label.find("_fail");
- if (foundIndex != std::string::npos) {
- elementLabels.insert(label.substr(0, foundIndex));
- } else if (label.compare("failed") == 0) {
- buildFailLabel = true;
- } else if (label.compare("failsafe") == 0) {
- buildFailSafeLabel = true;
- } else {
- STORM_LOG_WARN("Label '" << label << "' not known.");
- }
- }
- }
-
- template<typename ValueType, typename StateType>
- ExplicitDFTModelBuilderApprox<ValueType, StateType>::ExplicitDFTModelBuilderApprox(storm::storage::DFT<ValueType> const& dft, storm::storage::DFTIndependentSymmetries const& symmetries, bool enableDC) :
- dft(dft),
- stateGenerationInfo(std::make_shared<storm::storage::DFTStateGenerationInfo>(dft.buildStateGenerationInfo(symmetries))),
- enableDC(enableDC),
- usedHeuristic(storm::settings::getModule<storm::settings::modules::DFTSettings>().getApproximationHeuristic()),
- generator(dft, *stateGenerationInfo, enableDC, mergeFailedStates),
- matrixBuilder(!generator.isDeterministicModel()),
- stateStorage(((dft.stateVectorSize() / 64) + 1) * 64),
- // TODO Matthias: make choosable
- //explorationQueue(dft.nrElements()+1, 0, 1)
- explorationQueue(200, 0, 0.9)
- {
- // Intentionally left empty.
- // TODO Matthias: remove again
- usedHeuristic = storm::builder::ApproximationHeuristic::DEPTH;
-
- // Compute independent subtrees
- if (dft.topLevelType() == storm::storage::DFTElementType::OR) {
- // We only support this for approximation with top level element OR
- for (auto const& child : dft.getGate(dft.getTopLevelIndex())->children()) {
- // Consider all children of the top level gate
- std::vector<size_t> isubdft;
- if (child->nrParents() > 1 || child->hasOutgoingDependencies()) {
- STORM_LOG_TRACE("child " << child->name() << "does not allow modularisation.");
- isubdft.clear();
- } else if (dft.isGate(child->id())) {
- isubdft = dft.getGate(child->id())->independentSubDft(false);
- } else {
- STORM_LOG_ASSERT(dft.isBasicElement(child->id()), "Child is no BE.");
- if(dft.getBasicElement(child->id())->hasIngoingDependencies()) {
- STORM_LOG_TRACE("child " << child->name() << "does not allow modularisation.");
- isubdft.clear();
- } else {
- isubdft = {child->id()};
- }
- }
- if(isubdft.empty()) {
- subtreeBEs.clear();
- break;
- } else {
- // Add new independent subtree
- std::vector<size_t> subtree;
- for (size_t id : isubdft) {
- if (dft.isBasicElement(id)) {
- subtree.push_back(id);
- }
- }
- subtreeBEs.push_back(subtree);
- }
- }
- }
- if (subtreeBEs.empty()) {
- // Consider complete tree
- std::vector<size_t> subtree;
- for (size_t id = 0; id < dft.nrElements(); ++id) {
- if (dft.isBasicElement(id)) {
- subtree.push_back(id);
- }
- }
- subtreeBEs.push_back(subtree);
- }
-
- for (auto tree : subtreeBEs) {
- std::stringstream stream;
- stream << "Subtree: ";
- for (size_t id : tree) {
- stream << id << ", ";
- }
- STORM_LOG_TRACE(stream.str());
- }
- }
-
- template<typename ValueType, typename StateType>
- void ExplicitDFTModelBuilderApprox<ValueType, StateType>::buildModel(LabelOptions const& labelOpts, size_t iteration, double approximationThreshold) {
- STORM_LOG_TRACE("Generating DFT state space");
-
- if (iteration < 1) {
- // Initialize
- modelComponents.markovianStates = storm::storage::BitVector(INITIAL_BITVECTOR_SIZE);
-
- if(mergeFailedStates) {
- // Introduce explicit fail state
- storm::generator::StateBehavior<ValueType, StateType> behavior = generator.createMergeFailedState([this] (DFTStatePointer const& state) {
- this->failedStateId = newIndex++;
- matrixBuilder.stateRemapping.push_back(0);
- return this->failedStateId;
- } );
-
- matrixBuilder.setRemapping(failedStateId);
- STORM_LOG_ASSERT(!behavior.empty(), "Behavior is empty.");
- matrixBuilder.newRowGroup();
- setMarkovian(behavior.begin()->isMarkovian());
-
- // Now add self loop.
- // TODO Matthias: maybe use general method.
- STORM_LOG_ASSERT(behavior.getNumberOfChoices() == 1, "Wrong number of choices for failed state.");
- STORM_LOG_ASSERT(behavior.begin()->size() == 1, "Wrong number of transitions for failed state.");
- std::pair<StateType, ValueType> stateProbabilityPair = *(behavior.begin()->begin());
- STORM_LOG_ASSERT(stateProbabilityPair.first == failedStateId, "No self loop for failed state.");
- STORM_LOG_ASSERT(storm::utility::isOne<ValueType>(stateProbabilityPair.second), "Probability for failed state != 1.");
- matrixBuilder.addTransition(stateProbabilityPair.first, stateProbabilityPair.second);
- matrixBuilder.finishRow();
- }
-
- // Build initial state
- this->stateStorage.initialStateIndices = generator.getInitialStates(std::bind(&ExplicitDFTModelBuilderApprox::getOrAddStateIndex, this, std::placeholders::_1));
- STORM_LOG_ASSERT(stateStorage.initialStateIndices.size() == 1, "Only one initial state assumed.");
- initialStateIndex = stateStorage.initialStateIndices[0];
- STORM_LOG_TRACE("Initial state: " << initialStateIndex);
- // Initialize heuristic values for inital state
- STORM_LOG_ASSERT(!statesNotExplored.at(initialStateIndex).second, "Heuristic for initial state is already initialized");
- ExplorationHeuristicPointer heuristic = std::make_shared<ExplorationHeuristic>(initialStateIndex);
- heuristic->markExpand();
- statesNotExplored[initialStateIndex].second = heuristic;
- explorationQueue.push(heuristic);
- } else {
- initializeNextIteration();
- }
-
- if (approximationThreshold > 0) {
- switch (usedHeuristic) {
- case storm::builder::ApproximationHeuristic::NONE:
- // Do not change anything
- approximationThreshold = dft.nrElements()+10;
- break;
- case storm::builder::ApproximationHeuristic::DEPTH:
- approximationThreshold = iteration + 1;
- break;
- case storm::builder::ApproximationHeuristic::PROBABILITY:
- case storm::builder::ApproximationHeuristic::BOUNDDIFFERENCE:
- approximationThreshold = 10 * std::pow(2, iteration);
- break;
- }
- }
- exploreStateSpace(approximationThreshold);
-
- size_t stateSize = stateStorage.getNumberOfStates() + (mergeFailedStates ? 1 : 0);
- modelComponents.markovianStates.resize(stateSize);
- modelComponents.deterministicModel = generator.isDeterministicModel();
-
- // Fix the entries in the transition matrix according to the mapping of ids to row group indices
- STORM_LOG_ASSERT(matrixBuilder.getRemapping(initialStateIndex) == initialStateIndex, "Initial state should not be remapped.");
- // TODO Matthias: do not consider all rows?
- STORM_LOG_TRACE("Remap matrix: " << matrixBuilder.stateRemapping << ", offset: " << matrixBuilder.mappingOffset);
- matrixBuilder.remap();
-
- STORM_LOG_TRACE("State remapping: " << matrixBuilder.stateRemapping);
- STORM_LOG_TRACE("Markovian states: " << modelComponents.markovianStates);
- STORM_LOG_DEBUG("Model has " << stateSize << " states");
- STORM_LOG_DEBUG("Model is " << (generator.isDeterministicModel() ? "deterministic" : "non-deterministic"));
-
- // Build transition matrix
- modelComponents.transitionMatrix = matrixBuilder.builder.build(stateSize, stateSize);
- if (stateSize <= 15) {
- STORM_LOG_TRACE("Transition matrix: " << std::endl << modelComponents.transitionMatrix);
- } else {
- STORM_LOG_TRACE("Transition matrix: too big to print");
- }
-
- buildLabeling(labelOpts);
- }
-
- template<typename ValueType, typename StateType>
- void ExplicitDFTModelBuilderApprox<ValueType, StateType>::initializeNextIteration() {
- STORM_LOG_TRACE("Refining DFT state space");
-
- // TODO Matthias: should be easier now as skipped states all are at the end of the matrix
- // Push skipped states to explore queue
- // TODO Matthias: remove
- for (auto const& skippedState : skippedStates) {
- statesNotExplored[skippedState.second.first->getId()] = skippedState.second;
- explorationQueue.push(skippedState.second.second);
- }
-
- // Initialize matrix builder again
- // TODO Matthias: avoid copy
- std::vector<uint_fast64_t> copyRemapping = matrixBuilder.stateRemapping;
- matrixBuilder = MatrixBuilder(!generator.isDeterministicModel());
- matrixBuilder.stateRemapping = copyRemapping;
- StateType nrStates = modelComponents.transitionMatrix.getRowGroupCount();
- STORM_LOG_ASSERT(nrStates == matrixBuilder.stateRemapping.size(), "No. of states does not coincide with mapping size.");
-
- // Start by creating a remapping from the old indices to the new indices
- std::vector<StateType> indexRemapping = std::vector<StateType>(nrStates, 0);
- auto iterSkipped = skippedStates.begin();
- size_t skippedBefore = 0;
- for (size_t i = 0; i < indexRemapping.size(); ++i) {
- while (iterSkipped != skippedStates.end() && iterSkipped->first <= i) {
- STORM_LOG_ASSERT(iterSkipped->first < indexRemapping.size(), "Skipped is too high.");
- ++skippedBefore;
- ++iterSkipped;
- }
- indexRemapping[i] = i - skippedBefore;
- }
-
- // Set remapping
- size_t nrExpandedStates = nrStates - skippedBefore;
- matrixBuilder.mappingOffset = nrStates;
- STORM_LOG_TRACE("# expanded states: " << nrExpandedStates);
- StateType skippedIndex = nrExpandedStates;
- std::map<StateType, std::pair<DFTStatePointer, ExplorationHeuristicPointer>> skippedStatesNew;
- for (size_t id = 0; id < matrixBuilder.stateRemapping.size(); ++id) {
- StateType index = matrixBuilder.getRemapping(id);
- auto itFind = skippedStates.find(index);
- if (itFind != skippedStates.end()) {
- // Set new mapping for skipped state
- matrixBuilder.stateRemapping[id] = skippedIndex;
- skippedStatesNew[skippedIndex] = itFind->second;
- indexRemapping[index] = skippedIndex;
- ++skippedIndex;
- } else {
- // Set new mapping for expanded state
- matrixBuilder.stateRemapping[id] = indexRemapping[index];
- }
- }
- STORM_LOG_TRACE("New state remapping: " << matrixBuilder.stateRemapping);
- std::stringstream ss;
- ss << "Index remapping:" << std::endl;
- for (auto tmp : indexRemapping) {
- ss << tmp << " ";
- }
- STORM_LOG_TRACE(ss.str());
-
- // Remap markovian states
- storm::storage::BitVector markovianStatesNew = storm::storage::BitVector(modelComponents.markovianStates.size(), true);
- // Iterate over all not set bits
- modelComponents.markovianStates.complement();
- size_t index = modelComponents.markovianStates.getNextSetIndex(0);
- while (index < modelComponents.markovianStates.size()) {
- markovianStatesNew.set(indexRemapping[index], false);
- index = modelComponents.markovianStates.getNextSetIndex(index+1);
- }
- STORM_LOG_ASSERT(modelComponents.markovianStates.size() - modelComponents.markovianStates.getNumberOfSetBits() == markovianStatesNew.getNumberOfSetBits(), "Remapping of markovian states is wrong.");
- STORM_LOG_ASSERT(markovianStatesNew.size() == nrStates, "No. of states does not coincide with markovian size.");
- modelComponents.markovianStates = markovianStatesNew;
-
- // Build submatrix for expanded states
- // TODO Matthias: only use row groups when necessary
- for (StateType oldRowGroup = 0; oldRowGroup < modelComponents.transitionMatrix.getRowGroupCount(); ++oldRowGroup) {
- if (indexRemapping[oldRowGroup] < nrExpandedStates) {
- // State is expanded -> copy to new matrix
- matrixBuilder.newRowGroup();
- for (StateType oldRow = modelComponents.transitionMatrix.getRowGroupIndices()[oldRowGroup]; oldRow < modelComponents.transitionMatrix.getRowGroupIndices()[oldRowGroup+1]; ++oldRow) {
- for (typename storm::storage::SparseMatrix<ValueType>::const_iterator itEntry = modelComponents.transitionMatrix.begin(oldRow); itEntry != modelComponents.transitionMatrix.end(oldRow); ++itEntry) {
- auto itFind = skippedStates.find(itEntry->getColumn());
- if (itFind != skippedStates.end()) {
- // Set id for skipped states as we remap it later
- matrixBuilder.addTransition(matrixBuilder.mappingOffset + itFind->second.first->getId(), itEntry->getValue());
- } else {
- // Set newly remapped index for expanded states
- matrixBuilder.addTransition(indexRemapping[itEntry->getColumn()], itEntry->getValue());
- }
- }
- matrixBuilder.finishRow();
- }
- }
- }
-
- skippedStates = skippedStatesNew;
-
- STORM_LOG_ASSERT(matrixBuilder.getCurrentRowGroup() == nrExpandedStates, "Row group size does not match.");
- skippedStates.clear();
- }
-
- template<typename ValueType, typename StateType>
- void ExplicitDFTModelBuilderApprox<ValueType, StateType>::exploreStateSpace(double approximationThreshold) {
- size_t nrExpandedStates = 0;
- size_t nrSkippedStates = 0;
- // TODO Matthias: do not empty queue every time but break before
- while (!explorationQueue.empty()) {
- // Get the first state in the queue
- ExplorationHeuristicPointer currentExplorationHeuristic = explorationQueue.popTop();
- StateType currentId = currentExplorationHeuristic->getId();
- auto itFind = statesNotExplored.find(currentId);
- STORM_LOG_ASSERT(itFind != statesNotExplored.end(), "Id " << currentId << " not found");
- DFTStatePointer currentState = itFind->second.first;
- STORM_LOG_ASSERT(currentExplorationHeuristic == itFind->second.second, "Exploration heuristics do not match");
- STORM_LOG_ASSERT(currentState->getId() == currentId, "Ids do not match");
- // Remove it from the list of not explored states
- statesNotExplored.erase(itFind);
- STORM_LOG_ASSERT(stateStorage.stateToId.contains(currentState->status()), "State is not contained in state storage.");
- STORM_LOG_ASSERT(stateStorage.stateToId.getValue(currentState->status()) == currentId, "Ids of states do not coincide.");
-
- // Get concrete state if necessary
- if (currentState->isPseudoState()) {
- // Create concrete state from pseudo state
- currentState->construct();
- }
- STORM_LOG_ASSERT(!currentState->isPseudoState(), "State is pseudo state.");
-
- // Remember that the current row group was actually filled with the transitions of a different state
- matrixBuilder.setRemapping(currentId);
-
- matrixBuilder.newRowGroup();
-
- // Try to explore the next state
- generator.load(currentState);
-
- //if (approximationThreshold > 0.0 && nrExpandedStates > approximationThreshold && !currentExplorationHeuristic->isExpand()) {
- if (approximationThreshold > 0.0 && currentExplorationHeuristic->isSkip(approximationThreshold)) {
- // Skip the current state
- ++nrSkippedStates;
- STORM_LOG_TRACE("Skip expansion of state: " << dft.getStateString(currentState));
- setMarkovian(true);
- // Add transition to target state with temporary value 0
- // TODO Matthias: what to do when there is no unique target state?
- matrixBuilder.addTransition(failedStateId, storm::utility::zero<ValueType>());
- // Remember skipped state
- skippedStates[matrixBuilder.getCurrentRowGroup() - 1] = std::make_pair(currentState, currentExplorationHeuristic);
- matrixBuilder.finishRow();
- } else {
- // Explore the current state
- ++nrExpandedStates;
- storm::generator::StateBehavior<ValueType, StateType> behavior = generator.expand(std::bind(&ExplicitDFTModelBuilderApprox::getOrAddStateIndex, this, std::placeholders::_1));
- STORM_LOG_ASSERT(!behavior.empty(), "Behavior is empty.");
- setMarkovian(behavior.begin()->isMarkovian());
-
- // Now add all choices.
- for (auto const& choice : behavior) {
- // Add the probabilistic behavior to the matrix.
- for (auto const& stateProbabilityPair : choice) {
- STORM_LOG_ASSERT(!storm::utility::isZero(stateProbabilityPair.second), "Probability zero.");
- // Set transition to state id + offset. This helps in only remapping all previously skipped states.
- matrixBuilder.addTransition(matrixBuilder.mappingOffset + stateProbabilityPair.first, stateProbabilityPair.second);
- // Set heuristic values for reached states
- auto iter = statesNotExplored.find(stateProbabilityPair.first);
- if (iter != statesNotExplored.end()) {
- // Update heuristic values
- DFTStatePointer state = iter->second.first;
- if (!iter->second.second) {
- // Initialize heuristic values
- ExplorationHeuristicPointer heuristic = std::make_shared<ExplorationHeuristic>(stateProbabilityPair.first, *currentExplorationHeuristic, stateProbabilityPair.second, choice.getTotalMass());
- iter->second.second = heuristic;
- if (state->hasFailed(dft.getTopLevelIndex()) || state->isFailsafe(dft.getTopLevelIndex()) || state->nrFailableDependencies() > 0 || (state->nrFailableDependencies() == 0 && state->nrFailableBEs() == 0)) {
- // Do not skip absorbing state or if reached by dependencies
- iter->second.second->markExpand();
- }
- if (usedHeuristic == storm::builder::ApproximationHeuristic::BOUNDDIFFERENCE) {
- // Compute bounds for heuristic now
- if (state->isPseudoState()) {
- // Create concrete state from pseudo state
- state->construct();
- }
- STORM_LOG_ASSERT(!currentState->isPseudoState(), "State is pseudo state.");
-
- // Initialize bounds
- // TODO Mathias: avoid hack
- ValueType lowerBound = getLowerBound(state);
- ValueType upperBound = getUpperBound(state);
- heuristic->setBounds(lowerBound, upperBound);
- }
-
- explorationQueue.push(heuristic);
- } else if (!iter->second.second->isExpand()) {
- double oldPriority = iter->second.second->getPriority();
- if (iter->second.second->updateHeuristicValues(*currentExplorationHeuristic, stateProbabilityPair.second, choice.getTotalMass())) {
- // Update priority queue
- explorationQueue.update(iter->second.second, oldPriority);
- }
- }
- }
- }
- matrixBuilder.finishRow();
- }
- }
- } // end exploration
-
- STORM_LOG_INFO("Expanded " << nrExpandedStates << " states");
- STORM_LOG_INFO("Skipped " << nrSkippedStates << " states");
- STORM_LOG_ASSERT(nrSkippedStates == skippedStates.size(), "Nr skipped states is wrong");
- }
-
- template<typename ValueType, typename StateType>
- void ExplicitDFTModelBuilderApprox<ValueType, StateType>::buildLabeling(LabelOptions const& labelOpts) {
- // Build state labeling
- modelComponents.stateLabeling = storm::models::sparse::StateLabeling(modelComponents.transitionMatrix.getRowGroupCount());
- // Initial state
- modelComponents.stateLabeling.addLabel("init");
- STORM_LOG_ASSERT(matrixBuilder.getRemapping(initialStateIndex) == initialStateIndex, "Initial state should not be remapped.");
- modelComponents.stateLabeling.addLabelToState("init", initialStateIndex);
- // Label all states corresponding to their status (failed, failsafe, failed BE)
- if(labelOpts.buildFailLabel) {
- modelComponents.stateLabeling.addLabel("failed");
- }
- if(labelOpts.buildFailSafeLabel) {
- modelComponents.stateLabeling.addLabel("failsafe");
- }
-
- // Collect labels for all necessary elements
- for (size_t id = 0; id < dft.nrElements(); ++id) {
- std::shared_ptr<storage::DFTElement<ValueType> const> element = dft.getElement(id);
- if (labelOpts.buildAllLabels || labelOpts.elementLabels.count(element->name()) > 0) {
- modelComponents.stateLabeling.addLabel(element->name() + "_fail");
- }
- }
-
- // Set labels to states
- if (mergeFailedStates) {
- modelComponents.stateLabeling.addLabelToState("failed", failedStateId);
- }
- for (auto const& stateIdPair : stateStorage.stateToId) {
- storm::storage::BitVector state = stateIdPair.first;
- size_t stateId = matrixBuilder.getRemapping(stateIdPair.second);
- if (!mergeFailedStates && labelOpts.buildFailLabel && dft.hasFailed(state, *stateGenerationInfo)) {
- modelComponents.stateLabeling.addLabelToState("failed", stateId);
- }
- if (labelOpts.buildFailSafeLabel && dft.isFailsafe(state, *stateGenerationInfo)) {
- modelComponents.stateLabeling.addLabelToState("failsafe", stateId);
- }
- // Set fail status for each necessary element
- for (size_t id = 0; id < dft.nrElements(); ++id) {
- std::shared_ptr<storage::DFTElement<ValueType> const> element = dft.getElement(id);
- if ((labelOpts.buildAllLabels || labelOpts.elementLabels.count(element->name()) > 0) && storm::storage::DFTState<ValueType>::hasFailed(state, stateGenerationInfo->getStateIndex(element->id()))) {
- modelComponents.stateLabeling.addLabelToState(element->name() + "_fail", stateId);
- }
- }
- }
-
- STORM_LOG_TRACE(modelComponents.stateLabeling);
- }
-
- template<typename ValueType, typename StateType>
- std::shared_ptr<storm::models::sparse::Model<ValueType>> ExplicitDFTModelBuilderApprox<ValueType, StateType>::getModel() {
- STORM_LOG_ASSERT(skippedStates.size() == 0, "Concrete model has skipped states");
- return createModel(false);
- }
-
- template<typename ValueType, typename StateType>
- std::shared_ptr<storm::models::sparse::Model<ValueType>> ExplicitDFTModelBuilderApprox<ValueType, StateType>::getModelApproximation(bool lowerBound, bool expectedTime) {
- if (expectedTime) {
- // TODO Matthias: handle case with no skipped states
- changeMatrixBound(modelComponents.transitionMatrix, lowerBound);
- return createModel(true);
- } else {
- // Change model for probabilities
- // TODO Matthias: make nicer
- storm::storage::SparseMatrix<ValueType> matrix = modelComponents.transitionMatrix;
- storm::models::sparse::StateLabeling labeling = modelComponents.stateLabeling;
- if (lowerBound) {
- // Set self loop for lower bound
- for (auto it = skippedStates.begin(); it != skippedStates.end(); ++it) {
- auto matrixEntry = matrix.getRow(it->first, 0).begin();
- STORM_LOG_ASSERT(matrixEntry->getColumn() == failedStateId, "Transition has wrong target state.");
- STORM_LOG_ASSERT(!it->second.first->isPseudoState(), "State is still pseudo state.");
- matrixEntry->setValue(storm::utility::one<ValueType>());
- matrixEntry->setColumn(it->first);
- }
- } else {
- // Make skipped states failed states for upper bound
- storm::storage::BitVector failedStates = modelComponents.stateLabeling.getStates("failed");
- for (auto it = skippedStates.begin(); it != skippedStates.end(); ++it) {
- failedStates.set(it->first);
- }
- labeling.setStates("failed", failedStates);
- }
-
- std::shared_ptr<storm::models::sparse::Model<ValueType>> model;
- if (modelComponents.deterministicModel) {
- model = std::make_shared<storm::models::sparse::Ctmc<ValueType>>(std::move(matrix), std::move(labeling));
- } else {
- // Build MA
- // Compute exit rates
- // TODO Matthias: avoid computing multiple times
- modelComponents.exitRates = std::vector<ValueType>(modelComponents.markovianStates.size());
- std::vector<typename storm::storage::SparseMatrix<ValueType>::index_type> indices = matrix.getRowGroupIndices();
- for (StateType stateIndex = 0; stateIndex < modelComponents.markovianStates.size(); ++stateIndex) {
- if (modelComponents.markovianStates[stateIndex]) {
- modelComponents.exitRates[stateIndex] = matrix.getRowSum(indices[stateIndex]);
- } else {
- modelComponents.exitRates[stateIndex] = storm::utility::zero<ValueType>();
- }
- }
- STORM_LOG_TRACE("Exit rates: " << modelComponents.exitRates);
-
- storm::storage::sparse::ModelComponents<ValueType> maComponents(std::move(matrix), std::move(labeling));
- maComponents.rateTransitions = true;
- maComponents.markovianStates = modelComponents.markovianStates;
- maComponents.exitRates = modelComponents.exitRates;
- std::shared_ptr<storm::models::sparse::MarkovAutomaton<ValueType>> ma = std::make_shared<storm::models::sparse::MarkovAutomaton<ValueType>>(std::move(maComponents));
- if (ma->hasOnlyTrivialNondeterminism()) {
- // Markov automaton can be converted into CTMC
- // TODO Matthias: change components which were not moved accordingly
- model = ma->convertToCTMC();
- } else {
- model = ma;
- }
-
- }
-
- if (model->getNumberOfStates() <= 15) {
- STORM_LOG_TRACE("Transition matrix: " << std::endl << model->getTransitionMatrix());
- } else {
- STORM_LOG_TRACE("Transition matrix: too big to print");
- }
- return model;
- }
- }
-
- template<typename ValueType, typename StateType>
- std::shared_ptr<storm::models::sparse::Model<ValueType>> ExplicitDFTModelBuilderApprox<ValueType, StateType>::createModel(bool copy) {
- std::shared_ptr<storm::models::sparse::Model<ValueType>> model;
-
- if (modelComponents.deterministicModel) {
- // Build CTMC
- if (copy) {
- model = std::make_shared<storm::models::sparse::Ctmc<ValueType>>(modelComponents.transitionMatrix, modelComponents.stateLabeling);
- } else {
- model = std::make_shared<storm::models::sparse::Ctmc<ValueType>>(std::move(modelComponents.transitionMatrix), std::move(modelComponents.stateLabeling));
- }
- } else {
- // Build MA
- // Compute exit rates
- // TODO Matthias: avoid computing multiple times
- modelComponents.exitRates = std::vector<ValueType>(modelComponents.markovianStates.size());
- std::vector<typename storm::storage::SparseMatrix<ValueType>::index_type> indices = modelComponents.transitionMatrix.getRowGroupIndices();
- for (StateType stateIndex = 0; stateIndex < modelComponents.markovianStates.size(); ++stateIndex) {
- if (modelComponents.markovianStates[stateIndex]) {
- modelComponents.exitRates[stateIndex] = modelComponents.transitionMatrix.getRowSum(indices[stateIndex]);
- } else {
- modelComponents.exitRates[stateIndex] = storm::utility::zero<ValueType>();
- }
- }
- STORM_LOG_TRACE("Exit rates: " << modelComponents.exitRates);
-
- std::shared_ptr<storm::models::sparse::MarkovAutomaton<ValueType>> ma;
- if (copy) {
- storm::storage::sparse::ModelComponents<ValueType> maComponents(modelComponents.transitionMatrix, modelComponents.stateLabeling);
- maComponents.rateTransitions = true;
- maComponents.markovianStates = modelComponents.markovianStates;
- maComponents.exitRates = modelComponents.exitRates;
- std::shared_ptr<storm::models::sparse::MarkovAutomaton<ValueType>> ma = std::make_shared<storm::models::sparse::MarkovAutomaton<ValueType>>(std::move(maComponents));
- } else {
- storm::storage::sparse::ModelComponents<ValueType> maComponents(std::move(modelComponents.transitionMatrix), std::move(modelComponents.stateLabeling));
- maComponents.rateTransitions = true;
- maComponents.markovianStates = std::move(modelComponents.markovianStates);
- maComponents.exitRates = std::move(modelComponents.exitRates);
- std::shared_ptr<storm::models::sparse::MarkovAutomaton<ValueType>> ma = std::make_shared<storm::models::sparse::MarkovAutomaton<ValueType>>(std::move(maComponents));
- }
- if (ma->hasOnlyTrivialNondeterminism()) {
- // Markov automaton can be converted into CTMC
- // TODO Matthias: change components which were not moved accordingly
- model = ma->convertToCTMC();
- } else {
- model = ma;
- }
- }
-
- if (model->getNumberOfStates() <= 15) {
- STORM_LOG_TRACE("Transition matrix: " << std::endl << model->getTransitionMatrix());
- } else {
- STORM_LOG_TRACE("Transition matrix: too big to print");
- }
- return model;
- }
-
- template<typename ValueType, typename StateType>
- void ExplicitDFTModelBuilderApprox<ValueType, StateType>::changeMatrixBound(storm::storage::SparseMatrix<ValueType> & matrix, bool lowerBound) const {
- // Set lower bound for skipped states
- for (auto it = skippedStates.begin(); it != skippedStates.end(); ++it) {
- auto matrixEntry = matrix.getRow(it->first, 0).begin();
- STORM_LOG_ASSERT(matrixEntry->getColumn() == failedStateId, "Transition has wrong target state.");
- STORM_LOG_ASSERT(!it->second.first->isPseudoState(), "State is still pseudo state.");
-
- ExplorationHeuristicPointer heuristic = it->second.second;
- if (storm::utility::isZero(heuristic->getUpperBound())) {
- // Initialize bounds
- ValueType lowerBound = getLowerBound(it->second.first);
- ValueType upperBound = getUpperBound(it->second.first);
- heuristic->setBounds(lowerBound, upperBound);
- }
-
- // Change bound
- if (lowerBound) {
- matrixEntry->setValue(it->second.second->getLowerBound());
- } else {
- matrixEntry->setValue(it->second.second->getUpperBound());
- }
- }
- }
-
- template<typename ValueType, typename StateType>
- ValueType ExplicitDFTModelBuilderApprox<ValueType, StateType>::getLowerBound(DFTStatePointer const& state) const {
- // Get the lower bound by considering the failure of all possible BEs
- ValueType lowerBound = storm::utility::zero<ValueType>();
- for (size_t index = 0; index < state->nrFailableBEs(); ++index) {
- lowerBound += state->getFailableBERate(index);
- }
- return lowerBound;
- }
-
- template<typename ValueType, typename StateType>
- ValueType ExplicitDFTModelBuilderApprox<ValueType, StateType>::getUpperBound(DFTStatePointer const& state) const {
- if (state->hasFailed(dft.getTopLevelIndex())) {
- return storm::utility::zero<ValueType>();
- }
-
- // Get the upper bound by considering the failure of all BEs
- ValueType upperBound = storm::utility::one<ValueType>();
- ValueType rateSum = storm::utility::zero<ValueType>();
-
- // Compute for each independent subtree
- for (std::vector<size_t> const& subtree : subtreeBEs) {
- // Get all possible rates
- std::vector<ValueType> rates;
- storm::storage::BitVector coldBEs(subtree.size(), false);
- for (size_t i = 0; i < subtree.size(); ++i) {
- size_t id = subtree[i];
- if (state->isOperational(id)) {
- // Get BE rate
- ValueType rate = state->getBERate(id);
- if (storm::utility::isZero<ValueType>(rate)) {
- // Get active failure rate for cold BE
- rate = dft.getBasicElement(id)->activeFailureRate();
- if (storm::utility::isZero<ValueType>(rate)) {
- // Ignore BE which cannot fail
- continue;
- }
- // Mark BE as cold
- coldBEs.set(i, true);
- }
- rates.push_back(rate);
- rateSum += rate;
- }
- }
-
- STORM_LOG_ASSERT(rates.size() > 0, "No rates failable");
-
- // Sort rates
- std::sort(rates.begin(), rates.end());
- std::vector<size_t> rateCount(rates.size(), 0);
- size_t lastIndex = 0;
- for (size_t i = 0; i < rates.size(); ++i) {
- if (rates[lastIndex] != rates[i]) {
- lastIndex = i;
- }
- ++rateCount[lastIndex];
- }
-
- for (size_t i = 0; i < rates.size(); ++i) {
- // Cold BEs cannot fail in the first step
- if (!coldBEs.get(i) && rateCount[i] > 0) {
- std::iter_swap(rates.begin() + i, rates.end() - 1);
- // Compute AND MTTF of subtree without current rate and scale with current rate
- upperBound += rates.back() * rateCount[i] * computeMTTFAnd(rates, rates.size() - 1);
- // Swap back
- // TODO try to avoid swapping back
- std::iter_swap(rates.begin() + i, rates.end() - 1);
- }
- }
- }
-
- STORM_LOG_TRACE("Upper bound is " << (rateSum / upperBound) << " for state " << state->getId());
- STORM_LOG_ASSERT(!storm::utility::isZero(upperBound), "Upper bound is 0");
- STORM_LOG_ASSERT(!storm::utility::isZero(rateSum), "State is absorbing");
- return rateSum / upperBound;
- }
-
- template<typename ValueType, typename StateType>
- ValueType ExplicitDFTModelBuilderApprox<ValueType, StateType>::computeMTTFAnd(std::vector<ValueType> const& rates, size_t size) const {
- ValueType result = storm::utility::zero<ValueType>();
- if (size == 0) {
- return result;
- }
-
- // TODO Matthias: works only for <64 BEs!
- // WARNING: this code produces wrong results for more than 32 BEs
- /*for (size_t i = 1; i < 4 && i <= rates.size(); ++i) {
- size_t permutation = smallestIntWithNBitsSet(static_cast<size_t>(i));
- ValueType sum = storm::utility::zero<ValueType>();
- do {
- ValueType permResult = storm::utility::zero<ValueType>();
- for(size_t j = 0; j < rates.size(); ++j) {
- if(permutation & static_cast<size_t>(1 << static_cast<size_t>(j))) {
- // WARNING: if the first bit is set, it also recognizes the 32nd bit as set
- // TODO: fix
- permResult += rates[j];
- }
- }
- permutation = nextBitPermutation(permutation);
- STORM_LOG_ASSERT(!storm::utility::isZero(permResult), "PermResult is 0");
- sum += storm::utility::one<ValueType>() / permResult;
- } while(permutation < (static_cast<size_t>(1) << rates.size()) && permutation != 0);
- if (i % 2 == 0) {
- result -= sum;
- } else {
- result += sum;
- }
- }*/
-
- // Compute result with permutations of size <= 3
- ValueType one = storm::utility::one<ValueType>();
- for (size_t i1 = 0; i1 < size; ++i1) {
- // + 1/a
- ValueType sum = rates[i1];
- result += one / sum;
- for (size_t i2 = 0; i2 < i1; ++i2) {
- // - 1/(a+b)
- ValueType sum2 = sum + rates[i2];
- result -= one / sum2;
- for (size_t i3 = 0; i3 < i2; ++i3) {
- // + 1/(a+b+c)
- result += one / (sum2 + rates[i3]);
- }
- }
- }
-
- STORM_LOG_ASSERT(!storm::utility::isZero(result), "UpperBound is 0");
- return result;
- }
-
- template<typename ValueType, typename StateType>
- StateType ExplicitDFTModelBuilderApprox<ValueType, StateType>::getOrAddStateIndex(DFTStatePointer const& state) {
- StateType stateId;
- bool changed = false;
-
- if (stateGenerationInfo->hasSymmetries()) {
- // Order state by symmetry
- STORM_LOG_TRACE("Check for symmetry: " << dft.getStateString(state));
- changed = state->orderBySymmetry();
- STORM_LOG_TRACE("State " << (changed ? "changed to " : "did not change") << (changed ? dft.getStateString(state) : ""));
- }
-
- if (stateStorage.stateToId.contains(state->status())) {
- // State already exists
- stateId = stateStorage.stateToId.getValue(state->status());
- STORM_LOG_TRACE("State " << dft.getStateString(state) << " with id " << stateId << " already exists");
- if (!changed) {
- // Check if state is pseudo state
- // If state is explored already the possible pseudo state was already constructed
- auto iter = statesNotExplored.find(stateId);
- if (iter != statesNotExplored.end() && iter->second.first->isPseudoState()) {
- // Create pseudo state now
- STORM_LOG_ASSERT(iter->second.first->getId() == stateId, "Ids do not match.");
- STORM_LOG_ASSERT(iter->second.first->status() == state->status(), "Pseudo states do not coincide.");
- state->setId(stateId);
- // Update mapping to map to concrete state now
- // TODO Matthias: just change pointer?
- statesNotExplored[stateId] = std::make_pair(state, iter->second.second);
- // We do not push the new state on the exploration queue as the pseudo state was already pushed
- STORM_LOG_TRACE("Created pseudo state " << dft.getStateString(state));
- }
- }
- } else {
- // State does not exist yet
- STORM_LOG_ASSERT(state->isPseudoState() == changed, "State type (pseudo/concrete) wrong.");
- // Create new state
- state->setId(newIndex++);
- stateId = stateStorage.stateToId.findOrAdd(state->status(), state->getId());
- STORM_LOG_ASSERT(stateId == state->getId(), "Ids do not match.");
- // Insert state as not yet explored
- ExplorationHeuristicPointer nullHeuristic;
- statesNotExplored[stateId] = std::make_pair(state, nullHeuristic);
- // Reserve one slot for the new state in the remapping
- matrixBuilder.stateRemapping.push_back(0);
- STORM_LOG_TRACE("New " << (state->isPseudoState() ? "pseudo" : "concrete") << " state: " << dft.getStateString(state));
- }
- return stateId;
- }
-
- template<typename ValueType, typename StateType>
- void ExplicitDFTModelBuilderApprox<ValueType, StateType>::setMarkovian(bool markovian) {
- if (matrixBuilder.getCurrentRowGroup() > modelComponents.markovianStates.size()) {
- // Resize BitVector
- modelComponents.markovianStates.resize(modelComponents.markovianStates.size() + INITIAL_BITVECTOR_SIZE);
- }
- modelComponents.markovianStates.set(matrixBuilder.getCurrentRowGroup() - 1, markovian);
- }
-
- template<typename ValueType, typename StateType>
- void ExplicitDFTModelBuilderApprox<ValueType, StateType>::printNotExplored() const {
- std::cout << "states not explored:" << std::endl;
- for (auto it : statesNotExplored) {
- std::cout << it.first << " -> " << dft.getStateString(it.second.first) << std::endl;
- }
- }
-
-
- // Explicitly instantiate the class.
- template class ExplicitDFTModelBuilderApprox<double>;
-
-#ifdef STORM_HAVE_CARL
- template class ExplicitDFTModelBuilderApprox<storm::RationalFunction>;
-#endif
-
- } // namespace builder
-} // namespace storm
-
-
diff --git a/src/storm-dft/builder/ExplicitDFTModelBuilderApprox.h b/src/storm-dft/builder/ExplicitDFTModelBuilderApprox.h
deleted file mode 100644
index 802aefe1b..000000000
--- a/src/storm-dft/builder/ExplicitDFTModelBuilderApprox.h
+++ /dev/null
@@ -1,362 +0,0 @@
-#pragma once
-
-#include <boost/container/flat_set.hpp>
-#include <boost/optional/optional.hpp>
-#include <stack>
-#include <unordered_set>
-#include <limits>
-
-#include "storm/models/sparse/StateLabeling.h"
-#include "storm/models/sparse/ChoiceLabeling.h"
-#include "storm/models/sparse/StandardRewardModel.h"
-#include "storm/models/sparse/Model.h"
-#include "storm/storage/SparseMatrix.h"
-#include "storm/storage/sparse/StateStorage.h"
-
-#include "storm-dft/builder/DftExplorationHeuristic.h"
-#include "storm-dft/generator/DftNextStateGenerator.h"
-#include "storm-dft/storage/dft/DFT.h"
-#include "storm-dft/storage/dft/SymmetricUnits.h"
-#include "storm-dft/storage/BucketPriorityQueue.h"
-
-namespace storm {
- namespace builder {
-
- /*!
- * Build a Markov chain from DFT.
- */
- template<typename ValueType, typename StateType = uint32_t>
- class ExplicitDFTModelBuilderApprox {
-
- using DFTStatePointer = std::shared_ptr<storm::storage::DFTState<ValueType>>;
- // TODO Matthias: make choosable
- using ExplorationHeuristic = DFTExplorationHeuristicDepth<ValueType>;
- using ExplorationHeuristicPointer = std::shared_ptr<ExplorationHeuristic>;
-
-
- // A structure holding the individual components of a model.
- struct ModelComponents {
- // Constructor
- ModelComponents();
-
- // The transition matrix.
- storm::storage::SparseMatrix<ValueType> transitionMatrix;
-
- // The state labeling.
- storm::models::sparse::StateLabeling stateLabeling;
-
- // The Markovian states.
- storm::storage::BitVector markovianStates;
-
- // The exit rates.
- std::vector<ValueType> exitRates;
-
- // A vector that stores a labeling for each choice.
- boost::optional<storm::models::sparse::ChoiceLabeling> choiceLabeling;
-
- // A flag indicating if the model is deterministic.
- bool deterministicModel;
- };
-
- // A class holding the information for building the transition matrix.
- class MatrixBuilder {
- public:
- // Constructor
- MatrixBuilder(bool canHaveNondeterminism);
-
- /*!
- * Set a mapping from a state id to the index in the matrix.
- *
- * @param id Id of the state.
- */
- void setRemapping(StateType id) {
- STORM_LOG_ASSERT(id < stateRemapping.size(), "Invalid index for remapping.");
- stateRemapping[id] = currentRowGroup;
- }
-
- /*!
- * Create a new row group if the model is nondeterministic.
- */
- void newRowGroup() {
- if (canHaveNondeterminism) {
- builder.newRowGroup(currentRow);
- }
- ++currentRowGroup;
- }
-
- /*!
- * Add a transition from the current row.
- *
- * @param index Target index
- * @param value Value of transition
- */
- void addTransition(StateType index, ValueType value) {
- builder.addNextValue(currentRow, index, value);
- }
-
- /*!
- * Finish the current row.
- */
- void finishRow() {
- ++currentRow;
- }
-
- /*!
- * Remap the columns in the matrix.
- */
- void remap() {
- builder.replaceColumns(stateRemapping, mappingOffset);
- }
-
- /*!
- * Get the current row group.
- *
- * @return The current row group.
- */
- StateType getCurrentRowGroup() {
- return currentRowGroup;
- }
-
- /*!
- * Get the remapped state for the given id.
- *
- * @param id State.
- *
- * @return Remapped index.
- */
- StateType getRemapping(StateType id) {
- STORM_LOG_ASSERT(id < stateRemapping.size(), "Invalid index for remapping.");
- return stateRemapping[id];
- }
-
- // Matrix builder.
- storm::storage::SparseMatrixBuilder<ValueType> builder;
-
- // Offset to distinguish states which will not be remapped anymore and those which will.
- size_t mappingOffset;
-
- // A mapping from state ids to the row group indices in which they actually reside.
- // TODO Matthias: avoid hack with fixed int type
- std::vector<uint_fast64_t> stateRemapping;
-
- private:
-
- // Index of the current row group.
- StateType currentRowGroup;
-
- // Index of the current row.
- StateType currentRow;
-
- // Flag indicating if row groups are needed.
- bool canHaveNondeterminism;
- };
-
- public:
- // A structure holding the labeling options.
- struct LabelOptions {
- // Constructor
- LabelOptions(std::vector<std::shared_ptr<storm::logic::Formula const>> properties, bool buildAllLabels = false);
-
- // Flag indicating if the general fail label should be included.
- bool buildFailLabel;
-
- // Flag indicating if the general failsafe label should be included.
- bool buildFailSafeLabel;
-
- // Flag indicating if all possible labels should be included.
- bool buildAllLabels;
-
- // Set of element names whose fail label to include.
- std::set<std::string> elementLabels;
- };
-
- /*!
- * Constructor.
- *
- * @param dft DFT.
- * @param symmetries Symmetries in the dft.
- * @param enableDC Flag indicating if dont care propagation should be used.
- */
- ExplicitDFTModelBuilderApprox(storm::storage::DFT<ValueType> const& dft, storm::storage::DFTIndependentSymmetries const& symmetries, bool enableDC);
-
- /*!
- * Build model from DFT.
- *
- * @param labelOpts Options for labeling.
- * @param iteration Current number of iteration.
- * @param approximationThreshold Threshold determining when to skip exploring states.
- */
- void buildModel(LabelOptions const& labelOpts, size_t iteration, double approximationThreshold = 0.0);
-
- /*!
- * Get the built model.
- *
- * @return The model built from the DFT.
- */
- std::shared_ptr<storm::models::sparse::Model<ValueType>> getModel();
-
- /*!
- * Get the built approximation model for either the lower or upper bound.
- *
- * @param lowerBound If true, the lower bound model is returned, else the upper bound model
- * @param expectedTime If true, the bounds for expected time are computed, else the bounds for probabilities.
- *
- * @return The model built from the DFT.
- */
- std::shared_ptr<storm::models::sparse::Model<ValueType>> getModelApproximation(bool lowerBound, bool expectedTime);
-
- private:
-
- /*!
- * Explore state space of DFT.
- *
- * @param approximationThreshold Threshold to determine when to skip states.
- */
- void exploreStateSpace(double approximationThreshold);
-
- /*!
- * Initialize the matrix for a refinement iteration.
- */
- void initializeNextIteration();
-
- /*!
- * Build the labeling.
- *
- * @param labelOpts Options for labeling.
- */
- void buildLabeling(LabelOptions const& labelOpts);
-
- /*!
- * Add a state to the explored states (if not already there). It also handles pseudo states.
- *
- * @param state The state to add.
- *
- * @return Id of state.
- */
- StateType getOrAddStateIndex(DFTStatePointer const& state);
-
- /*!
- * Set markovian flag for the current state.
- *
- * @param markovian Flag indicating if the state is markovian.
- */
- void setMarkovian(bool markovian);
-
- /**
- * Change matrix to reflect the lower or upper approximation bound.
- *
- * @param matrix Matrix to change. The change are reflected here.
- * @param lowerBound Flag indicating if the lower bound should be used. Otherwise the upper bound is used.
- */
- void changeMatrixBound(storm::storage::SparseMatrix<ValueType> & matrix, bool lowerBound) const;
-
- /*!
- * Get lower bound approximation for state.
- *
- * @param state The state.
- *
- * @return Lower bound approximation.
- */
- ValueType getLowerBound(DFTStatePointer const& state) const;
-
- /*!
- * Get upper bound approximation for state.
- *
- * @param state The state.
- *
- * @return Upper bound approximation.
- */
- ValueType getUpperBound(DFTStatePointer const& state) const;
-
- /*!
- * Compute the MTTF of an AND gate via a closed formula.
- * The used formula is 1/( 1/a + 1/b + 1/c + ... - 1/(a+b) - 1/(a+c) - ... + 1/(a+b+c) + ... - ...)
- *
- * @param rates List of rates of children of AND.
- * @param size Only indices < size are considered in the vector.
- * @return MTTF.
- */
- ValueType computeMTTFAnd(std::vector<ValueType> const& rates, size_t size) const;
-
- /*!
- * Compares the priority of two states.
- *
- * @param idA Id of first state
- * @param idB Id of second state
- *
- * @return True if the priority of the first state is greater then the priority of the second one.
- */
- bool isPriorityGreater(StateType idA, StateType idB) const;
-
- void printNotExplored() const;
-
- /*!
- * Create the model model from the model components.
- *
- * @param copy If true, all elements of the model component are copied (used for approximation). If false
- * they are moved to reduce the memory overhead.
- *
- * @return The model built from the model components.
- */
- std::shared_ptr<storm::models::sparse::Model<ValueType>> createModel(bool copy);
-
- // Initial size of the bitvector.
- const size_t INITIAL_BITVECTOR_SIZE = 20000;
- // Offset used for pseudo states.
- const StateType OFFSET_PSEUDO_STATE = std::numeric_limits<StateType>::max() / 2;
-
- // Dft
- storm::storage::DFT<ValueType> const& dft;
-
- // General information for state generation
- // TODO Matthias: use const reference
- std::shared_ptr<storm::storage::DFTStateGenerationInfo> stateGenerationInfo;
-
- // Flag indication if dont care propagation should be used.
- bool enableDC = true;
-
- //TODO Matthias: make changeable
- const bool mergeFailedStates = true;
-
- // Heuristic used for approximation
- storm::builder::ApproximationHeuristic usedHeuristic;
-
- // Current id for new state
- size_t newIndex = 0;
-
- // Id of failed state
- size_t failedStateId = 0;
-
- // Id of initial state
- size_t initialStateIndex = 0;
-
- // Next state generator for exploring the state space
- storm::generator::DftNextStateGenerator<ValueType, StateType> generator;
-
- // Structure for the components of the model.
- ModelComponents modelComponents;
-
- // Structure for the transition matrix builder.
- MatrixBuilder matrixBuilder;
-
- // Internal information about the states that were explored.
- storm::storage::sparse::StateStorage<StateType> stateStorage;
-
- // A priority queue of states that still need to be explored.
- storm::storage::BucketPriorityQueue<ValueType> explorationQueue;
-
- // A mapping of not yet explored states from the id to the tuple (state object, heuristic values).
- std::map<StateType, std::pair<DFTStatePointer, ExplorationHeuristicPointer>> statesNotExplored;
-
- // Holds all skipped states which were not yet expanded. More concretely it is a mapping from matrix indices
- // to the corresponding skipped states.
- // Notice that we need an ordered map here to easily iterate in increasing order over state ids.
- // TODO remove again
- std::map<StateType, std::pair<DFTStatePointer, ExplorationHeuristicPointer>> skippedStates;
-
- // List of independent subtrees and the BEs contained in them.
- std::vector<std::vector<size_t>> subtreeBEs;
- };
-
- }
-}
diff --git a/src/storm-dft/generator/DftNextStateGenerator.cpp b/src/storm-dft/generator/DftNextStateGenerator.cpp
index 7b86d1faa..0002cd6a3 100644
--- a/src/storm-dft/generator/DftNextStateGenerator.cpp
+++ b/src/storm-dft/generator/DftNextStateGenerator.cpp
@@ -4,7 +4,7 @@
#include "storm/utility/macros.h"
#include "storm/exceptions/NotImplementedException.h"
#include "storm/settings/SettingsManager.h"
-#include "storm-dft/settings/modules/DFTSettings.h"
+#include "storm-dft/settings/modules/FaultTreeSettings.h"
namespace storm {
namespace generator {
@@ -71,7 +71,7 @@ namespace storm {
// Let BE fail
while (currentFailable < failableCount) {
- if (storm::settings::getModule<storm::settings::modules::DFTSettings>().isTakeFirstDependency() && hasDependencies && currentFailable > 0) {
+ if (storm::settings::getModule<storm::settings::modules::FaultTreeSettings>().isTakeFirstDependency() && hasDependencies && currentFailable > 0) {
// We discard further exploration as we already chose one dependent event
break;
}
diff --git a/src/storm-dft/modelchecker/dft/DFTModelChecker.cpp b/src/storm-dft/modelchecker/dft/DFTModelChecker.cpp
index d6b7e9138..d2b435c1c 100644
--- a/src/storm-dft/modelchecker/dft/DFTModelChecker.cpp
+++ b/src/storm-dft/modelchecker/dft/DFTModelChecker.cpp
@@ -6,9 +6,8 @@
#include "storm/utility/DirectEncodingExporter.h"
#include "storm-dft/builder/ExplicitDFTModelBuilder.h"
-#include "storm-dft/builder/ExplicitDFTModelBuilderApprox.h"
#include "storm-dft/storage/dft/DFTIsomorphism.h"
-#include "storm-dft/settings/modules/DFTSettings.h"
+#include "storm-dft/settings/modules/FaultTreeSettings.h"
namespace storm {
@@ -192,8 +191,8 @@ namespace storm {
// Build a single CTMC
STORM_LOG_INFO("Building Model...");
- storm::builder::ExplicitDFTModelBuilderApprox<ValueType> builder(ft, symmetries, enableDC);
- typename storm::builder::ExplicitDFTModelBuilderApprox<ValueType>::LabelOptions labeloptions(properties);
+ storm::builder::ExplicitDFTModelBuilder<ValueType> builder(ft, symmetries, enableDC);
+ typename storm::builder::ExplicitDFTModelBuilder<ValueType>::LabelOptions labeloptions(properties);
builder.buildModel(labeloptions, 0, 0.0);
std::shared_ptr<storm::models::sparse::Model<ValueType>> model = builder.getModel();
explorationTimer.stop();
@@ -244,9 +243,8 @@ namespace storm {
// Build a single CTMC
STORM_LOG_INFO("Building Model...");
-
- storm::builder::ExplicitDFTModelBuilderApprox<ValueType> builder(dft, symmetries, enableDC);
- typename storm::builder::ExplicitDFTModelBuilderApprox<ValueType>::LabelOptions labeloptions(properties);
+ storm::builder::ExplicitDFTModelBuilder<ValueType> builder(dft, symmetries, enableDC);
+ typename storm::builder::ExplicitDFTModelBuilder<ValueType>::LabelOptions labeloptions(properties);
builder.buildModel(labeloptions, 0, 0.0);
std::shared_ptr<storm::models::sparse::Model<ValueType>> model = builder.getModel();
model->printModelInformationToStream(std::cout);
@@ -277,8 +275,8 @@ namespace storm {
approximation_result approxResult = std::make_pair(storm::utility::zero<ValueType>(), storm::utility::zero<ValueType>());
std::shared_ptr<storm::models::sparse::Model<ValueType>> model;
std::vector<ValueType> newResult;
- storm::builder::ExplicitDFTModelBuilderApprox<ValueType> builder(dft, symmetries, enableDC);
- typename storm::builder::ExplicitDFTModelBuilderApprox<ValueType>::LabelOptions labeloptions(properties);
+ storm::builder::ExplicitDFTModelBuilder<ValueType> builder(dft, symmetries, enableDC);
+ typename storm::builder::ExplicitDFTModelBuilder<ValueType>::LabelOptions labeloptions(properties);
// TODO Matthias: compute approximation for all properties simultaneously?
std::shared_ptr<const storm::logic::Formula> property = properties[0];
@@ -342,18 +340,10 @@ namespace storm {
} else {
// Build a single Markov Automaton
STORM_LOG_INFO("Building Model...");
- std::shared_ptr<storm::models::sparse::Model<ValueType>> model;
- // TODO Matthias: use only one builder if everything works again
- if (storm::settings::getModule<storm::settings::modules::DFTSettings>().isApproximationErrorSet()) {
- storm::builder::ExplicitDFTModelBuilderApprox<ValueType> builder(dft, symmetries, enableDC);
- typename storm::builder::ExplicitDFTModelBuilderApprox<ValueType>::LabelOptions labeloptions(properties, storm::settings::getModule<storm::settings::modules::IOSettings>().isExportExplicitSet());
- builder.buildModel(labeloptions, 0, 0.0);
- model = builder.getModel();
- } else {
- storm::builder::ExplicitDFTModelBuilder<ValueType> builder(dft, symmetries, enableDC);
- typename storm::builder::ExplicitDFTModelBuilder<ValueType>::LabelOptions labeloptions;
- model = builder.buildModel(labeloptions);
- }
+ storm::builder::ExplicitDFTModelBuilder<ValueType> builder(dft, symmetries, enableDC);
+ typename storm::builder::ExplicitDFTModelBuilder<ValueType>::LabelOptions labeloptions(properties, storm::settings::getModule<storm::settings::modules::IOSettings>().isExportExplicitSet());
+ builder.buildModel(labeloptions, 0, 0.0);
+ std::shared_ptr<storm::models::sparse::Model<ValueType>> model = builder.getModel();
model->printModelInformationToStream(std::cout);
explorationTimer.stop();
diff --git a/src/storm-dft/settings/DftSettings.cpp b/src/storm-dft/settings/DftSettings.cpp
new file mode 100644
index 000000000..ce48c6fd9
--- /dev/null
+++ b/src/storm-dft/settings/DftSettings.cpp
@@ -0,0 +1,51 @@
+#include "storm-dft/settings/DftSettings.h"
+
+#include "storm-dft/settings/modules/DftIOSettings.h"
+#include "storm-dft/settings/modules/FaultTreeSettings.h"
+
+#include "storm/settings/SettingsManager.h"
+#include "storm/settings/modules/GeneralSettings.h"
+#include "storm/settings/modules/CoreSettings.h"
+#include "storm/settings/modules/IOSettings.h"
+#include "storm/settings/modules/DebugSettings.h"
+#include "storm/settings/modules/EigenEquationSolverSettings.h"
+#include "storm/settings/modules/GmmxxEquationSolverSettings.h"
+#include "storm/settings/modules/NativeEquationSolverSettings.h"
+#include "storm/settings/modules/EliminationSettings.h"
+#include "storm/settings/modules/MinMaxEquationSolverSettings.h"
+#include "storm/settings/modules/BisimulationSettings.h"
+#include "storm/settings/modules/ResourceSettings.h"
+#include "storm/settings/modules/JaniExportSettings.h"
+#include "storm/settings/modules/GSPNSettings.h"
+#include "storm/settings/modules/GSPNExportSettings.h"
+
+
+namespace storm {
+ namespace settings {
+ void initializeDftSettings(std::string const& name, std::string const& executableName) {
+ storm::settings::mutableManager().setName(name, executableName);
+
+ // Register relevant settings modules.
+ storm::settings::addModule<storm::settings::modules::GeneralSettings>();
+ storm::settings::addModule<storm::settings::modules::DftIOSettings>();
+ storm::settings::addModule<storm::settings::modules::FaultTreeSettings>();
+ storm::settings::addModule<storm::settings::modules::IOSettings>();
+ storm::settings::addModule<storm::settings::modules::CoreSettings>();
+
+ storm::settings::addModule<storm::settings::modules::DebugSettings>();
+ storm::settings::addModule<storm::settings::modules::NativeEquationSolverSettings>();
+ storm::settings::addModule<storm::settings::modules::GmmxxEquationSolverSettings>();
+ storm::settings::addModule<storm::settings::modules::EigenEquationSolverSettings>();
+ storm::settings::addModule<storm::settings::modules::EliminationSettings>();
+ storm::settings::addModule<storm::settings::modules::MinMaxEquationSolverSettings>();
+ // storm::settings::addModule<storm::settings::modules::BisimulationSettings>();
+ storm::settings::addModule<storm::settings::modules::ResourceSettings>();
+
+ // For translation into JANI via GSPN.
+ storm::settings::addModule<storm::settings::modules::JaniExportSettings>();
+ storm::settings::addModule<storm::settings::modules::GSPNSettings>();
+ storm::settings::addModule<storm::settings::modules::GSPNExportSettings>();
+ }
+
+ }
+}
diff --git a/src/storm-dft/settings/DftSettings.h b/src/storm-dft/settings/DftSettings.h
new file mode 100644
index 000000000..8f67ec0b7
--- /dev/null
+++ b/src/storm-dft/settings/DftSettings.h
@@ -0,0 +1,11 @@
+#pragma once
+
+#include <string>
+
+namespace storm {
+ namespace settings {
+
+ void initializeDftSettings(std::string const& name, std::string const& executableName);
+
+ }
+}
diff --git a/src/storm-dft/settings/modules/DFTSettings.cpp b/src/storm-dft/settings/modules/DFTSettings.cpp
deleted file mode 100644
index 1a8d59d70..000000000
--- a/src/storm-dft/settings/modules/DFTSettings.cpp
+++ /dev/null
@@ -1,189 +0,0 @@
-#include "DFTSettings.h"
-
-#include "storm/settings/SettingsManager.h"
-#include "storm/settings/SettingMemento.h"
-#include "storm/settings/Option.h"
-#include "storm/settings/OptionBuilder.h"
-#include "storm/settings/ArgumentBuilder.h"
-#include "storm/settings/Argument.h"
-
-#include "storm/exceptions/InvalidSettingsException.h"
-#include "storm/exceptions/IllegalArgumentValueException.h"
-
-namespace storm {
- namespace settings {
- namespace modules {
-
- const std::string DFTSettings::moduleName = "dft";
- const std::string DFTSettings::dftFileOptionName = "dftfile";
- const std::string DFTSettings::dftFileOptionShortName = "dft";
- const std::string DFTSettings::dftJsonFileOptionName = "dftfile-json";
- const std::string DFTSettings::dftJsonFileOptionShortName = "dftjson";
- const std::string DFTSettings::symmetryReductionOptionName = "symmetryreduction";
- const std::string DFTSettings::symmetryReductionOptionShortName = "symred";
- const std::string DFTSettings::modularisationOptionName = "modularisation";
- const std::string DFTSettings::disableDCOptionName = "disabledc";
- const std::string DFTSettings::approximationErrorOptionName = "approximation";
- const std::string DFTSettings::approximationErrorOptionShortName = "approx";
- const std::string DFTSettings::approximationHeuristicOptionName = "approximationheuristic";
- const std::string DFTSettings::propExpectedTimeOptionName = "expectedtime";
- const std::string DFTSettings::propExpectedTimeOptionShortName = "mttf";
- const std::string DFTSettings::propProbabilityOptionName = "probability";
- const std::string DFTSettings::propTimeboundOptionName = "timebound";
- const std::string DFTSettings::propTimepointsOptionName = "timepoints";
- const std::string DFTSettings::minValueOptionName = "min";
- const std::string DFTSettings::maxValueOptionName = "max";
- const std::string DFTSettings::firstDependencyOptionName = "firstdep";
- const std::string DFTSettings::transformToGspnOptionName = "gspn";
- const std::string DFTSettings::exportToJsonOptionName = "export-json";
-#ifdef STORM_HAVE_Z3
- const std::string DFTSettings::solveWithSmtOptionName = "smt";
-#endif
-
- DFTSettings::DFTSettings() : ModuleSettings(moduleName) {
- this->addOption(storm::settings::OptionBuilder(moduleName, dftFileOptionName, false, "Parses the model given in the Galileo format.").setShortName(dftFileOptionShortName)
- .addArgument(storm::settings::ArgumentBuilder::createStringArgument("filename", "The name of the file from which to read the DFT model.").addValidatorString(ArgumentValidatorFactory::createExistingFileValidator()).build()).build());
- this->addOption(storm::settings::OptionBuilder(moduleName, dftJsonFileOptionName, false, "Parses the model given in the Cytoscape JSON format.").setShortName(dftJsonFileOptionShortName)
- .addArgument(storm::settings::ArgumentBuilder::createStringArgument("filename", "The name of the JSON file from which to read the DFT model.").addValidatorString(ArgumentValidatorFactory::createExistingFileValidator()).build()).build());
- this->addOption(storm::settings::OptionBuilder(moduleName, symmetryReductionOptionName, false, "Exploit symmetric structure of model.").setShortName(symmetryReductionOptionShortName).build());
- this->addOption(storm::settings::OptionBuilder(moduleName, modularisationOptionName, false, "Use modularisation (not applicable for expected time).").build());
- this->addOption(storm::settings::OptionBuilder(moduleName, disableDCOptionName, false, "Disable Dont Care propagation.").build());
- this->addOption(storm::settings::OptionBuilder(moduleName, firstDependencyOptionName, false, "Avoid non-determinism by always taking the first possible dependency.").build());
- this->addOption(storm::settings::OptionBuilder(moduleName, approximationErrorOptionName, false, "Approximation error allowed.").setShortName(approximationErrorOptionShortName).addArgument(storm::settings::ArgumentBuilder::createDoubleArgument("error", "The relative approximation error to use.").addValidatorDouble(ArgumentValidatorFactory::createDoubleGreaterEqualValidator(0.0)).build()).build());
- this->addOption(storm::settings::OptionBuilder(moduleName, approximationHeuristicOptionName, false, "Set the heuristic used for approximation.").addArgument(storm::settings::ArgumentBuilder::createStringArgument("heuristic", "Sets which heuristic is used for approximation. Must be in {depth, probability}. Default is").setDefaultValueString("depth").addValidatorString(ArgumentValidatorFactory::createMultipleChoiceValidator({"depth", "rateratio"})).build()).build());
- this->addOption(storm::settings::OptionBuilder(moduleName, propExpectedTimeOptionName, false, "Compute expected time of system failure.").setShortName(propExpectedTimeOptionShortName).build());
- this->addOption(storm::settings::OptionBuilder(moduleName, propProbabilityOptionName, false, "Compute probability of system failure.").build());
- this->addOption(storm::settings::OptionBuilder(moduleName, propTimeboundOptionName, false, "Compute probability of system failure up to given timebound.").addArgument(storm::settings::ArgumentBuilder::createDoubleArgument("time", "The timebound to use.").addValidatorDouble(ArgumentValidatorFactory::createDoubleGreaterValidator(0.0)).build()).build());
- this->addOption(storm::settings::OptionBuilder(moduleName, propTimepointsOptionName, false, "Compute probability of system failure up to given timebound for a set of given timepoints [starttime, starttime+inc, starttime+2inc, ... ,endtime]").addArgument(storm::settings::ArgumentBuilder::createDoubleArgument("starttime", "The timebound to start from.").addValidatorDouble(ArgumentValidatorFactory::createDoubleGreaterEqualValidator(0.0)).build()).addArgument(storm::settings::ArgumentBuilder::createDoubleArgument("endtime", "The timebound to end with.").addValidatorDouble(ArgumentValidatorFactory::createDoubleGreaterEqualValidator(0.0)).build()).addArgument(storm::settings::ArgumentBuilder::createDoubleArgument("inc", "The value to increment with to get the next timepoint.").addValidatorDouble(ArgumentValidatorFactory::createDoubleGreaterEqualValidator(0.0)).build()).build());
- this->addOption(storm::settings::OptionBuilder(moduleName, minValueOptionName, false, "Compute minimal value in case of non-determinism.").build());
- this->addOption(storm::settings::OptionBuilder(moduleName, maxValueOptionName, false, "Compute maximal value in case of non-determinism.").build());
-#ifdef STORM_HAVE_Z3
- this->addOption(storm::settings::OptionBuilder(moduleName, solveWithSmtOptionName, true, "Solve the DFT with SMT.").build());
-#endif
- this->addOption(storm::settings::OptionBuilder(moduleName, transformToGspnOptionName, false, "Transform DFT to GSPN.").build());
- this->addOption(storm::settings::OptionBuilder(moduleName, exportToJsonOptionName, false, "Export the model to the Cytoscape JSON format.").addArgument(storm::settings::ArgumentBuilder::createStringArgument("filename", "The name of the JSON file to export to.").build()).build());
- }
-
- bool DFTSettings::isDftFileSet() const {
- return this->getOption(dftFileOptionName).getHasOptionBeenSet();
- }
-
- std::string DFTSettings::getDftFilename() const {
- return this->getOption(dftFileOptionName).getArgumentByName("filename").getValueAsString();
- }
-
- bool DFTSettings::isDftJsonFileSet() const {
- return this->getOption(dftJsonFileOptionName).getHasOptionBeenSet();
- }
-
- std::string DFTSettings::getDftJsonFilename() const {
- return this->getOption(dftJsonFileOptionName).getArgumentByName("filename").getValueAsString();
- }
-
- bool DFTSettings::useSymmetryReduction() const {
- return this->getOption(symmetryReductionOptionName).getHasOptionBeenSet();
- }
-
- bool DFTSettings::useModularisation() const {
- return this->getOption(modularisationOptionName).getHasOptionBeenSet();
- }
-
- bool DFTSettings::isDisableDC() const {
- return this->getOption(disableDCOptionName).getHasOptionBeenSet();
- }
-
- bool DFTSettings::isApproximationErrorSet() const {
- return this->getOption(approximationErrorOptionName).getHasOptionBeenSet();
- }
-
- double DFTSettings::getApproximationError() const {
- return this->getOption(approximationErrorOptionName).getArgumentByName("error").getValueAsDouble();
- }
-
- storm::builder::ApproximationHeuristic DFTSettings::getApproximationHeuristic() const {
- if (!isApproximationErrorSet() || getApproximationError() == 0.0) {
- // No approximation is done
- return storm::builder::ApproximationHeuristic::NONE;
- }
- std::string heuristicAsString = this->getOption(approximationHeuristicOptionName).getArgumentByName("heuristic").getValueAsString();
- if (heuristicAsString == "depth") {
- return storm::builder::ApproximationHeuristic::DEPTH;
- } else if (heuristicAsString == "probability") {
- return storm::builder::ApproximationHeuristic::PROBABILITY;
- }
- STORM_LOG_THROW(false, storm::exceptions::IllegalArgumentValueException, "Illegal value '" << heuristicAsString << "' set as heuristic for approximation.");
- }
-
- bool DFTSettings::usePropExpectedTime() const {
- return this->getOption(propExpectedTimeOptionName).getHasOptionBeenSet();
- }
-
- bool DFTSettings::usePropProbability() const {
- return this->getOption(propProbabilityOptionName).getHasOptionBeenSet();
- }
-
- bool DFTSettings::usePropTimebound() const {
- return this->getOption(propTimeboundOptionName).getHasOptionBeenSet();
- }
-
- double DFTSettings::getPropTimebound() const {
- return this->getOption(propTimeboundOptionName).getArgumentByName("time").getValueAsDouble();
- }
-
- bool DFTSettings::usePropTimepoints() const {
- return this->getOption(propTimepointsOptionName).getHasOptionBeenSet();
- }
-
- std::vector<double> DFTSettings::getPropTimepoints() const {
- double starttime = this->getOption(propTimepointsOptionName).getArgumentByName("starttime").getValueAsDouble();
- double endtime = this->getOption(propTimepointsOptionName).getArgumentByName("endtime").getValueAsDouble();
- double inc = this->getOption(propTimepointsOptionName).getArgumentByName("inc").getValueAsDouble();
- std::vector<double> timepoints;
- for (double time = starttime; time <= endtime; time += inc) {
- timepoints.push_back(time);
- }
- return timepoints;
- }
-
- bool DFTSettings::isComputeMinimalValue() const {
- return this->getOption(minValueOptionName).getHasOptionBeenSet();
- }
-
- bool DFTSettings::isComputeMaximalValue() const {
- return this->getOption(maxValueOptionName).getHasOptionBeenSet();
- }
-
- bool DFTSettings::isTakeFirstDependency() const {
- return this->getOption(firstDependencyOptionName).getHasOptionBeenSet();
- }
-
-#ifdef STORM_HAVE_Z3
- bool DFTSettings::solveWithSMT() const {
- return this->getOption(solveWithSmtOptionName).getHasOptionBeenSet();
- }
-#endif
-
- bool DFTSettings::isTransformToGspn() const {
- return this->getOption(transformToGspnOptionName).getHasOptionBeenSet();
- }
-
- bool DFTSettings::isExportToJson() const {
- return this->getOption(exportToJsonOptionName).getHasOptionBeenSet();
- }
-
- std::string DFTSettings::getExportJsonFilename() const {
- return this->getOption(exportToJsonOptionName).getArgumentByName("filename").getValueAsString();
- }
-
- void DFTSettings::finalize() {
- }
-
- bool DFTSettings::check() const {
- // Ensure that at most one of min or max is set
- STORM_LOG_THROW(!isComputeMinimalValue() || !isComputeMaximalValue(), storm::exceptions::InvalidSettingsException, "Min and max can not both be set.");
- return true;
- }
-
- } // namespace modules
- } // namespace settings
-} // namespace storm
diff --git a/src/storm-dft/settings/modules/DftIOSettings.cpp b/src/storm-dft/settings/modules/DftIOSettings.cpp
new file mode 100644
index 000000000..cf656333d
--- /dev/null
+++ b/src/storm-dft/settings/modules/DftIOSettings.cpp
@@ -0,0 +1,123 @@
+#include "DftIOSettings.h"
+
+#include "storm/settings/SettingsManager.h"
+#include "storm/settings/SettingMemento.h"
+#include "storm/settings/Option.h"
+#include "storm/settings/OptionBuilder.h"
+#include "storm/settings/ArgumentBuilder.h"
+#include "storm/settings/Argument.h"
+#include "storm/exceptions/InvalidSettingsException.h"
+
+namespace storm {
+ namespace settings {
+ namespace modules {
+
+ const std::string DftIOSettings::moduleName = "dftIO";
+ const std::string DftIOSettings::dftFileOptionName = "dftfile";
+ const std::string DftIOSettings::dftFileOptionShortName = "dft";
+ const std::string DftIOSettings::dftJsonFileOptionName = "dftfile-json";
+ const std::string DftIOSettings::dftJsonFileOptionShortName = "dftjson";
+ const std::string DftIOSettings::propExpectedTimeOptionName = "expectedtime";
+ const std::string DftIOSettings::propExpectedTimeOptionShortName = "mttf";
+ const std::string DftIOSettings::propProbabilityOptionName = "probability";
+ const std::string DftIOSettings::propTimeboundOptionName = "timebound";
+ const std::string DftIOSettings::propTimepointsOptionName = "timepoints";
+ const std::string DftIOSettings::minValueOptionName = "min";
+ const std::string DftIOSettings::maxValueOptionName = "max";
+ const std::string DftIOSettings::transformToGspnOptionName = "gspn";
+ const std::string DftIOSettings::exportToJsonOptionName = "export-json";
+
+ DftIOSettings::DftIOSettings() : ModuleSettings(moduleName) {
+ this->addOption(storm::settings::OptionBuilder(moduleName, dftFileOptionName, false, "Parses the model given in the Galileo format.").setShortName(dftFileOptionShortName)
+ .addArgument(storm::settings::ArgumentBuilder::createStringArgument("filename", "The name of the file from which to read the DFT model.").addValidatorString(ArgumentValidatorFactory::createExistingFileValidator()).build()).build());
+ this->addOption(storm::settings::OptionBuilder(moduleName, dftJsonFileOptionName, false, "Parses the model given in the Cytoscape JSON format.").setShortName(dftJsonFileOptionShortName)
+ .addArgument(storm::settings::ArgumentBuilder::createStringArgument("filename", "The name of the JSON file from which to read the DFT model.").addValidatorString(ArgumentValidatorFactory::createExistingFileValidator()).build()).build());
+ this->addOption(storm::settings::OptionBuilder(moduleName, propExpectedTimeOptionName, false, "Compute expected time of system failure.").setShortName(propExpectedTimeOptionShortName).build());
+ this->addOption(storm::settings::OptionBuilder(moduleName, propProbabilityOptionName, false, "Compute probability of system failure.").build());
+ this->addOption(storm::settings::OptionBuilder(moduleName, propTimeboundOptionName, false, "Compute probability of system failure up to given timebound.").addArgument(storm::settings::ArgumentBuilder::createDoubleArgument("time", "The timebound to use.").addValidatorDouble(ArgumentValidatorFactory::createDoubleGreaterValidator(0.0)).build()).build());
+ this->addOption(storm::settings::OptionBuilder(moduleName, propTimepointsOptionName, false, "Compute probability of system failure up to given timebound for a set of given timepoints [starttime, starttime+inc, starttime+2inc, ... ,endtime]").addArgument(storm::settings::ArgumentBuilder::createDoubleArgument("starttime", "The timebound to start from.").addValidatorDouble(ArgumentValidatorFactory::createDoubleGreaterEqualValidator(0.0)).build()).addArgument(storm::settings::ArgumentBuilder::createDoubleArgument("endtime", "The timebound to end with.").addValidatorDouble(ArgumentValidatorFactory::createDoubleGreaterEqualValidator(0.0)).build()).addArgument(storm::settings::ArgumentBuilder::createDoubleArgument("inc", "The value to increment with to get the next timepoint.").addValidatorDouble(ArgumentValidatorFactory::createDoubleGreaterEqualValidator(0.0)).build()).build());
+ this->addOption(storm::settings::OptionBuilder(moduleName, minValueOptionName, false, "Compute minimal value in case of non-determinism.").build());
+ this->addOption(storm::settings::OptionBuilder(moduleName, maxValueOptionName, false, "Compute maximal value in case of non-determinism.").build());
+ this->addOption(storm::settings::OptionBuilder(moduleName, transformToGspnOptionName, false, "Transform DFT to GSPN.").build());
+ this->addOption(storm::settings::OptionBuilder(moduleName, exportToJsonOptionName, false, "Export the model to the Cytoscape JSON format.").addArgument(storm::settings::ArgumentBuilder::createStringArgument("filename", "The name of the JSON file to export to.").build()).build());
+ }
+
+ bool DftIOSettings::isDftFileSet() const {
+ return this->getOption(dftFileOptionName).getHasOptionBeenSet();
+ }
+
+ std::string DftIOSettings::getDftFilename() const {
+ return this->getOption(dftFileOptionName).getArgumentByName("filename").getValueAsString();
+ }
+
+ bool DftIOSettings::isDftJsonFileSet() const {
+ return this->getOption(dftJsonFileOptionName).getHasOptionBeenSet();
+ }
+
+ std::string DftIOSettings::getDftJsonFilename() const {
+ return this->getOption(dftJsonFileOptionName).getArgumentByName("filename").getValueAsString();
+ }
+
+ bool DftIOSettings::usePropExpectedTime() const {
+ return this->getOption(propExpectedTimeOptionName).getHasOptionBeenSet();
+ }
+
+ bool DftIOSettings::usePropProbability() const {
+ return this->getOption(propProbabilityOptionName).getHasOptionBeenSet();
+ }
+
+ bool DftIOSettings::usePropTimebound() const {
+ return this->getOption(propTimeboundOptionName).getHasOptionBeenSet();
+ }
+
+ double DftIOSettings::getPropTimebound() const {
+ return this->getOption(propTimeboundOptionName).getArgumentByName("time").getValueAsDouble();
+ }
+
+ bool DftIOSettings::usePropTimepoints() const {
+ return this->getOption(propTimepointsOptionName).getHasOptionBeenSet();
+ }
+
+ std::vector<double> DftIOSettings::getPropTimepoints() const {
+ double starttime = this->getOption(propTimepointsOptionName).getArgumentByName("starttime").getValueAsDouble();
+ double endtime = this->getOption(propTimepointsOptionName).getArgumentByName("endtime").getValueAsDouble();
+ double inc = this->getOption(propTimepointsOptionName).getArgumentByName("inc").getValueAsDouble();
+ std::vector<double> timepoints;
+ for (double time = starttime; time <= endtime; time += inc) {
+ timepoints.push_back(time);
+ }
+ return timepoints;
+ }
+
+ bool DftIOSettings::isComputeMinimalValue() const {
+ return this->getOption(minValueOptionName).getHasOptionBeenSet();
+ }
+
+ bool DftIOSettings::isComputeMaximalValue() const {
+ return this->getOption(maxValueOptionName).getHasOptionBeenSet();
+ }
+
+ bool DftIOSettings::isTransformToGspn() const {
+ return this->getOption(transformToGspnOptionName).getHasOptionBeenSet();
+ }
+
+ bool DftIOSettings::isExportToJson() const {
+ return this->getOption(exportToJsonOptionName).getHasOptionBeenSet();
+ }
+
+ std::string DftIOSettings::getExportJsonFilename() const {
+ return this->getOption(exportToJsonOptionName).getArgumentByName("filename").getValueAsString();
+ }
+
+ void DftIOSettings::finalize() {
+ }
+
+ bool DftIOSettings::check() const {
+ // Ensure that at most one of min or max is set
+ STORM_LOG_THROW(!isComputeMinimalValue() || !isComputeMaximalValue(), storm::exceptions::InvalidSettingsException, "Min and max can not both be set.");
+ return true;
+ }
+
+ } // namespace modules
+ } // namespace settings
+} // namespace storm
diff --git a/src/storm-dft/settings/modules/DFTSettings.h b/src/storm-dft/settings/modules/DftIOSettings.h
similarity index 63%
rename from src/storm-dft/settings/modules/DFTSettings.h
rename to src/storm-dft/settings/modules/DftIOSettings.h
index c04ef1a23..8a8fbcdd1 100644
--- a/src/storm-dft/settings/modules/DFTSettings.h
+++ b/src/storm-dft/settings/modules/DftIOSettings.h
@@ -1,24 +1,21 @@
#pragma once
-#include "storm-config.h"
#include "storm/settings/modules/ModuleSettings.h"
-#include "storm-dft/builder/DftExplorationHeuristic.h"
-
namespace storm {
namespace settings {
namespace modules {
/*!
- * This class represents the settings for DFT model checking.
+ * This class represents the settings for IO operations concerning DFTs.
*/
- class DFTSettings : public ModuleSettings {
+ class DftIOSettings : public ModuleSettings {
public:
/*!
- * Creates a new set of DFT settings.
+ * Creates a new set of IO settings for DFTs.
*/
- DFTSettings();
+ DftIOSettings();
/*!
* Retrieves whether the dft file option was set.
@@ -48,48 +45,6 @@ namespace storm {
*/
std::string getDftJsonFilename() const;
- /*!
- * Retrieves whether the option to use symmetry reduction is set.
- *
- * @return True iff the option was set.
- */
- bool useSymmetryReduction() const;
-
- /*!
- * Retrieves whether the option to use modularisation is set.
- *
- * @return True iff the option was set.
- */
- bool useModularisation() const;
-
- /*!
- * Retrieves whether the option to disable Dont Care propagation is set.
- *
- * @return True iff the option was set.
- */
- bool isDisableDC() const;
-
- /*!
- * Retrieves whether the option to compute an approximation is set.
- *
- * @return True iff the option was set.
- */
- bool isApproximationErrorSet() const;
-
- /*!
- * Retrieves the relative error allowed for approximating the model checking result.
- *
- * @return The allowed errorbound.
- */
- double getApproximationError() const;
-
- /*!
- * Retrieves the heuristic used for approximation.
- *
- * @return The heuristic to use.
- */
- storm::builder::ApproximationHeuristic getApproximationHeuristic() const;
-
/*!
* Retrieves whether the property expected time should be used.
*
@@ -146,13 +101,6 @@ namespace storm {
*/
bool isComputeMaximalValue() const;
- /*!
- * Retrieves whether the non-determinism should be avoided by always taking the first possible dependency.
- *
- * @return True iff the option was set.
- */
- bool isTakeFirstDependency() const;
-
/*!
* Retrieves whether the DFT should be transformed into a GSPN.
*
@@ -174,15 +122,6 @@ namespace storm {
*/
std::string getExportJsonFilename() const;
-#ifdef STORM_HAVE_Z3
- /*!
- * Retrieves whether the DFT should be checked via SMT.
- *
- * @return True iff the option was set.
- */
- bool solveWithSMT() const;
-#endif
-
bool check() const override;
void finalize() override;
@@ -195,13 +134,6 @@ namespace storm {
static const std::string dftFileOptionShortName;
static const std::string dftJsonFileOptionName;
static const std::string dftJsonFileOptionShortName;
- static const std::string symmetryReductionOptionName;
- static const std::string symmetryReductionOptionShortName;
- static const std::string modularisationOptionName;
- static const std::string disableDCOptionName;
- static const std::string approximationErrorOptionName;
- static const std::string approximationErrorOptionShortName;
- static const std::string approximationHeuristicOptionName;
static const std::string propExpectedTimeOptionName;
static const std::string propExpectedTimeOptionShortName;
static const std::string propProbabilityOptionName;
@@ -209,10 +141,6 @@ namespace storm {
static const std::string propTimepointsOptionName;
static const std::string minValueOptionName;
static const std::string maxValueOptionName;
- static const std::string firstDependencyOptionName;
-#ifdef STORM_HAVE_Z3
- static const std::string solveWithSmtOptionName;
-#endif
static const std::string transformToGspnOptionName;
static const std::string exportToJsonOptionName;
diff --git a/src/storm-dft/settings/modules/FaultTreeSettings.cpp b/src/storm-dft/settings/modules/FaultTreeSettings.cpp
new file mode 100644
index 000000000..7c9ef14af
--- /dev/null
+++ b/src/storm-dft/settings/modules/FaultTreeSettings.cpp
@@ -0,0 +1,93 @@
+#include "FaultTreeSettings.h"
+
+#include "storm/settings/SettingsManager.h"
+#include "storm/settings/SettingMemento.h"
+#include "storm/settings/Option.h"
+#include "storm/settings/OptionBuilder.h"
+#include "storm/settings/ArgumentBuilder.h"
+#include "storm/settings/Argument.h"
+#include "storm/exceptions/IllegalArgumentValueException.h"
+
+namespace storm {
+ namespace settings {
+ namespace modules {
+
+ const std::string FaultTreeSettings::moduleName = "dft";
+ const std::string FaultTreeSettings::symmetryReductionOptionName = "symmetryreduction";
+ const std::string FaultTreeSettings::symmetryReductionOptionShortName = "symred";
+ const std::string FaultTreeSettings::modularisationOptionName = "modularisation";
+ const std::string FaultTreeSettings::disableDCOptionName = "disabledc";
+ const std::string FaultTreeSettings::approximationErrorOptionName = "approximation";
+ const std::string FaultTreeSettings::approximationErrorOptionShortName = "approx";
+ const std::string FaultTreeSettings::approximationHeuristicOptionName = "approximationheuristic";
+ const std::string FaultTreeSettings::firstDependencyOptionName = "firstdep";
+#ifdef STORM_HAVE_Z3
+ const std::string FaultTreeSettings::solveWithSmtOptionName = "smt";
+#endif
+
+ FaultTreeSettings::FaultTreeSettings() : ModuleSettings(moduleName) {
+ this->addOption(storm::settings::OptionBuilder(moduleName, symmetryReductionOptionName, false, "Exploit symmetric structure of model.").setShortName(symmetryReductionOptionShortName).build());
+ this->addOption(storm::settings::OptionBuilder(moduleName, modularisationOptionName, false, "Use modularisation (not applicable for expected time).").build());
+ this->addOption(storm::settings::OptionBuilder(moduleName, disableDCOptionName, false, "Disable Dont Care propagation.").build());
+ this->addOption(storm::settings::OptionBuilder(moduleName, firstDependencyOptionName, false, "Avoid non-determinism by always taking the first possible dependency.").build());
+ this->addOption(storm::settings::OptionBuilder(moduleName, approximationErrorOptionName, false, "Approximation error allowed.").setShortName(approximationErrorOptionShortName).addArgument(storm::settings::ArgumentBuilder::createDoubleArgument("error", "The relative approximation error to use.").addValidatorDouble(ArgumentValidatorFactory::createDoubleGreaterEqualValidator(0.0)).build()).build());
+ this->addOption(storm::settings::OptionBuilder(moduleName, approximationHeuristicOptionName, false, "Set the heuristic used for approximation.").addArgument(storm::settings::ArgumentBuilder::createStringArgument("heuristic", "Sets which heuristic is used for approximation. Must be in {depth, probability}. Default is").setDefaultValueString("depth").addValidatorString(ArgumentValidatorFactory::createMultipleChoiceValidator({"depth", "rateratio"})).build()).build());
+#ifdef STORM_HAVE_Z3
+ this->addOption(storm::settings::OptionBuilder(moduleName, solveWithSmtOptionName, true, "Solve the DFT with SMT.").build());
+#endif
+ }
+
+ bool FaultTreeSettings::useSymmetryReduction() const {
+ return this->getOption(symmetryReductionOptionName).getHasOptionBeenSet();
+ }
+
+ bool FaultTreeSettings::useModularisation() const {
+ return this->getOption(modularisationOptionName).getHasOptionBeenSet();
+ }
+
+ bool FaultTreeSettings::isDisableDC() const {
+ return this->getOption(disableDCOptionName).getHasOptionBeenSet();
+ }
+
+ bool FaultTreeSettings::isApproximationErrorSet() const {
+ return this->getOption(approximationErrorOptionName).getHasOptionBeenSet();
+ }
+
+ double FaultTreeSettings::getApproximationError() const {
+ return this->getOption(approximationErrorOptionName).getArgumentByName("error").getValueAsDouble();
+ }
+
+ storm::builder::ApproximationHeuristic FaultTreeSettings::getApproximationHeuristic() const {
+ if (!isApproximationErrorSet() || getApproximationError() == 0.0) {
+ // No approximation is done
+ return storm::builder::ApproximationHeuristic::NONE;
+ }
+ std::string heuristicAsString = this->getOption(approximationHeuristicOptionName).getArgumentByName("heuristic").getValueAsString();
+ if (heuristicAsString == "depth") {
+ return storm::builder::ApproximationHeuristic::DEPTH;
+ } else if (heuristicAsString == "probability") {
+ return storm::builder::ApproximationHeuristic::PROBABILITY;
+ }
+ STORM_LOG_THROW(false, storm::exceptions::IllegalArgumentValueException, "Illegal value '" << heuristicAsString << "' set as heuristic for approximation.");
+ }
+
+ bool FaultTreeSettings::isTakeFirstDependency() const {
+ return this->getOption(firstDependencyOptionName).getHasOptionBeenSet();
+ }
+
+#ifdef STORM_HAVE_Z3
+ bool FaultTreeSettings::solveWithSMT() const {
+ return this->getOption(solveWithSmtOptionName).getHasOptionBeenSet();
+ }
+#endif
+
+ void FaultTreeSettings::finalize() {
+ }
+
+ bool FaultTreeSettings::check() const {
+ return true;
+ }
+
+ } // namespace modules
+ } // namespace settings
+} // namespace storm
diff --git a/src/storm-dft/settings/modules/FaultTreeSettings.h b/src/storm-dft/settings/modules/FaultTreeSettings.h
new file mode 100644
index 000000000..171d5c38e
--- /dev/null
+++ b/src/storm-dft/settings/modules/FaultTreeSettings.h
@@ -0,0 +1,104 @@
+#pragma once
+
+#include "storm/settings/modules/ModuleSettings.h"
+#include "storm-dft/builder/DftExplorationHeuristic.h"
+#include "storm-config.h"
+
+namespace storm {
+ namespace settings {
+ namespace modules {
+
+ /*!
+ * This class represents the settings for DFT model checking.
+ */
+ class FaultTreeSettings : public ModuleSettings {
+ public:
+
+ /*!
+ * Creates a new set of DFT settings.
+ */
+ FaultTreeSettings();
+
+ /*!
+ * Retrieves whether the option to use symmetry reduction is set.
+ *
+ * @return True iff the option was set.
+ */
+ bool useSymmetryReduction() const;
+
+ /*!
+ * Retrieves whether the option to use modularisation is set.
+ *
+ * @return True iff the option was set.
+ */
+ bool useModularisation() const;
+
+ /*!
+ * Retrieves whether the option to disable Dont Care propagation is set.
+ *
+ * @return True iff the option was set.
+ */
+ bool isDisableDC() const;
+
+ /*!
+ * Retrieves whether the option to compute an approximation is set.
+ *
+ * @return True iff the option was set.
+ */
+ bool isApproximationErrorSet() const;
+
+ /*!
+ * Retrieves the relative error allowed for approximating the model checking result.
+ *
+ * @return The allowed errorbound.
+ */
+ double getApproximationError() const;
+
+ /*!
+ * Retrieves the heuristic used for approximation.
+ *
+ * @return The heuristic to use.
+ */
+ storm::builder::ApproximationHeuristic getApproximationHeuristic() const;
+
+ /*!
+ * Retrieves whether the non-determinism should be avoided by always taking the first possible dependency.
+ *
+ * @return True iff the option was set.
+ */
+ bool isTakeFirstDependency() const;
+
+#ifdef STORM_HAVE_Z3
+ /*!
+ * Retrieves whether the DFT should be checked via SMT.
+ *
+ * @return True iff the option was set.
+ */
+ bool solveWithSMT() const;
+#endif
+
+ bool check() const override;
+ void finalize() override;
+
+ // The name of the module.
+ static const std::string moduleName;
+
+ private:
+ // Define the string names of the options as constants.
+ static const std::string symmetryReductionOptionName;
+ static const std::string symmetryReductionOptionShortName;
+ static const std::string modularisationOptionName;
+ static const std::string disableDCOptionName;
+ static const std::string approximationErrorOptionName;
+ static const std::string approximationErrorOptionShortName;
+ static const std::string approximationHeuristicOptionName;
+ static const std::string firstDependencyOptionName;
+#ifdef STORM_HAVE_Z3
+ static const std::string solveWithSmtOptionName;
+#endif
+
+ };
+
+ } // namespace modules
+ } // namespace settings
+} // namespace storm
diff --git a/src/storm-pars-cli/CMakeLists.txt b/src/storm-pars-cli/CMakeLists.txt
index bda5ad6c2..9e2f6f315 100644
--- a/src/storm-pars-cli/CMakeLists.txt
+++ b/src/storm-pars-cli/CMakeLists.txt
@@ -1,6 +1,6 @@
# Create storm-pars.
add_executable(storm-pars-cli ${PROJECT_SOURCE_DIR}/src/storm-pars-cli/storm-pars.cpp)
-target_link_libraries(storm-pars-cli storm-pars) # Adding headers for xcode
+target_link_libraries(storm-pars-cli storm-pars storm-cli-utilities) # Adding headers for xcode
set_target_properties(storm-pars-cli PROPERTIES OUTPUT_NAME "storm-pars")
add_dependencies(binaries storm-pars-cli)
diff --git a/src/storm-pars-cli/storm-pars.cpp b/src/storm-pars-cli/storm-pars.cpp
index 5fa744c59..907688ef4 100644
--- a/src/storm-pars-cli/storm-pars.cpp
+++ b/src/storm-pars-cli/storm-pars.cpp
@@ -7,6 +7,7 @@
#include "storm/settings/SettingsManager.h"
#include "storm/api/storm.h"
#include "storm-cli-utilities/cli.h"
+#include "storm-cli-utilities/model-handling.h"
#include "storm/models/ModelBase.h"
#include "storm/storage/SymbolicModelDescription.h"
#include "storm/utility/file.h"
@@ -23,8 +24,6 @@
#include "storm/exceptions/InvalidSettingsException.h"
#include "storm/exceptions/NotSupportedException.h"
-#include "storm-cli-utilities/cli.cpp"
-
namespace storm {
namespace pars {
diff --git a/src/storm-pars/modelchecker/region/RegionModelChecker.cpp b/src/storm-pars/modelchecker/region/RegionModelChecker.cpp
index 23ba29489..ab0142d0b 100644
--- a/src/storm-pars/modelchecker/region/RegionModelChecker.cpp
+++ b/src/storm-pars/modelchecker/region/RegionModelChecker.cpp
@@ -17,6 +17,7 @@
#include "storm/settings/SettingsManager.h"
#include "storm/settings/modules/CoreSettings.h"
+#include "storm/exceptions/NotImplementedException.h"
namespace storm {
@@ -43,6 +44,12 @@ namespace storm {
return std::make_unique<storm::modelchecker::RegionCheckResult<ParametricType>>(std::move(result));
}
+ template <typename ParametricType>
+ ParametricType RegionModelChecker<ParametricType>::getBoundAtInitState(storm::storage::ParameterRegion<ParametricType> const& region, storm::solver::OptimizationDirection const& dirForParameters) {
+ STORM_LOG_THROW(false, storm::exceptions::NotImplementedException, "The selected region model checker does not support this functionality.");
+ return storm::utility::zero<ParametricType>();
+ }
+
template <typename ParametricType>
std::unique_ptr<storm::modelchecker::RegionRefinementCheckResult<ParametricType>> RegionModelChecker<ParametricType>::performRegionRefinement(storm::storage::ParameterRegion<ParametricType> const& region, boost::optional<ParametricType> const& coverageThreshold, boost::optional<uint64_t> depthThreshold, RegionResultHypothesis const& hypothesis) {
STORM_LOG_INFO("Applying refinement on region: " << region.toString(true) << " .");
diff --git a/src/storm-pars/modelchecker/region/RegionModelChecker.h b/src/storm-pars/modelchecker/region/RegionModelChecker.h
index c1a558800..595d1e8f0 100644
--- a/src/storm-pars/modelchecker/region/RegionModelChecker.h
+++ b/src/storm-pars/modelchecker/region/RegionModelChecker.h
@@ -42,6 +42,8 @@ namespace storm {
*/
std::unique_ptr<storm::modelchecker::RegionCheckResult<ParametricType>> analyzeRegions(std::vector<storm::storage::ParameterRegion<ParametricType>> const& regions, std::vector<RegionResultHypothesis> const& hypotheses, bool sampleVerticesOfRegion = false) ;
+ virtual ParametricType getBoundAtInitState(storm::storage::ParameterRegion<ParametricType> const& region, storm::solver::OptimizationDirection const& dirForParameters);
+
/*!
* Iteratively refines the region until the region analysis yields a conclusive result (AllSat or AllViolated).
* @param region the considered region
diff --git a/src/storm-pars/modelchecker/region/SparseDtmcParameterLiftingModelChecker.cpp b/src/storm-pars/modelchecker/region/SparseDtmcParameterLiftingModelChecker.cpp
index 119e3791d..8ac2bdea8 100644
--- a/src/storm-pars/modelchecker/region/SparseDtmcParameterLiftingModelChecker.cpp
+++ b/src/storm-pars/modelchecker/region/SparseDtmcParameterLiftingModelChecker.cpp
@@ -6,6 +6,8 @@
#include "storm/modelchecker/propositional/SparsePropositionalModelChecker.h"
#include "storm/modelchecker/results/ExplicitQualitativeCheckResult.h"
#include "storm/modelchecker/results/ExplicitQuantitativeCheckResult.h"
+#include "storm/modelchecker/prctl/helper/DsMpiUpperRewardBoundsComputer.h"
+#include "storm/modelchecker/prctl/helper/BaierUpperRewardBoundsComputer.h"
#include "storm/models/sparse/Dtmc.h"
#include "storm/models/sparse/StandardRewardModel.h"
#include "storm/solver/StandardMinMaxLinearEquationSolver.h"
@@ -17,6 +19,8 @@
#include "storm/exceptions/InvalidPropertyException.h"
#include "storm/exceptions/NotSupportedException.h"
#include "storm/exceptions/UnexpectedException.h"
+#include "storm/exceptions/UncheckedRequirementException.h"
+
namespace storm {
namespace modelchecker {
@@ -27,7 +31,7 @@ namespace storm {
}
template <typename SparseModelType, typename ConstantType>
- SparseDtmcParameterLiftingModelChecker<SparseModelType, ConstantType>::SparseDtmcParameterLiftingModelChecker(std::unique_ptr<storm::solver::MinMaxLinearEquationSolverFactory<ConstantType>>&& solverFactory) : solverFactory(std::move(solverFactory)) {
+ SparseDtmcParameterLiftingModelChecker<SparseModelType, ConstantType>::SparseDtmcParameterLiftingModelChecker(std::unique_ptr<storm::solver::MinMaxLinearEquationSolverFactory<ConstantType>>&& solverFactory) : solverFactory(std::move(solverFactory)), solvingRequiresUpperRewardBounds(false) {
// Intentionally left empty
}
@@ -109,6 +113,8 @@ namespace storm {
// We know some bounds for the results so set them
lowerResultBound = storm::utility::zero<ConstantType>();
upperResultBound = storm::utility::one<ConstantType>();
+ // No requirements for bounded formulas
+ solverFactory->setRequirementsChecked(true);
}
template <typename SparseModelType, typename ConstantType>
@@ -139,6 +145,12 @@ namespace storm {
// We know some bounds for the results so set them
lowerResultBound = storm::utility::zero<ConstantType>();
upperResultBound = storm::utility::one<ConstantType>();
+
+ auto req = solverFactory->getRequirements(storm::solver::EquationSystemType::UntilProbabilities);
+ req.clearBounds();
+ req.clearNoEndComponents(); // We never have end components within the maybestates (assuming graph-preserving instantiations).
+ STORM_LOG_THROW(req.empty(), storm::exceptions::UncheckedRequirementException, "Unchecked solver requirement.");
+ solverFactory->setRequirementsChecked(true);
}
template <typename SparseModelType, typename ConstantType>
@@ -172,6 +184,17 @@ namespace storm {
// We only know a lower bound for the result
lowerResultBound = storm::utility::zero<ConstantType>();
+
+ auto req = solverFactory->getRequirements(storm::solver::EquationSystemType::ReachabilityRewards);
+ req.clearNoEndComponents(); // We never have end components within the maybestates (assuming graph-preserving instantiations).
+ req.clearLowerBounds();
+ if (req.requiresUpperBounds()) {
+ solvingRequiresUpperRewardBounds = true;
+ req.clearUpperBounds();
+ }
+ STORM_LOG_THROW(req.empty(), storm::exceptions::UncheckedRequirementException, "Unchecked solver requirement.");
+ solverFactory->setRequirementsChecked(true);
+
}
@@ -200,6 +223,9 @@ namespace storm {
// We only know a lower bound for the result
lowerResultBound = storm::utility::zero<ConstantType>();
+
+ // No requirements for bounded reward formula
+ solverFactory->setRequirementsChecked(true);
}
template <typename SparseModelType, typename ConstantType>
@@ -228,7 +254,23 @@ namespace storm {
}
auto solver = solverFactory->create(parameterLifter->getMatrix());
if (lowerResultBound) solver->setLowerBound(lowerResultBound.get());
- if (upperResultBound) solver->setUpperBound(upperResultBound.get());
+ if (upperResultBound) {
+ solver->setUpperBound(upperResultBound.get());
+ } else if (solvingRequiresUpperRewardBounds) {
+ // For the min-case, we use DS-MPI, for the max-case variant 2 of the Baier et al. paper (CAV'17).
+ std::vector<ConstantType> oneStepProbs;
+ oneStepProbs.reserve(parameterLifter->getMatrix().getRowCount());
+ for (uint64_t row = 0; row < parameterLifter->getMatrix().getRowCount(); ++row) {
+ oneStepProbs.push_back(storm::utility::one<ConstantType>() - parameterLifter->getMatrix().getRowSum(row));
+ }
+ if (dirForParameters == storm::OptimizationDirection::Minimize) {
+ storm::modelchecker::helper::DsMpiMdpUpperRewardBoundsComputer<ConstantType> dsmpi(parameterLifter->getMatrix(), parameterLifter->getVector(), oneStepProbs);
+ solver->setUpperBounds(dsmpi.computeUpperBounds());
+ } else {
+ storm::modelchecker::helper::BaierUpperRewardBoundsComputer<ConstantType> baier(parameterLifter->getMatrix(), parameterLifter->getVector(), oneStepProbs);
+ solver->setUpperBound(baier.computeUpperBound());
+ }
+ }
if (!stepBound) solver->setTrackScheduler(true);
if (storm::solver::minimize(dirForParameters) && minSchedChoices && !stepBound) solver->setInitialScheduler(std::move(minSchedChoices.get()));
if (storm::solver::maximize(dirForParameters) && maxSchedChoices && !stepBound) solver->setInitialScheduler(std::move(maxSchedChoices.get()));
@@ -247,7 +289,7 @@ namespace storm {
}
// Invoke the solver
- if(stepBound) {
+ if (stepBound) {
assert(*stepBound > 0);
x = std::vector<ConstantType>(maybeStates.getNumberOfSetBits(), storm::utility::zero<ConstantType>());
solver->repeatedMultiply(dirForParameters, x, ¶meterLifter->getVector(), *stepBound);
diff --git a/src/storm-pars/modelchecker/region/SparseDtmcParameterLiftingModelChecker.h b/src/storm-pars/modelchecker/region/SparseDtmcParameterLiftingModelChecker.h
index d6f51032b..b4a8644b6 100644
--- a/src/storm-pars/modelchecker/region/SparseDtmcParameterLiftingModelChecker.h
+++ b/src/storm-pars/modelchecker/region/SparseDtmcParameterLiftingModelChecker.h
@@ -12,7 +12,6 @@
#include "storm/solver/MinMaxLinearEquationSolver.h"
#include "storm/logic/FragmentSpecification.h"
-
namespace storm {
namespace modelchecker {
@@ -49,12 +48,13 @@ namespace storm {
storm::storage::BitVector maybeStates;
std::vector<ConstantType> resultsForNonMaybeStates;
boost::optional<uint_fast64_t> stepBound;
-
+
std::unique_ptr<storm::modelchecker::SparseDtmcInstantiationModelChecker<SparseModelType, ConstantType>> instantiationChecker;
-
+
std::unique_ptr<storm::transformer::ParameterLifter<typename SparseModelType::ValueType, ConstantType>> parameterLifter;
std::unique_ptr<storm::solver::MinMaxLinearEquationSolverFactory<ConstantType>> solverFactory;
-
+ bool solvingRequiresUpperRewardBounds;
+
// Results from the most recent solver call.
boost::optional<std::vector<uint_fast64_t>> minSchedChoices, maxSchedChoices;
std::vector<ConstantType> x;
diff --git a/src/storm-pars/modelchecker/region/SparseParameterLiftingModelChecker.cpp b/src/storm-pars/modelchecker/region/SparseParameterLiftingModelChecker.cpp
index d0b2af22b..1accd68cc 100644
--- a/src/storm-pars/modelchecker/region/SparseParameterLiftingModelChecker.cpp
+++ b/src/storm-pars/modelchecker/region/SparseParameterLiftingModelChecker.cpp
@@ -4,6 +4,7 @@
#include "storm/logic/FragmentSpecification.h"
#include "storm/modelchecker/results/ExplicitQuantitativeCheckResult.h"
#include "storm/modelchecker/results/ExplicitQualitativeCheckResult.h"
+#include "storm/utility/vector.h"
#include "storm/models/sparse/Dtmc.h"
#include "storm/models/sparse/Mdp.h"
#include "storm/models/sparse/StandardRewardModel.h"
@@ -130,6 +131,18 @@ namespace storm {
}
}
+ template <typename SparseModelType, typename ConstantType>
+ std::unique_ptr<QuantitativeCheckResult<ConstantType>> SparseParameterLiftingModelChecker<SparseModelType, ConstantType>::getBound(storm::storage::ParameterRegion<typename SparseModelType::ValueType> const& region, storm::solver::OptimizationDirection const& dirForParameters) {
+ STORM_LOG_WARN_COND(this->currentCheckTask->getFormula().hasQuantitativeResult(), "Computing quantitative bounds for a qualitative formula...");
+ return std::make_unique<ExplicitQuantitativeCheckResult<ConstantType>>(std::move(computeQuantitativeValues(region, dirForParameters)->template asExplicitQuantitativeCheckResult<ConstantType>()));
+ }
+
+ template <typename SparseModelType, typename ConstantType>
+ typename SparseModelType::ValueType SparseParameterLiftingModelChecker<SparseModelType, ConstantType>::getBoundAtInitState(storm::storage::ParameterRegion<typename SparseModelType::ValueType> const& region, storm::solver::OptimizationDirection const& dirForParameters) {
+ STORM_LOG_THROW(this->parametricModel->getInitialStates().getNumberOfSetBits() == 1, storm::exceptions::NotSupportedException, "Getting a bound at the initial state requires a model with a single initial state.");
+ return storm::utility::convertNumber<typename SparseModelType::ValueType>(getBound(region, dirForParameters)->template asExplicitQuantitativeCheckResult<ConstantType>()[*this->parametricModel->getInitialStates().begin()]);
+ }
+
template <typename SparseModelType, typename ConstantType>
SparseModelType const& SparseParameterLiftingModelChecker<SparseModelType, ConstantType>::getConsideredParametricModel() const {
return *parametricModel;
diff --git a/src/storm-pars/modelchecker/region/SparseParameterLiftingModelChecker.h b/src/storm-pars/modelchecker/region/SparseParameterLiftingModelChecker.h
index e0cabd5f0..cb993ad4f 100644
--- a/src/storm-pars/modelchecker/region/SparseParameterLiftingModelChecker.h
+++ b/src/storm-pars/modelchecker/region/SparseParameterLiftingModelChecker.h
@@ -45,6 +45,9 @@ namespace storm {
*/
std::unique_ptr<CheckResult> check(storm::storage::ParameterRegion<typename SparseModelType::ValueType> const& region, storm::solver::OptimizationDirection const& dirForParameters);
+ std::unique_ptr<QuantitativeCheckResult<ConstantType>> getBound(storm::storage::ParameterRegion<typename SparseModelType::ValueType> const& region, storm::solver::OptimizationDirection const& dirForParameters);
+ virtual typename SparseModelType::ValueType getBoundAtInitState(storm::storage::ParameterRegion<typename SparseModelType::ValueType> const& region, storm::solver::OptimizationDirection const& dirForParameters) override;
+
SparseModelType const& getConsideredParametricModel() const;
CheckTask<storm::logic::Formula, ConstantType> const& getCurrentCheckTask() const;
diff --git a/src/storm/analysis/GraphConditions.cpp b/src/storm/analysis/GraphConditions.cpp
index be8073bf7..663bf2b52 100644
--- a/src/storm/analysis/GraphConditions.cpp
+++ b/src/storm/analysis/GraphConditions.cpp
@@ -35,6 +35,8 @@ namespace storm {
void ConstraintCollector<ValueType>::wellformedRequiresNonNegativeEntries(std::vector<ValueType> const& vec) {
for(auto const& entry : vec) {
if (!storm::utility::isConstant(entry)) {
+ auto const& transitionVars = entry.gatherVariables();
+ variableSet.insert(transitionVars.begin(), transitionVars.end());
if (entry.denominator().isConstant()) {
if (entry.denominatorAsNumber() > 0) {
wellformedConstraintSet.emplace(entry.nominator().polynomialWithCoefficient(), storm::CompareRelation::GEQ);
diff --git a/src/storm/builder/jit/ExplicitJitJaniModelBuilder.cpp b/src/storm/builder/jit/ExplicitJitJaniModelBuilder.cpp
index 54779b96a..245e9d54d 100644
--- 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)
diff --git a/src/storm/modelchecker/prctl/helper/DsMpiUpperRewardBoundsComputer.h b/src/storm/modelchecker/prctl/helper/DsMpiUpperRewardBoundsComputer.h
index f54c810fb..7f2bb4278 100644
--- a/src/storm/modelchecker/prctl/helper/DsMpiUpperRewardBoundsComputer.h
+++ b/src/storm/modelchecker/prctl/helper/DsMpiUpperRewardBoundsComputer.h
@@ -1,6 +1,7 @@
#pragma once
#include <vector>
+#include <cstdint>
namespace storm {
namespace storage {
diff --git a/src/storm/models/sparse/MarkovAutomaton.cpp b/src/storm/models/sparse/MarkovAutomaton.cpp
index 485aa8a64..ca79ccfac 100644
--- a/src/storm/models/sparse/MarkovAutomaton.cpp
+++ b/src/storm/models/sparse/MarkovAutomaton.cpp
@@ -50,7 +50,9 @@ namespace storm {
if (components.exitRates) {
exitRates = std::move(components.exitRates.get());
- } else {
+ }
+
+ if (components.rateTransitions) {
this->turnRatesToProbabilities();
}
closed = this->checkIsClosed();
@@ -150,7 +152,7 @@ namespace storm {
uint_fast64_t row = this->getTransitionMatrix().getRowGroupIndices()[state];
if (this->markovianStates.get(state)) {
if (assertRates) {
- STORM_LOG_THROW(this->exitRates[state] == this->getTransitionMatrix().getRowSum(row), storm::exceptions::InvalidArgumentException, "The specified exit rate is inconsistent with the rate matrix. Difference is " << (this->exitRates[state] - this->getTransitionMatrix().getRowSum(row)) << ".");
+ STORM_LOG_THROW(this->exitRates[state] == this->getTransitionMatrix().getRowSum(row), storm::exceptions::InvalidArgumentException, "The specified exit rate is inconsistent with the rate matrix. Difference is " << (this->exitRates[state] - this->getTransitionMatrix().getRowSum(row)) << ".");
} else {
this->exitRates.push_back(this->getTransitionMatrix().getRowSum(row));
}
@@ -159,7 +161,11 @@ namespace storm {
}
++row;
} else {
- this->exitRates.push_back(storm::utility::zero<ValueType>());
+ if (assertRates) {
+ STORM_LOG_THROW(storm::utility::isZero<ValueType>(this->exitRates[state]), storm::exceptions::InvalidArgumentException, "The specified exit rate for (non-Markovian) choice should be 0.");
+ } else {
+ this->exitRates.push_back(storm::utility::zero<ValueType>());
+ }
}
for (; row < this->getTransitionMatrix().getRowGroupIndices()[state+1]; ++row) {
STORM_LOG_THROW(storm::utility::isOne(this->getTransitionMatrix().getRowSum(row)), storm::exceptions::InvalidArgumentException, "Entries of transition matrix do not sum up to one for (non-Markovian) choice " << row << " of state " << state << " (sum is " << this->getTransitionMatrix().getRowSum(row) << ").");
diff --git a/src/storm/models/sparse/MarkovAutomaton.h b/src/storm/models/sparse/MarkovAutomaton.h
index 249766b62..89c73f83c 100644
--- a/src/storm/models/sparse/MarkovAutomaton.h
+++ b/src/storm/models/sparse/MarkovAutomaton.h
@@ -22,7 +22,7 @@ namespace storm {
* For hybrid states (i.e., states with Markovian and probabilistic transitions), it is assumed that the first
* choice corresponds to the markovian transitions.
*
- * @param transitionMatrix The matrix representing the transitions in the model in terms of rates (markocian choices) and probabilities (probabilistic choices).
+ * @param transitionMatrix The matrix representing the transitions in the model in terms of rates (Markovian choices) and probabilities (probabilistic choices).
* @param stateLabeling The labeling of the states.
* @param markovianStates A bit vector indicating the Markovian states of the automaton (i.e., states with at least one markovian transition).
* @param rewardModels A mapping of reward model names to reward models.
@@ -38,7 +38,7 @@ namespace storm {
* For hybrid states (i.e., states with Markovian and probabilistic transitions), it is assumed that the first
* choice corresponds to the markovian transitions.
*
- * @param transitionMatrix The matrix representing the transitions in the model in terms of rates (markocian choices) and probabilities (probabilistic choices).
+ * @param transitionMatrix The matrix representing the transitions in the model in terms of rates (Markovian choices) and probabilities (probabilistic choices).
* @param stateLabeling The labeling of the states.
* @param markovianStates A bit vector indicating the Markovian states of the automaton (i.e., states with at least one markovian transition).
* @param rewardModels A mapping of reward model names to reward models.
diff --git a/src/storm/parser/DirectEncodingParser.cpp b/src/storm/parser/DirectEncodingParser.cpp
index c18d1965c..45768f908 100644
--- a/src/storm/parser/DirectEncodingParser.cpp
+++ b/src/storm/parser/DirectEncodingParser.cpp
@@ -3,6 +3,9 @@
#include <iostream>
#include <string>
+#include <boost/algorithm/string.hpp>
+#include <boost/algorithm/string/predicate.hpp>
+
#include "storm/models/sparse/MarkovAutomaton.h"
#include "storm/models/sparse/Ctmc.h"
@@ -18,6 +21,7 @@
#include "storm/utility/macros.h"
#include "storm/utility/file.h"
+
namespace storm {
namespace parser {
@@ -58,46 +62,62 @@ namespace storm {
// Initialize
ValueParser<ValueType> valueParser;
+ bool sawType = false;
+ bool sawParameters = false;
+ size_t nrStates = 0;
+ storm::models::ModelType type;
+
+ std::vector<std::string> rewardModelNames;
+
+ std::shared_ptr<storm::storage::sparse::ModelComponents<ValueType, RewardModelType>> modelComponents;
// Parse header
- std::getline(file, line);
- STORM_LOG_THROW(line == "// Exported by storm", storm::exceptions::WrongFormatException, "Expected header information.");
- std::getline(file, line);
- STORM_LOG_THROW(boost::starts_with(line, "// Original model type: "), storm::exceptions::WrongFormatException, "Expected header information.");
- // Parse model type
- std::getline(file, line);
- STORM_LOG_THROW(boost::starts_with(line, "@type: "), storm::exceptions::WrongFormatException, "Expected model type.");
- storm::models::ModelType type = storm::models::getModelType(line.substr(7));
- STORM_LOG_TRACE("Model type: " << type);
- STORM_LOG_THROW(type != storm::models::ModelType::MarkovAutomaton, storm::exceptions::NotSupportedException, "Markov Automata in DRN format are not supported (unclear indication of Markovian Choices in DRN format)");
- STORM_LOG_THROW(type != storm::models::ModelType::S2pg, storm::exceptions::NotSupportedException, "Stochastic Two Player Games in DRN format are not supported.");
-
- // Parse parameters
- std::getline(file, line);
- STORM_LOG_THROW(line == "@parameters", storm::exceptions::WrongFormatException, "Expected parameter declaration.");
- std::getline(file, line);
- if (line != "") {
- std::vector<std::string> parameters;
- boost::split(parameters, line, boost::is_any_of(" "));
- for (std::string parameter : parameters) {
- STORM_LOG_TRACE("New parameter: " << parameter);
- valueParser.addParameter(parameter);
+ while(std::getline(file, line)) {
+ if(line.empty() || boost::starts_with(line, "//")) {
+ continue;
}
- }
- // Parse no. states
- std::getline(file, line);
- STORM_LOG_THROW(line == "@nr_states", storm::exceptions::WrongFormatException, "Expected number of states.");
- std::getline(file, line);
- size_t nrStates = boost::lexical_cast<size_t>(line);
- STORM_LOG_TRACE("Model type: " << type);
+ if (boost::starts_with(line, "@type: ")) {
+ STORM_LOG_THROW(!sawType, storm::exceptions::WrongFormatException, "Type declared twice");
+ type = storm::models::getModelType(line.substr(7));
+ STORM_LOG_TRACE("Model type: " << type);
+ STORM_LOG_THROW(type != storm::models::ModelType::MarkovAutomaton, storm::exceptions::NotSupportedException, "Markov Automata in DRN format are not supported (unclear indication of Markovian Choices in DRN format)");
+ STORM_LOG_THROW(type != storm::models::ModelType::S2pg, storm::exceptions::NotSupportedException, "Stochastic Two Player Games in DRN format are not supported.");
+ sawType = true;
+ }
+ if(line == "@parameters") {
+ std::getline(file, line);
+ if (line != "") {
+ std::vector<std::string> parameters;
+ boost::split(parameters, line, boost::is_any_of(" "));
+ for (std::string parameter : parameters) {
+ STORM_LOG_TRACE("New parameter: " << parameter);
+ valueParser.addParameter(parameter);
+ }
+ }
+ sawParameters = true;
+ }
+ if(line == "@reward_models") {
+ STORM_LOG_THROW(rewardModelNames.size() == 0, storm::exceptions::WrongFormatException, "Reward model names declared twice");
+ std::getline(file, line);
+ boost::split(rewardModelNames, line, boost::is_any_of("\t "));
+ }
+ if(line == "@nr_states") {
+ STORM_LOG_THROW(nrStates == 0, storm::exceptions::WrongFormatException, "Number states declared twice");
+ std::getline(file, line);
+ nrStates = boost::lexical_cast<size_t>(line);
- std::getline(file, line);
- STORM_LOG_THROW(line == "@model", storm::exceptions::WrongFormatException, "Expected model declaration.");
+ }
+ if(line == "@model") {
+ STORM_LOG_THROW(sawType, storm::exceptions::WrongFormatException, "Type has to be declared before model.");
+ STORM_LOG_THROW(sawParameters, storm::exceptions::WrongFormatException, "Parameters have to be declared before model.");
+ STORM_LOG_THROW(nrStates != 0, storm::exceptions::WrongFormatException, "Nr States has to be declared before model.");
- // Construct model components
- std::shared_ptr<storm::storage::sparse::ModelComponents<ValueType, RewardModelType>> modelComponents = parseStates(file, type, nrStates, valueParser);
-
+ // Construct model components
+ modelComponents = parseStates(file, type, nrStates, valueParser, rewardModelNames);
+ break;
+ }
+ }
// Done parsing
storm::utility::closeFile(file);
@@ -106,13 +126,14 @@ namespace storm {
}
template<typename ValueType, typename RewardModelType>
- std::shared_ptr<storm::storage::sparse::ModelComponents<ValueType, RewardModelType>> DirectEncodingParser<ValueType, RewardModelType>::parseStates(std::istream& file, storm::models::ModelType type, size_t stateSize, ValueParser<ValueType> const& valueParser) {
+ std::shared_ptr<storm::storage::sparse::ModelComponents<ValueType, RewardModelType>> DirectEncodingParser<ValueType, RewardModelType>::parseStates(std::istream& file, storm::models::ModelType type, size_t stateSize, ValueParser<ValueType> const& valueParser, std::vector<std::string> const& rewardModelNames) {
// Initialize
auto modelComponents = std::make_shared<storm::storage::sparse::ModelComponents<ValueType, RewardModelType>>();
bool nonDeterministic = (type == storm::models::ModelType::Mdp || type == storm::models::ModelType::MarkovAutomaton);
storm::storage::SparseMatrixBuilder<ValueType> builder = storm::storage::SparseMatrixBuilder<ValueType>(0, 0, 0, false, nonDeterministic, 0);
modelComponents->stateLabeling = storm::models::sparse::StateLabeling(stateSize);
-
+ std::vector<std::vector<ValueType>> stateRewards;
+
// We parse rates for continuous time models.
if (type == storm::models::ModelType::Ctmc) {
modelComponents->rateTransitions = true;
@@ -146,10 +167,18 @@ namespace storm {
// Rewards found
size_t posEndReward = line.find(']');
STORM_LOG_THROW(posEndReward != std::string::npos, storm::exceptions::WrongFormatException, "] missing.");
- std::string rewards = line.substr(1, posEndReward-1);
- STORM_LOG_TRACE("State rewards: " << rewards);
- // TODO import rewards
- STORM_LOG_WARN("Rewards were not imported");
+ std::string rewardsStr = line.substr(1, posEndReward-1);
+ STORM_LOG_TRACE("State rewards: " << rewardsStr);
+ std::vector<std::string> rewards;
+ boost::split(rewards, rewardsStr, boost::is_any_of(","));
+ if (stateRewards.size() < rewards.size()) {
+ stateRewards.resize(rewards.size(), std::vector<ValueType>(stateSize, storm::utility::zero<ValueType>()));
+ }
+ auto stateRewardsIt = stateRewards.begin();
+ for (auto const& rew : rewards) {
+ (*stateRewardsIt)[state] = valueParser.parseValue(rew);
+ ++stateRewardsIt;
+ }
line = line.substr(posEndReward+1);
}
// Check for labels
@@ -188,6 +217,7 @@ namespace storm {
STORM_LOG_THROW(posEndReward != std::string::npos, storm::exceptions::WrongFormatException, "] missing.");
std::string rewards = line.substr(1, posEndReward-1);
STORM_LOG_TRACE("Transition rewards: " << rewards);
+ STORM_LOG_WARN("Transition rewards [" << rewards << "] not parsed.");
// TODO save rewards
line = line.substr(posEndReward+1);
}
@@ -207,6 +237,16 @@ namespace storm {
STORM_LOG_TRACE("Finished parsing");
modelComponents->transitionMatrix = builder.build(row + 1, stateSize, nonDeterministic ? stateSize : 0);
+
+ for (uint64_t i = 0; i < stateRewards.size(); ++i) {
+ std::string rewardModelName;
+ if (rewardModelNames.size() <= i) {
+ rewardModelName = "rew" + std::to_string(i);
+ } else {
+ rewardModelName = rewardModelNames[i];
+ }
+ modelComponents->rewardModels.emplace(rewardModelName, storm::models::sparse::StandardRewardModel<ValueType>(std::move(stateRewards[i])));
+ }
STORM_LOG_TRACE("Built matrix");
return modelComponents;
}
diff --git a/src/storm/parser/DirectEncodingParser.h b/src/storm/parser/DirectEncodingParser.h
index 43a5a6f8b..db1bac12e 100644
--- a/src/storm/parser/DirectEncodingParser.h
+++ b/src/storm/parser/DirectEncodingParser.h
@@ -75,7 +75,7 @@ namespace storm {
*
* @return Transition matrix.
*/
- static std::shared_ptr<storm::storage::sparse::ModelComponents<ValueType, RewardModelType>> parseStates(std::istream& file, storm::models::ModelType type, size_t stateSize, ValueParser<ValueType> const& valueParser);
+ static std::shared_ptr<storm::storage::sparse::ModelComponents<ValueType, RewardModelType>> parseStates(std::istream& file, storm::models::ModelType type, size_t stateSize, ValueParser<ValueType> const& valueParser, std::vector<std::string> const& rewardModelNames);
};
} // namespace parser
diff --git a/src/storm/parser/ExpressionParser.cpp b/src/storm/parser/ExpressionParser.cpp
index 3292a03f9..f78e47d13 100644
--- a/src/storm/parser/ExpressionParser.cpp
+++ b/src/storm/parser/ExpressionParser.cpp
@@ -197,7 +197,7 @@ namespace storm {
try {
// Start parsing.
bool succeeded = qi::phrase_parse(iter, last, *this, boost::spirit::ascii::space | qi::lit("//") >> *(qi::char_ - (qi::eol | qi::eoi)) >> (qi::eol | qi::eoi), result);
- STORM_LOG_THROW(succeeded, storm::exceptions::WrongFormatException, "Could not parse expression.");
+ STORM_LOG_THROW(succeeded, storm::exceptions::WrongFormatException, "Could not parse expression '" << expressionString << "'.");
STORM_LOG_DEBUG("Parsed expression successfully.");
} catch (qi::expectation_failure<PositionIteratorType> const& e) {
STORM_LOG_THROW(false, storm::exceptions::WrongFormatException, e.what_);
diff --git a/src/storm/settings/modules/EigenEquationSolverSettings.cpp b/src/storm/settings/modules/EigenEquationSolverSettings.cpp
index 3047a13a4..e43bda28b 100644
--- a/src/storm/settings/modules/EigenEquationSolverSettings.cpp
+++ b/src/storm/settings/modules/EigenEquationSolverSettings.cpp
@@ -113,6 +113,7 @@ namespace storm {
case EigenEquationSolverSettings::LinearEquationMethod::DGMRES: out << "dgmres"; break;
case EigenEquationSolverSettings::LinearEquationMethod::SparseLU: out << "sparselu"; break;
}
+ return out;
}
} // namespace modules
diff --git a/src/storm/solver/AbstractEquationSolver.h b/src/storm/solver/AbstractEquationSolver.h
index 4e27517fa..22e9d0f56 100644
--- a/src/storm/solver/AbstractEquationSolver.h
+++ b/src/storm/solver/AbstractEquationSolver.h
@@ -2,6 +2,7 @@
#define STORM_SOLVER_ABSTRACTEQUATIONSOLVER_H_
#include <memory>
+#include <chrono>
#include <boost/optional.hpp>
diff --git a/src/storm/solver/IterativeMinMaxLinearEquationSolver.cpp b/src/storm/solver/IterativeMinMaxLinearEquationSolver.cpp
index 696425cbc..f5061580a 100644
--- a/src/storm/solver/IterativeMinMaxLinearEquationSolver.cpp
+++ b/src/storm/solver/IterativeMinMaxLinearEquationSolver.cpp
@@ -277,6 +277,12 @@ namespace storm {
}
}
+ // In case we perform value iteration and need to retrieve a scheduler, end components are forbidden
+ if (this->getSettings().getSolutionMethod() == IterativeMinMaxLinearEquationSolverSettings<ValueType>::SolutionMethod::ValueIteration && this->isTrackSchedulerSet()) {
+ requirements.requireNoEndComponents();
+ }
+
+ // Guide requirements by whether or not we force soundness.
if (this->getSettings().getForceSoundness()) {
if (this->getSettings().getSolutionMethod() == IterativeMinMaxLinearEquationSolverSettings<ValueType>::SolutionMethod::ValueIteration) {
// Require both bounds now.
@@ -430,7 +436,7 @@ namespace storm {
// If requested, we store the scheduler for retrieval.
if (this->isTrackSchedulerSet()) {
this->schedulerChoices = std::vector<uint_fast64_t>(this->A->getRowGroupCount());
- this->linEqSolverA->multiplyAndReduce(dir, this->A->getRowGroupIndices(), x, &b, *currentX, &this->schedulerChoices.get());
+ this->linEqSolverA->multiplyAndReduce(dir, this->A->getRowGroupIndices(), x, &b, *auxiliaryRowGroupVector.get(), &this->schedulerChoices.get());
}
if (!this->isCachingEnabled()) {
diff --git a/src/storm/solver/LpMinMaxLinearEquationSolver.cpp b/src/storm/solver/LpMinMaxLinearEquationSolver.cpp
index 2f360f513..024bcf260 100644
--- a/src/storm/solver/LpMinMaxLinearEquationSolver.cpp
+++ b/src/storm/solver/LpMinMaxLinearEquationSolver.cpp
@@ -108,6 +108,21 @@ namespace storm {
StandardMinMaxLinearEquationSolver<ValueType>::clearCache();
}
+
+ template<typename ValueType>
+ MinMaxLinearEquationSolverRequirements LpMinMaxLinearEquationSolver<ValueType>::getRequirements(EquationSystemType const& equationSystemType, boost::optional<storm::solver::OptimizationDirection> const& direction) const {
+
+ MinMaxLinearEquationSolverRequirements requirements;
+
+ // In case we need to retrieve a scheduler, end components are forbidden
+ if (this->isTrackSchedulerSet()) {
+ requirements.requireNoEndComponents();
+ }
+
+ return requirements;
+ }
+
+
template<typename ValueType>
LpMinMaxLinearEquationSolverFactory<ValueType>::LpMinMaxLinearEquationSolverFactory(bool trackScheduler) : StandardMinMaxLinearEquationSolverFactory<ValueType>(MinMaxMethodSelection::LinearProgramming, trackScheduler), lpSolverFactory(std::make_unique<storm::utility::solver::LpSolverFactory<ValueType>>()) {
// Intentionally left empty
diff --git a/src/storm/solver/LpMinMaxLinearEquationSolver.h b/src/storm/solver/LpMinMaxLinearEquationSolver.h
index a31ac710b..3e5af458f 100644
--- a/src/storm/solver/LpMinMaxLinearEquationSolver.h
+++ b/src/storm/solver/LpMinMaxLinearEquationSolver.h
@@ -18,6 +18,8 @@ namespace storm {
virtual void clearCache() const override;
+ virtual MinMaxLinearEquationSolverRequirements getRequirements(EquationSystemType const& equationSystemType, boost::optional<storm::solver::OptimizationDirection> const& direction = boost::none) const override;
+
private:
std::unique_ptr<storm::utility::solver::LpSolverFactory<ValueType>> lpSolverFactory;
};
diff --git a/src/storm/storage/SparseMatrix.cpp b/src/storm/storage/SparseMatrix.cpp
index c8f53a342..bf1b15d14 100644
--- a/src/storm/storage/SparseMatrix.cpp
+++ b/src/storm/storage/SparseMatrix.cpp
@@ -1497,8 +1497,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>();
@@ -1509,9 +1510,8 @@ namespace storm {
diagonalElement += it->getValue();
}
}
-
+ assert(!storm::utility::isZero(diagonalElement));
*resultIterator = ((storm::utility::one<ValueType>() - omega) * *resultIterator) + (omega / diagonalElement) * (*bIt - tmpValue);
- ++currentRow;
}
}
diff --git a/src/storm/utility/DirectEncodingExporter.cpp b/src/storm/utility/DirectEncodingExporter.cpp
index 6bdd629a7..e0913a0f2 100644
--- a/src/storm/utility/DirectEncodingExporter.cpp
+++ b/src/storm/utility/DirectEncodingExporter.cpp
@@ -46,6 +46,11 @@ namespace storm {
}
}
os << std::endl;
+ os << "@reward_models" << std::endl;
+ for (auto const& rewardModel : sparseModel->getRewardModels()) {
+ os << rewardModel.first << " ";
+ }
+ os << std::endl;
os << "@nr_states" << std::endl << sparseModel->getNumberOfStates() << std::endl;
os << "@model" << std::endl;
diff --git a/travis/build-helper.sh b/travis/build-helper.sh
index 8d73c87e7..04c2dc52e 100755
--- 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++
;;
diff --git a/travis/dockerfiles/Dockerfile.debian-9 b/travis/dockerfiles/Dockerfile.debian-9
deleted file mode 100644
index 3735b38fd..000000000
--- a/travis/dockerfiles/Dockerfile.debian-9
+++ /dev/null
@@ -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
diff --git a/travis/dockerfiles/Dockerfile.storm b/travis/dockerfiles/Dockerfile.storm
deleted file mode 100644
index 272b97825..000000000
--- a/travis/dockerfiles/Dockerfile.storm
+++ /dev/null
@@ -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
diff --git a/travis/dockerfiles/Dockerfile.ubuntu-16.10 b/travis/dockerfiles/Dockerfile.ubuntu-16.10
deleted file mode 100644
index a612faccb..000000000
--- a/travis/dockerfiles/Dockerfile.ubuntu-16.10
+++ /dev/null
@@ -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
diff --git a/travis/dockerfiles/build_carl.sh b/travis/dockerfiles/build_carl.sh
deleted file mode 100755
index fc3d43d22..000000000
--- a/travis/dockerfiles/build_carl.sh
+++ /dev/null
@@ -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"
diff --git a/travis/dockerfiles/build_docker.sh b/travis/dockerfiles/build_docker.sh
deleted file mode 100755
index 280710566..000000000
--- a/travis/dockerfiles/build_docker.sh
+++ /dev/null
@@ -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
diff --git a/travis/dockerfiles/build_storm.sh b/travis/dockerfiles/build_storm.sh
deleted file mode 100755
index 4c11b708d..000000000
--- a/travis/dockerfiles/build_storm.sh
+++ /dev/null
@@ -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"
diff --git a/travis/generate_travis.py b/travis/generate_travis.py
index 14e058a85..508568a34 100644
--- 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"),
- #("debian-9", "gcc", "-6"),
+ ("ubuntu-16.10", "gcc", ""),
+ #("debian-9", "gcc", ""),
]
# 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"
diff --git a/travis/install_linux.sh b/travis/install_linux.sh
index c7ef04886..62a7d75f6 100755
--- 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
diff --git a/travis/install_osx.sh b/travis/install_osx.sh
index 8d703a82a..89e155730 100755
--- 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
diff --git a/util/astyle/options.astyle b/util/astyle/options.astyle
deleted file mode 100644
index 5f02d356d..000000000
--- a/util/astyle/options.astyle
+++ /dev/null
@@ -1,34 +0,0 @@
-# Select overall style.
---style=google
---mode=c
---recursive
-
-# Attach brackets to namespaces and classes.
---attach-namespaces
---attach-classes
-
-# Of course, namespaces should also be indented.
---indent-namespaces
-
-# C++ comments starting in column 1 are also supposed to be indented properly.
---indent-col1-comments
-
-# Add space padding around operators.
---pad-oper
-
-# Put the pointer/reference operators next to the variable.
---align-pointer=type
-
-# Add brackets to conditional one-line statements.
---add-brackets
-
-# Convert tabs to spaces in non-indentation part of the line as well.
---convert-tabs
-
-# Remove spaces in definition of C++ templates.
---close-templates
-
-# Don't let lines get too long.
---max-code-length=140
-
---verbose
diff --git a/util/checklist/storage.ods b/util/checklist/storage.ods
deleted file mode 100644
index d05761496..000000000
Binary files a/util/checklist/storage.ods and /dev/null differ
diff --git a/util/osx-package/package.sh b/util/osx-package/package.sh
deleted file mode 100644
index 0db5b2b5d..000000000
--- a/util/osx-package/package.sh
+++ /dev/null
@@ -1,10 +0,0 @@
-#!/bin/sh
-
-DYLIBBUNDLER_DIR=/Users/chris/work/macdylibbundler/
-
-mkdir -p $1
-mkdir -p $1/bin
-mkdir -p $1/lib
-cp $2 $1/bin
-$DYLIBBUNDLER_DIR/dylibbundler -cd -od -b -p @executable_path/../lib -x $1/bin/storm -d $1/lib
-python packager.py --bin storm --dir $1
diff --git a/util/osx-package/packager.py b/util/osx-package/packager.py
deleted file mode 100644
index 60b26a8b8..000000000
--- a/util/osx-package/packager.py
+++ /dev/null
@@ -1,103 +0,0 @@
-import argparse
-import subprocess
-import os
-from shutil import copyfile
-
-def get_dependencies(file):
- # Call otool -L file to obtain the dependencies.
- proc = subprocess.Popen(["otool", "-L", args.binary], stdout=subprocess.PIPE)
- result = {}
- for line_bytes in proc.stdout:
- line = line_bytes.decode("utf-8").strip()
- lib = line.split()[0]
- if (lib.startswith("@")):
- lib = lib.split("/", 1)[1]
- (base, file) = os.path.split(lib)
- print(base + " // " + file)
-
- return result
-
-def create_package(args):
- create_package_dirs(args.dir)
- copy_binary_to_package_dir(args.bin, args.binary_basename, args.dir)
- run_dylibbundler(args.bundler_binary, args.dir, args.binary_basename)
- pass
-
-def parse_arguments():
- parser = argparse.ArgumentParser(description='Package the storm binary on Mac OS.')
- parser.add_argument('--bin', dest='bin', help='the binary to package', default='storm')
- parser.add_argument('--dir', dest='dir', help='the root directory of the package (will be created if it does not exist)', default='.')
- parser.add_argument('--dylibbundler', dest='bundler_binary', help='the binary of the dylibbundler', default='dylibbundler')
- args = parser.parse_args()
- args.binary_dir = os.path.split(args.bin)[0]
- args.binary_basename = os.path.split(args.bin)[1]
- return args
-
-def create_package_dirs(root_dir):
- if not os.path.exists(root_dir):
- os.makedirs(root_dir)
- if not os.path.exists(root_dir + "/bin"):
- os.makedirs(root_dir + "/bin")
- if not os.path.exists(root_dir + "/lib"):
- os.makedirs(root_dir + "/bin")
- pass
-
-def copy_binary_to_package_dir(binary, binary_basename, root_dir):
- copyfile(binary, root_dir + "/bin/storm")
- pass
-
-def run_dylibbundler(bundler_binary, root_dir, binary_basename):
- command = [bundler_binary, "-cd", "-od", "-b", "-p", "@executable_path/../lib", "-x", root_dir + "/bin/" + binary_basename, "-d", root_dir + "/lib"]
- print("executing " + str(command))
- #proc = subprocess.Popen(command, stdin=subprocess.PIPE, stdout=subprocess.PIPE)
- pass
-
-def fix_paths(root_dir, binary_basename):
- fix_paths_file(root_dir + "/bin/" + binary_basename)
- for file in os.listdir(root_dir + "/lib"):
- fix_paths_file(root_dir + "/lib/" + file)
- pass
- pass
-
-def fix_paths_file(file):
- print("fixing paths for " + file)
- fixable_deps = get_fixable_deps(file)
- for (path, lib) in fixable_deps:
- change_fixable_dep(file, path, lib)
-
-native_libs = ["libc++.1.dylib", "libSystem.B.dylib"]
-
-def get_fixable_deps(file):
- # Call otool -L file to obtain the dependencies.
- proc = subprocess.Popen(["otool", "-L", file], stdin=subprocess.PIPE, stdout=subprocess.PIPE)
- result = []
- for line_bytes in proc.stdout:
- line = line_bytes.decode("utf-8").strip()
- lib = line.split()[0]
- if lib.startswith("@rpath/"):
- result.append(("@rpath", lib.split("/", 1)[1]))
- elif lib.startswith("/"):
- path_file = os.path.split(lib)
- if path_file[1] not in native_libs:
- result.append((path_file[0], path_file[1]))
- return result
-
-def change_fixable_dep(file, path, lib):
- # Call install_name_tool to change the fixable dependencies
- command = ["install_name_tool", "-change", path + "/" + lib, "@executable_path/../lib/" + lib, file]
- print("executing " + str(command))
- proc = subprocess.Popen(command, stdout=subprocess.PIPE)
- #print ("after call to install_name_tool")
- #proc = subprocess.Popen(["otool", "-L", file], stdout=subprocess.PIPE)
- #for line_bytes in proc.stdout:
- # line = line_bytes.decode("utf-8").strip()
- # print(line)
- pass
-
-if __name__ == "__main__":
- args = parse_arguments()
-
- #create_package(args)
- fix_paths(args.dir, args.binary_basename)
-
-