diff --git a/src/storm/api/transformation.h b/src/storm/api/transformation.h index c501c10cf..4c51e1fa4 100644 --- a/src/storm/api/transformation.h +++ b/src/storm/api/transformation.h @@ -13,21 +13,24 @@ namespace storm { /*! * Transforms the given continuous model to a discrete time model. - * If such a transformation does not preserve one of the given formulas, an error is issued. + * If such a transformation does not preserve one of the given formulas, a warning is issued. */ template - std::shared_ptr> transformContinuousToDiscreteTimeSparseModel(std::shared_ptr> const& model, std::vector> const& formulas) { + std::pair>, std::vector>> transformContinuousToDiscreteTimeSparseModel(std::shared_ptr> const& model, std::vector> const& formulas) { storm::transformer::ContinuousToDiscreteTimeModelTransformer transformer; - for (auto const& formula : formulas) { - STORM_LOG_THROW(transformer.preservesFormula(*formula), storm::exceptions::InvalidOperationException, "Transformation to discrete time model does not preserve formula " << *formula << "."); + std::string timeRewardName = "_time"; + while(model->hasRewardModel(timeRewardName)) { + timeRewardName += "_"; } + auto newFormulas = transformer.checkAndTransformFormulas(formulas, timeRewardName) + STORM_LOG_WARN_COND(newFormulas.size() == formulas.size(), "Transformation of a " << model->getType() << " to a discrete time model does not preserve all properties."); if (model->isOfType(storm::models::ModelType::Ctmc)) { - return transformer.transform(*model->template as>()); + return std::make_pair(transformer.transform(*model->template as>()), newFormulas); } else if (model->isOfType(storm::models::ModelType::MarkovAutomaton)) { - return transformer.transform(*model->template as>()); + return std::make_pair(transformer.transform(*model->template as>()), newFormulas); } else { STORM_LOG_THROW(false, storm::exceptions::NotSupportedException, "Transformation of a " << model->getType() << " to a discrete time model is not supported"); } @@ -40,18 +43,21 @@ namespace storm { * If such a transformation does not preserve one of the given formulas, an error is issued. */ template - std::shared_ptr> transformContinuousToDiscreteTimeSparseModel(storm::models::sparse::Model&& model, std::vector> const& formulas) { + std::pair>, std::vector>> transformContinuousToDiscreteTimeSparseModel(storm::models::sparse::Model&& model, std::vector> const& formulas) { storm::transformer::ContinuousToDiscreteTimeModelTransformer transformer; - for (auto const& formula : formulas) { - STORM_LOG_THROW(transformer.preservesFormula(*formula), storm::exceptions::InvalidOperationException, "Transformation to discrete time model does not preserve formula " << *formula << "."); + std::string timeRewardName = "_time"; + while(model.hasRewardModel(timeRewardName)) { + timeRewardName += "_"; } - + auto newFormulas = transformer.checkAndTransformFormulas(formulas, timeRewardName) + STORM_LOG_WARN_COND(newFormulas.size() == formulas.size(), "Transformation of a " << model->getType() << " to a discrete time model does not preserve all properties."); + if (model.isOfType(storm::models::ModelType::Ctmc)) { - return transformer.transform(std::move(*model.template as>())); + return std::make_pair(transformer.transform(std::move(*model.template as>())), newFormulas); } else if (model.isOfType(storm::models::ModelType::MarkovAutomaton)) { - return transformer.transform(std::move(*model.template as>())); + return std::make_pair(transformer.transform(std::move(*model.template as>())), newFormulas); } else { STORM_LOG_THROW(false, storm::exceptions::NotSupportedException, "Transformation of a " << model.getType() << " to a discrete time model is not supported."); } diff --git a/src/storm/logic/ExpectedTimeToExpectedRewardVisitor.cpp b/src/storm/logic/ExpectedTimeToExpectedRewardVisitor.cpp new file mode 100644 index 000000000..d240446a6 --- /dev/null +++ b/src/storm/logic/ExpectedTimeToExpectedRewardVisitor.cpp @@ -0,0 +1,28 @@ +#include "storm/logic/ExpectedTimeToExpectedRewardVisitor.h" +#include "storm/logic/Formulas.h" + +#include "storm/utility/macros.h" + +#include "storm/exceptions/InvalidPropertyException.h" + +namespace storm { + namespace logic { + + ExpectedTimeToExpectedRewardVisitor::ExpectedTimeToExpectedRewardVisitor(std::string const& timeRewardModelName) : timeRewardModelName(timeRewardModelName) { + // Intentionally left empty + } + + std::shared_ptr ExpectedTimeToExpectedRewardVisitor::substitute(Formula const& f) const { + boost::any result = f.accept(*this, boost::any()); + return boost::any_cast>(result); + } + + boost::any ExpectedTimeToExpectedRewardVisitor::visit(TimeOperatorFormula const& f, boost::any const& data) const { + STORM_LOG_THROW(f.getSubformula().isEventuallyFormula(), storm::exceptions::InvalidPropertyException, "Expected eventually formula within time operator. Got " << f << " instead."); + std::shared_ptr subsubformula = boost::any_cast>(f.getSubformula().asEventuallyFormula().getSubformula().accept(*this, data)); + STORM_LOG_THROW(f.getSubformula().isReachabilityTimeFormula(), storm::exceptions::InvalidPropertyException, "Expected time path formula within time operator. Got " << f << " instead."); + std::shared_ptr subformula = std::make_shared(subsubformula, storm::logic::FormulaContext::Reward); + return std::static_pointer_cast(std::make_shared(subformula, timeRewardModelName, f.getOperatorInformation())); + } + } +} diff --git a/src/storm/logic/ExpectedTimeToExpectedRewardVisitor.h b/src/storm/logic/ExpectedTimeToExpectedRewardVisitor.h new file mode 100644 index 000000000..b182a8520 --- /dev/null +++ b/src/storm/logic/ExpectedTimeToExpectedRewardVisitor.h @@ -0,0 +1,25 @@ +#pragma once + +#include + +#include "storm/logic/CloneVisitor.h" + +#include "storm/storage/expressions/Expression.h" + +namespace storm { + namespace logic { + + class ExpectedTimeToExpectedRewardVisitor : public CloneVisitor { + public: + ExpectedTimeToExpectedRewardVisitor(std::string const& timeRewardModelName); + + std::shared_ptr substitute(Formula const& f) const; + + virtual boost::any visit(TimeOperatorFormula const& f, boost::any const& data) const override; + + private: + std::string const& timeRewardModelName; + }; + + } +} diff --git a/src/storm/transformer/ContinuousToDiscreteTimeModelTransformer.cpp b/src/storm/transformer/ContinuousToDiscreteTimeModelTransformer.cpp index 20357f400..411c60821 100644 --- a/src/storm/transformer/ContinuousToDiscreteTimeModelTransformer.cpp +++ b/src/storm/transformer/ContinuousToDiscreteTimeModelTransformer.cpp @@ -5,7 +5,7 @@ #include "storm/models/sparse/StandardRewardModel.h" #include "storm/logic/Formulas.h" #include "storm/logic/FragmentSpecification.h" -#include "storm/logic/CloneVisitor.h" +#include "storm/logic/ExpectedTimeToExpectedRewardVisitor.h" #include "storm/utility/macros.h" #include "storm/utility/vector.h" @@ -93,7 +93,22 @@ namespace storm { fragment.setReachabilityRewardFormulasAllowed(true); return formula.isInFragment(fragment); } - + + template + std::vector> ContinuousToDiscreteTimeModelTransformer::checkAndTransformFormulas(std::vector> const& formulas, std::string const& timeRewardName) { + std::vector> result; + storm::logic::ExpectedTimeToExpectedRewardVisitor v(timeRewardName); + for (auto const& f : formulas) { + // Translate expected time formulas + auto newF = v.substitute(*f); + if(preservesFormula(*newF)) { + result.push_back(newF); + } else { + STORM_LOG_INFO("Continuous to discrete time transformation does not preserve formula " << *f); + } + } + return result; + } template std::shared_ptr> ContinuousToDiscreteTimeModelTransformer::transform(storm::models::sparse::MarkovAutomaton const& ma, boost::optional const& timeRewardModelName) { diff --git a/src/storm/transformer/ContinuousToDiscreteTimeModelTransformer.h b/src/storm/transformer/ContinuousToDiscreteTimeModelTransformer.h index d26b96c1f..b9e1d699a 100644 --- a/src/storm/transformer/ContinuousToDiscreteTimeModelTransformer.h +++ b/src/storm/transformer/ContinuousToDiscreteTimeModelTransformer.h @@ -18,7 +18,13 @@ namespace storm { // If this method returns true, the given formula is preserced by the transformation static bool preservesFormula(storm::logic::Formula const& formula); - + + // Checks whether the given formulas are preserved. + // Expected time formulas are translated to expected reward formulas. + // The returned vector only contains formulas that are preserved by the transformation. + static std::vector> checkAndTransformFormulas(std::vector> const& formulas, std::string const& timeRewardName); + + // Transforms the given CTMC to its underlying (aka embedded) DTMC. // A reward model for time is added if a corresponding reward model name is given static std::shared_ptr> transform(storm::models::sparse::Ctmc const& ctmc, boost::optional const& timeRewardModelName = boost::none);