diff --git a/src/storm-pars-cli/storm-pars.cpp b/src/storm-pars-cli/storm-pars.cpp index 4495f26c1..6b3763321 100644 --- a/src/storm-pars-cli/storm-pars.cpp +++ b/src/storm-pars-cli/storm-pars.cpp @@ -45,6 +45,16 @@ namespace storm { bool graphPreserving; bool exact; }; + + struct PreprocessResult { + PreprocessResult(std::shared_ptr const& model, bool changed) : changed(changed), model(model) { + // Intentionally left empty. + } + + bool changed; + std::shared_ptr model; + boost::optional>> formulas; + }; template std::vector> parseRegions(std::shared_ptr const& model) { @@ -127,64 +137,76 @@ namespace storm { } template - std::pair, bool> preprocessSparseModel(std::shared_ptr> const& model, SymbolicInput const& input) { + PreprocessResult preprocessSparseModel(std::shared_ptr> const& model, SymbolicInput const& input) { auto generalSettings = storm::settings::getModule(); auto bisimulationSettings = storm::settings::getModule(); auto parametricSettings = storm::settings::getModule(); - std::pair, bool> result = std::make_pair(model, false); + PreprocessResult result(model, false); - if (result.first->isOfType(storm::models::ModelType::MarkovAutomaton)) { - result.first = storm::cli::preprocessSparseMarkovAutomaton(result.first->template as>()); - result.second = true; + if (result.model->isOfType(storm::models::ModelType::MarkovAutomaton)) { + result.model = storm::cli::preprocessSparseMarkovAutomaton(result.model->template as>()); + result.changed = true; } if (generalSettings.isBisimulationSet()) { - result.first = storm::cli::preprocessSparseModelBisimulation(result.first->template as>(), input, bisimulationSettings); - result.second = true; + result.model = storm::cli::preprocessSparseModelBisimulation(result.model->template as>(), input, bisimulationSettings); + result.changed = true; } - if (parametricSettings.transformContinuousModel() && (result.first->isOfType(storm::models::ModelType::Ctmc) || result.first->isOfType(storm::models::ModelType::MarkovAutomaton))) { - result.first = storm::api::transformContinuousToDiscreteTimeSparseModel(std::move(*result.first->template as>()), storm::api::extractFormulasFromProperties(input.properties)); - result.second = true; + if (parametricSettings.transformContinuousModel() && (model->isOfType(storm::models::ModelType::Ctmc) || model->isOfType(storm::models::ModelType::MarkovAutomaton))) { + auto transformResult = storm::api::transformContinuousToDiscreteTimeSparseModel(std::move(*model->template as>()), storm::api::extractFormulasFromProperties(input.properties)); + result.model = transformResult.first; + // Set transformed properties as new properties in input + result.formulas = transformResult.second; + result.changed = true; } return result; } template - std::pair, bool> preprocessDdModel(std::shared_ptr> const& model, SymbolicInput const& input) { - - std::pair, bool> result = std::make_pair(model, false); - + PreprocessResult preprocessDdModel(std::shared_ptr> const& model, SymbolicInput const& input) { auto coreSettings = storm::settings::getModule(); + auto generalSettings = storm::settings::getModule(); + auto bisimulationSettings = storm::settings::getModule(); + + PreprocessResult result(model, false); + if (coreSettings.getEngine() == storm::settings::modules::CoreSettings::Engine::Hybrid) { - // Currently, hybrid engine for parametric models just referrs to building the model symbolically. + // Currently, hybrid engine for parametric models just refers to building the model symbolically. STORM_LOG_INFO("Translating symbolic model to sparse model..."); - result.first = storm::api::transformSymbolicToSparseModel(model); - result.second = true; + result.model = storm::api::transformSymbolicToSparseModel(model); + result.changed = true; // Invoke preprocessing on the sparse model - auto sparsePreprocessingResult = storm::pars::preprocessSparseModel(result.first->as>(), input); - if (sparsePreprocessingResult.second) { - result.first = sparsePreprocessingResult.first; + PreprocessResult sparsePreprocessingResult = storm::pars::preprocessSparseModel(result.model->as>(), input); + if (sparsePreprocessingResult.changed) { + result.model = sparsePreprocessingResult.model; + result.formulas = sparsePreprocessingResult.formulas; + } + } else { + STORM_LOG_ASSERT(coreSettings.getEngine() == storm::settings::modules::CoreSettings::Engine::Dd, "Expected Dd engine."); + if (generalSettings.isBisimulationSet()) { + result.model = storm::cli::preprocessDdModelBisimulation(result.model->template as>(), input, bisimulationSettings); + result.changed = true; } } return result; } template - std::pair, bool> preprocessModel(std::shared_ptr const& model, SymbolicInput const& input) { + PreprocessResult preprocessModel(std::shared_ptr const& model, SymbolicInput const& input) { storm::utility::Stopwatch preprocessingWatch(true); - - std::pair, bool> result = std::make_pair(model, false); + + PreprocessResult result(model, false); if (model->isSparseModel()) { - result = storm::pars::preprocessSparseModel(result.first->as>(), input); + result = storm::pars::preprocessSparseModel(result.model->as>(), input); } else { STORM_LOG_ASSERT(model->isSymbolicModel(), "Unexpected model type."); - result = storm::pars::preprocessDdModel(result.first->as>(), input); + result = storm::pars::preprocessDdModel(result.model->as>(), input); } - if (result.second) { + if (result.changed) { STORM_PRINT_AND_LOG(std::endl << "Time for model preprocessing: " << preprocessingWatch << "." << std::endl << std::endl); } return result; @@ -353,6 +375,11 @@ namespace storm { boost::optional rationalFunction = result->asExplicitQuantitativeCheckResult()[*model->getInitialStates().begin()]; storm::api::exportParametricResultToFile(rationalFunction, storm::analysis::ConstraintCollector(*dtmc), parametricSettings.exportResultPath()); } + else if (parametricSettings.exportResultToFile() && model->isOfType(storm::models::ModelType::Ctmc)) { + auto ctmc = model->template as>(); + boost::optional rationalFunction = result->asExplicitQuantitativeCheckResult()[*model->getInitialStates().begin()]; + storm::api::exportParametricResultToFile(rationalFunction, storm::analysis::ConstraintCollector(*ctmc), parametricSettings.exportResultPath()); + } }); } else { STORM_LOG_TRACE("Sampling the model at given points."); @@ -461,11 +488,47 @@ namespace storm { } } } - + + template + void verifyPropertiesWithSymbolicEngine(std::shared_ptr> const& model, SymbolicInput const& input, SampleInformation const& samples) { + if (samples.empty()) { + verifyProperties(input.properties, + [&model] (std::shared_ptr const& formula) { + std::unique_ptr result = storm::api::verifyWithDdEngine(model, storm::api::createTask(formula, true)); + if (result) { + result->filter(storm::modelchecker::SymbolicQualitativeCheckResult(model->getReachableStates(), model->getInitialStates())); + } + return result; + }, + [&model] (std::unique_ptr const& result) { + auto parametricSettings = storm::settings::getModule(); + if (parametricSettings.exportResultToFile() && model->isOfType(storm::models::ModelType::Dtmc)) { + //auto dtmc = model->template as>(); + //boost::optional rationalFunction = result->asSymbolicQuantitativeCheckResult().sum(); + //storm::api::exportParametricResultToFile(rationalFunction, storm::analysis::ConstraintCollector(*dtmc), parametricSettings.exportResultPath()); + } + }); + } else { + STORM_LOG_THROW(false, storm::exceptions::NotSupportedException, "Sampling is not supported in the symbolic engine."); + } + } + + template + void verifyWithDdEngine(std::shared_ptr> const& model, SymbolicInput const& input, std::vector> const& regions, SampleInformation const& samples) { + if (regions.empty()) { + storm::pars::verifyPropertiesWithSymbolicEngine(model, input, samples); + } else { + STORM_LOG_THROW(false, storm::exceptions::NotSupportedException, "Region verification is not supported in the symbolic engine."); + } + } + template void verifyParametricModel(std::shared_ptr const& model, SymbolicInput const& input, std::vector> const& regions, SampleInformation const& samples) { - STORM_LOG_ASSERT(model->isSparseModel(), "Unexpected model type."); - storm::pars::verifyWithSparseEngine(model->as>(), input, regions, samples); + if (model->isSparseModel()) { + storm::pars::verifyWithSparseEngine(model->as>(), input, regions, samples); + } else { + storm::pars::verifyWithDdEngine(model->as>(), input, regions, samples); + } } template @@ -492,8 +555,20 @@ namespace storm { if (model) { auto preprocessingResult = storm::pars::preprocessModel(model, input); - if (preprocessingResult.second) { - model = preprocessingResult.first; + if (preprocessingResult.changed) { + model = preprocessingResult.model; + + if (preprocessingResult.formulas) { + std::vector newProperties; + for (size_t i = 0; i < preprocessingResult.formulas.get().size(); ++i) { + auto formula = preprocessingResult.formulas.get().at(i); + STORM_LOG_ASSERT(i < input.properties.size(), "Index " << i << " greater than number of properties."); + storm::jani::Property property = input.properties.at(i); + newProperties.push_back(storm::jani::Property(property.getName(), formula, property.getUndefinedConstants(), property.getComment())); + } + input.properties = newProperties; + } + model->printModelInformationToStream(std::cout); } } diff --git a/src/storm-pars/api/region.h b/src/storm-pars/api/region.h index ee8d44bff..c032426e5 100644 --- a/src/storm-pars/api/region.h +++ b/src/storm-pars/api/region.h @@ -91,7 +91,7 @@ namespace storm { if (consideredModel->isOfType(storm::models::ModelType::Ctmc) || consideredModel->isOfType(storm::models::ModelType::MarkovAutomaton)) { STORM_LOG_WARN("Parameter lifting not supported for continuous time models. Transforming continuous model to discrete model..."); std::vector> taskFormulaAsVector { task.getFormula().asSharedPointer() }; - consideredModel = storm::api::transformContinuousToDiscreteTimeSparseModel(consideredModel, taskFormulaAsVector); + consideredModel = storm::api::transformContinuousToDiscreteTimeSparseModel(consideredModel, taskFormulaAsVector).first; STORM_LOG_THROW(consideredModel->isOfType(storm::models::ModelType::Dtmc) || consideredModel->isOfType(storm::models::ModelType::Mdp), storm::exceptions::UnexpectedException, "Transformation to discrete time model has failed."); } @@ -121,7 +121,7 @@ namespace storm { if (consideredModel->isOfType(storm::models::ModelType::Ctmc) || consideredModel->isOfType(storm::models::ModelType::MarkovAutomaton)) { STORM_LOG_WARN("Parameter lifting not supported for continuous time models. Transforming continuous model to discrete model..."); std::vector> taskFormulaAsVector { task.getFormula().asSharedPointer() }; - consideredModel = storm::api::transformContinuousToDiscreteTimeSparseModel(consideredModel, taskFormulaAsVector); + consideredModel = storm::api::transformContinuousToDiscreteTimeSparseModel(consideredModel, taskFormulaAsVector).first; STORM_LOG_THROW(consideredModel->isOfType(storm::models::ModelType::Dtmc) || consideredModel->isOfType(storm::models::ModelType::Mdp), storm::exceptions::UnexpectedException, "Transformation to discrete time model has failed."); } diff --git a/src/storm-parsers/parser/DirectEncodingParser.cpp b/src/storm-parsers/parser/DirectEncodingParser.cpp index 160ada212..5e4eee7ab 100644 --- a/src/storm-parsers/parser/DirectEncodingParser.cpp +++ b/src/storm-parsers/parser/DirectEncodingParser.cpp @@ -106,13 +106,13 @@ namespace storm { // Initialize auto modelComponents = std::make_shared>(); bool nonDeterministic = (type == storm::models::ModelType::Mdp || type == storm::models::ModelType::MarkovAutomaton || type == storm::models::ModelType::Pomdp); - bool continousTime = (type == storm::models::ModelType::Ctmc || type == storm::models::ModelType::MarkovAutomaton); + bool continuousTime = (type == storm::models::ModelType::Ctmc || type == storm::models::ModelType::MarkovAutomaton); storm::storage::SparseMatrixBuilder builder = storm::storage::SparseMatrixBuilder(0, 0, 0, false, nonDeterministic, 0); modelComponents->stateLabeling = storm::models::sparse::StateLabeling(stateSize); modelComponents->observabilityClasses = std::vector(); modelComponents->observabilityClasses->resize(stateSize); std::vector> stateRewards; - if (continousTime) { + if (continuousTime) { modelComponents->exitRates = std::vector(stateSize); if (type == storm::models::ModelType::MarkovAutomaton) { modelComponents->markovianStates = storm::storage::BitVector(stateSize); diff --git a/src/storm/analysis/GraphConditions.cpp b/src/storm/analysis/GraphConditions.cpp index c11fccb0b..8fa6c194a 100644 --- a/src/storm/analysis/GraphConditions.cpp +++ b/src/storm/analysis/GraphConditions.cpp @@ -56,47 +56,70 @@ namespace storm { template void ConstraintCollector::process(storm::models::sparse::Model const& model) { - for(uint_fast64_t action = 0; action < model.getTransitionMatrix().getRowCount(); ++action) { - ValueType sum = storm::utility::zero(); - - for (auto transitionIt = model.getTransitionMatrix().begin(action); transitionIt != model.getTransitionMatrix().end(action); ++transitionIt) { - auto const& transition = *transitionIt; - sum += transition.getValue(); - if (!storm::utility::isConstant(transition.getValue())) { - auto const& transitionVars = transition.getValue().gatherVariables(); - variableSet.insert(transitionVars.begin(), transitionVars.end()); - // Assert: 0 <= transition <= 1 + + if (model.getType() != storm::models::ModelType::Ctmc) { + + for(uint_fast64_t action = 0; action < model.getTransitionMatrix().getRowCount(); ++action) { + ValueType sum = storm::utility::zero(); + + for (auto transitionIt = model.getTransitionMatrix().begin(action); transitionIt != model.getTransitionMatrix().end(action); ++transitionIt) { + auto const& transition = *transitionIt; + sum += transition.getValue(); + if (!storm::utility::isConstant(transition.getValue())) { + auto const& transitionVars = transition.getValue().gatherVariables(); + variableSet.insert(transitionVars.begin(), transitionVars.end()); + // Assert: 0 <= transition <= 1 + if (transition.getValue().denominator().isConstant()) { + assert(transition.getValue().denominator().constantPart() != 0); + if (transition.getValue().denominator().constantPart() > 0) { + // Assert: nom <= denom + wellformedConstraintSet.emplace((transition.getValue().nominator() - transition.getValue().denominator()).polynomialWithCoefficient(), storm::CompareRelation::LEQ); + // Assert: nom >= 0 + wellformedConstraintSet.emplace(transition.getValue().nominator().polynomialWithCoefficient(), storm::CompareRelation::GEQ); + } else if (transition.getValue().denominator().constantPart() < 0) { + // Assert nom >= denom + wellformedConstraintSet.emplace((transition.getValue().nominator() - transition.getValue().denominator()).polynomialWithCoefficient(), storm::CompareRelation::GEQ); + // Assert: nom <= 0 + wellformedConstraintSet.emplace(transition.getValue().nominator().polynomialWithCoefficient(), storm::CompareRelation::LEQ); + } else { + STORM_LOG_ASSERT(false, "Denominator must not equal 0."); + } + } else { + // Assert: denom != 0 + wellformedConstraintSet.emplace(transition.getValue().denominator().polynomialWithCoefficient(), storm::CompareRelation::NEQ); + // Assert: transition >= 0 <==> if denom > 0 then nom >= 0 else nom <= 0 + wellformedConstraintSet.emplace(carl::FormulaType::ITE, typename ConstraintType::val(transition.getValue().denominator().polynomialWithCoefficient(), storm::CompareRelation::GREATER), typename ConstraintType::val(transition.getValue().nominator().polynomialWithCoefficient(), storm::CompareRelation::GEQ), typename ConstraintType::val(transition.getValue().nominator().polynomialWithCoefficient(), storm::CompareRelation::LEQ)); + // TODO: Assert: transition <= 1 <==> if denom > 0 then nom - denom <= 0 else nom - denom >= 0 + } + // Assert: transition > 0 + graphPreservingConstraintSet.emplace(transition.getValue().nominator().polynomialWithCoefficient(), storm::CompareRelation::NEQ); + } + } + STORM_LOG_ASSERT(!storm::utility::isConstant(sum) || storm::utility::isOne(sum), "If the sum is a constant, it must be equal to 1."); + if(!storm::utility::isConstant(sum)) { + // Assert: sum == 1 + wellformedConstraintSet.emplace((sum.nominator() - sum.denominator()).polynomialWithCoefficient(), storm::CompareRelation::EQ); + } + } + } else { + for (auto const& transition : model.getTransitionMatrix()) { + if(!transition.getValue().isConstant()) { if (transition.getValue().denominator().isConstant()) { assert(transition.getValue().denominator().constantPart() != 0); if (transition.getValue().denominator().constantPart() > 0) { - // Assert: nom <= denom - wellformedConstraintSet.emplace((transition.getValue().nominator() - transition.getValue().denominator()).polynomialWithCoefficient(), storm::CompareRelation::LEQ); - // Assert: nom >= 0 wellformedConstraintSet.emplace(transition.getValue().nominator().polynomialWithCoefficient(), storm::CompareRelation::GEQ); } else if (transition.getValue().denominator().constantPart() < 0) { - // Assert nom >= denom - wellformedConstraintSet.emplace((transition.getValue().nominator() - transition.getValue().denominator()).polynomialWithCoefficient(), storm::CompareRelation::GEQ); - // Assert: nom <= 0 wellformedConstraintSet.emplace(transition.getValue().nominator().polynomialWithCoefficient(), storm::CompareRelation::LEQ); } else { - STORM_LOG_ASSERT(false, "Denominator must not equal 0."); + assert(false); // Should fail before. } } else { - // Assert: denom != 0 wellformedConstraintSet.emplace(transition.getValue().denominator().polynomialWithCoefficient(), storm::CompareRelation::NEQ); - // Assert: transition >= 0 <==> if denom > 0 then nom >= 0 else nom <= 0 wellformedConstraintSet.emplace(carl::FormulaType::ITE, typename ConstraintType::val(transition.getValue().denominator().polynomialWithCoefficient(), storm::CompareRelation::GREATER), typename ConstraintType::val(transition.getValue().nominator().polynomialWithCoefficient(), storm::CompareRelation::GEQ), typename ConstraintType::val(transition.getValue().nominator().polynomialWithCoefficient(), storm::CompareRelation::LEQ)); - // TODO: Assert: transition <= 1 <==> if denom > 0 then nom - denom <= 0 else nom - denom >= 0 } - // Assert: transition > 0 graphPreservingConstraintSet.emplace(transition.getValue().nominator().polynomialWithCoefficient(), storm::CompareRelation::NEQ); } } - STORM_LOG_ASSERT(!storm::utility::isConstant(sum) || storm::utility::isOne(sum), "If the sum is a constant, it must be equal to 1."); - if(!storm::utility::isConstant(sum)) { - // Assert: sum == 1 - wellformedConstraintSet.emplace((sum.nominator() - sum.denominator()).polynomialWithCoefficient(), storm::CompareRelation::EQ); - } } if (model.getType() == storm::models::ModelType::Ctmc) { diff --git a/src/storm/api/transformation.h b/src/storm/api/transformation.h index c501c10cf..0fb25b2f2 100644 --- a/src/storm/api/transformation.h +++ b/src/storm/api/transformation.h @@ -13,25 +13,28 @@ 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>(), timeRewardName), newFormulas); } else if (model->isOfType(storm::models::ModelType::MarkovAutomaton)) { - return transformer.transform(*model->template as>()); + return std::make_pair(transformer.transform(*model->template as>(), timeRewardName), newFormulas); } else { STORM_LOG_THROW(false, storm::exceptions::NotSupportedException, "Transformation of a " << model->getType() << " to a discrete time model is not supported"); } - return nullptr; + return std::make_pair(nullptr, newFormulas);; } /*! @@ -40,22 +43,25 @@ 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>()), timeRewardName), 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>()), timeRewardName), newFormulas); } else { STORM_LOG_THROW(false, storm::exceptions::NotSupportedException, "Transformation of a " << model.getType() << " to a discrete time model is not supported."); } - return nullptr; + return std::make_pair(nullptr, newFormulas);; } 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/storage/dd/bisimulation/QuotientExtractor.cpp b/src/storm/storage/dd/bisimulation/QuotientExtractor.cpp index 1ba224331..36f7f1fe3 100644 --- a/src/storm/storage/dd/bisimulation/QuotientExtractor.cpp +++ b/src/storm/storage/dd/bisimulation/QuotientExtractor.cpp @@ -998,6 +998,8 @@ namespace storm { // Check quotient matrix for sanity. if (std::is_same::value) { STORM_LOG_ASSERT(quotientTransitionMatrix.greater(storm::utility::one()).isZero(), "Illegal entries in quotient matrix."); + } else if (std::is_same::value) { + // No comparison for rational functions } else { STORM_LOG_ASSERT(quotientTransitionMatrix.greater(storm::utility::one() + storm::utility::convertNumber(1e-6)).isZero(), "Illegal entries in quotient matrix."); } 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..26a95fdd8 100644 --- a/src/storm/transformer/ContinuousToDiscreteTimeModelTransformer.h +++ b/src/storm/transformer/ContinuousToDiscreteTimeModelTransformer.h @@ -16,9 +16,15 @@ namespace storm { class ContinuousToDiscreteTimeModelTransformer { public: - // If this method returns true, the given formula is preserced by the transformation + // If this method returns true, the given formula is preserved 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);