From a01e46779f85031824253068ef2f19f28bc1d404 Mon Sep 17 00:00:00 2001 From: dehnert Date: Wed, 20 Jan 2016 13:57:31 +0100 Subject: [PATCH 1/6] CMake now requiring hwloc for sylvan under linux Former-commit-id: d9425c362ccdebcaed3aae3f1ae1c644e6b1e2d0 --- CMakeLists.txt | 21 ++++ resources/cmake/FindHwloc.cmake | 179 ++++++++++++++++++++++++++++++++ 2 files changed, 200 insertions(+) create mode 100644 resources/cmake/FindHwloc.cmake diff --git a/CMakeLists.txt b/CMakeLists.txt index 5f5fcdb72..8911a9506 100644 --- a/CMakeLists.txt +++ b/CMakeLists.txt @@ -58,6 +58,18 @@ endif() # Base path for test files set(STORM_CPP_TESTS_BASE_PATH "${PROJECT_SOURCE_DIR}/test") +# Auto-detect operating system. +if(${CMAKE_SYSTEM_NAME} MATCHES "Darwin") + # Mac OS + set(OPERATING_SYSTEM "Mac OS") +elseif(${CMAKE_SYSTEM_NAME} MATCHES "Linux") + # Linux + set(OPERATING_SYSTEM "Linux") +else() + # Assuming Windows. + set(OPERATING_SYSTEM "Windows") +ENDIF() +message(STATUS "Detected operating system: ${OPERATING_SYSTEM}") ############################################################# ## @@ -536,6 +548,15 @@ set(Sylvan_INCLUDE_DIR "${STORM_SYLVAN_ROOT}/src") message(STATUS "Linking with shipped version of sylvan (in directory ${STORM_SYLVAN_ROOT}).") include_directories("${Sylvan_INCLUDE_DIR}") list(APPEND STORM_LINK_LIBRARIES "${binary_dir}/src/libsylvan.a") +if(${OPERATING_SYSTEM} MATCHES "Linux") + find_package(Hwloc REQUIRED) + if(NOT Hwloc_FOUND) + message(SEND_ERROR "HWLOC is required but was not found.") + else() + message(STATUS "Linking with HWLOC: ${Hwloc_FOUND} ${Hwloc_LIBRARIES}") + list(APPEND STORM_LINK_LIBRARIES ${Hwloc_LIBRARIES}) + endif() +endif() ############################################################# ## diff --git a/resources/cmake/FindHwloc.cmake b/resources/cmake/FindHwloc.cmake new file mode 100644 index 000000000..d1b5b488e --- /dev/null +++ b/resources/cmake/FindHwloc.cmake @@ -0,0 +1,179 @@ +# FindHwloc +# ---------- +# +# Try to find Portable Hardware Locality (hwloc) libraries. +# http://www.open-mpi.org/software/hwloc +# +# You may declare HWLOC_ROOT environment variable to tell where +# your hwloc library is installed. +# +# Once done this will define:: +# +# Hwloc_FOUND - True if hwloc was found +# Hwloc_INCLUDE_DIRS - include directories for hwloc +# Hwloc_LIBRARIES - link against these libraries to use hwloc +# Hwloc_VERSION - version +# Hwloc_CFLAGS - include directories as compiler flags +# Hwloc_LDLFAGS - link paths and libs as compiler flags +# + +#============================================================================= +# Copyright 2014 Mikael Lepistö +# +# Distributed under the OSI-approved BSD License (the "License"); +# +# This software is distributed WITHOUT ANY WARRANTY; without even the +# implied warranty of MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE. +# See the License for more information. +#============================================================================= + +if(WIN32) + find_path(Hwloc_INCLUDE_DIR + NAMES + hwloc.h + PATHS + ENV "PROGRAMFILES(X86)" + ENV HWLOC_ROOT + PATH_SUFFIXES + include + ) + + find_library(Hwloc_LIBRARY + NAMES + libhwloc.lib + PATHS + ENV "PROGRAMFILES(X86)" + ENV HWLOC_ROOT + PATH_SUFFIXES + lib + ) + + # + # Check if the found library can be used to linking + # + SET (_TEST_SOURCE "${CMAKE_BINARY_DIR}${CMAKE_FILES_DIRECTORY}/linktest.c") + FILE (WRITE "${_TEST_SOURCE}" + " + #include + int main() + { + hwloc_topology_t topology; + int nbcores; + hwloc_topology_init(&topology); + hwloc_topology_load(topology); + nbcores = hwloc_get_nbobjs_by_type(topology, HWLOC_OBJ_CORE); + hwloc_topology_destroy(topology); + return 0; + } + " + ) + + TRY_COMPILE(_LINK_SUCCESS ${CMAKE_BINARY_DIR} "${_TEST_SOURCE}" + CMAKE_FLAGS + "-DINCLUDE_DIRECTORIES:STRING=${Hwloc_INCLUDE_DIR}" + CMAKE_FLAGS + "-DLINK_LIBRARIES:STRING=${Hwloc_LIBRARY}" + ) + + IF(NOT _LINK_SUCCESS) + if(CMAKE_SIZEOF_VOID_P EQUAL 8) + message(STATUS "You are building 64bit target.") + ELSE() + message(STATUS "You are building 32bit code. If you like to build x64 use e.g. -G 'Visual Studio 12 Win64' generator." ) + ENDIF() + message(FATAL_ERROR "Library found, but linking test program failed.") + ENDIF() + + # + # Resolve version if some compiled binary found... + # + find_program(HWLOC_INFO_EXECUTABLE + NAMES + hwloc-info + PATHS + ENV HWLOC_ROOT + PATH_SUFFIXES + bin + ) + + if(HWLOC_INFO_EXECUTABLE) + execute_process( + COMMAND ${HWLOC_INFO_EXECUTABLE} "--version" + OUTPUT_VARIABLE HWLOC_VERSION_LINE + OUTPUT_STRIP_TRAILING_WHITESPACE + ) + string(REGEX MATCH "([0-9]+.[0-9]+)$" + Hwloc_VERSION "${HWLOC_VERSION_LINE}") + unset(HWLOC_VERSION_LINE) + endif() + + # + # All good + # + + set(Hwloc_LIBRARIES ${Hwloc_LIBRARY}) + set(Hwloc_INCLUDE_DIRS ${Hwloc_INCLUDE_DIR}) + + include(FindPackageHandleStandardArgs) + find_package_handle_standard_args( + Hwloc + FOUND_VAR Hwloc_FOUND + REQUIRED_VARS Hwloc_LIBRARY Hwloc_INCLUDE_DIR + VERSION_VAR Hwloc_VERSION) + + mark_as_advanced( + Hwloc_INCLUDE_DIR + Hwloc_LIBRARY) + + foreach(arg ${Hwloc_INCLUDE_DIRS}) + set(Hwloc_CFLAGS "${Hwloc_CFLAGS} /I${arg}") + endforeach() + + set(Hwloc_LDFLAGS "${Hwloc_LIBRARY}") + +else() + + # Find with pkgconfig + find_package(PkgConfig) + + if(HWLOC_ROOT) + set(ENV{PKG_CONFIG_PATH} "${HWLOC_ROOT}/lib/pkgconfig") + else() + foreach(PREFIX ${CMAKE_PREFIX_PATH}) + set(PKG_CONFIG_PATH "${PKG_CONFIG_PATH}:${PREFIX}/lib/pkgconfig") + endforeach() + set(ENV{PKG_CONFIG_PATH} "${PKG_CONFIG_PATH}:$ENV{PKG_CONFIG_PATH}") + endif() + + if(hwloc_FIND_REQUIRED) + set(_hwloc_OPTS "REQUIRED") + elseif(hwloc_FIND_QUIETLY) + set(_hwloc_OPTS "QUIET") + else() + set(_hwloc_output 1) + endif() + + if(hwloc_FIND_VERSION) + if(hwloc_FIND_VERSION_EXACT) + pkg_check_modules(Hwloc ${_hwloc_OPTS} hwloc=${hwloc_FIND_VERSION}) + else() + pkg_check_modules(Hwloc ${_hwloc_OPTS} hwloc>=${hwloc_FIND_VERSION}) + endif() + else() + pkg_check_modules(Hwloc ${_hwloc_OPTS} hwloc) + endif() + + if(Hwloc_FOUND) + include(FindPackageHandleStandardArgs) + find_package_handle_standard_args(Hwloc DEFAULT_MSG Hwloc_LIBRARIES) + + if(NOT ${Hwloc_VERSION} VERSION_LESS 1.7.0) + set(Hwloc_GL_FOUND 1) + endif() + + if(_hwloc_output) + message(STATUS + "Found hwloc ${Hwloc_VERSION} in ${Hwloc_INCLUDE_DIRS}:${Hwloc_LIBRARIES}") + endif() + endif() +endif() From 2ea5fd7418486c6585067a94dc1abedd21190201 Mon Sep 17 00:00:00 2001 From: dehnert Date: Wed, 20 Jan 2016 14:41:00 +0100 Subject: [PATCH 2/6] fix in sylvan, minor changes to cmake list Former-commit-id: 96adc0c187657ce954008072759cb01542c8f526 --- CMakeLists.txt | 3 +-- resources/3rdparty/sylvan/src/sylvan_mtbdd.h | 1 - 2 files changed, 1 insertion(+), 3 deletions(-) diff --git a/CMakeLists.txt b/CMakeLists.txt index 8911a9506..2abc6a992 100644 --- a/CMakeLists.txt +++ b/CMakeLists.txt @@ -549,11 +549,10 @@ message(STATUS "Linking with shipped version of sylvan (in directory ${STORM_SYL include_directories("${Sylvan_INCLUDE_DIR}") list(APPEND STORM_LINK_LIBRARIES "${binary_dir}/src/libsylvan.a") if(${OPERATING_SYSTEM} MATCHES "Linux") - find_package(Hwloc REQUIRED) + find_package(Hwloc QUIET) if(NOT Hwloc_FOUND) message(SEND_ERROR "HWLOC is required but was not found.") else() - message(STATUS "Linking with HWLOC: ${Hwloc_FOUND} ${Hwloc_LIBRARIES}") list(APPEND STORM_LINK_LIBRARIES ${Hwloc_LIBRARIES}) endif() endif() diff --git a/resources/3rdparty/sylvan/src/sylvan_mtbdd.h b/resources/3rdparty/sylvan/src/sylvan_mtbdd.h index 731b5be0f..1a7de3f57 100644 --- a/resources/3rdparty/sylvan/src/sylvan_mtbdd.h +++ b/resources/3rdparty/sylvan/src/sylvan_mtbdd.h @@ -224,7 +224,6 @@ TASK_DECL_3(MTBDD, mtbdd_abstract_op_plus, MTBDD, MTBDD, int); * For Integer/Double MTBDDs, mtbdd_false is interpreted as "0" or "0.0". */ TASK_DECL_2(MTBDD, mtbdd_op_minus, MTBDD*, MTBDD*); -TASK_DECL_3(MTBDD, mtbdd_abstract_op_minus, MTBDD, MTBDD, int); /** * Binary operation Times (for MTBDDs of same type) From ebbd03c15b29b4d25438f413cb35ad5091efec17 Mon Sep 17 00:00:00 2001 From: dehnert Date: Thu, 21 Jan 2016 16:48:06 +0100 Subject: [PATCH 3/6] fixed some warning-related stuff. introduced abstraction-refinement engine in options and entrypoints that currently only throws not-implemented exception Former-commit-id: 7a4bb8e18c6140bf6424291e5ec957edbfb187b9 --- CMakeLists.txt | 2 +- src/cli/entrypoints.h | 85 ++++++++++++++---------- src/parser/SpiritParserDefinitions.h | 5 ++ src/settings/modules/GeneralSettings.cpp | 7 +- src/settings/modules/GeneralSettings.h | 2 +- src/utility/storm.h | 3 + 6 files changed, 63 insertions(+), 41 deletions(-) diff --git a/CMakeLists.txt b/CMakeLists.txt index 2abc6a992..9f6a50f70 100644 --- a/CMakeLists.txt +++ b/CMakeLists.txt @@ -85,7 +85,7 @@ if(CMAKE_COMPILER_IS_GNUCC) set(CMAKE_CXX_FLAGS_RELEASE "${CMAKE_CXX_FLAGS_RELEASE} -funroll-loops") set(CMAKE_C_FLAGS_RELEASE "${CMAKE_C_FLAGS_RELEASE} -funroll-loops") add_definitions(-DBOOST_RESULT_OF_USE_DECLTYPE) - set(CMAKE_CXX_FLAGS "${CMAKE_CXX_FLAGS} -std=c++14 -Wall -pedantic -Wno-deprecated-declarations -Wno-unused-local-typedefs") + set(CMAKE_CXX_FLAGS "${CMAKE_CXX_FLAGS} -std=c++14 -Wall -pedantic -Wno-deprecated-declarations -Wno-unused-local-typedefs -Wno-unknown-pragmas") set(CMAKE_C_FLAGS "${CMAKE_C_FLAGS} -Wall -pedantic -Wno-deprecated-declarations") # Turn on popcnt instruction if desired (yes by default) diff --git a/src/cli/entrypoints.h b/src/cli/entrypoints.h index 93f9e1777..4eaa264cb 100644 --- a/src/cli/entrypoints.h +++ b/src/cli/entrypoints.h @@ -3,6 +3,8 @@ #include "src/utility/storm.h" +#include "src/exceptions/NotImplementedException.h" + namespace storm { namespace cli { @@ -47,6 +49,11 @@ namespace storm { } #endif + template + void verifySymbolicModelWithAbstractionRefinementEngine(storm::prism::Program const& program, std::vector> const& formulas) { + STORM_LOG_THROW(false, storm::exceptions::NotImplementedException, "Abstraction Refinement is not yet implemented."); + } + template void verifySymbolicModelWithHybridEngine(std::shared_ptr> model, std::vector> const& formulas) { for (auto const& formula : formulas) { @@ -108,50 +115,56 @@ namespace storm { template void buildAndCheckSymbolicModel(storm::prism::Program const& program, std::vector> const& formulas) { - storm::storage::ModelProgramPair modelProgramPair = buildSymbolicModel(program, formulas); - STORM_LOG_THROW(modelProgramPair.model != nullptr, storm::exceptions::InvalidStateException, "Model could not be constructed for an unknown reason."); - - // Preprocess the model if needed. - BRANCH_ON_MODELTYPE(modelProgramPair.model, modelProgramPair.model, ValueType, LibraryType, preprocessModel, formulas); - - // Print some information about the model. - modelProgramPair.model->printModelInformationToStream(std::cout); + storm::settings::modules::GeneralSettings const& settings = storm::settings::generalSettings(); - // Verify the model, if a formula was given. - if (!formulas.empty()) { - // There may be constants of the model appearing in the formulas, so we replace all their occurrences - // by their definitions in the translated program. + if (settings.getEngine() == storm::settings::modules::GeneralSettings::Engine::AbstractionRefinement) { + verifySymbolicModelWithAbstractionRefinementEngine(program, formulas); + } else { + storm::storage::ModelProgramPair modelProgramPair = buildSymbolicModel(program, formulas); + STORM_LOG_THROW(modelProgramPair.model != nullptr, storm::exceptions::InvalidStateException, "Model could not be constructed for an unknown reason."); - // Start by building a mapping from constants of the (translated) model to their defining expressions. - std::map constantSubstitution; - for (auto const& constant : modelProgramPair.program.getConstants()) { - if (constant.isDefined()) { - constantSubstitution.emplace(constant.getExpressionVariable(), constant.getExpression()); - } - } + // Preprocess the model if needed. + BRANCH_ON_MODELTYPE(modelProgramPair.model, modelProgramPair.model, ValueType, LibraryType, preprocessModel, formulas); - std::vector> preparedFormulas; - for (auto const& formula : formulas) { - preparedFormulas.emplace_back(formula->substitute(constantSubstitution)); - } + // Print some information about the model. + modelProgramPair.model->printModelInformationToStream(std::cout); - if (modelProgramPair.model->isSparseModel()) { - if(storm::settings::generalSettings().isCounterexampleSet()) { - // If we were requested to generate a counterexample, we now do so for each formula. - for(auto const& formula : preparedFormulas) { - generateCounterexample(program, modelProgramPair.model->as>(), formula); + // Verify the model, if a formula was given. + if (!formulas.empty()) { + // There may be constants of the model appearing in the formulas, so we replace all their occurrences + // by their definitions in the translated program. + + // Start by building a mapping from constants of the (translated) model to their defining expressions. + std::map constantSubstitution; + for (auto const& constant : modelProgramPair.program.getConstants()) { + if (constant.isDefined()) { + constantSubstitution.emplace(constant.getExpressionVariable(), constant.getExpression()); } - } else { - verifySparseModel(modelProgramPair.model->as>(), preparedFormulas); } - } else if (modelProgramPair.model->isSymbolicModel()) { - if (storm::settings::generalSettings().getEngine() == storm::settings::modules::GeneralSettings::Engine::Hybrid) { - verifySymbolicModelWithHybridEngine(modelProgramPair.model->as>(), preparedFormulas); + + std::vector> preparedFormulas; + for (auto const& formula : formulas) { + preparedFormulas.emplace_back(formula->substitute(constantSubstitution)); + } + + if (modelProgramPair.model->isSparseModel()) { + if(settings.isCounterexampleSet()) { + // If we were requested to generate a counterexample, we now do so for each formula. + for(auto const& formula : preparedFormulas) { + generateCounterexample(program, modelProgramPair.model->as>(), formula); + } + } else { + verifySparseModel(modelProgramPair.model->as>(), preparedFormulas); + } + } else if (modelProgramPair.model->isSymbolicModel()) { + if (settings.getEngine() == storm::settings::modules::GeneralSettings::Engine::Hybrid) { + verifySymbolicModelWithHybridEngine(modelProgramPair.model->as>(), preparedFormulas); + } else { + verifySymbolicModelWithSymbolicEngine(modelProgramPair.model->as>(), preparedFormulas); + } } else { - verifySymbolicModelWithSymbolicEngine(modelProgramPair.model->as>(), preparedFormulas); + STORM_LOG_THROW(false, storm::exceptions::InvalidSettingsException, "Invalid input model type."); } - } else { - STORM_LOG_THROW(false, storm::exceptions::InvalidSettingsException, "Invalid input model type."); } } } diff --git a/src/parser/SpiritParserDefinitions.h b/src/parser/SpiritParserDefinitions.h index 20c922863..b4d1e183d 100644 --- a/src/parser/SpiritParserDefinitions.h +++ b/src/parser/SpiritParserDefinitions.h @@ -1,6 +1,9 @@ #ifndef STORM_PARSER_SPIRITPARSERDEFINITIONS_H_ #define STORM_PARSER_SPIRITPARSERDEFINITIONS_H_ +#pragma clang diagnostic push +#pragma clang diagnostic ignored "-Wno-#pragma-messages" + // Include boost spirit. #define BOOST_SPIRIT_USE_PHOENIX_V3 #include @@ -9,6 +12,8 @@ #include #include +#pragma clang diagnostic pop + namespace qi = boost::spirit::qi; namespace phoenix = boost::phoenix; diff --git a/src/settings/modules/GeneralSettings.cpp b/src/settings/modules/GeneralSettings.cpp index 701422587..95a48931b 100644 --- a/src/settings/modules/GeneralSettings.cpp +++ b/src/settings/modules/GeneralSettings.cpp @@ -96,9 +96,9 @@ namespace storm { .addArgument(storm::settings::ArgumentBuilder::createStringArgument("filename", "The file from which to read the choice labels.").addValidationFunctionString(storm::settings::ArgumentValidators::existingReadableFileValidator()).build()).build()); this->addOption(storm::settings::OptionBuilder(moduleName, dontFixDeadlockOptionName, false, "If the model contains deadlock states, they need to be fixed by setting this option.").setShortName(dontFixDeadlockOptionShortName).build()); - std::vector engines = {"sparse", "hybrid", "dd"}; + std::vector engines = {"sparse", "hybrid", "dd", "abs"}; this->addOption(storm::settings::OptionBuilder(moduleName, engineOptionName, false, "Sets which engine is used for model building and model checking.").setShortName(engineOptionShortName) - .addArgument(storm::settings::ArgumentBuilder::createStringArgument("name", "The name of the engine to use. Available are {sparse, hybrid, dd}.").addValidationFunctionString(storm::settings::ArgumentValidators::stringInListValidator(engines)).setDefaultValueString("sparse").build()).build()); + .addArgument(storm::settings::ArgumentBuilder::createStringArgument("name", "The name of the engine to use. Available are {sparse, hybrid, dd, ar}.").addValidationFunctionString(storm::settings::ArgumentValidators::stringInListValidator(engines)).setDefaultValueString("sparse").build()).build()); std::vector linearEquationSolver = {"gmm++", "native"}; this->addOption(storm::settings::OptionBuilder(moduleName, eqSolverOptionName, false, "Sets which solver is preferred for solving systems of linear equations.") @@ -346,10 +346,11 @@ namespace storm { engine = GeneralSettings::Engine::Hybrid; } else if (engineStr == "dd") { engine = GeneralSettings::Engine::Dd; + } else if (engineStr == "abs") { + engine = GeneralSettings::Engine::AbstractionRefinement; } else { STORM_LOG_THROW(false, storm::exceptions::IllegalArgumentValueException, "Unknown engine '" << engineStr << "'."); } - } bool GeneralSettings::check() const { diff --git a/src/settings/modules/GeneralSettings.h b/src/settings/modules/GeneralSettings.h index d6803b600..8144c0a1f 100644 --- a/src/settings/modules/GeneralSettings.h +++ b/src/settings/modules/GeneralSettings.h @@ -27,7 +27,7 @@ namespace storm { // An enumeration of all engines. enum class Engine { - Sparse, Hybrid, Dd + Sparse, Hybrid, Dd, AbstractionRefinement }; /*! diff --git a/src/utility/storm.h b/src/utility/storm.h index af70bb89c..03e297ca5 100644 --- a/src/utility/storm.h +++ b/src/utility/storm.h @@ -232,6 +232,9 @@ namespace storm { STORM_LOG_THROW(ddModel != nullptr, storm::exceptions::InvalidArgumentException, "Dd engine requires a dd input model"); return verifySymbolicModelWithDdEngine(ddModel, formula); } + case storm::settings::modules::GeneralSettings::Engine::AbstractionRefinement: { + STORM_LOG_ASSERT(false, "This position should not be reached, as at this point no model has been built."); + } } } From 0f8bd821250a285eb8f68521ec38a5121b093d43 Mon Sep 17 00:00:00 2001 From: dehnert Date: Thu, 21 Jan 2016 16:50:14 +0100 Subject: [PATCH 4/6] corrected clang pragma Former-commit-id: 1f8a475d9576baad70e2f3c706b5977c5ceb1b6e --- src/parser/SpiritParserDefinitions.h | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/src/parser/SpiritParserDefinitions.h b/src/parser/SpiritParserDefinitions.h index b4d1e183d..abd13bc94 100644 --- a/src/parser/SpiritParserDefinitions.h +++ b/src/parser/SpiritParserDefinitions.h @@ -2,7 +2,7 @@ #define STORM_PARSER_SPIRITPARSERDEFINITIONS_H_ #pragma clang diagnostic push -#pragma clang diagnostic ignored "-Wno-#pragma-messages" +#pragma clang diagnostic ignored "-W#pragma-messages" // Include boost spirit. #define BOOST_SPIRIT_USE_PHOENIX_V3 From e20942393e4eaddecbc358649fe4e410a51de31a Mon Sep 17 00:00:00 2001 From: dehnert Date: Fri, 22 Jan 2016 13:23:59 +0100 Subject: [PATCH 5/6] added some primes Former-commit-id: f0da396762c4dd37e355fe1a33b5e62d664630a1 --- src/storage/BitVectorHashMap.cpp | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/src/storage/BitVectorHashMap.cpp b/src/storage/BitVectorHashMap.cpp index 1726847ab..c184b764b 100644 --- a/src/storage/BitVectorHashMap.cpp +++ b/src/storage/BitVectorHashMap.cpp @@ -7,7 +7,7 @@ namespace storm { namespace storage { template - const std::vector BitVectorHashMap::sizes = {5, 13, 31, 79, 163, 277, 499, 1021, 2029, 3989, 8059, 16001, 32099, 64301, 127921, 256499, 511111, 1024901, 2048003, 4096891, 8192411, 15485863, 32142191}; + const std::vector BitVectorHashMap::sizes = {5, 13, 31, 79, 163, 277, 499, 1021, 2029, 3989, 8059, 16001, 32099, 64301, 127921, 256499, 511111, 1024901, 2048003, 4096891, 8192411, 15485863, 32142191, 64285127, 128572517, 257148523, 514299959, 102863003}; template BitVectorHashMap::BitVectorHashMapIterator::BitVectorHashMapIterator(BitVectorHashMap const& map, BitVector::const_iterator indexIt) : map(map), indexIt(indexIt) { From fdf2d81c61dfc925803954824ee16724aaa1f099 Mon Sep 17 00:00:00 2001 From: dehnert Date: Fri, 22 Jan 2016 13:47:50 +0100 Subject: [PATCH 6/6] added missing template parameter Former-commit-id: 2cbeafe0d08e47f25deb50c1886c9dc3c1aa63f3 --- src/cli/entrypoints.h | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/src/cli/entrypoints.h b/src/cli/entrypoints.h index 4eaa264cb..79de987ee 100644 --- a/src/cli/entrypoints.h +++ b/src/cli/entrypoints.h @@ -118,7 +118,7 @@ namespace storm { storm::settings::modules::GeneralSettings const& settings = storm::settings::generalSettings(); if (settings.getEngine() == storm::settings::modules::GeneralSettings::Engine::AbstractionRefinement) { - verifySymbolicModelWithAbstractionRefinementEngine(program, formulas); + verifySymbolicModelWithAbstractionRefinementEngine(program, formulas); } else { storm::storage::ModelProgramPair modelProgramPair = buildSymbolicModel(program, formulas); STORM_LOG_THROW(modelProgramPair.model != nullptr, storm::exceptions::InvalidStateException, "Model could not be constructed for an unknown reason.");