From 9e9767ceeb8e982e77ad1b16adbd822412caf816 Mon Sep 17 00:00:00 2001 From: Thomas Knoll Date: Fri, 4 Aug 2023 10:24:44 +0200 Subject: [PATCH] changed shield export handling --- resources/3rdparty/cudd-3.0.0/config.h.in | 10 ++++++---- src/storm-cli-utilities/model-handling.h | 9 +++++++++ src/storm/api/export.h | 9 +++++++++ .../prctl/SparseMdpPrctlModelChecker.cpp | 2 ++ .../prctl/SparseMdpPrctlModelChecker.h | 2 +- .../modelchecker/results/CheckResult.cpp | 4 ++++ src/storm/modelchecker/results/CheckResult.h | 1 + .../ExplicitQuantitativeCheckResult.cpp | 16 +++++++++++++++ src/storm/shields/AbstractShield.cpp | 10 ++++++++++ src/storm/shields/AbstractShield.h | 3 +++ src/storm/shields/OptimalShield.cpp | 1 + src/storm/shields/PostShield.cpp | 1 + src/storm/shields/PreShield.cpp | 1 + src/storm/shields/ShieldHandling.cpp | 20 ++++++++++++++++++- src/storm/shields/ShieldHandling.h | 3 +++ 15 files changed, 86 insertions(+), 6 deletions(-) diff --git a/resources/3rdparty/cudd-3.0.0/config.h.in b/resources/3rdparty/cudd-3.0.0/config.h.in index 1bea1dd11..8d78585dd 100644 --- a/resources/3rdparty/cudd-3.0.0/config.h.in +++ b/resources/3rdparty/cudd-3.0.0/config.h.in @@ -33,9 +33,6 @@ /* Define to 1 if you have the header file. */ #undef HAVE_MATH_H -/* Define to 1 if you have the header file. */ -#undef HAVE_MEMORY_H - /* Define to 1 if your compiler supports enough C++11 */ #undef HAVE_MODERN_CXX @@ -57,6 +54,9 @@ /* Define to 1 if you have the header file. */ #undef HAVE_STDINT_H +/* Define to 1 if you have the header file. */ +#undef HAVE_STDIO_H + /* Define to 1 if you have the header file. */ #undef HAVE_STDLIB_H @@ -139,7 +139,9 @@ /* The size of `void *', as computed by sizeof. */ #undef SIZEOF_VOID_P -/* Define to 1 if you have the ANSI C header files. */ +/* Define to 1 if all of the C90 standard headers exist (not just the ones + required in a freestanding environment). This macro is provided for + backward compatibility; new code need not use it. */ #undef STDC_HEADERS /* Define to 1 to use system qsort */ diff --git a/src/storm-cli-utilities/model-handling.h b/src/storm-cli-utilities/model-handling.h index e41bdf47f..efcad6579 100644 --- a/src/storm-cli-utilities/model-handling.h +++ b/src/storm-cli-utilities/model-handling.h @@ -1043,6 +1043,15 @@ namespace storm { STORM_LOG_THROW(false, storm::exceptions::NotSupportedException, "Scheduler export not supported for this property."); } } + if (result->isExplicitQuantitativeCheckResult()) { + if (result-> template asExplicitQuantitativeCheckResult().hasShield()) { + auto shield = result->template asExplicitQuantitativeCheckResult().getShield(); + STORM_PRINT_AND_LOG("Exporting shield ..."); + + storm::api::exportShield(sparseModel, shield); + } + } + if (ioSettings.isExportCheckResultSet()) { STORM_LOG_WARN_COND(sparseModel->hasStateValuations(), "No information of state valuations available. The result output will use internal state ids. You might be interested in building the model with state valuations using --buildstateval."); STORM_LOG_WARN_COND(exportCount == 0, "Prepending " << exportCount << " to file name for this property because there are multiple properties."); diff --git a/src/storm/api/export.h b/src/storm/api/export.h index 6f4b82f77..078c2fc46 100644 --- a/src/storm/api/export.h +++ b/src/storm/api/export.h @@ -11,6 +11,7 @@ #include "storm/modelchecker/results/ExplicitQuantitativeCheckResult.h" #include "storm/modelchecker/results/ExplicitQualitativeCheckResult.h" #include "storm/exceptions/NotSupportedException.h" +#include "storm/shields/AbstractShield.h" namespace storm { @@ -62,6 +63,14 @@ namespace storm { } storm::utility::closeFile(stream); } + + template + void exportShield(std::shared_ptr> const& model, std::shared_ptr> const& shield) { + std::ofstream stream; + storm::utility::openFile(shield->getShieldFileName(), stream); + shield->printToStream(stream, model); + storm::utility::closeFile(stream); + } template inline void exportCheckResultToJson(std::shared_ptr> const& model, std::unique_ptr const& checkResult, std::string const& filename) { diff --git a/src/storm/modelchecker/prctl/SparseMdpPrctlModelChecker.cpp b/src/storm/modelchecker/prctl/SparseMdpPrctlModelChecker.cpp index 5a96c23ef..d45e592fe 100644 --- a/src/storm/modelchecker/prctl/SparseMdpPrctlModelChecker.cpp +++ b/src/storm/modelchecker/prctl/SparseMdpPrctlModelChecker.cpp @@ -135,6 +135,8 @@ namespace storm { std::unique_ptr result(new ExplicitQuantitativeCheckResult(std::move(ret.values))); if(checkTask.isShieldingTask()) { tempest::shields::createShield(std::make_shared>(this->getModel()), std::move(ret.choiceValues), checkTask.getShieldingExpression(), checkTask.getOptimizationDirection(), std::move(ret.maybeStates), storm::storage::BitVector(ret.maybeStates.size(), true)); + auto shield = tempest::shields::createShieldTest(std::make_shared>(this->getModel()), std::move(ret.choiceValues), checkTask.getShieldingExpression(), checkTask.getOptimizationDirection(), std::move(ret.maybeStates), storm::storage::BitVector(ret.maybeStates.size(), true)); + result->asExplicitQuantitativeCheckResult().setShield(std::move(shield)); } else if (checkTask.isProduceSchedulersSet() && ret.scheduler) { result->asExplicitQuantitativeCheckResult().setScheduler(std::move(ret.scheduler)); } diff --git a/src/storm/modelchecker/prctl/SparseMdpPrctlModelChecker.h b/src/storm/modelchecker/prctl/SparseMdpPrctlModelChecker.h index 3feb0802d..cdb87ec75 100644 --- a/src/storm/modelchecker/prctl/SparseMdpPrctlModelChecker.h +++ b/src/storm/modelchecker/prctl/SparseMdpPrctlModelChecker.h @@ -4,7 +4,7 @@ #include "storm/modelchecker/propositional/SparsePropositionalModelChecker.h" #include "storm/models/sparse/Mdp.h" #include "storm/solver/MinMaxLinearEquationSolver.h" - +#include "storm/shields/AbstractShield.h" namespace storm { diff --git a/src/storm/modelchecker/results/CheckResult.cpp b/src/storm/modelchecker/results/CheckResult.cpp index 26eb24946..28be6339f 100644 --- a/src/storm/modelchecker/results/CheckResult.cpp +++ b/src/storm/modelchecker/results/CheckResult.cpp @@ -166,6 +166,10 @@ namespace storm { bool CheckResult::hasScheduler() const { return false; } + + bool CheckResult::hasShield() const { + return false; + } // Explicitly instantiate the template functions. template QuantitativeCheckResult& CheckResult::asQuantitativeCheckResult(); diff --git a/src/storm/modelchecker/results/CheckResult.h b/src/storm/modelchecker/results/CheckResult.h index 740a8269d..bfb462949 100644 --- a/src/storm/modelchecker/results/CheckResult.h +++ b/src/storm/modelchecker/results/CheckResult.h @@ -113,6 +113,7 @@ namespace storm { SymbolicParetoCurveCheckResult const& asSymbolicParetoCurveCheckResult() const; virtual bool hasScheduler() const; + virtual bool hasShield() const; virtual std::ostream& writeToStream(std::ostream& out) const = 0; }; diff --git a/src/storm/modelchecker/results/ExplicitQuantitativeCheckResult.cpp b/src/storm/modelchecker/results/ExplicitQuantitativeCheckResult.cpp index ee7c2d91d..af654b505 100644 --- a/src/storm/modelchecker/results/ExplicitQuantitativeCheckResult.cpp +++ b/src/storm/modelchecker/results/ExplicitQuantitativeCheckResult.cpp @@ -204,6 +204,11 @@ namespace storm { bool ExplicitQuantitativeCheckResult::hasScheduler() const { return static_cast(scheduler); } + + template + bool ExplicitQuantitativeCheckResult::hasShield() const { + return static_cast(shield); + } template void ExplicitQuantitativeCheckResult::setScheduler(std::unique_ptr>&& scheduler) { @@ -222,6 +227,17 @@ namespace storm { return *scheduler.get(); } + template + void ExplicitQuantitativeCheckResult::setShield(std::unique_ptr> shield) { + this->shield = std::move(shield); + } + + template + std::shared_ptr::IndexType>> const& ExplicitQuantitativeCheckResult::getShield() const { + STORM_LOG_THROW(this->hasScheduler(), storm::exceptions::InvalidOperationException, "Unable to retrieve non-existing scheduler."); + return shield.get(); + } + template void print(std::ostream& out, ValueType const& value) { if (value == storm::utility::infinity()) { diff --git a/src/storm/shields/AbstractShield.cpp b/src/storm/shields/AbstractShield.cpp index 779f3b894..c81ac2ecc 100644 --- a/src/storm/shields/AbstractShield.cpp +++ b/src/storm/shields/AbstractShield.cpp @@ -34,10 +34,20 @@ namespace tempest { return std::string(boost::core::demangled_name(BOOST_CORE_TYPEID(*this))); } + template + std::string AbstractShield::getShieldFileName() const { + return shieldingExpression->getFilename() + ".shield"; + } + + template + void AbstractShield::printToStream(std::ostream& out, std::shared_ptr> const& model) const { + // construct().printToStream(out, shieldingExpression, model) + } // Explicitly instantiate appropriate template class AbstractShield::index_type>; #ifdef STORM_HAVE_CARL template class AbstractShield::index_type>; + template class AbstractShield::index_type>; #endif } } diff --git a/src/storm/shields/AbstractShield.h b/src/storm/shields/AbstractShield.h index b479efe71..3a0ee4dd4 100644 --- a/src/storm/shields/AbstractShield.h +++ b/src/storm/shields/AbstractShield.h @@ -49,6 +49,9 @@ namespace tempest { storm::OptimizationDirection getOptimizationDirection(); std::string getClassName() const; + std::string getShieldFileName() const; + + void printToStream(std::ostream& out, std::shared_ptr> const& model) const; protected: AbstractShield(std::vector const& rowGroupIndices, std::shared_ptr const& shieldingExpression, storm::OptimizationDirection optimizationDirection, storm::storage::BitVector relevantStates, boost::optional coalitionStates); diff --git a/src/storm/shields/OptimalShield.cpp b/src/storm/shields/OptimalShield.cpp index 8be4b1fef..b1e35a5c1 100644 --- a/src/storm/shields/OptimalShield.cpp +++ b/src/storm/shields/OptimalShield.cpp @@ -68,6 +68,7 @@ namespace tempest { template class OptimalShield::index_type>; #ifdef STORM_HAVE_CARL template class OptimalShield::index_type>; + #endif } } diff --git a/src/storm/shields/PostShield.cpp b/src/storm/shields/PostShield.cpp index 5ef487ad0..63eb452d8 100644 --- a/src/storm/shields/PostShield.cpp +++ b/src/storm/shields/PostShield.cpp @@ -71,6 +71,7 @@ namespace tempest { template class PostShield::index_type>; #ifdef STORM_HAVE_CARL template class PostShield::index_type>; + #endif } } diff --git a/src/storm/shields/PreShield.cpp b/src/storm/shields/PreShield.cpp index a16b777c7..3fad08b82 100644 --- a/src/storm/shields/PreShield.cpp +++ b/src/storm/shields/PreShield.cpp @@ -71,6 +71,7 @@ namespace tempest { template class PreShield::index_type>; #ifdef STORM_HAVE_CARL template class PreShield::index_type>; + #endif } } diff --git a/src/storm/shields/ShieldHandling.cpp b/src/storm/shields/ShieldHandling.cpp index 007959d5d..b3e0bcdcf 100644 --- a/src/storm/shields/ShieldHandling.cpp +++ b/src/storm/shields/ShieldHandling.cpp @@ -22,7 +22,22 @@ namespace tempest { storm::utility::closeFile(stream); } storm::utility::closeFile(stream); - } + } + + template + std::unique_ptr> createShieldTest(std::shared_ptr> model, std::vector const& choiceValues, std::shared_ptr const& shieldingExpression, storm::OptimizationDirection optimizationDirection, storm::storage::BitVector relevantStates, boost::optional coalitionStates) { + if(coalitionStates.is_initialized()) coalitionStates.get().complement(); + if(shieldingExpression->isPreSafetyShield()) { + PreShield shield(model->getTransitionMatrix().getRowGroupIndices(), choiceValues, shieldingExpression, optimizationDirection, relevantStates, coalitionStates); + return std::make_unique>(shield); + } else if(shieldingExpression->isPostSafetyShield()) { + PostShield shield(model->getTransitionMatrix().getRowGroupIndices(), choiceValues, shieldingExpression, optimizationDirection, relevantStates, coalitionStates); + return std::make_unique>(shield); + } else { + STORM_LOG_THROW(false, storm::exceptions::InvalidArgumentException, "Unknown Shielding Type: " + shieldingExpression->typeToString()); + } + } + template void createQuantitativeShield(std::shared_ptr> model, std::vector const& choiceValues, std::shared_ptr const& shieldingExpression, storm::OptimizationDirection optimizationDirection, storm::storage::BitVector relevantStates, boost::optional coalitionStates) { @@ -43,9 +58,12 @@ namespace tempest { } // Explicitly instantiate appropriate template void createShield::index_type>(std::shared_ptr> model, std::vector const& choiceValues, std::shared_ptr const& shieldingExpression, storm::OptimizationDirection optimizationDirection, storm::storage::BitVector relevantStates, boost::optional coalitionStates); + template std::unique_ptr::index_type>> createShieldTest::index_type>(std::shared_ptr> model, std::vector const& choiceValues, std::shared_ptr const& shieldingExpression, storm::OptimizationDirection optimizationDirection, storm::storage::BitVector relevantStates, boost::optional coalitionStates); template void createQuantitativeShield::index_type>(std::shared_ptr> model, std::vector const& choiceValues, std::shared_ptr const& shieldingExpression, storm::OptimizationDirection optimizationDirection, storm::storage::BitVector relevantStates, boost::optional coalitionStates); #ifdef STORM_HAVE_CARL template void createShield::index_type>(std::shared_ptr> model, std::vector const& choiceValues, std::shared_ptr const& shieldingExpression, storm::OptimizationDirection optimizationDirection, storm::storage::BitVector relevantStates, boost::optional coalitionStates); + template std::unique_ptr::index_type>> createShieldTest::index_type>(std::shared_ptr> model, std::vector const& choiceValues, std::shared_ptr const& shieldingExpression, storm::OptimizationDirection optimizationDirection, storm::storage::BitVector relevantStates, boost::optional coalitionStates); + template void createQuantitativeShield::index_type>(std::shared_ptr> model, std::vector const& choiceValues, std::shared_ptr const& shieldingExpression, storm::OptimizationDirection optimizationDirection, storm::storage::BitVector relevantStates, boost::optional coalitionStates); #endif } diff --git a/src/storm/shields/ShieldHandling.h b/src/storm/shields/ShieldHandling.h index 768888a7d..c36d38258 100644 --- a/src/storm/shields/ShieldHandling.h +++ b/src/storm/shields/ShieldHandling.h @@ -26,6 +26,9 @@ namespace tempest { template void createShield(std::shared_ptr> model, std::vector const& choiceValues, std::shared_ptr const& shieldingExpression, storm::OptimizationDirection optimizationDirection, storm::storage::BitVector relevantStates, boost::optional coalitionStates); + template + std::unique_ptr> createShieldTest(std::shared_ptr> model, std::vector const& choiceValues, std::shared_ptr const& shieldingExpression, storm::OptimizationDirection optimizationDirection, storm::storage::BitVector relevantStates, boost::optional coalitionStates); + template void createQuantitativeShield(std::shared_ptr> model, std::vector const& choiceValues, std::shared_ptr const& shieldingExpression, storm::OptimizationDirection optimizationDirection, storm::storage::BitVector relevantStates, boost::optional coalitionStates); }