diff --git a/src/storm-cli-utilities/model-handling.h b/src/storm-cli-utilities/model-handling.h
index 257453e92..524d772be 100644
--- a/src/storm-cli-utilities/model-handling.h
+++ b/src/storm-cli-utilities/model-handling.h
@@ -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);
}
}
}
diff --git a/src/storm/logic/RewardAccumulationEliminationVisitor.cpp b/src/storm/logic/RewardAccumulationEliminationVisitor.cpp
index 0cefa9a7d..710f959f1 100644
--- a/src/storm/logic/RewardAccumulationEliminationVisitor.cpp
+++ b/src/storm/logic/RewardAccumulationEliminationVisitor.cpp
@@ -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>>;
-
}
}
diff --git a/src/storm/logic/RewardAccumulationEliminationVisitor.h b/src/storm/logic/RewardAccumulationEliminationVisitor.h
index 80915b8e9..0b77901d9 100644
--- a/src/storm/logic/RewardAccumulationEliminationVisitor.h
+++ b/src/storm/logic/RewardAccumulationEliminationVisitor.h
@@ -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;
};
}
diff --git a/src/storm/logic/TimeBoundType.h b/src/storm/logic/TimeBoundType.h
index 23f850105..ec9a753b0 100644
--- a/src/storm/logic/TimeBoundType.h
+++ b/src/storm/logic/TimeBoundType.h
@@ -51,7 +51,6 @@ namespace storm {
}
bool hasRewardAccumulation() const {
- assert(isRewardBound());
return rewardAccumulation.is_initialized();
}
diff --git a/src/storm/storage/jani/EdgeContainer.h b/src/storm/storage/jani/EdgeContainer.h
index faa33a418..c2bdfe80c 100644
--- a/src/storm/storage/jani/EdgeContainer.h
+++ b/src/storm/storage/jani/EdgeContainer.h
@@ -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;