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

eliminate reward accumulations on jani level

tempestpy_adaptions
TimQu 6 years ago
parent
6cc0369a1c
commit
8050f8fc67
5 changed files with 49 additions and 95 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. 41
      src/storm-cli-utilities/model-handling.h
  2. 88
      src/storm/logic/RewardAccumulationEliminationVisitor.cpp
  3. 12
      src/storm/logic/RewardAccumulationEliminationVisitor.h
  4. 1
      src/storm/logic/TimeBoundType.h
  5. 2
      src/storm/storage/jani/EdgeContainer.h

41
src/storm-cli-utilities/model-handling.h
View File

@ -23,7 +23,6 @@
#include "storm/models/ModelBase.h"
#include "storm/exceptions/OptionParserException.h"
#include "storm/exceptions/UnexpectedException.h"
#include "storm/modelchecker/results/SymbolicQualitativeCheckResult.h"
@ -126,6 +125,10 @@ namespace storm {
}
if (!output.properties.empty()) {
output.properties = storm::api::substituteConstantsInProperties(output.properties, constantDefinitions);
if (output.model.is_initialized() && output.model->isJaniModel()) {
storm::logic::RewardAccumulationEliminationVisitor v(output.model->asJaniModel());
v.eliminateRewardAccumulations(output.properties);
}
}
// Check whether conversion for PRISM to JANI is requested or necessary.
@ -384,7 +387,6 @@ namespace storm {
std::pair<std::shared_ptr<storm::models::ModelBase>, bool> result = std::make_pair(model, false);
if (model->isSparseModel()) {
STORM_LOG_THROW((std::is_same<BuildValueType, ExportValueType>::value), storm::exceptions::UnexpectedException, "Build-Value Type and ExportValueType should be the same in the sparse engine.");
result = preprocessSparseModel<BuildValueType>(result.first->as<storm::models::sparse::Model<BuildValueType>>(), input);
} else {
STORM_LOG_ASSERT(model->isSymbolicModel(), "Unexpected model type.");
@ -399,29 +401,6 @@ namespace storm {
return result;
}
template <typename ModelType>
storm::jani::Property preprocessProperty(std::shared_ptr<ModelType> const& model, storm::jani::Property const& property) {
storm::logic::RewardAccumulationEliminationVisitor<typename ModelType::RewardModelType> v(model->getRewardModels(), model->getType());
auto formula = v.eliminateRewardAccumulations(*property.getFilter().getFormula());
auto states = v.eliminateRewardAccumulations(*property.getFilter().getStatesFormula());
storm::jani::FilterExpression fe(formula, property.getFilter().getFilterType(), states);
return storm::jani::Property(property.getName(), fe, property.getComment());
}
template <storm::dd::DdType DdType, typename ValueType>
std::vector<storm::jani::Property> preprocessProperties(std::shared_ptr<storm::models::ModelBase> const& model, SymbolicInput const& input) {
std::vector<storm::jani::Property> resultProperties;
for (auto const& property : input.properties) {
if (model->isSparseModel()) {
resultProperties.push_back(preprocessProperty(model->as<storm::models::sparse::Model<ValueType>>(), property));
} else {
STORM_LOG_ASSERT(model->isSymbolicModel(), "Unexpected model type.");
resultProperties.push_back(preprocessProperty(model->as<storm::models::symbolic::Model<DdType, ValueType>>(), property));
}
}
return resultProperties;
}
void printComputingCounterexample(storm::jani::Property const& property) {
STORM_PRINT("Computing counterexample for property " << *property.getRawFormula() << " ..." << std::endl);
}
@ -696,7 +675,7 @@ namespace storm {
}
template <storm::dd::DdType DdType, typename BuildValueType, typename VerificationValueType = BuildValueType>
std::shared_ptr<storm::models::ModelBase> buildPreprocessExportModelWithValueTypeAndDdlib(SymbolicInput& input, storm::settings::modules::CoreSettings::Engine engine) {
std::shared_ptr<storm::models::ModelBase> buildPreprocessExportModelWithValueTypeAndDdlib(SymbolicInput const& input, storm::settings::modules::CoreSettings::Engine engine) {
auto ioSettings = storm::settings::getModule<storm::settings::modules::IOSettings>();
auto buildSettings = storm::settings::getModule<storm::settings::modules::BuildSettings>();
std::shared_ptr<storm::models::ModelBase> model;
@ -716,9 +695,6 @@ namespace storm {
model = preprocessingResult.first;
model->printModelInformationToStream(std::cout);
}
if (!input.properties.empty()) {
input.properties = preprocessProperties<DdType, VerificationValueType>(model, input);
}
exportModel<DdType, BuildValueType>(model, input);
}
return model;
@ -737,16 +713,15 @@ namespace storm {
} else if (engine == storm::settings::modules::CoreSettings::Engine::Exploration) {
verifyWithExplorationEngine<VerificationValueType>(input);
} else {
SymbolicInput preprocessedInput = input;
std::shared_ptr<storm::models::ModelBase> model = buildPreprocessExportModelWithValueTypeAndDdlib<DdType, BuildValueType, VerificationValueType>(preprocessedInput, engine);
std::shared_ptr<storm::models::ModelBase> model = buildPreprocessExportModelWithValueTypeAndDdlib<DdType, BuildValueType, VerificationValueType>(input, engine);
if (model) {
if (coreSettings.isCounterexampleSet()) {
auto ioSettings = storm::settings::getModule<storm::settings::modules::IOSettings>();
generateCounterexamples<VerificationValueType>(model, preprocessedInput);
generateCounterexamples<VerificationValueType>(model, input);
} else {
auto ioSettings = storm::settings::getModule<storm::settings::modules::IOSettings>();
verifyModel<DdType, VerificationValueType>(model, preprocessedInput, coreSettings);
verifyModel<DdType, VerificationValueType>(model, input, coreSettings);
}
}
}

88
src/storm/logic/RewardAccumulationEliminationVisitor.cpp
View File

@ -1,39 +1,35 @@
#include "storm/logic/RewardAccumulationEliminationVisitor.h"
#include "storm/logic/Formulas.h"
#include "storm/storage/jani/Model.h"
#include "storm/storage/jani/traverser/AssignmentsFinder.h"
#include "storm/utility/macros.h"
#include "storm/exceptions/UnexpectedException.h"
#include "storm/exceptions/InvalidPropertyException.h"
#include "storm/storage/dd/DdManager.h"
#include "storm/storage/dd/Add.h"
#include "storm/storage/dd/Bdd.h"
#include "storm/models/sparse/StandardRewardModel.h"
#include "storm/models/symbolic/StandardRewardModel.h"
namespace storm {
namespace logic {
template <class RewardModelType>
RewardAccumulationEliminationVisitor<RewardModelType>::RewardAccumulationEliminationVisitor(std::unordered_map<std::string, RewardModelType> const& rewardModels, storm::models::ModelType const& modelType) : rewardModels(rewardModels) {
if (modelType == storm::models::ModelType::Dtmc || modelType == storm::models::ModelType::Mdp || modelType == storm::models::ModelType::S2pg) {
isDiscreteTimeModel = true;
} else if (modelType == storm::models::ModelType::Ctmc || modelType == storm::models::ModelType::MarkovAutomaton) {
isDiscreteTimeModel = false;
} else {
STORM_LOG_THROW(false, storm::exceptions::UnexpectedException, "Unhandled model type " << modelType << ".");
}
RewardAccumulationEliminationVisitor::RewardAccumulationEliminationVisitor(storm::jani::Model const& model) : model(model) {
// Intentionally left empty
}
template <class RewardModelType>
std::shared_ptr<Formula> RewardAccumulationEliminationVisitor<RewardModelType>::eliminateRewardAccumulations(Formula const& f) const {
std::shared_ptr<Formula> RewardAccumulationEliminationVisitor::eliminateRewardAccumulations(Formula const& f) const {
boost::any result = f.accept(*this, boost::any());
return boost::any_cast<std::shared_ptr<Formula>>(result);
}
template <class RewardModelType>
boost::any RewardAccumulationEliminationVisitor<RewardModelType>::visit(BoundedUntilFormula const& f, boost::any const& data) const {
void RewardAccumulationEliminationVisitor::eliminateRewardAccumulations(std::vector<storm::jani::Property>& properties) const {
for (auto& p : properties) {
auto formula = eliminateRewardAccumulations(*p.getFilter().getFormula());
auto states = eliminateRewardAccumulations(*p.getFilter().getStatesFormula());
storm::jani::FilterExpression fe(formula, p.getFilter().getFilterType(), states);
p = storm::jani::Property(p.getName(), storm::jani::FilterExpression(formula, p.getFilter().getFilterType(), states), p.getComment());
}
}
boost::any RewardAccumulationEliminationVisitor::visit(BoundedUntilFormula const& f, boost::any const& data) const {
std::vector<boost::optional<TimeBound>> lowerBounds, upperBounds;
std::vector<TimeBoundReference> timeBoundReferences;
for (uint64_t i = 0; i < f.getDimension(); ++i) {
@ -68,8 +64,7 @@ namespace storm {
}
}
template <class RewardModelType>
boost::any RewardAccumulationEliminationVisitor<RewardModelType>::visit(CumulativeRewardFormula const& f, boost::any const& data) const {
boost::any RewardAccumulationEliminationVisitor::visit(CumulativeRewardFormula const& f, boost::any const& data) const {
boost::optional<storm::logic::RewardAccumulation> rewAcc;
STORM_LOG_THROW(!data.empty(), storm::exceptions::UnexpectedException, "Formula " << f << " does not seem to be a subformula of a reward operator.");
auto rewName = boost::any_cast<boost::optional<std::string>>(data);
@ -91,14 +86,13 @@ namespace storm {
return std::static_pointer_cast<Formula>(std::make_shared<CumulativeRewardFormula>(bounds, timeBoundReferences, rewAcc));
}
template <class RewardModelType>
boost::any RewardAccumulationEliminationVisitor<RewardModelType>::visit(EventuallyFormula const& f, boost::any const& data) const {
boost::any RewardAccumulationEliminationVisitor::visit(EventuallyFormula const& f, boost::any const& data) const {
std::shared_ptr<Formula> subformula = boost::any_cast<std::shared_ptr<Formula>>(f.getSubformula().accept(*this, data));
if (f.hasRewardAccumulation()) {
if (f.isTimePathFormula()) {
if (isDiscreteTimeModel && ((!f.getRewardAccumulation().isExitSet() && !f.getRewardAccumulation().isStepsSet()) || (f.getRewardAccumulation().isStepsSet() && f.getRewardAccumulation().isExitSet()))) {
if (model.isDiscreteTimeModel() && ((!f.getRewardAccumulation().isExitSet() && !f.getRewardAccumulation().isStepsSet()) || (f.getRewardAccumulation().isStepsSet() && f.getRewardAccumulation().isExitSet()))) {
return std::static_pointer_cast<Formula>(std::make_shared<EventuallyFormula>(subformula, f.getContext(), f.getRewardAccumulation()));
} else if (!isDiscreteTimeModel && (!f.getRewardAccumulation().isTimeSet() || f.getRewardAccumulation().isExitSet() || f.getRewardAccumulation().isStepsSet())) {
} else if (!model.isDiscreteTimeModel() && (!f.getRewardAccumulation().isTimeSet() || f.getRewardAccumulation().isExitSet() || f.getRewardAccumulation().isStepsSet())) {
return std::static_pointer_cast<Formula>(std::make_shared<EventuallyFormula>(subformula, f.getContext(), f.getRewardAccumulation()));
}
} else if (f.isRewardPathFormula()) {
@ -112,14 +106,12 @@ namespace storm {
return std::static_pointer_cast<Formula>(std::make_shared<EventuallyFormula>(subformula, f.getContext()));
}
template <class RewardModelType>
boost::any RewardAccumulationEliminationVisitor<RewardModelType>::visit(RewardOperatorFormula const& f, boost::any const& data) const {
boost::any RewardAccumulationEliminationVisitor::visit(RewardOperatorFormula const& f, boost::any const& data) const {
std::shared_ptr<Formula> subformula = boost::any_cast<std::shared_ptr<Formula>>(f.getSubformula().accept(*this, f.getOptionalRewardModelName()));
return std::static_pointer_cast<Formula>(std::make_shared<RewardOperatorFormula>(subformula, f.getOptionalRewardModelName(), f.getOperatorInformation()));
}
template <class RewardModelType>
boost::any RewardAccumulationEliminationVisitor<RewardModelType>::visit(TotalRewardFormula const& f, boost::any const& data) const {
boost::any RewardAccumulationEliminationVisitor::visit(TotalRewardFormula const& f, boost::any const& data) const {
STORM_LOG_THROW(!data.empty(), storm::exceptions::UnexpectedException, "Formula " << f << " does not seem to be a subformula of a reward operator.");
auto rewName = boost::any_cast<boost::optional<std::string>>(data);
if (f.hasRewardAccumulation() || canEliminate(f.getRewardAccumulation(), rewName)) {
@ -129,23 +121,22 @@ namespace storm {
}
}
template <class RewardModelType>
bool RewardAccumulationEliminationVisitor<RewardModelType>::canEliminate(storm::logic::RewardAccumulation const& accumulation, boost::optional<std::string> rewardModelName) const {
auto rewModelIt = rewardModels.end();
if (rewardModelName.is_initialized()){
rewModelIt = rewardModels.find(rewardModelName.get());
STORM_LOG_THROW(rewModelIt != rewardModels.end(), storm::exceptions::InvalidPropertyException, "Unable to find reward model with name " << rewardModelName.get());
} else if (rewardModels.size() == 1) {
rewModelIt = rewardModels.begin();
} else {
STORM_LOG_THROW(false, storm::exceptions::InvalidPropertyException, "Multiple reward models were defined but no reward model name was given for at least one property.");
bool RewardAccumulationEliminationVisitor::canEliminate(storm::logic::RewardAccumulation const& accumulation, boost::optional<std::string> rewardModelName) const {
STORM_LOG_THROW(rewardModelName.is_initialized(), storm::exceptions::InvalidPropertyException, "Unable to find transient variable with for unique reward model.");
storm::jani::AssignmentsFinder::ResultType assignmentKinds;
STORM_LOG_THROW(model.hasGlobalVariable(rewardModelName.get()), storm::exceptions::InvalidPropertyException, "Unable to find transient variable with name " << rewardModelName.get() << ".");
storm::jani::Variable const& transientVar = model.getGlobalVariable(rewardModelName.get());
if (transientVar.getInitExpression().containsVariables() || !storm::utility::isZero(transientVar.getInitExpression().evaluateAsRational())) {
assignmentKinds.hasLocationAssignment = true;
assignmentKinds.hasEdgeAssignment = true;
assignmentKinds.hasEdgeDestinationAssignment = true;
}
RewardModelType const& rewardModel = rewModelIt->second;
if ((rewardModel.hasStateActionRewards() || rewardModel.hasTransitionRewards()) && !accumulation.isStepsSet()) {
assignmentKinds = storm::jani::AssignmentsFinder().find(model, transientVar);
if ((assignmentKinds.hasEdgeAssignment || assignmentKinds.hasEdgeDestinationAssignment) && !accumulation.isStepsSet()) {
return false;
}
if (rewardModel.hasStateRewards()) {
if (isDiscreteTimeModel) {
if (assignmentKinds.hasLocationAssignment) {
if (model.isDiscreteTimeModel()) {
if (!accumulation.isExitSet()) {
return false;
}
@ -158,16 +149,5 @@ namespace storm {
}
return true;
}
template class RewardAccumulationEliminationVisitor<storm::models::sparse::StandardRewardModel<double>>;
template class RewardAccumulationEliminationVisitor<storm::models::sparse::StandardRewardModel<storm::RationalNumber>>;
template class RewardAccumulationEliminationVisitor<storm::models::sparse::StandardRewardModel<storm::RationalFunction>>;
template class RewardAccumulationEliminationVisitor<storm::models::sparse::StandardRewardModel<storm::Interval>>;
template class RewardAccumulationEliminationVisitor<storm::models::symbolic::StandardRewardModel<storm::dd::DdType::CUDD, double>>;
template class RewardAccumulationEliminationVisitor<storm::models::symbolic::StandardRewardModel<storm::dd::DdType::Sylvan, double>>;
template class RewardAccumulationEliminationVisitor<storm::models::symbolic::StandardRewardModel<storm::dd::DdType::Sylvan, storm::RationalNumber>>;
template class RewardAccumulationEliminationVisitor<storm::models::symbolic::StandardRewardModel<storm::dd::DdType::Sylvan, storm::RationalFunction>>;
}
}

12
src/storm/logic/RewardAccumulationEliminationVisitor.h
View File

@ -5,21 +5,22 @@
#include "storm/logic/CloneVisitor.h"
#include "storm/logic/RewardAccumulation.h"
#include "storm/models/ModelType.h"
#include "storm/storage/jani/Model.h"
#include "storm/storage/jani/Property.h"
namespace storm {
namespace logic {
template <class RewardModelType>
class RewardAccumulationEliminationVisitor : public CloneVisitor {
public:
RewardAccumulationEliminationVisitor(std::unordered_map<std::string, RewardModelType> const& rewardModels, storm::models::ModelType const& modelType);
RewardAccumulationEliminationVisitor(storm::jani::Model const& model);
/*!
* Eliminates any reward accumulations of the formula, where the presence of the reward accumulation does not change the result of the formula
*/
std::shared_ptr<Formula> eliminateRewardAccumulations(Formula const& f) const;
void eliminateRewardAccumulations(std::vector<storm::jani::Property>& properties) const;
virtual boost::any visit(BoundedUntilFormula const& f, boost::any const& data) const override;
virtual boost::any visit(CumulativeRewardFormula const& f, boost::any const& data) const override;
@ -31,8 +32,7 @@ namespace storm {
private:
bool canEliminate(storm::logic::RewardAccumulation const& accumulation, boost::optional<std::string> rewardModelName) const;
std::unordered_map<std::string, RewardModelType> const& rewardModels;
bool isDiscreteTimeModel;
storm::jani::Model const& model;
};
}

1
src/storm/logic/TimeBoundType.h
View File

@ -51,7 +51,6 @@ namespace storm {
}
bool hasRewardAccumulation() const {
assert(isRewardBound());
return rewardAccumulation.is_initialized();
}

2
src/storm/storage/jani/EdgeContainer.h
View File

@ -95,7 +95,7 @@ namespace storm {
void clearConcreteEdges();
std::vector<Edge> const& getConcreteEdges() const;
std::vector<Edge> & getConcreteEdges();
TemplateEdgeContainer const& getTemplateEdges const;
TemplateEdgeContainer const& getTemplateEdges() const;
size_t size() const;

Write Preview
Loading…
Cancel
Save