From 83c3a75ecf14ba658239611139c068f85e52647a Mon Sep 17 00:00:00 2001 From: Thomas Knoll Date: Fri, 4 Aug 2023 10:58:08 +0200 Subject: [PATCH] added create shield for quantitative shield --- src/storm/shields/ShieldHandling.cpp | 18 ++++++++++++++++++ src/storm/shields/ShieldHandling.h | 4 ++++ 2 files changed, 22 insertions(+) diff --git a/src/storm/shields/ShieldHandling.cpp b/src/storm/shields/ShieldHandling.cpp index b3e0bcdcf..fffe74fe6 100644 --- a/src/storm/shields/ShieldHandling.cpp +++ b/src/storm/shields/ShieldHandling.cpp @@ -56,15 +56,33 @@ namespace tempest { } storm::utility::closeFile(stream); } + + template + std::unique_ptr> createQuantitativeShieldTest(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(); // TODO CHECK THIS!!! + if(shieldingExpression->isOptimalPreShield()) { + PreShield shield(model->getTransitionMatrix().getRowGroupIndices(), choiceValues, shieldingExpression, optimizationDirection, relevantStates, coalitionStates); + return std::make_unique>(shield); + } else if(shieldingExpression->isOptimalPostShield()) { + 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()); + } + } + // 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); + template std::unique_ptr::index_type>> createQuantitativeShieldTest::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); + template std::unique_ptr::index_type>> createQuantitativeShieldTest::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 c36d38258..86aea2eba 100644 --- a/src/storm/shields/ShieldHandling.h +++ b/src/storm/shields/ShieldHandling.h @@ -31,5 +31,9 @@ namespace tempest { 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); + + template + std::unique_ptr> createQuantitativeShieldTest(std::shared_ptr> model, std::vector const& choiceValues, std::shared_ptr const& shieldingExpression, storm::OptimizationDirection optimizationDirection, storm::storage::BitVector relevantStates, boost::optional coalitionStates); + } }