changed shield export handling

resources/3rdparty/cudd-3.0.0/config.h.in

@@ -33,9 +33,6 @@
 /* Define to 1 if you have the <math.h> header file. */
 #undef HAVE_MATH_H
 
-/* Define to 1 if you have the <memory.h> 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 <stdint.h> header file. */
 #undef HAVE_STDINT_H
 
+/* Define to 1 if you have the <stdio.h> header file. */
+#undef HAVE_STDIO_H
+
 /* Define to 1 if you have the <stdlib.h> 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 */

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<ValueType>().hasShield()) {
+                                                    auto shield = result->template asExplicitQuantitativeCheckResult<ValueType>().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.");

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 <typename ValueType, typename IndexType>
+        void exportShield(std::shared_ptr<storm::models::sparse::Model<ValueType>> const& model, std::shared_ptr<tempest::shields::AbstractShield<ValueType, IndexType>> const& shield) {
+            std::ofstream stream;
+            storm::utility::openFile(shield->getShieldFileName(), stream);
+            shield->printToStream(stream, model);
+            storm::utility::closeFile(stream);
+        }
         
         template <typename ValueType>
         inline void exportCheckResultToJson(std::shared_ptr<storm::models::sparse::Model<ValueType>> const& model, std::unique_ptr<storm::modelchecker::CheckResult> const& checkResult, std::string const& filename) {

src/storm/modelchecker/prctl/SparseMdpPrctlModelChecker.cpp

@@ -135,6 +135,8 @@ namespace storm {
             std::unique_ptr<CheckResult> result(new ExplicitQuantitativeCheckResult<ValueType>(std::move(ret.values)));
             if(checkTask.isShieldingTask()) {
                 tempest::shields::createShield<ValueType>(std::make_shared<storm::models::sparse::Mdp<ValueType>>(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<ValueType>(std::make_shared<storm::models::sparse::Mdp<ValueType>>(this->getModel()), std::move(ret.choiceValues), checkTask.getShieldingExpression(), checkTask.getOptimizationDirection(), std::move(ret.maybeStates), storm::storage::BitVector(ret.maybeStates.size(), true));
+                result->asExplicitQuantitativeCheckResult<ValueType>().setShield(std::move(shield));                    
             } else if (checkTask.isProduceSchedulersSet() && ret.scheduler) {
                 result->asExplicitQuantitativeCheckResult<ValueType>().setScheduler(std::move(ret.scheduler));
             }

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 {
     

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<double>& CheckResult::asQuantitativeCheckResult();

src/storm/modelchecker/results/CheckResult.h

@@ -113,6 +113,7 @@ namespace storm {
             SymbolicParetoCurveCheckResult<Type, ValueType> const& asSymbolicParetoCurveCheckResult() const;
 
             virtual bool hasScheduler() const;
+            virtual bool hasShield() const;
 
             virtual std::ostream& writeToStream(std::ostream& out) const = 0;
         };

src/storm/modelchecker/results/ExplicitQuantitativeCheckResult.cpp

@@ -204,6 +204,11 @@ namespace storm {
         bool ExplicitQuantitativeCheckResult<ValueType>::hasScheduler() const {
             return static_cast<bool>(scheduler);
         }
+
+        template<typename ValueType>
+        bool ExplicitQuantitativeCheckResult<ValueType>::hasShield() const {
+            return static_cast<bool>(shield);
+        }
         
         template<typename ValueType>
         void ExplicitQuantitativeCheckResult<ValueType>::setScheduler(std::unique_ptr<storm::storage::Scheduler<ValueType>>&& scheduler) {
@@ -222,6 +227,17 @@ namespace storm {
             return *scheduler.get();
         }
 
+        template<typename ValueType>
+        void ExplicitQuantitativeCheckResult<ValueType>::setShield(std::unique_ptr<tempest::shields::AbstractShield<ValueType, IndexType>> shield) {
+            this->shield = std::move(shield);
+        }
+
+        template<typename ValueType>
+        std::shared_ptr<tempest::shields::AbstractShield<ValueType,typename ExplicitQuantitativeCheckResult<ValueType>::IndexType>> const& ExplicitQuantitativeCheckResult<ValueType>::getShield() const {
+            STORM_LOG_THROW(this->hasScheduler(), storm::exceptions::InvalidOperationException, "Unable to retrieve non-existing scheduler.");
+            return shield.get();
+        }
+
         template<typename ValueType>
         void print(std::ostream& out, ValueType const& value) {
             if (value == storm::utility::infinity<ValueType>()) {

src/storm/shields/AbstractShield.cpp

@@ -34,10 +34,20 @@ namespace tempest {
             return std::string(boost::core::demangled_name(BOOST_CORE_TYPEID(*this)));
         }
 
+        template<typename ValueType, typename IndexType>
+        std::string AbstractShield<ValueType, IndexType>::getShieldFileName() const {
+            return shieldingExpression->getFilename() + ".shield";
+        }
+
+        template<typename ValueType, typename IndexType>
+        void AbstractShield<ValueType, IndexType>::printToStream(std::ostream& out, std::shared_ptr<storm::models::sparse::Model<ValueType>> const& model) const {
+          //  construct().printToStream(out, shieldingExpression, model)
+        }
         // Explicitly instantiate appropriate
         template class AbstractShield<double, typename storm::storage::SparseMatrix<double>::index_type>;
 #ifdef STORM_HAVE_CARL
         template class AbstractShield<storm::RationalNumber, typename storm::storage::SparseMatrix<storm::RationalNumber>::index_type>;
+        template class AbstractShield<storm::RationalFunction, typename storm::storage::SparseMatrix<storm::RationalFunction>::index_type>;
 #endif
     }
 }

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<storm::models::sparse::Model<ValueType>> const& model) const;
 
         protected:
             AbstractShield(std::vector<IndexType> const& rowGroupIndices, std::shared_ptr<storm::logic::ShieldExpression const> const& shieldingExpression, storm::OptimizationDirection optimizationDirection, storm::storage::BitVector relevantStates, boost::optional<storm::storage::BitVector> coalitionStates);

src/storm/shields/OptimalShield.cpp

@@ -68,6 +68,7 @@ namespace tempest {
         template class OptimalShield<double, typename storm::storage::SparseMatrix<double>::index_type>;
 #ifdef STORM_HAVE_CARL
         template class OptimalShield<storm::RationalNumber, typename storm::storage::SparseMatrix<storm::RationalNumber>::index_type>;
+        
 #endif
     }
 }

src/storm/shields/PostShield.cpp

@@ -71,6 +71,7 @@ namespace tempest {
         template class PostShield<double, typename storm::storage::SparseMatrix<double>::index_type>;
 #ifdef STORM_HAVE_CARL
         template class PostShield<storm::RationalNumber, typename storm::storage::SparseMatrix<storm::RationalNumber>::index_type>;
+    
 #endif
     }
 }

src/storm/shields/PreShield.cpp

@@ -71,6 +71,7 @@ namespace tempest {
         template class PreShield<double, typename storm::storage::SparseMatrix<double>::index_type>;
 #ifdef STORM_HAVE_CARL
         template class PreShield<storm::RationalNumber, typename storm::storage::SparseMatrix<storm::RationalNumber>::index_type>;
+      
 #endif
     }
 }

src/storm/shields/ShieldHandling.cpp

@@ -22,7 +22,22 @@ namespace tempest {
                 storm::utility::closeFile(stream);
             }
             storm::utility::closeFile(stream);
-        }
+        }        
+
+        template<typename ValueType, typename IndexType>
+        std::unique_ptr<tempest::shields::AbstractShield<ValueType, IndexType>> createShieldTest(std::shared_ptr<storm::models::sparse::Model<ValueType>> model, std::vector<ValueType> const& choiceValues, std::shared_ptr<storm::logic::ShieldExpression const> const& shieldingExpression, storm::OptimizationDirection optimizationDirection, storm::storage::BitVector relevantStates, boost::optional<storm::storage::BitVector> coalitionStates) {
+            if(coalitionStates.is_initialized()) coalitionStates.get().complement();
+            if(shieldingExpression->isPreSafetyShield()) {
+                PreShield<ValueType, IndexType> shield(model->getTransitionMatrix().getRowGroupIndices(), choiceValues, shieldingExpression, optimizationDirection, relevantStates, coalitionStates);
+                return std::make_unique<tempest::shields::PreShield<ValueType, IndexType>>(shield);
+            } else if(shieldingExpression->isPostSafetyShield()) {
+                PostShield<ValueType, IndexType> shield(model->getTransitionMatrix().getRowGroupIndices(), choiceValues, shieldingExpression, optimizationDirection, relevantStates, coalitionStates);
+                return std::make_unique<tempest::shields::PostShield<ValueType, IndexType>>(shield);
+            } else {
+                STORM_LOG_THROW(false, storm::exceptions::InvalidArgumentException, "Unknown Shielding Type: " + shieldingExpression->typeToString());
+            }
+        }   
+
 
         template<typename ValueType, typename IndexType>
         void createQuantitativeShield(std::shared_ptr<storm::models::sparse::Model<ValueType>> model, std::vector<ValueType> const& choiceValues, std::shared_ptr<storm::logic::ShieldExpression const> const& shieldingExpression, storm::OptimizationDirection optimizationDirection, storm::storage::BitVector relevantStates, boost::optional<storm::storage::BitVector> coalitionStates) {
@@ -43,9 +58,12 @@ namespace tempest {
         }
         // Explicitly instantiate appropriate
         template void createShield<double, typename storm::storage::SparseMatrix<double>::index_type>(std::shared_ptr<storm::models::sparse::Model<double>> model, std::vector<double> const& choiceValues, std::shared_ptr<storm::logic::ShieldExpression const> const& shieldingExpression, storm::OptimizationDirection optimizationDirection, storm::storage::BitVector relevantStates, boost::optional<storm::storage::BitVector> coalitionStates);
+        template std::unique_ptr<tempest::shields::AbstractShield<double, typename storm::storage::SparseMatrix<double>::index_type>> createShieldTest<double, typename storm::storage::SparseMatrix<double>::index_type>(std::shared_ptr<storm::models::sparse::Model<double>> model, std::vector<double> const& choiceValues, std::shared_ptr<storm::logic::ShieldExpression const> const& shieldingExpression, storm::OptimizationDirection optimizationDirection, storm::storage::BitVector relevantStates, boost::optional<storm::storage::BitVector> coalitionStates);
         template void createQuantitativeShield<double, typename storm::storage::SparseMatrix<double>::index_type>(std::shared_ptr<storm::models::sparse::Model<double>> model, std::vector<double> const& choiceValues, std::shared_ptr<storm::logic::ShieldExpression const> const& shieldingExpression, storm::OptimizationDirection optimizationDirection, storm::storage::BitVector relevantStates, boost::optional<storm::storage::BitVector> coalitionStates);
 #ifdef STORM_HAVE_CARL
         template void createShield<storm::RationalNumber, typename storm::storage::SparseMatrix<storm::RationalNumber>::index_type>(std::shared_ptr<storm::models::sparse::Model<storm::RationalNumber>> model, std::vector<storm::RationalNumber> const& choiceValues, std::shared_ptr<storm::logic::ShieldExpression const> const& shieldingExpression, storm::OptimizationDirection optimizationDirection, storm::storage::BitVector relevantStates, boost::optional<storm::storage::BitVector> coalitionStates);
+        template std::unique_ptr<tempest::shields::AbstractShield<storm::RationalNumber, typename storm::storage::SparseMatrix<storm::RationalNumber>::index_type>> createShieldTest<storm::RationalNumber, typename storm::storage::SparseMatrix<storm::RationalNumber>::index_type>(std::shared_ptr<storm::models::sparse::Model<storm::RationalNumber>> model, std::vector<storm::RationalNumber> const& choiceValues, std::shared_ptr<storm::logic::ShieldExpression const> const& shieldingExpression, storm::OptimizationDirection optimizationDirection, storm::storage::BitVector relevantStates, boost::optional<storm::storage::BitVector> coalitionStates);
+        
         template void createQuantitativeShield<storm::RationalNumber, typename storm::storage::SparseMatrix<storm::RationalNumber>::index_type>(std::shared_ptr<storm::models::sparse::Model<storm::RationalNumber>> model, std::vector<storm::RationalNumber> const& choiceValues, std::shared_ptr<storm::logic::ShieldExpression const> const& shieldingExpression, storm::OptimizationDirection optimizationDirection, storm::storage::BitVector relevantStates, boost::optional<storm::storage::BitVector> coalitionStates);
 #endif
     }

src/storm/shields/ShieldHandling.h

@@ -26,6 +26,9 @@ namespace tempest {
         template<typename ValueType, typename IndexType = storm::storage::sparse::state_type>
         void createShield(std::shared_ptr<storm::models::sparse::Model<ValueType>> model, std::vector<ValueType> const& choiceValues, std::shared_ptr<storm::logic::ShieldExpression const> const& shieldingExpression, storm::OptimizationDirection optimizationDirection, storm::storage::BitVector relevantStates, boost::optional<storm::storage::BitVector> coalitionStates);
 
+        template<typename ValueType, typename IndexType = storm::storage::sparse::state_type>
+        std::unique_ptr<tempest::shields::AbstractShield<ValueType, IndexType>> createShieldTest(std::shared_ptr<storm::models::sparse::Model<ValueType>> model, std::vector<ValueType> const& choiceValues, std::shared_ptr<storm::logic::ShieldExpression const> const& shieldingExpression, storm::OptimizationDirection optimizationDirection, storm::storage::BitVector relevantStates, boost::optional<storm::storage::BitVector> coalitionStates);
+
         template<typename ValueType, typename IndexType = storm::storage::sparse::state_type>
         void createQuantitativeShield(std::shared_ptr<storm::models::sparse::Model<ValueType>> model, std::vector<ValueType> const& choiceValues, std::shared_ptr<storm::logic::ShieldExpression const> const& shieldingExpression, storm::OptimizationDirection optimizationDirection, storm::storage::BitVector relevantStates, boost::optional<storm::storage::BitVector> coalitionStates);
     }