sp
/
tempest
1
0
Fork 0
Code Issues Pull Requests Projects Releases Wiki Activity
Browse Source

changed shield-handling.h to ShieldHandling.cpp and ShieldHandling.h 

renamed createOptimalShield() to createQuantitativShield()
tempestpy_adaptions
Lukas Posch 3 years ago
committed by Stefan Pranger
parent
a63d8cda6b
commit
79447073d0
4 changed files with 81 additions and 62 deletions
Whitespace
Show all changes Ignore whitespace when comparing lines Ignore changes in amount of whitespace Ignore changes in whitespace at EOL
Split View
Diff Options
Show Stats Download Patch File Download Diff File
  1. 4
      src/storm/modelchecker/rpatl/SparseSmgRpatlModelChecker.cpp
  2. 47
      src/storm/shields/ShieldHandling.cpp
  3. 32
      src/storm/shields/ShieldHandling.h
  4. 60
      src/storm/shields/shield-handling.h

4
src/storm/modelchecker/rpatl/SparseSmgRpatlModelChecker.cpp
View File

@ -24,7 +24,7 @@
#include "storm/models/sparse/StandardRewardModel.h"
#include "storm/shields/shield-handling.h"
#include "storm/shields/ShieldHandling.h"
#include "storm/settings/modules/GeneralSettings.h"
@ -212,7 +212,7 @@ namespace storm {
std::unique_ptr<CheckResult> result(new ExplicitQuantitativeCheckResult<ValueType>(std::move(values)));
if(checkTask.isShieldingTask()) {
tempest::shields::createOptimalShield<ValueType>(std::make_shared<storm::models::sparse::Smg<ValueType>>(this->getModel()), helper.getProducedOptimalChoices(), checkTask.getShieldingExpression(), checkTask.getOptimizationDirection(), statesOfCoalition, statesOfCoalition);
tempest::shields::createQuantitativeShield<ValueType>(std::make_shared<storm::models::sparse::Smg<ValueType>>(this->getModel()), helper.getProducedOptimalChoices(), checkTask.getShieldingExpression(), checkTask.getOptimizationDirection(), statesOfCoalition, statesOfCoalition);
} else if (checkTask.isProduceSchedulersSet()) {
result->asExplicitQuantitativeCheckResult<ValueType>().setScheduler(std::make_unique<storm::storage::Scheduler<ValueType>>(helper.extractScheduler()));
}

47
src/storm/shields/ShieldHandling.cpp
View File

@ -0,0 +1,47 @@
#include "ShieldHandling.h"
namespace tempest {
namespace shields {
std::string shieldFilename(std::shared_ptr<storm::logic::ShieldExpression const> const& shieldingExpression) {
return shieldingExpression->getFilename() + ".shield";
}
template<typename ValueType, typename IndexType>
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) {
std::ofstream stream;
storm::utility::openFile(shieldFilename(shieldingExpression), stream);
if(shieldingExpression->isPreSafetyShield()) {
PreSafetyShield<ValueType, IndexType> shield(model->getTransitionMatrix().getRowGroupIndices(), choiceValues, shieldingExpression, optimizationDirection, relevantStates, coalitionStates);
shield.construct().printToStream(stream, shieldingExpression, model);
} else if(shieldingExpression->isPostSafetyShield()) {
PostSafetyShield<ValueType, IndexType> shield(model->getTransitionMatrix().getRowGroupIndices(), choiceValues, shieldingExpression, optimizationDirection, relevantStates, coalitionStates);
shield.construct().printToStream(stream, shieldingExpression, model);
} else {
STORM_LOG_THROW(false, storm::exceptions::InvalidArgumentException, "Unknown Shielding Type: " + shieldingExpression->typeToString());
storm::utility::closeFile(stream);
}
storm::utility::closeFile(stream);
}
template<typename ValueType, typename IndexType>
void createQuantitativeShield(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()) {
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, "Unknown Shielding Type: " + shieldingExpression->typeToString());
storm::utility::closeFile(stream);
}
storm::utility::closeFile(stream);
}
// 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 void createQuantitativeShield<double, typename storm::storage::SparseMatrix<double>::index_type>(std::shared_ptr<storm::models::sparse::Model<double>> 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);
#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 void createQuantitativeShield<storm::RationalNumber, typename storm::storage::SparseMatrix<storm::RationalNumber>::index_type>(std::shared_ptr<storm::models::sparse::Model<storm::RationalNumber>> 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);
#endif
}
}

32
src/storm/shields/ShieldHandling.h
View File

@ -0,0 +1,32 @@
#pragma once
#include <iostream>
#include <boost/optional.hpp>
#include <memory>
#include "storm/storage/Scheduler.h"
#include "storm/storage/BitVector.h"
#include "storm/logic/ShieldExpression.h"
#include "storm/shields/AbstractShield.h"
#include "storm/shields/PreSafetyShield.h"
#include "storm/shields/PostSafetyShield.h"
#include "storm/shields/OptimalShield.h"
#include "storm/io/file.h"
#include "storm/utility/macros.h"
#include "storm/exceptions/InvalidArgumentException.h"
namespace tempest {
namespace shields {
std::string shieldFilename(std::shared_ptr<storm::logic::ShieldExpression const> const& shieldingExpression);
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>
void createQuantitativeShield(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);
}
}

60
src/storm/shields/shield-handling.h
View File

@ -1,60 +0,0 @@
#pragma once
#include <iostream>
#include <boost/optional.hpp>
#include <memory>
#include "storm/storage/Scheduler.h"
#include "storm/storage/BitVector.h"
#include "storm/logic/ShieldExpression.h"
#include "storm/shields/AbstractShield.h"
#include "storm/shields/PreSafetyShield.h"
#include "storm/shields/PostSafetyShield.h"
#include "storm/shields/OptimalShield.h"
#include "storm/io/file.h"
#include "storm/utility/macros.h"
#include "storm/exceptions/InvalidArgumentException.h"
namespace tempest {
namespace shields {
std::string shieldFilename(std::shared_ptr<storm::logic::ShieldExpression const> const& shieldingExpression) {
return shieldingExpression->getFilename() + ".shield";
}
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) {
std::ofstream stream;
storm::utility::openFile(shieldFilename(shieldingExpression), stream);
if(shieldingExpression->isPreSafetyShield()) {
PreSafetyShield<ValueType, IndexType> shield(model->getTransitionMatrix().getRowGroupIndices(), choiceValues, shieldingExpression, optimizationDirection, relevantStates, coalitionStates);
shield.construct().printToStream(stream, shieldingExpression, model);
} else if(shieldingExpression->isPostSafetyShield()) {
PostSafetyShield<ValueType, IndexType> shield(model->getTransitionMatrix().getRowGroupIndices(), choiceValues, shieldingExpression, optimizationDirection, relevantStates, coalitionStates);
shield.construct().printToStream(stream, shieldingExpression, model);
} else {
STORM_LOG_THROW(false, storm::exceptions::InvalidArgumentException, "Unknown Shielding Type: " + shieldingExpression->typeToString());
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()) {
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, "Unknown Shielding Type: " + shieldingExpression->typeToString());
storm::utility::closeFile(stream);
}
storm::utility::closeFile(stream);
}
}
}
Write Preview
Loading…
Cancel
Save