|  | @ -12,6 +12,7 @@ | 
		
	
		
			
				|  |  | #include "storm/shields/AbstractShield.h" |  |  | #include "storm/shields/AbstractShield.h" | 
		
	
		
			
				|  |  | #include "storm/shields/PreSafetyShield.h" |  |  | #include "storm/shields/PreSafetyShield.h" | 
		
	
		
			
				|  |  | #include "storm/shields/PostSafetyShield.h" |  |  | #include "storm/shields/PostSafetyShield.h" | 
		
	
		
			
				|  |  |  |  |  | #include "storm/shields/OptimalShield.h" | 
		
	
		
			
				|  |  | 
 |  |  | 
 | 
		
	
		
			
				|  |  | #include "storm/io/file.h" |  |  | #include "storm/io/file.h" | 
		
	
		
			
				|  |  | #include "storm/utility/macros.h" |  |  | #include "storm/utility/macros.h" | 
		
	
	
		
			
				|  | @ -22,11 +23,7 @@ | 
		
	
		
			
				|  |  | namespace tempest { |  |  | namespace tempest { | 
		
	
		
			
				|  |  |     namespace shields { |  |  |     namespace shields { | 
		
	
		
			
				|  |  |         std::string shieldFilename(std::shared_ptr<storm::logic::ShieldExpression const> const& shieldingExpression) { |  |  |         std::string shieldFilename(std::shared_ptr<storm::logic::ShieldExpression const> const& shieldingExpression) { | 
		
	
		
			
				|  |  |             std::stringstream filename; |  |  |  | 
		
	
		
			
				|  |  |             filename << shieldingExpression->typeToString() << "_"; |  |  |  | 
		
	
		
			
				|  |  |             filename << shieldingExpression->comparisonToString(); |  |  |  | 
		
	
		
			
				|  |  |             filename << shieldingExpression->getValue() << ".shield"; |  |  |  | 
		
	
		
			
				|  |  |             return filename.str(); |  |  |  | 
		
	
		
			
				|  |  |  |  |  |             return shieldingExpression->getFilename() + ".shield"; | 
		
	
		
			
				|  |  |         } |  |  |         } | 
		
	
		
			
				|  |  | 
 |  |  | 
 | 
		
	
		
			
				|  |  |         template<typename ValueType, typename IndexType = storm::storage::sparse::state_type> |  |  |         template<typename ValueType, typename IndexType = storm::storage::sparse::state_type> | 
		
	
	
		
			
				|  | @ -35,13 +32,28 @@ namespace tempest { | 
		
	
		
			
				|  |  |             storm::utility::openFile(shieldFilename(shieldingExpression), stream); |  |  |             storm::utility::openFile(shieldFilename(shieldingExpression), stream); | 
		
	
		
			
				|  |  |             if(shieldingExpression->isPreSafetyShield()) { |  |  |             if(shieldingExpression->isPreSafetyShield()) { | 
		
	
		
			
				|  |  |                 PreSafetyShield<ValueType, IndexType> shield(model->getTransitionMatrix().getRowGroupIndices(), choiceValues, shieldingExpression, optimizationDirection, relevantStates, coalitionStates); |  |  |                 PreSafetyShield<ValueType, IndexType> shield(model->getTransitionMatrix().getRowGroupIndices(), choiceValues, shieldingExpression, optimizationDirection, relevantStates, coalitionStates); | 
		
	
		
			
				|  |  |                 shield.construct().printToStream(stream, model); |  |  |  | 
		
	
		
			
				|  |  |  |  |  |                 shield.construct().printToStream(stream, shieldingExpression, model); | 
		
	
		
			
				|  |  |             } else if(shieldingExpression->isPostSafetyShield()) { |  |  |             } else if(shieldingExpression->isPostSafetyShield()) { | 
		
	
		
			
				|  |  |                 PostSafetyShield<ValueType, IndexType> shield(model->getTransitionMatrix().getRowGroupIndices(), choiceValues, shieldingExpression, optimizationDirection, relevantStates, coalitionStates); |  |  |                 PostSafetyShield<ValueType, IndexType> shield(model->getTransitionMatrix().getRowGroupIndices(), choiceValues, shieldingExpression, optimizationDirection, relevantStates, coalitionStates); | 
		
	
		
			
				|  |  |                 shield.construct().printToStream(stream, model); |  |  |  | 
		
	
		
			
				|  |  |             } else if(shieldingExpression->isOptimalShield()) { |  |  |  | 
		
	
		
			
				|  |  |  |  |  |                 shield.construct().printToStream(stream, shieldingExpression, model); | 
		
	
		
			
				|  |  |  |  |  |             } else { | 
		
	
		
			
				|  |  |  |  |  |                 STORM_LOG_THROW(false, storm::exceptions::InvalidArgumentException, "Cannot create " + shieldingExpression->typeToString() + " shields yet"); | 
		
	
		
			
				|  |  |  |  |  |                 storm::utility::closeFile(stream); | 
		
	
		
			
				|  |  |  |  |  |             } | 
		
	
		
			
				|  |  |  |  |  |             storm::utility::closeFile(stream); | 
		
	
		
			
				|  |  |  |  |  |         } | 
		
	
		
			
				|  |  |  |  |  | 
 | 
		
	
		
			
				|  |  |  |  |  |         template<typename ValueType, typename IndexType = storm::storage::sparse::state_type> | 
		
	
		
			
				|  |  |  |  |  |         void createOptimalShield(std::shared_ptr<storm::models::sparse::Model<ValueType>> model, std::vector<uint64_t> const& precomputedChoices, std::shared_ptr<storm::logic::ShieldExpression const> const& shieldingExpression, storm::OptimizationDirection optimizationDirection, storm::storage::BitVector relevantStates, boost::optional<storm::storage::BitVector> coalitionStates) { | 
		
	
		
			
				|  |  |  |  |  |             std::ofstream stream; | 
		
	
		
			
				|  |  |  |  |  |             storm::utility::openFile(shieldFilename(shieldingExpression), stream); | 
		
	
		
			
				|  |  |  |  |  |             if(shieldingExpression->isOptimalShield()) { | 
		
	
		
			
				|  |  |  |  |  |                 STORM_LOG_DEBUG("createOptimalShield"); | 
		
	
		
			
				|  |  |  |  |  |                 OptimalShield<ValueType, IndexType> shield(model->getTransitionMatrix().getRowGroupIndices(), precomputedChoices, shieldingExpression, optimizationDirection, relevantStates, coalitionStates); | 
		
	
		
			
				|  |  |  |  |  |                 shield.construct().printToStream(stream, shieldingExpression, model); | 
		
	
		
			
				|  |  |  |  |  |             } else { | 
		
	
		
			
				|  |  |  |  |  |                 STORM_LOG_THROW(false, storm::exceptions::InvalidArgumentException, "Cannot create " + shieldingExpression->typeToString() + " shields yet"); | 
		
	
		
			
				|  |  |                 storm::utility::closeFile(stream); |  |  |                 storm::utility::closeFile(stream); | 
		
	
		
			
				|  |  |                 STORM_LOG_THROW(false, storm::exceptions::InvalidArgumentException, "Cannot create optimal shields yet"); |  |  |  | 
		
	
		
			
				|  |  |             } |  |  |             } | 
		
	
		
			
				|  |  |             storm::utility::closeFile(stream); |  |  |             storm::utility::closeFile(stream); | 
		
	
		
			
				|  |  |         } |  |  |         } | 
		
	
	
		
			
				|  | 
 |