diff --git a/.gitignore b/.gitignore index ae1598ee9..88a8bf3d9 100644 --- a/.gitignore +++ b/.gitignore @@ -47,5 +47,6 @@ build//CMakeLists.txt # CMake generated/configured files src/utility/storm-version.cpp .DS_Store +.idea *.out diff --git a/CMakeLists.txt b/CMakeLists.txt index 5f5fcdb72..2abc6a992 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,14 @@ 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 QUIET) + if(NOT Hwloc_FOUND) + message(SEND_ERROR "HWLOC is required but was not found.") + else() + 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) 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() diff --git a/src/cli/entrypoints.h b/src/cli/entrypoints.h index 1c24bc091..93f9e1777 100644 --- a/src/cli/entrypoints.h +++ b/src/cli/entrypoints.h @@ -108,14 +108,14 @@ namespace storm { template void buildAndCheckSymbolicModel(storm::prism::Program const& program, std::vector> const& formulas) { - std::pair, storm::prism::Program> modelProgramPair = buildSymbolicModel(program, formulas); - STORM_LOG_THROW(modelProgramPair.first != nullptr, storm::exceptions::InvalidStateException, "Model could not be constructed for an unknown reason."); + 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.first, modelProgramPair.first, ValueType, LibraryType, preprocessModel, formulas); + BRANCH_ON_MODELTYPE(modelProgramPair.model, modelProgramPair.model, ValueType, LibraryType, preprocessModel, formulas); // Print some information about the model. - modelProgramPair.first->printModelInformationToStream(std::cout); + modelProgramPair.model->printModelInformationToStream(std::cout); // Verify the model, if a formula was given. if (!formulas.empty()) { @@ -124,7 +124,7 @@ namespace storm { // Start by building a mapping from constants of the (translated) model to their defining expressions. std::map constantSubstitution; - for (auto const& constant : modelProgramPair.second.getConstants()) { + for (auto const& constant : modelProgramPair.program.getConstants()) { if (constant.isDefined()) { constantSubstitution.emplace(constant.getExpressionVariable(), constant.getExpression()); } @@ -135,20 +135,20 @@ namespace storm { preparedFormulas.emplace_back(formula->substitute(constantSubstitution)); } - if (modelProgramPair.first->isSparseModel()) { + 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.first->as>(), formula); + generateCounterexample(program, modelProgramPair.model->as>(), formula); } } else { - verifySparseModel(modelProgramPair.first->as>(), preparedFormulas); + verifySparseModel(modelProgramPair.model->as>(), preparedFormulas); } - } else if (modelProgramPair.first->isSymbolicModel()) { + } else if (modelProgramPair.model->isSymbolicModel()) { if (storm::settings::generalSettings().getEngine() == storm::settings::modules::GeneralSettings::Engine::Hybrid) { - verifySymbolicModelWithHybridEngine(modelProgramPair.first->as>(), preparedFormulas); + verifySymbolicModelWithHybridEngine(modelProgramPair.model->as>(), preparedFormulas); } else { - verifySymbolicModelWithSymbolicEngine(modelProgramPair.first->as>(), preparedFormulas); + verifySymbolicModelWithSymbolicEngine(modelProgramPair.model->as>(), preparedFormulas); } } else { STORM_LOG_THROW(false, storm::exceptions::InvalidSettingsException, "Invalid input model type."); diff --git a/src/storage/ModelProgramPair.h b/src/storage/ModelProgramPair.h new file mode 100644 index 000000000..c50b6d306 --- /dev/null +++ b/src/storage/ModelProgramPair.h @@ -0,0 +1,12 @@ +#include "../models/ModelBase.h" +#include "prism/Program.h" + + +namespace storm { + namespace storage { + struct ModelProgramPair { + std::shared_ptr model; + storm::prism::Program program; + }; + } +} \ No newline at end of file diff --git a/src/utility/storm.h b/src/utility/storm.h index d607f01ad..af70bb89c 100644 --- a/src/utility/storm.h +++ b/src/utility/storm.h @@ -46,6 +46,7 @@ // Headers for model processing. #include "src/storage/bisimulation/DeterministicModelBisimulationDecomposition.h" #include "src/storage/bisimulation/NondeterministicModelBisimulationDecomposition.h" +#include "src/storage/ModelProgramPair.h" // Headers for model checking. #include "src/modelchecker/prctl/SparseDtmcPrctlModelChecker.h" @@ -83,8 +84,8 @@ namespace storm { std::vector> parseFormulasForProgram(std::string const& inputString, storm::prism::Program const& program); template - std::pair, storm::prism::Program> buildSymbolicModel(storm::prism::Program const& program, std::vector> const& formulas) { - std::pair, storm::prism::Program> result; + storm::storage::ModelProgramPair buildSymbolicModel(storm::prism::Program const& program, std::vector> const& formulas) { + storm::storage::ModelProgramPair result; storm::settings::modules::GeneralSettings settings = storm::settings::generalSettings(); @@ -103,16 +104,16 @@ namespace storm { } storm::builder::ExplicitPrismModelBuilder builder; - result.first = builder.translateProgram(program, options); - result.second = builder.getTranslatedProgram(); + result.model = builder.translateProgram(program, options); + result.program = builder.getTranslatedProgram(); } else if (settings.getEngine() == storm::settings::modules::GeneralSettings::Engine::Dd || settings.getEngine() == storm::settings::modules::GeneralSettings::Engine::Hybrid) { typename storm::builder::DdPrismModelBuilder::Options options; options = typename storm::builder::DdPrismModelBuilder::Options(formulas); options.addConstantDefinitionsFromString(program, constants); storm::builder::DdPrismModelBuilder builder; - result.first = builder.translateProgram(program, options); - result.second = builder.getTranslatedProgram(); + result.model = builder.translateProgram(program, options); + result.program = builder.getTranslatedProgram(); } return result;