From 2e035f39578c64798b4cff6b2b2c02cfc11480a0 Mon Sep 17 00:00:00 2001 From: TimQu Date: Mon, 23 Jul 2018 10:11:42 +0200 Subject: [PATCH] started working on conversion binary --- src/CMakeLists.txt | 3 +- src/storm-conv-cli/CMakeLists.txt | 9 + src/storm-conv-cli/storm-conv.cpp | 539 ++++++++++++++++++++++++++++++ src/storm-conv/CMakeLists.txt | 40 +++ src/storm-conv/api/storm-conv.h | 4 + 5 files changed, 594 insertions(+), 1 deletion(-) create mode 100644 src/storm-conv-cli/CMakeLists.txt create mode 100644 src/storm-conv-cli/storm-conv.cpp create mode 100644 src/storm-conv/CMakeLists.txt create mode 100644 src/storm-conv/api/storm-conv.h diff --git a/src/CMakeLists.txt b/src/CMakeLists.txt index 7239a9676..6c61656ab 100644 --- a/src/CMakeLists.txt +++ b/src/CMakeLists.txt @@ -16,7 +16,8 @@ add_subdirectory(storm-dft) add_subdirectory(storm-dft-cli) add_subdirectory(storm-pars) add_subdirectory(storm-pars-cli) - +add_subdirectory(storm-conv) +add_subdirectory(storm-conv-cli) add_subdirectory(test) diff --git a/src/storm-conv-cli/CMakeLists.txt b/src/storm-conv-cli/CMakeLists.txt new file mode 100644 index 000000000..72a311b11 --- /dev/null +++ b/src/storm-conv-cli/CMakeLists.txt @@ -0,0 +1,9 @@ +# Create storm-conv. +add_executable(storm-conv-cli ${PROJECT_SOURCE_DIR}/src/storm-conv-cli/storm-conv.cpp) +target_link_libraries(storm-conv-cli storm-conv storm-cli-utilities) # Adding headers for xcode +set_target_properties(storm-conv-cli PROPERTIES OUTPUT_NAME "storm-conv") + +add_dependencies(binaries storm-conv-cli) + +# installation +install(TARGETS storm-conv-cli EXPORT storm_Targets RUNTIME DESTINATION bin LIBRARY DESTINATION lib OPTIONAL) diff --git a/src/storm-conv-cli/storm-conv.cpp b/src/storm-conv-cli/storm-conv.cpp new file mode 100644 index 000000000..badcb0212 --- /dev/null +++ b/src/storm-conv-cli/storm-conv.cpp @@ -0,0 +1,539 @@ + +#include "storm-pars/api/storm-pars.h" +#include "storm-pars/settings/ParsSettings.h" +#include "storm-pars/settings/modules/ParametricSettings.h" +#include "storm-pars/settings/modules/RegionSettings.h" + +#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" +#include "storm/utility/initialize.h" +#include "storm/utility/Stopwatch.h" +#include "storm/utility/macros.h" + +#include "storm-pars/modelchecker/instantiation/SparseCtmcInstantiationModelChecker.h" + +#include "storm/settings/modules/GeneralSettings.h" +#include "storm/settings/modules/CoreSettings.h" +#include "storm/settings/modules/IOSettings.h" +#include "storm/settings/modules/BisimulationSettings.h" + +#include "storm/exceptions/BaseException.h" +#include "storm/exceptions/InvalidSettingsException.h" +#include "storm/exceptions/NotSupportedException.h" + +namespace storm { + namespace pars { + + typedef typename storm::cli::SymbolicInput SymbolicInput; + + template + struct SampleInformation { + SampleInformation(bool graphPreserving = false, bool exact = false) : graphPreserving(graphPreserving), exact(exact) { + // Intentionally left empty. + } + + bool empty() const { + return cartesianProducts.empty(); + } + + std::vector::type, std::vector::type>>> cartesianProducts; + bool graphPreserving; + bool exact; + }; + + template + std::vector> parseRegions(std::shared_ptr const& model) { + std::vector> result; + auto regionSettings = storm::settings::getModule(); + if (regionSettings.isRegionSet()) { + result = storm::api::parseRegions(regionSettings.getRegionString(), *model); + } + return result; + } + + template + SampleInformation parseSamples(std::shared_ptr const& model, std::string const& sampleString, bool graphPreserving) { + STORM_LOG_THROW(!model || model->isSparseModel(), storm::exceptions::NotSupportedException, "Sampling is only supported for sparse models."); + + SampleInformation sampleInfo(graphPreserving); + if (sampleString.empty()) { + return sampleInfo; + } + + // Get all parameters from the model. + std::set::type> modelParameters; + auto const& sparseModel = *model->as>(); + modelParameters = storm::models::sparse::getProbabilityParameters(sparseModel); + auto rewParameters = storm::models::sparse::getRewardParameters(sparseModel); + modelParameters.insert(rewParameters.begin(), rewParameters.end()); + + std::vector cartesianProducts; + boost::split(cartesianProducts, sampleString, boost::is_any_of(";")); + for (auto& product : cartesianProducts) { + boost::trim(product); + + // Get the values string for each variable. + std::vector valuesForVariables; + boost::split(valuesForVariables, product, boost::is_any_of(",")); + for (auto& values : valuesForVariables) { + boost::trim(values); + } + + std::set::type> encounteredParameters; + sampleInfo.cartesianProducts.emplace_back(); + auto& newCartesianProduct = sampleInfo.cartesianProducts.back(); + for (auto const& varValues : valuesForVariables) { + auto equalsPosition = varValues.find("="); + STORM_LOG_THROW(equalsPosition != varValues.npos, storm::exceptions::WrongFormatException, "Incorrect format of samples."); + std::string variableName = varValues.substr(0, equalsPosition); + boost::trim(variableName); + std::string values = varValues.substr(equalsPosition + 1); + boost::trim(values); + + bool foundParameter = false; + typename utility::parametric::VariableType::type theParameter; + for (auto const& parameter : modelParameters) { + std::stringstream parameterStream; + parameterStream << parameter; + if (parameterStream.str() == variableName) { + foundParameter = true; + theParameter = parameter; + encounteredParameters.insert(parameter); + } + } + STORM_LOG_THROW(foundParameter, storm::exceptions::WrongFormatException, "Unknown parameter '" << variableName << "'."); + + std::vector splitValues; + boost::split(splitValues, values, boost::is_any_of(":")); + STORM_LOG_THROW(!splitValues.empty(), storm::exceptions::WrongFormatException, "Expecting at least one value per parameter."); + + auto& list = newCartesianProduct[theParameter]; + + for (auto& value : splitValues) { + boost::trim(value); + list.push_back(storm::utility::convertNumber::type>(value)); + } + } + + STORM_LOG_THROW(encounteredParameters == modelParameters, storm::exceptions::WrongFormatException, "Variables for all parameters are required when providing samples."); + } + + return sampleInfo; + } + + template + std::pair, bool> preprocessSparseModel(std::shared_ptr> const& model, SymbolicInput const& input) { + auto generalSettings = storm::settings::getModule(); + auto bisimulationSettings = storm::settings::getModule(); + auto parametricSettings = storm::settings::getModule(); + + std::pair, bool> result = std::make_pair(model, false); + + if (result.first->isOfType(storm::models::ModelType::MarkovAutomaton)) { + result.first = storm::cli::preprocessSparseMarkovAutomaton(result.first->template as>()); + result.second = true; + } + + if (generalSettings.isBisimulationSet()) { + result.first = storm::cli::preprocessSparseModelBisimulation(result.first->template as>(), input, bisimulationSettings); + result.second = true; + } + + if (parametricSettings.transformContinuousModel() && (result.first->isOfType(storm::models::ModelType::Ctmc) || result.first->isOfType(storm::models::ModelType::MarkovAutomaton))) { + result.first = storm::api::transformContinuousToDiscreteTimeSparseModel(std::move(*result.first->template as>()), storm::api::extractFormulasFromProperties(input.properties)); + result.second = true; + } + + return result; + } + + template + std::pair, bool> preprocessDdModel(std::shared_ptr> const& model, SymbolicInput const& input) { + + std::pair, bool> result = std::make_pair(model, false); + + auto coreSettings = storm::settings::getModule(); + if (coreSettings.getEngine() == storm::settings::modules::CoreSettings::Engine::Hybrid) { + // Currently, hybrid engine for parametric models just referrs to building the model symbolically. + STORM_LOG_INFO("Translating symbolic model to sparse model..."); + result.first = storm::api::transformSymbolicToSparseModel(model); + result.second = true; + // Invoke preprocessing on the sparse model + auto sparsePreprocessingResult = storm::pars::preprocessSparseModel(result.first->as>(), input); + if (sparsePreprocessingResult.second) { + result.first = sparsePreprocessingResult.first; + } + } + return result; + } + + template + std::pair, bool> preprocessModel(std::shared_ptr const& model, SymbolicInput const& input) { + storm::utility::Stopwatch preprocessingWatch(true); + + std::pair, bool> result = std::make_pair(model, false); + if (model->isSparseModel()) { + result = storm::pars::preprocessSparseModel(result.first->as>(), input); + } else { + STORM_LOG_ASSERT(model->isSymbolicModel(), "Unexpected model type."); + result = storm::pars::preprocessDdModel(result.first->as>(), input); + } + + if (result.second) { + STORM_PRINT_AND_LOG(std::endl << "Time for model preprocessing: " << preprocessingWatch << "." << std::endl << std::endl); + } + return result; + } + + template + void printInitialStatesResult(std::unique_ptr const& result, storm::jani::Property const& property, storm::utility::Stopwatch* watch = nullptr, storm::utility::parametric::Valuation const* valuation = nullptr) { + if (result) { + STORM_PRINT_AND_LOG("Result (initial states)"); + if (valuation) { + bool first = true; + std::stringstream ss; + for (auto const& entry : *valuation) { + if (!first) { + ss << ", "; + } else { + first = false; + } + ss << entry.first << "=" << entry.second; + } + + STORM_PRINT_AND_LOG(" for instance [" << ss.str() << "]"); + } + STORM_PRINT_AND_LOG(": ") + + auto const* regionCheckResult = dynamic_cast const*>(result.get()); + if (regionCheckResult != nullptr) { + auto regionSettings = storm::settings::getModule(); + std::stringstream outStream; + if (regionSettings.isPrintFullResultSet()) { + regionCheckResult->writeToStream(outStream); + } else { + regionCheckResult->writeCondensedToStream(outStream); + } + outStream << std::endl; + if (!regionSettings.isPrintNoIllustrationSet()) { + auto const* regionRefinementCheckResult = dynamic_cast const*>(regionCheckResult); + if (regionRefinementCheckResult != nullptr) { + regionRefinementCheckResult->writeIllustrationToStream(outStream); + } + } + outStream << std::endl; + STORM_PRINT_AND_LOG(outStream.str()); + } else { + STORM_PRINT_AND_LOG(*result << std::endl); + } + if (watch) { + STORM_PRINT_AND_LOG("Time for model checking: " << *watch << "." << std::endl << std::endl); + } + } else { + STORM_PRINT_AND_LOG(" failed, property is unsupported by selected engine/settings." << std::endl); + } + } + + template + void verifyProperties(std::vector const& properties, std::function(std::shared_ptr const& formula)> const& verificationCallback, std::function const&)> const& postprocessingCallback) { + for (auto const& property : properties) { + storm::cli::printModelCheckingProperty(property); + storm::utility::Stopwatch watch(true); + std::unique_ptr result = verificationCallback(property.getRawFormula()); + watch.stop(); + printInitialStatesResult(result, property, &watch); + postprocessingCallback(result); + } + } + + template class ModelCheckerType, typename ModelType, typename ValueType, typename SolveValueType = double> + void verifyPropertiesAtSamplePoints(ModelType const& model, SymbolicInput const& input, SampleInformation const& samples) { + + // When samples are provided, we create an instantiation model checker. + ModelCheckerType modelchecker(model); + + for (auto const& property : input.properties) { + storm::cli::printModelCheckingProperty(property); + + modelchecker.specifyFormula(storm::api::createTask(property.getRawFormula(), true)); + modelchecker.setInstantiationsAreGraphPreserving(samples.graphPreserving); + + storm::utility::parametric::Valuation valuation; + + std::vector::type> parameters; + std::vector::type>::const_iterator> iterators; + std::vector::type>::const_iterator> iteratorEnds; + + storm::utility::Stopwatch watch(true); + for (auto const& product : samples.cartesianProducts) { + parameters.clear(); + iterators.clear(); + iteratorEnds.clear(); + + for (auto const& entry : product) { + parameters.push_back(entry.first); + iterators.push_back(entry.second.cbegin()); + iteratorEnds.push_back(entry.second.cend()); + } + + bool done = false; + while (!done) { + // Read off valuation. + for (uint64_t i = 0; i < parameters.size(); ++i) { + valuation[parameters[i]] = *iterators[i]; + } + + storm::utility::Stopwatch valuationWatch(true); + std::unique_ptr result = modelchecker.check(Environment(), valuation); + valuationWatch.stop(); + + if (result) { + result->filter(storm::modelchecker::ExplicitQualitativeCheckResult(model.getInitialStates())); + } + printInitialStatesResult(result, property, &valuationWatch, &valuation); + + for (uint64_t i = 0; i < parameters.size(); ++i) { + ++iterators[i]; + if (iterators[i] == iteratorEnds[i]) { + // Reset iterator and proceed to move next iterator. + iterators[i] = product.at(parameters[i]).cbegin(); + + // If the last iterator was removed, we are done. + if (i == parameters.size() - 1) { + done = true; + } + } else { + // If an iterator was moved but not reset, we have another valuation to check. + break; + } + } + + } + } + + watch.stop(); + STORM_PRINT_AND_LOG("Overall time for sampling all instances: " << watch << std::endl << std::endl); + } + } + + template + void verifyPropertiesAtSamplePoints(std::shared_ptr> const& model, SymbolicInput const& input, SampleInformation const& samples) { + if (model->isOfType(storm::models::ModelType::Dtmc)) { + verifyPropertiesAtSamplePoints, ValueType, SolveValueType>(*model->template as>(), input, samples); + } else if (model->isOfType(storm::models::ModelType::Ctmc)) { + verifyPropertiesAtSamplePoints, ValueType, SolveValueType>(*model->template as>(), input, samples); + } else if (model->isOfType(storm::models::ModelType::Ctmc)) { + verifyPropertiesAtSamplePoints, ValueType, SolveValueType>(*model->template as>(), input, samples); + } else { + STORM_LOG_THROW(false, storm::exceptions::NotSupportedException, "Sampling is currently only supported for DTMCs, CTMCs and MDPs."); + } + } + + template + void verifyPropertiesWithSparseEngine(std::shared_ptr> const& model, SymbolicInput const& input, SampleInformation const& samples) { + + if (samples.empty()) { + verifyProperties(input.properties, + [&model] (std::shared_ptr const& formula) { + std::unique_ptr result = storm::api::verifyWithSparseEngine(model, storm::api::createTask(formula, true)); + if (result) { + result->filter(storm::modelchecker::ExplicitQualitativeCheckResult(model->getInitialStates())); + } + return result; + }, + [&model] (std::unique_ptr const& result) { + auto parametricSettings = storm::settings::getModule(); + if (parametricSettings.exportResultToFile() && model->isOfType(storm::models::ModelType::Dtmc)) { + auto dtmc = model->template as>(); + boost::optional rationalFunction = result->asExplicitQuantitativeCheckResult()[*model->getInitialStates().begin()]; + storm::api::exportParametricResultToFile(rationalFunction, storm::analysis::ConstraintCollector(*dtmc), parametricSettings.exportResultPath()); + } + }); + } else { + STORM_LOG_TRACE("Sampling the model at given points."); + + if (samples.exact) { + verifyPropertiesAtSamplePoints(model, input, samples); + } else { + verifyPropertiesAtSamplePoints(model, input, samples); + } + } + } + + template + void verifyRegionsWithSparseEngine(std::shared_ptr> const& model, SymbolicInput const& input, std::vector> const& regions) { + STORM_LOG_ASSERT(!regions.empty(), "Can not analyze an empty set of regions."); + + auto parametricSettings = storm::settings::getModule(); + auto regionSettings = storm::settings::getModule(); + + std::function(std::shared_ptr const& formula)> verificationCallback; + std::function const&)> postprocessingCallback; + + STORM_PRINT_AND_LOG(std::endl); + if (regionSettings.isHypothesisSet()) { + STORM_PRINT_AND_LOG("Checking hypothesis " << regionSettings.getHypothesis() << " on "); + } else { + STORM_PRINT_AND_LOG("Analyzing "); + } + if (regions.size() == 1) { + STORM_PRINT_AND_LOG("parameter region " << regions.front()); + } else { + STORM_PRINT_AND_LOG(regions.size() << " parameter regions"); + } + auto engine = regionSettings.getRegionCheckEngine(); + STORM_PRINT_AND_LOG(" using " << engine); + + // Check the given set of regions with or without refinement + if (regionSettings.isRefineSet()) { + STORM_LOG_THROW(regions.size() == 1, storm::exceptions::NotSupportedException, "Region refinement is not supported for multiple initial regions."); + STORM_PRINT_AND_LOG(" with iterative refinement until " << (1.0 - regionSettings.getCoverageThreshold()) * 100.0 << "% is covered." << (regionSettings.isDepthLimitSet() ? " Depth limit is " + std::to_string(regionSettings.getDepthLimit()) + "." : "") << std::endl); + verificationCallback = [&] (std::shared_ptr const& formula) { + ValueType refinementThreshold = storm::utility::convertNumber(regionSettings.getCoverageThreshold()); + boost::optional optionalDepthLimit; + if (regionSettings.isDepthLimitSet()) { + optionalDepthLimit = regionSettings.getDepthLimit(); + } + std::unique_ptr> result = storm::api::checkAndRefineRegionWithSparseEngine(model, storm::api::createTask(formula, true), regions.front(), engine, refinementThreshold, optionalDepthLimit, regionSettings.getHypothesis()); + return result; + }; + } else { + STORM_PRINT_AND_LOG("." << std::endl); + verificationCallback = [&] (std::shared_ptr const& formula) { + std::unique_ptr result = storm::api::checkRegionsWithSparseEngine(model, storm::api::createTask(formula, true), regions, engine, regionSettings.getHypothesis()); + return result; + }; + } + + postprocessingCallback = [&] (std::unique_ptr const& result) { + if (parametricSettings.exportResultToFile()) { + storm::api::exportRegionCheckResultToFile(result, parametricSettings.exportResultPath()); + } + }; + + verifyProperties(input.properties, verificationCallback, postprocessingCallback); + } + + template + void verifyWithSparseEngine(std::shared_ptr> const& model, SymbolicInput const& input, std::vector> const& regions, SampleInformation const& samples) { + if (regions.empty()) { + storm::pars::verifyPropertiesWithSparseEngine(model, input, samples); + } else { + storm::pars::verifyRegionsWithSparseEngine(model, input, regions); + } + } + + template + void verifyParametricModel(std::shared_ptr const& model, SymbolicInput const& input, std::vector> const& regions, SampleInformation const& samples) { + STORM_LOG_ASSERT(model->isSparseModel(), "Unexpected model type."); + storm::pars::verifyWithSparseEngine(model->as>(), input, regions, samples); + } + + template + void processInputWithValueTypeAndDdlib(SymbolicInput& input) { + auto coreSettings = storm::settings::getModule(); + auto ioSettings = storm::settings::getModule(); + + auto buildSettings = storm::settings::getModule(); + auto parSettings = storm::settings::getModule(); + + auto engine = coreSettings.getEngine(); + STORM_LOG_THROW(engine == storm::settings::modules::CoreSettings::Engine::Sparse || engine == storm::settings::modules::CoreSettings::Engine::Hybrid || engine == storm::settings::modules::CoreSettings::Engine::Dd, storm::exceptions::InvalidSettingsException, "The selected engine is not supported for parametric models."); + + std::shared_ptr model; + if (!buildSettings.isNoBuildModelSet()) { + model = storm::cli::buildModel(engine, input, ioSettings); + } + + if (model) { + model->printModelInformationToStream(std::cout); + } + + STORM_LOG_THROW(model || input.properties.empty(), storm::exceptions::InvalidSettingsException, "No input model."); + + if (model) { + auto preprocessingResult = storm::pars::preprocessModel(model, input); + if (preprocessingResult.second) { + model = preprocessingResult.first; + model->printModelInformationToStream(std::cout); + } + } + + std::vector> regions = parseRegions(model); + std::string samplesAsString = parSettings.getSamples(); + SampleInformation samples; + if (!samplesAsString.empty()) { + samples = parseSamples(model, samplesAsString, parSettings.isSamplesAreGraphPreservingSet()); + samples.exact = parSettings.isSampleExactSet(); + } + + if (model) { + storm::cli::exportModel(model, input); + } + + if (parSettings.onlyObtainConstraints()) { + STORM_LOG_THROW(parSettings.exportResultToFile(), storm::exceptions::InvalidSettingsException, "When computing constraints, export path has to be specified."); + storm::api::exportParametricResultToFile(boost::none, storm::analysis::ConstraintCollector(*(model->as>())), parSettings.exportResultPath()); + return; + } + + if (model) { + verifyParametricModel(model, input, regions, samples); + } + } + + void processOptions() { + // Start by setting some urgent options (log levels, resources, etc.) + storm::cli::setUrgentOptions(); + + // Parse and preprocess symbolic input (PRISM, JANI, properties, etc.) + SymbolicInput symbolicInput = storm::cli::parseAndPreprocessSymbolicInput(); + + auto coreSettings = storm::settings::getModule(); + auto engine = coreSettings.getEngine(); + STORM_LOG_WARN_COND(engine != storm::settings::modules::CoreSettings::Engine::Dd || engine != storm::settings::modules::CoreSettings::Engine::Hybrid || coreSettings.getDdLibraryType() == storm::dd::DdType::Sylvan, "The selected DD library does not support parametric models. Switching to Sylvan..."); + + processInputWithValueTypeAndDdlib(symbolicInput); + } + + } +} + + +/*! + * Main entry point of the executable storm-pars. + */ +int main(const int argc, const char** argv) { + + try { + storm::utility::setUp(); + storm::cli::printHeader("Storm-pars", argc, argv); + storm::settings::initializeParsSettings("Storm-pars", "storm-pars"); + + storm::utility::Stopwatch totalTimer(true); + if (!storm::cli::parseOptions(argc, argv)) { + return -1; + } + + storm::pars::processOptions(); + + totalTimer.stop(); + if (storm::settings::getModule().isPrintTimeAndMemorySet()) { + storm::cli::printTimeAndMemoryStatistics(totalTimer.getTimeInMilliseconds()); + } + + storm::utility::cleanUp(); + return 0; + } catch (storm::exceptions::BaseException const& exception) { + STORM_LOG_ERROR("An exception caused Storm-pars to terminate. The message of the exception is: " << exception.what()); + return 1; + } catch (std::exception const& exception) { + STORM_LOG_ERROR("An unexpected exception occurred and caused Storm-pars to terminate. The message of this exception is: " << exception.what()); + return 2; + } +} diff --git a/src/storm-conv/CMakeLists.txt b/src/storm-conv/CMakeLists.txt new file mode 100644 index 000000000..4ead2828e --- /dev/null +++ b/src/storm-conv/CMakeLists.txt @@ -0,0 +1,40 @@ +file(GLOB_RECURSE ALL_FILES ${PROJECT_SOURCE_DIR}/src/storm-conv/*.h ${PROJECT_SOURCE_DIR}/src/storm-conv/*.cpp) + +register_source_groups_from_filestructure("${ALL_FILES}" storm-conv) + + + +file(GLOB_RECURSE STORM_CONV_SOURCES ${PROJECT_SOURCE_DIR}/src/storm-conv/*/*.cpp) +file(GLOB_RECURSE STORM_CONV_HEADERS ${PROJECT_SOURCE_DIR}/src/storm-conv/*/*.h) + + +# Create storm-conv. +add_library(storm-conv SHARED ${STORM_CONV_SOURCES} ${STORM_CONV_HEADERS}) + +# Remove define symbol for shared libstorm. +set_target_properties(storm-conv PROPERTIES DEFINE_SYMBOL "") +#add_dependencies(storm resources) +list(APPEND STORM_TARGETS storm-conv) +set(STORM_TARGETS ${STORM_TARGETS} PARENT_SCOPE) + +target_link_libraries(storm-conv PUBLIC storm ${STORM_CONV_LINK_LIBRARIES}) + +# Install storm headers to include directory. +foreach(HEADER ${STORM_CONV_HEADERS}) + string(REGEX REPLACE "${PROJECT_SOURCE_DIR}/src/?" "" RELATIVE_HEADER_PATH ${HEADER}) + string(REGEX MATCH "(.*)[/\\]" RELATIVE_DIRECTORY ${RELATIVE_HEADER_PATH}) + string(REGEX REPLACE "${RELATIVE_DIRECTORY}/?" "" HEADER_FILENAME ${RELATIVE_HEADER_PATH}) + add_custom_command( + OUTPUT ${CMAKE_BINARY_DIR}/include/${RELATIVE_DIRECTORY}${HEADER_FILENAME} + COMMAND ${CMAKE_COMMAND} -E make_directory ${CMAKE_BINARY_DIR}/include/${RELATIVE_DIRECTORY} + COMMAND ${CMAKE_COMMAND} -E copy ${HEADER} ${CMAKE_BINARY_DIR}/include/${RELATIVE_DIRECTORY}${HEADER_FILENAME} + DEPENDS ${HEADER} + ) + list(APPEND STORM_CONV_OUTPUT_HEADERS "${CMAKE_BINARY_DIR}/include/${RELATIVE_DIRECTORY}${HEADER_FILENAME}") +endforeach() +add_custom_target(copy_storm_conv_headers DEPENDS ${STORM_CONV_OUTPUT_HEADERS} ${STORM_CONV_HEADERS}) +add_dependencies(storm-conv copy_storm_conv_headers) + +# installation +install(TARGETS storm-conv EXPORT storm_Targets RUNTIME DESTINATION bin LIBRARY DESTINATION lib OPTIONAL) + diff --git a/src/storm-conv/api/storm-conv.h b/src/storm-conv/api/storm-conv.h new file mode 100644 index 000000000..a1a32ac05 --- /dev/null +++ b/src/storm-conv/api/storm-conv.h @@ -0,0 +1,4 @@ +#pragma once + +#include "storm-pars/api/region.h" +#include "storm-pars/api/export.h" \ No newline at end of file