Browse Source

Merge branch 'future' into menu_games

Former-commit-id: 92b1722891
main
dehnert 10 years ago
parent
commit
7c3333497a
  1. 1
      .gitignore
  2. 20
      CMakeLists.txt
  3. 1
      resources/3rdparty/sylvan/src/sylvan_mtbdd.h
  4. 179
      resources/cmake/FindHwloc.cmake
  5. 22
      src/cli/entrypoints.h
  6. 12
      src/storage/ModelProgramPair.h
  7. 13
      src/utility/storm.h

1
.gitignore

@ -47,5 +47,6 @@ build//CMakeLists.txt
# CMake generated/configured files
src/utility/storm-version.cpp
.DS_Store
.idea
*.out

20
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()
#############################################################
##

1
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)

179
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 <hwloc.h>
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()

22
src/cli/entrypoints.h

@ -108,14 +108,14 @@ namespace storm {
template<typename ValueType, storm::dd::DdType LibraryType>
void buildAndCheckSymbolicModel(storm::prism::Program const& program, std::vector<std::shared_ptr<storm::logic::Formula>> const& formulas) {
std::pair<std::shared_ptr<storm::models::ModelBase>, storm::prism::Program> modelProgramPair = buildSymbolicModel<ValueType, LibraryType>(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<ValueType, LibraryType>(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<storm::expressions::Variable, storm::expressions::Expression> 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<ValueType>(program, modelProgramPair.first->as<storm::models::sparse::Model<ValueType>>(), formula);
generateCounterexample<ValueType>(program, modelProgramPair.model->as<storm::models::sparse::Model<ValueType>>(), formula);
}
} else {
verifySparseModel<ValueType>(modelProgramPair.first->as<storm::models::sparse::Model<ValueType>>(), preparedFormulas);
verifySparseModel<ValueType>(modelProgramPair.model->as<storm::models::sparse::Model<ValueType>>(), 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<storm::models::symbolic::Model<LibraryType>>(), preparedFormulas);
verifySymbolicModelWithHybridEngine(modelProgramPair.model->as<storm::models::symbolic::Model<LibraryType>>(), preparedFormulas);
} else {
verifySymbolicModelWithSymbolicEngine(modelProgramPair.first->as<storm::models::symbolic::Model<LibraryType>>(), preparedFormulas);
verifySymbolicModelWithSymbolicEngine(modelProgramPair.model->as<storm::models::symbolic::Model<LibraryType>>(), preparedFormulas);
}
} else {
STORM_LOG_THROW(false, storm::exceptions::InvalidSettingsException, "Invalid input model type.");

12
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<storm::models::ModelBase> model;
storm::prism::Program program;
};
}
}

13
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<std::shared_ptr<storm::logic::Formula>> parseFormulasForProgram(std::string const& inputString, storm::prism::Program const& program);
template<typename ValueType, storm::dd::DdType LibraryType = storm::dd::DdType::CUDD>
std::pair<std::shared_ptr<storm::models::ModelBase>, storm::prism::Program> buildSymbolicModel(storm::prism::Program const& program, std::vector<std::shared_ptr<storm::logic::Formula>> const& formulas) {
std::pair<std::shared_ptr<storm::models::ModelBase>, storm::prism::Program> result;
storm::storage::ModelProgramPair buildSymbolicModel(storm::prism::Program const& program, std::vector<std::shared_ptr<storm::logic::Formula>> const& formulas) {
storm::storage::ModelProgramPair result;
storm::settings::modules::GeneralSettings settings = storm::settings::generalSettings();
@ -103,16 +104,16 @@ namespace storm {
}
storm::builder::ExplicitPrismModelBuilder<ValueType> 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<LibraryType>::Options options;
options = typename storm::builder::DdPrismModelBuilder<LibraryType>::Options(formulas);
options.addConstantDefinitionsFromString(program, constants);
storm::builder::DdPrismModelBuilder<LibraryType> builder;
result.first = builder.translateProgram(program, options);
result.second = builder.getTranslatedProgram();
result.model = builder.translateProgram(program, options);
result.program = builder.getTranslatedProgram();
}
return result;

Loading…
Cancel
Save