From 8a48f80a99515a130df193b7b5b673c870f37368 Mon Sep 17 00:00:00 2001 From: sjunges Date: Mon, 7 Sep 2015 18:26:46 +0200 Subject: [PATCH 1/4] use ccache as an option Former-commit-id: 9f7fa74225fb04b5b16e0178a1979e43f2195c5c --- CMakeLists.txt | 12 +++++++++++- 1 file changed, 11 insertions(+), 1 deletion(-) diff --git a/CMakeLists.txt b/CMakeLists.txt index 46b02df5c..bf0d72079 100644 --- a/CMakeLists.txt +++ b/CMakeLists.txt @@ -26,6 +26,7 @@ option(LINK_LIBCXXABI "Sets whether libc++abi should be linked." OFF) option(USE_LIBCXX "Sets whether the standard library is libc++." OFF) option(USE_CARL "Sets whether carl should be included." ON) option(FORCE_COLOR "Force color output" OFF) +option(STOMR_COMPILE_WITH_CCACHE "Compile using CCache" ON) set(GUROBI_ROOT "" CACHE STRING "A hint to the root directory of Gurobi (optional).") set(Z3_ROOT "" CACHE STRING "A hint to the root directory of Z3 (optional).") set(CUDA_ROOT "" CACHE STRING "The root directory of CUDA.") @@ -43,7 +44,16 @@ endif() message(STATUS "StoRM - Building ${CMAKE_BUILD_TYPE} version.") message(STATUS "StoRM - CMAKE_BUILD_TYPE (ENV): $ENV{CMAKE_BUILD_TYPE}") - +if(STOMR_COMPILE_WITH_CCACHE) + find_program(CCACHE_FOUND ccache) + if(CCACHE_FOUND) + message(STATUS "SToRM - Using ccache") + set_property(GLOBAL PROPERTY RULE_LAUNCH_COMPILE ccache) + set_property(GLOBAL PROPERTY RULE_LAUNCH_LINK ccache) + else() + message(STATUS "Could not find ccache") + endif() +endif() # Base path for test files set(STORM_CPP_TESTS_BASE_PATH "${PROJECT_SOURCE_DIR}/test") From 8fd0ee2ecd292a9c3159c3128e90f455ac18db57 Mon Sep 17 00:00:00 2001 From: sjunges Date: Mon, 7 Sep 2015 18:27:19 +0200 Subject: [PATCH 2/4] Formula to string added Former-commit-id: 53eb9bb5b43e50f3c385d09ed858a889678500b5 --- src/logic/Formula.cpp | 7 +++++++ src/logic/Formula.h | 1 + 2 files changed, 8 insertions(+) diff --git a/src/logic/Formula.cpp b/src/logic/Formula.cpp index 4037cb723..e621c1c78 100644 --- a/src/logic/Formula.cpp +++ b/src/logic/Formula.cpp @@ -1,4 +1,5 @@ #include "src/logic/Formulas.h" +#include namespace storm { namespace logic { @@ -404,6 +405,12 @@ namespace storm { return; } + std::string Formula::toString() const { + std::stringstream str2; + writeToStream(str2); + return str2.str(); + } + std::ostream& operator<<(std::ostream& out, Formula const& formula) { return formula.writeToStream(out); } diff --git a/src/logic/Formula.h b/src/logic/Formula.h index 3c3c3b5aa..4d831e456 100644 --- a/src/logic/Formula.h +++ b/src/logic/Formula.h @@ -174,6 +174,7 @@ namespace storm { std::shared_ptr asSharedPointer(); std::shared_ptr asSharedPointer() const; + std::string toString() const; virtual std::ostream& writeToStream(std::ostream& out) const = 0; virtual void gatherAtomicExpressionFormulas(std::vector>& atomicExpressionFormulas) const; From c281efcde348d0d29d0ef1e8c8d8acd52d9e37ab Mon Sep 17 00:00:00 2001 From: sjunges Date: Tue, 8 Sep 2015 11:28:44 +0200 Subject: [PATCH 3/4] refactored parts of the api Former-commit-id: 3457c238bb94d7a78a12cc95594112bf15563498 --- src/utility/storm.h | 153 ++++++++++++++++++++++++-------------------- 1 file changed, 85 insertions(+), 68 deletions(-) diff --git a/src/utility/storm.h b/src/utility/storm.h index 7fa547588..bb3a0a8a5 100644 --- a/src/utility/storm.h +++ b/src/utility/storm.h @@ -170,28 +170,26 @@ namespace storm { STORM_LOG_THROW(false, storm::exceptions::InvalidSettingsException, "Unable to generate counterexample for parametric model."); } #endif - + template - void verifySparseModel(std::shared_ptr> model, std::vector> const& formulas) { - for (auto const& formula : formulas) { + std::unique_ptr verifySparseModel(std::shared_ptr> model, std::shared_ptr const& formula) { - std::cout << std::endl << "Model checking property: " << *formula << " ..."; - std::unique_ptr result; - if (model->getType() == storm::models::ModelType::Dtmc) { - std::shared_ptr> dtmc = model->template as>(); - storm::modelchecker::SparseDtmcPrctlModelChecker> modelchecker(*dtmc); - if (modelchecker.canHandle(*formula)) { - result = modelchecker.check(*formula); - } else { - storm::modelchecker::SparseDtmcEliminationModelChecker> modelchecker2(*dtmc); - if (modelchecker2.canHandle(*formula)) { - result = modelchecker2.check(*formula); - } + std::unique_ptr result; + if (model->getType() == storm::models::ModelType::Dtmc) { + std::shared_ptr> dtmc = model->template as>(); + storm::modelchecker::SparseDtmcPrctlModelChecker> modelchecker(*dtmc); + if (modelchecker.canHandle(*formula)) { + result = modelchecker.check(*formula); + } else { + storm::modelchecker::SparseDtmcEliminationModelChecker> modelchecker2(*dtmc); + if (modelchecker2.canHandle(*formula)) { + result = modelchecker2.check(*formula); } - } else if (model->getType() == storm::models::ModelType::Mdp) { - std::shared_ptr> mdp = model->template as>(); + } + } else if (model->getType() == storm::models::ModelType::Mdp) { + std::shared_ptr> mdp = model->template as>(); #ifdef STORM_HAVE_CUDA - if (settings.isCudaSet()) { + if (settings.isCudaSet()) { storm::modelchecker::TopologicalValueIterationMdpPrctlModelChecker modelchecker(*mdp); result = modelchecker.check(*formula); } else { @@ -199,16 +197,24 @@ namespace storm { result = modelchecker.check(*formula); } #else - storm::modelchecker::SparseMdpPrctlModelChecker> modelchecker(*mdp); - result = modelchecker.check(*formula); + storm::modelchecker::SparseMdpPrctlModelChecker> modelchecker(*mdp); + result = modelchecker.check(*formula); #endif - } else if (model->getType() == storm::models::ModelType::Ctmc) { - std::shared_ptr> ctmc = model->template as>(); + } else if (model->getType() == storm::models::ModelType::Ctmc) { + std::shared_ptr> ctmc = model->template as>(); - storm::modelchecker::SparseCtmcCslModelChecker> modelchecker(*ctmc); - result = modelchecker.check(*formula); - } + storm::modelchecker::SparseCtmcCslModelChecker> modelchecker(*ctmc); + result = modelchecker.check(*formula); + } + return result; + } + + template + void verifySparseModel(std::shared_ptr> model, std::vector> const& formulas) { + for (auto const& formula : formulas) { + std::cout << std::endl << "Model checking property: " << *formula << " ..."; + std::unique_ptr result(verifySparseModel(model, formula)); if (result) { std::cout << " done." << std::endl; std::cout << "Result (initial states): "; @@ -270,33 +276,39 @@ namespace storm { } } #endif - + + template + std::unique_ptr verifySymbolicModelWithHybridEngine(std::shared_ptr> model, std::shared_ptr const& formula) { + std::unique_ptr result; + if (model->getType() == storm::models::ModelType::Dtmc) { + std::shared_ptr> dtmc = model->template as>(); + storm::modelchecker::HybridDtmcPrctlModelChecker modelchecker(*dtmc); + if (modelchecker.canHandle(*formula)) { + result = modelchecker.check(*formula); + } + } else if (model->getType() == storm::models::ModelType::Ctmc) { + std::shared_ptr> ctmc = model->template as>(); + storm::modelchecker::HybridCtmcCslModelChecker modelchecker(*ctmc); + if (modelchecker.canHandle(*formula)) { + result = modelchecker.check(*formula); + } + } else if (model->getType() == storm::models::ModelType::Mdp) { + std::shared_ptr> mdp = model->template as>(); + storm::modelchecker::HybridMdpPrctlModelChecker modelchecker(*mdp); + if (modelchecker.canHandle(*formula)) { + result = modelchecker.check(*formula); + } + } else { + STORM_LOG_THROW(false, storm::exceptions::NotImplementedException, "This functionality is not yet implemented."); + } + return result; + } + template void verifySymbolicModelWithHybridEngine(std::shared_ptr> model, std::vector> const& formulas) { for (auto const& formula : formulas) { std::cout << std::endl << "Model checking property: " << *formula << " ..."; - std::unique_ptr result; - if (model->getType() == storm::models::ModelType::Dtmc) { - std::shared_ptr> dtmc = model->template as>(); - storm::modelchecker::HybridDtmcPrctlModelChecker modelchecker(*dtmc); - if (modelchecker.canHandle(*formula)) { - result = modelchecker.check(*formula); - } - } else if (model->getType() == storm::models::ModelType::Ctmc) { - std::shared_ptr> ctmc = model->template as>(); - storm::modelchecker::HybridCtmcCslModelChecker modelchecker(*ctmc); - if (modelchecker.canHandle(*formula)) { - result = modelchecker.check(*formula); - } - } else if (model->getType() == storm::models::ModelType::Mdp) { - std::shared_ptr> mdp = model->template as>(); - storm::modelchecker::HybridMdpPrctlModelChecker modelchecker(*mdp); - if (modelchecker.canHandle(*formula)) { - result = modelchecker.check(*formula); - } - } else { - STORM_LOG_THROW(false, storm::exceptions::NotImplementedException, "This functionality is not yet implemented."); - } + std::unique_ptr result(verifySymbolicModelWithHybridEngine(model, formula)); if (result) { std::cout << " done." << std::endl; @@ -308,28 +320,33 @@ namespace storm { } } } - + + template + std::unique_ptr verifySymbolicModelWithDdEngine(std::shared_ptr> model, std::shared_ptr const& formula) { + std::unique_ptr result; + if (model->getType() == storm::models::ModelType::Dtmc) { + std::shared_ptr> dtmc = model->template as>(); + storm::modelchecker::SymbolicDtmcPrctlModelChecker modelchecker(*dtmc); + if (modelchecker.canHandle(*formula)) { + result = modelchecker.check(*formula); + } + } else if (model->getType() == storm::models::ModelType::Mdp) { + std::shared_ptr> mdp = model->template as>(); + storm::modelchecker::SymbolicMdpPrctlModelChecker modelchecker(*mdp); + if (modelchecker.canHandle(*formula)) { + result = modelchecker.check(*formula); + } + } else { + STORM_LOG_THROW(false, storm::exceptions::NotImplementedException, "This functionality is not yet implemented."); + } + return result; + } + template void verifySymbolicModelWithSymbolicEngine(std::shared_ptr> model, std::vector> const& formulas) { for (auto const& formula : formulas) { std::cout << std::endl << "Model checking property: " << *formula << " ..."; - std::unique_ptr result; - if (model->getType() == storm::models::ModelType::Dtmc) { - std::shared_ptr> dtmc = model->template as>(); - storm::modelchecker::SymbolicDtmcPrctlModelChecker modelchecker(*dtmc); - if (modelchecker.canHandle(*formula)) { - result = modelchecker.check(*formula); - } - } else if (model->getType() == storm::models::ModelType::Mdp) { - std::shared_ptr> mdp = model->template as>(); - storm::modelchecker::SymbolicMdpPrctlModelChecker modelchecker(*mdp); - if (modelchecker.canHandle(*formula)) { - result = modelchecker.check(*formula); - } - } else { - STORM_LOG_THROW(false, storm::exceptions::NotImplementedException, "This functionality is not yet implemented."); - } - + std::unique_ptr result(verifySymbolicModelWithDdEngine(model, formula)); if (result) { std::cout << " done." << std::endl; std::cout << "Result (initial states): "; @@ -340,8 +357,8 @@ namespace storm { } } } - - + + template void buildAndCheckSymbolicModel(storm::prism::Program const& program, std::vector> const& formulas) { std::shared_ptr model = buildSymbolicModel(program, formulas); From 649c928828d137b3450e0661131f22e0531b2daf Mon Sep 17 00:00:00 2001 From: sjunges Date: Tue, 8 Sep 2015 14:51:37 +0200 Subject: [PATCH 4/4] further refactored api / shifted some highlevel functionality to cli Former-commit-id: 0fc2dac6a7fba8642940f0769832daea820aecd8 --- src/cli/cli.cpp | 4 +- src/utility/storm.h | 144 ++++---------------------------------------- 2 files changed, 16 insertions(+), 132 deletions(-) diff --git a/src/cli/cli.cpp b/src/cli/cli.cpp index c9e0aa7e6..36b6df27e 100644 --- a/src/cli/cli.cpp +++ b/src/cli/cli.cpp @@ -1,4 +1,5 @@ #include "cli.h" +#include "entrypoints.h" #include "../utility/storm.h" @@ -7,6 +8,7 @@ #include "src/utility/storm-version.h" + // Includes for the linked libraries and versions header. #ifdef STORM_HAVE_INTELTBB # include "tbb/tbb_stddef.h" @@ -110,7 +112,7 @@ namespace storm { std::cout << "Compiled with CUDA support, but an error occured trying to find CUDA devices." << std::endl; } #endif - + // "Compute" the command line argument string with which STORM was invoked. std::stringstream commandStream; for (int i = 1; i < argc; ++i) { diff --git a/src/utility/storm.h b/src/utility/storm.h index bb3a0a8a5..19f84b85d 100644 --- a/src/utility/storm.h +++ b/src/utility/storm.h @@ -209,22 +209,7 @@ namespace storm { return result; } - - template - void verifySparseModel(std::shared_ptr> model, std::vector> const& formulas) { - for (auto const& formula : formulas) { - std::cout << std::endl << "Model checking property: " << *formula << " ..."; - std::unique_ptr result(verifySparseModel(model, formula)); - if (result) { - std::cout << " done." << std::endl; - std::cout << "Result (initial states): "; - result->filter(storm::modelchecker::ExplicitQualitativeCheckResult(model->getInitialStates())); - std::cout << *result << std::endl; - } else { - std::cout << " skipped, because the modelling formalism is currently unsupported." << std::endl; - } - } - } + #ifdef STORM_HAVE_CARL inline void exportParametricResultToFile(storm::RationalFunction const& result, storm::models::sparse::Dtmc::ConstraintCollector const& constraintCollector, std::string const& path) { @@ -242,39 +227,22 @@ namespace storm { std::copy(constraintCollector.getGraphPreservingConstraints().begin(), constraintCollector.getGraphPreservingConstraints().end(), std::ostream_iterator>(filestream, "\n")); filestream.close(); } - - template<> - inline void verifySparseModel(std::shared_ptr> model, std::vector> const& formulas) { - - for (auto const& formula : formulas) { - STORM_LOG_THROW(model->getType() == storm::models::ModelType::Dtmc, storm::exceptions::InvalidSettingsException, "Currently parametric verification is only available for DTMCs."); - std::shared_ptr> dtmc = model->template as>(); - - std::cout << std::endl << "Model checking property: " << *formula << " ..."; - std::unique_ptr result; - - storm::modelchecker::SparseDtmcEliminationModelChecker> modelchecker(*dtmc); - if (modelchecker.canHandle(*formula)) { - result = modelchecker.check(*formula); - } else { - STORM_LOG_THROW(false, storm::exceptions::InvalidSettingsException, "The parametric engine currently does not support this property."); - } - if (result) { - std::cout << " done." << std::endl; - std::cout << "Result (initial states): "; - result->filter(storm::modelchecker::ExplicitQualitativeCheckResult(dtmc->getInitialStates())); - std::cout << *result << std::endl; - } else { - std::cout << " skipped, because the modelling formalism is currently unsupported." << std::endl; - } + template<> + inline std::unique_ptr verifySparseModel(std::shared_ptr> model, std::shared_ptr const& formula) { + std::unique_ptr result; + std::shared_ptr> dtmc = model->template as>(); - storm::settings::modules::ParametricSettings const& parametricSettings = storm::settings::parametricSettings(); - if (parametricSettings.exportResultToFile()) { - exportParametricResultToFile(result->asExplicitQuantitativeCheckResult()[*dtmc->getInitialStates().begin()], storm::models::sparse::Dtmc::ConstraintCollector(*dtmc), parametricSettings.exportResultPath()); - } + storm::modelchecker::SparseDtmcEliminationModelChecker> modelchecker(*dtmc); + if (modelchecker.canHandle(*formula)) { + result = modelchecker.check(*formula); + } else { + STORM_LOG_THROW(false, storm::exceptions::InvalidSettingsException, "The parametric engine currently does not support this property."); } + return result; } + + #endif template @@ -304,22 +272,6 @@ namespace storm { return result; } - template - void verifySymbolicModelWithHybridEngine(std::shared_ptr> model, std::vector> const& formulas) { - for (auto const& formula : formulas) { - std::cout << std::endl << "Model checking property: " << *formula << " ..."; - std::unique_ptr result(verifySymbolicModelWithHybridEngine(model, formula)); - - if (result) { - std::cout << " done." << std::endl; - std::cout << "Result (initial states): "; - result->filter(storm::modelchecker::SymbolicQualitativeCheckResult(model->getReachableStates(), model->getInitialStates())); - std::cout << *result << std::endl; - } else { - std::cout << " skipped, because the modelling formalism is currently unsupported." << std::endl; - } - } - } template std::unique_ptr verifySymbolicModelWithDdEngine(std::shared_ptr> model, std::shared_ptr const& formula) { @@ -341,76 +293,6 @@ namespace storm { } return result; } - - template - void verifySymbolicModelWithSymbolicEngine(std::shared_ptr> model, std::vector> const& formulas) { - for (auto const& formula : formulas) { - std::cout << std::endl << "Model checking property: " << *formula << " ..."; - std::unique_ptr result(verifySymbolicModelWithDdEngine(model, formula)); - if (result) { - std::cout << " done." << std::endl; - std::cout << "Result (initial states): "; - result->filter(storm::modelchecker::SymbolicQualitativeCheckResult(model->getReachableStates(), model->getInitialStates())); - std::cout << *result << std::endl; - } else { - std::cout << " skipped, because the modelling formalism is currently unsupported." << std::endl; - } - } - } - - - template - void buildAndCheckSymbolicModel(storm::prism::Program const& program, std::vector> const& formulas) { - std::shared_ptr model = buildSymbolicModel(program, formulas); - STORM_LOG_THROW(model != nullptr, storm::exceptions::InvalidStateException, "Model could not be constructed for an unknown reason."); - - // Preprocess the model if needed. - model = preprocessModel(model, formulas); - - // Print some information about the model. - model->printModelInformationToStream(std::cout); - - // Verify the model, if a formula was given. - if (!formulas.empty()) { - if (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 : formulas) { - generateCounterexample(program, model->as>(), formula); - } - } else { - verifySparseModel(model->as>(), formulas); - } - } else if (model->isSymbolicModel()) { - if (storm::settings::generalSettings().getEngine() == storm::settings::modules::GeneralSettings::Engine::Hybrid) { - verifySymbolicModelWithHybridEngine(model->as>(), formulas); - } else { - verifySymbolicModelWithSymbolicEngine(model->as>(), formulas); - } - } else { - STORM_LOG_THROW(false, storm::exceptions::InvalidSettingsException, "Invalid input model type."); - } - } - } - - template - void buildAndCheckExplicitModel(std::vector> const& formulas) { - storm::settings::modules::GeneralSettings const& settings = storm::settings::generalSettings(); - - STORM_LOG_THROW(settings.isExplicitSet(), storm::exceptions::InvalidStateException, "Unable to build explicit model without model files."); - std::shared_ptr model = buildExplicitModel(settings.getTransitionFilename(), settings.getLabelingFilename(), settings.isStateRewardsSet() ? settings.getStateRewardsFilename() : boost::optional(), settings.isTransitionRewardsSet() ? settings.getTransitionRewardsFilename() : boost::optional(), settings.isChoiceLabelingSet() ? settings.getChoiceLabelingFilename() : boost::optional()); - // Preprocess the model if needed. - model = preprocessModel(model, formulas); - - // Print some information about the model. - model->printModelInformationToStream(std::cout); - - // Verify the model, if a formula was given. - if (!formulas.empty()) { - STORM_LOG_THROW(model->isSparseModel(), storm::exceptions::InvalidStateException, "Expected sparse model."); - verifySparseModel(model->as>(), formulas); - } - } }