diff --git a/src/storm-dft/builder/DFTBuilder.cpp b/src/storm-dft/builder/DFTBuilder.cpp index d3e635636..87bd5f407 100644 --- a/src/storm-dft/builder/DFTBuilder.cpp +++ b/src/storm-dft/builder/DFTBuilder.cpp @@ -140,7 +140,8 @@ namespace storm { if (children.size() <= 1) { STORM_LOG_ERROR("Sequence enforcers require at least two children"); } - if (mElements.count(name) != 0) { + if (nameInUse(name)) { + STORM_LOG_ERROR("Element with name '" << name << "' already exists."); return false; } DFTRestrictionPointer restr; @@ -166,8 +167,8 @@ namespace storm { template<typename ValueType> bool DFTBuilder<ValueType>::addStandardGate(std::string const& name, std::vector<std::string> const& children, storm::storage::DFTElementType tp) { STORM_LOG_ASSERT(children.size() > 0, "No child for " << name); - if(mElements.count(name) != 0) { - // Element with that name already exists. + if (nameInUse(name)) { + STORM_LOG_ERROR("Element with name '" << name << "' already exists."); return false; } DFTElementPointer element; diff --git a/src/storm-dft/builder/DFTBuilder.h b/src/storm-dft/builder/DFTBuilder.h index 4d9f2652f..479db529c 100644 --- a/src/storm-dft/builder/DFTBuilder.h +++ b/src/storm-dft/builder/DFTBuilder.h @@ -93,8 +93,8 @@ namespace storm { if(children.size() <= 1) { STORM_LOG_ERROR("Dependencies require at least two children"); } - if(mElements.count(name) != 0) { - // Element with that name already exists. + if (nameInUse(name)) { + STORM_LOG_ERROR("Element with name '" << name << "' already exists."); return false; } @@ -122,13 +122,11 @@ namespace storm { if(binaryDependencies) { for (size_t i = 1; i < children.size(); ++i) { std::string nameDep = name + "_" + std::to_string(i); - if (mElements.count(nameDep) != 0) { - // Element with that name already exists. - STORM_LOG_ERROR("Element with name: " << nameDep << " already exists."); + if (nameInUse(nameDep)) { + STORM_LOG_ERROR("Element with name '" << name << "' already exists."); return false; } - STORM_LOG_ASSERT(storm::utility::isOne(probability) || children.size() == 2, - "PDep with multiple children supported."); + STORM_LOG_ASSERT(storm::utility::isOne(probability) || children.size() == 2, "PDep with multiple children supported."); DFTDependencyPointer element = std::make_shared<storm::storage::DFTDependency<ValueType>>(mNextId++, nameDep, probability); mElements[element->name()] = element; mDependencyChildNames[element] = {trigger, children[i]}; @@ -146,8 +144,8 @@ namespace storm { bool addVotElement(std::string const& name, unsigned threshold, std::vector<std::string> const& children) { STORM_LOG_ASSERT(children.size() > 0, "Has no child."); - if(mElements.count(name) != 0) { - STORM_LOG_ERROR("Element with name: " << name << " already exists."); + if (nameInUse(name)) { + STORM_LOG_ERROR("Element with name '" << name << "' already exists."); return false; } // It is an and-gate @@ -174,19 +172,33 @@ namespace storm { //TODO Matthias: collect constraints for SMT solving //failureRate > 0 //0 <= dormancyFactor <= 1 - STORM_LOG_ASSERT(mElements.find(name) == mElements.end(), "Element '" << name << "' already exists."); + if (nameInUse(name)) { + STORM_LOG_ERROR("Element with name '" << name << "' already exists."); + return false; + } mElements[name] = std::make_shared<storm::storage::DFTBE<ValueType>>(mNextId++, name, failureRate, dormancyFactor, transient); return true; } void addLayoutInfo(std::string const& name, double x, double y) { - STORM_LOG_ASSERT(mElements.count(name) > 0, "Element '" << name << "' not found."); + if (!nameInUse(name)) { + STORM_LOG_ERROR("Element with name '" << name << "' not found."); + } mLayoutInfo[name] = storm::storage::DFTLayoutInfo(x, y); } bool setTopLevel(std::string const& tle) { mTopLevelIdentifier = tle; - return mElements.count(tle) > 0; + return nameInUse(tle); + } + + /** + * Check whether the name is already used. + * @param name Element name. + * @return True iff name is already in use. + */ + bool nameInUse(std::string const& name) { + return mElements.find(name) != mElements.end(); } std::string getUniqueName(std::string name); diff --git a/src/storm-dft/storage/dft/DftJsonExporter.cpp b/src/storm-dft/storage/dft/DftJsonExporter.cpp index 4fa2a8937..6dd3d2299 100644 --- a/src/storm-dft/storage/dft/DftJsonExporter.cpp +++ b/src/storm-dft/storage/dft/DftJsonExporter.cpp @@ -80,6 +80,8 @@ namespace storm { std::stringstream stream; stream << dependency->probability(); nodeData["probability"] = stream.str(); + } else { + nodeData["type"] = "fdep"; } } else if (element->isBasicElement()) { // Set BE specific data diff --git a/src/storm-pars-cli/storm-pars.cpp b/src/storm-pars-cli/storm-pars.cpp index 4c33bde22..626a27a3c 100644 --- a/src/storm-pars-cli/storm-pars.cpp +++ b/src/storm-pars-cli/storm-pars.cpp @@ -65,6 +65,16 @@ namespace storm { bool exact; }; + struct PreprocessResult { + PreprocessResult(std::shared_ptr<storm::models::ModelBase> const& model, bool changed) : changed(changed), model(model) { + // Intentionally left empty. + } + + bool changed; + std::shared_ptr<storm::models::ModelBase> model; + boost::optional<std::vector<std::shared_ptr<storm::logic::Formula const>>> formulas; + }; + template <typename ValueType> std::vector<storm::storage::ParameterRegion<ValueType>> parseRegions(std::shared_ptr<storm::models::ModelBase> const& model) { std::vector<storm::storage::ParameterRegion<ValueType>> result; @@ -146,64 +156,76 @@ namespace storm { } template <typename ValueType> - std::pair<std::shared_ptr<storm::models::ModelBase>, bool> preprocessSparseModel(std::shared_ptr<storm::models::sparse::Model<ValueType>> const& model, SymbolicInput const& input) { + PreprocessResult preprocessSparseModel(std::shared_ptr<storm::models::sparse::Model<ValueType>> const& model, SymbolicInput const& input) { auto generalSettings = storm::settings::getModule<storm::settings::modules::GeneralSettings>(); auto bisimulationSettings = storm::settings::getModule<storm::settings::modules::BisimulationSettings>(); auto parametricSettings = storm::settings::getModule<storm::settings::modules::ParametricSettings>(); - std::pair<std::shared_ptr<storm::models::ModelBase>, bool> result = std::make_pair(model, false); - - if (result.first->isOfType(storm::models::ModelType::MarkovAutomaton)) { - result.first = storm::cli::preprocessSparseMarkovAutomaton(result.first->template as<storm::models::sparse::MarkovAutomaton<ValueType>>()); - result.second = true; + PreprocessResult result(model, false); + + if (result.model->isOfType(storm::models::ModelType::MarkovAutomaton)) { + result.model = storm::cli::preprocessSparseMarkovAutomaton(result.model->template as<storm::models::sparse::MarkovAutomaton<ValueType>>()); + result.changed = true; } if (generalSettings.isBisimulationSet()) { - result.first = storm::cli::preprocessSparseModelBisimulation(result.first->template as<storm::models::sparse::Model<ValueType>>(), input, bisimulationSettings); - result.second = true; + result.model = storm::cli::preprocessSparseModelBisimulation(result.model->template as<storm::models::sparse::Model<ValueType>>(), 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::models::sparse::Model<ValueType>>()), 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::models::sparse::Model<ValueType>>()), 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 <storm::dd::DdType DdType, typename ValueType> - std::pair<std::shared_ptr<storm::models::ModelBase>, bool> preprocessDdModel(std::shared_ptr<storm::models::symbolic::Model<DdType, ValueType>> const& model, SymbolicInput const& input) { + PreprocessResult preprocessDdModel(std::shared_ptr<storm::models::symbolic::Model<DdType, ValueType>> const& model, SymbolicInput const& input) { + auto coreSettings = storm::settings::getModule<storm::settings::modules::CoreSettings>(); + auto generalSettings = storm::settings::getModule<storm::settings::modules::GeneralSettings>(); + auto bisimulationSettings = storm::settings::getModule<storm::settings::modules::BisimulationSettings>(); - std::pair<std::shared_ptr<storm::models::ModelBase>, bool> result = std::make_pair(model, false); + PreprocessResult result(model, false); - auto coreSettings = storm::settings::getModule<storm::settings::modules::CoreSettings>(); 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<ValueType>(result.first->as<storm::models::sparse::Model<ValueType>>(), input); - if (sparsePreprocessingResult.second) { - result.first = sparsePreprocessingResult.first; + PreprocessResult sparsePreprocessingResult = storm::pars::preprocessSparseModel<ValueType>(result.model->as<storm::models::sparse::Model<ValueType>>(), 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<storm::models::symbolic::Model<DdType, ValueType>>(), input, bisimulationSettings); + result.changed = true; } } return result; } template <storm::dd::DdType DdType, typename ValueType> - std::pair<std::shared_ptr<storm::models::ModelBase>, bool> preprocessModel(std::shared_ptr<storm::models::ModelBase> const& model, SymbolicInput const& input) { + PreprocessResult preprocessModel(std::shared_ptr<storm::models::ModelBase> const& model, SymbolicInput const& input) { storm::utility::Stopwatch preprocessingWatch(true); - std::pair<std::shared_ptr<storm::models::ModelBase>, bool> result = std::make_pair(model, false); + PreprocessResult result(model, false); if (model->isSparseModel()) { - result = storm::pars::preprocessSparseModel<ValueType>(result.first->as<storm::models::sparse::Model<ValueType>>(), input); + result = storm::pars::preprocessSparseModel<ValueType>(result.model->as<storm::models::sparse::Model<ValueType>>(), input); } else { STORM_LOG_ASSERT(model->isSymbolicModel(), "Unexpected model type."); - result = storm::pars::preprocessDdModel<DdType, ValueType>(result.first->as<storm::models::symbolic::Model<DdType, ValueType>>(), input); + result = storm::pars::preprocessDdModel<DdType, ValueType>(result.model->as<storm::models::symbolic::Model<DdType, ValueType>>(), input); } - if (result.second) { + if (result.changed) { STORM_PRINT_AND_LOG(std::endl << "Time for model preprocessing: " << preprocessingWatch << "." << std::endl << std::endl); } return result; @@ -481,10 +503,46 @@ namespace storm { } } + template <storm::dd::DdType DdType, typename ValueType> + void verifyPropertiesWithSymbolicEngine(std::shared_ptr<storm::models::symbolic::Model<DdType, ValueType>> const& model, SymbolicInput const& input, SampleInformation<ValueType> const& samples) { + if (samples.empty()) { + verifyProperties<ValueType>(input.properties, + [&model] (std::shared_ptr<storm::logic::Formula const> const& formula) { + std::unique_ptr<storm::modelchecker::CheckResult> result = storm::api::verifyWithDdEngine<DdType, ValueType>(model, storm::api::createTask<ValueType>(formula, true)); + if (result) { + result->filter(storm::modelchecker::SymbolicQualitativeCheckResult<DdType>(model->getReachableStates(), model->getInitialStates())); + } + return result; + }, + [&model] (std::unique_ptr<storm::modelchecker::CheckResult> const& result) { + auto parametricSettings = storm::settings::getModule<storm::settings::modules::ParametricSettings>(); + if (parametricSettings.exportResultToFile() && model->isOfType(storm::models::ModelType::Dtmc)) { + //auto dtmc = model->template as<storm::models::symbolic::Dtmc<DdType, ValueType>>(); + //boost::optional<ValueType> rationalFunction = result->asSymbolicQuantitativeCheckResult<DdType, ValueType>().sum(); + //storm::api::exportParametricResultToFile(rationalFunction, storm::analysis::ConstraintCollector<ValueType>(*dtmc), parametricSettings.exportResultPath()); + } + }); + } else { + STORM_LOG_THROW(false, storm::exceptions::NotSupportedException, "Sampling is not supported in the symbolic engine."); + } + } + + template <storm::dd::DdType DdType, typename ValueType> + void verifyWithDdEngine(std::shared_ptr<storm::models::symbolic::Model<DdType, ValueType>> const& model, SymbolicInput const& input, std::vector<storm::storage::ParameterRegion<ValueType>> const& regions, SampleInformation<ValueType> 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 <storm::dd::DdType DdType, typename ValueType> void verifyParametricModel(std::shared_ptr<storm::models::ModelBase> const& model, SymbolicInput const& input, std::vector<storm::storage::ParameterRegion<ValueType>> const& regions, SampleInformation<ValueType> const& samples) { - STORM_LOG_ASSERT(model->isSparseModel(), "Unexpected model type."); - storm::pars::verifyWithSparseEngine<ValueType>(model->as<storm::models::sparse::Model<ValueType>>(), input, regions, samples); + if (model->isSparseModel()) { + storm::pars::verifyWithSparseEngine<ValueType>(model->as<storm::models::sparse::Model<ValueType>>(), input, regions, samples); + } else { + storm::pars::verifyWithDdEngine<DdType, ValueType>(model->as<storm::models::symbolic::Model<DdType, ValueType>>(), input, regions, samples); + } } @@ -556,8 +614,20 @@ namespace storm { if (model) { auto preprocessingResult = storm::pars::preprocessModel<DdType, ValueType>(model, input); - if (preprocessingResult.second) { - model = preprocessingResult.first; + if (preprocessingResult.changed) { + model = preprocessingResult.model; + + if (preprocessingResult.formulas) { + std::vector<storm::jani::Property> 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 b6e6d9d55..282c52649 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<std::shared_ptr<storm::logic::Formula const>> 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."); } @@ -151,7 +151,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<std::shared_ptr<storm::logic::Formula const>> 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<storm::storage::sparse::ModelComponents<ValueType, RewardModelType>>(); 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<ValueType> builder = storm::storage::SparseMatrixBuilder<ValueType>(0, 0, 0, false, nonDeterministic, 0); modelComponents->stateLabeling = storm::models::sparse::StateLabeling(stateSize); modelComponents->observabilityClasses = std::vector<uint32_t>(); modelComponents->observabilityClasses->resize(stateSize); std::vector<std::vector<ValueType>> stateRewards; - if (continousTime) { + if (continuousTime) { modelComponents->exitRates = std::vector<ValueType>(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 663bf2b52..c11fccb0b 100644 --- a/src/storm/analysis/GraphConditions.cpp +++ b/src/storm/analysis/GraphConditions.cpp @@ -38,9 +38,10 @@ namespace storm { auto const& transitionVars = entry.gatherVariables(); variableSet.insert(transitionVars.begin(), transitionVars.end()); if (entry.denominator().isConstant()) { - if (entry.denominatorAsNumber() > 0) { + assert(entry.denominator().constantPart() != 0); + if (entry.denominator().constantPart() > 0) { wellformedConstraintSet.emplace(entry.nominator().polynomialWithCoefficient(), storm::CompareRelation::GEQ); - } else if (entry.denominatorAsNumber() < 0) { + } else if (entry.denominator().constantPart() < 0) { wellformedConstraintSet.emplace(entry.nominator().polynomialWithCoefficient(), storm::CompareRelation::LEQ); } else { assert(false); // Should fail before. @@ -117,9 +118,10 @@ namespace storm { for (auto const& entry : rewModelEntry.second.getTransitionRewardMatrix()) { if(!entry.getValue().isConstant()) { if (entry.getValue().denominator().isConstant()) { - if (entry.getValue().denominatorAsNumber() > 0) { + assert(entry.getValue().denominator().constantPart() != 0); + if (entry.getValue().denominator().constantPart() > 0) { wellformedConstraintSet.emplace(entry.getValue().nominator().polynomialWithCoefficient(), storm::CompareRelation::GEQ); - } else if (entry.getValue().denominatorAsNumber() < 0) { + } else if (entry.getValue().denominator().constantPart() < 0) { wellformedConstraintSet.emplace(entry.getValue().nominator().polynomialWithCoefficient(), storm::CompareRelation::LEQ); } else { assert(false); // Should fail before. 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 <typename ValueType> - std::shared_ptr<storm::models::sparse::Model<ValueType>> transformContinuousToDiscreteTimeSparseModel(std::shared_ptr<storm::models::sparse::Model<ValueType>> const& model, std::vector<std::shared_ptr<storm::logic::Formula const>> const& formulas) { + std::pair<std::shared_ptr<storm::models::sparse::Model<ValueType>>, std::vector<std::shared_ptr<storm::logic::Formula const>>> transformContinuousToDiscreteTimeSparseModel(std::shared_ptr<storm::models::sparse::Model<ValueType>> const& model, std::vector<std::shared_ptr<storm::logic::Formula const>> const& formulas) { storm::transformer::ContinuousToDiscreteTimeModelTransformer<ValueType> 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<storm::models::sparse::Ctmc<ValueType>>()); + return std::make_pair(transformer.transform(*model->template as<storm::models::sparse::Ctmc<ValueType>>(), timeRewardName), newFormulas); } else if (model->isOfType(storm::models::ModelType::MarkovAutomaton)) { - return transformer.transform(*model->template as<storm::models::sparse::MarkovAutomaton<ValueType>>()); + return std::make_pair(transformer.transform(*model->template as<storm::models::sparse::MarkovAutomaton<ValueType>>(), 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 <typename ValueType> - std::shared_ptr<storm::models::sparse::Model<ValueType>> transformContinuousToDiscreteTimeSparseModel(storm::models::sparse::Model<ValueType>&& model, std::vector<std::shared_ptr<storm::logic::Formula const>> const& formulas) { + std::pair<std::shared_ptr<storm::models::sparse::Model<ValueType>>, std::vector<std::shared_ptr<storm::logic::Formula const>>> transformContinuousToDiscreteTimeSparseModel(storm::models::sparse::Model<ValueType>&& model, std::vector<std::shared_ptr<storm::logic::Formula const>> const& formulas) { storm::transformer::ContinuousToDiscreteTimeModelTransformer<ValueType> 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<storm::models::sparse::Ctmc<ValueType>>())); + return std::make_pair(transformer.transform(std::move(*model.template as<storm::models::sparse::Ctmc<ValueType>>()), timeRewardName), newFormulas); } else if (model.isOfType(storm::models::ModelType::MarkovAutomaton)) { - return transformer.transform(std::move(*model.template as<storm::models::sparse::MarkovAutomaton<ValueType>>())); + return std::make_pair(transformer.transform(std::move(*model.template as<storm::models::sparse::MarkovAutomaton<ValueType>>()), 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<Formula> ExpectedTimeToExpectedRewardVisitor::substitute(Formula const& f) const { + boost::any result = f.accept(*this, boost::any()); + return boost::any_cast<std::shared_ptr<Formula>>(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<Formula> subsubformula = boost::any_cast<std::shared_ptr<Formula>>(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<Formula> subformula = std::make_shared<EventuallyFormula>(subsubformula, storm::logic::FormulaContext::Reward); + return std::static_pointer_cast<Formula>(std::make_shared<RewardOperatorFormula>(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 <map> + +#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<Formula> 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<ValueType, storm::RationalNumber>::value) { STORM_LOG_ASSERT(quotientTransitionMatrix.greater(storm::utility::one<ValueType>()).isZero(), "Illegal entries in quotient matrix."); + } else if (std::is_same<ValueType, storm::RationalFunction>::value) { + // No comparison for rational functions } else { STORM_LOG_ASSERT(quotientTransitionMatrix.greater(storm::utility::one<ValueType>() + storm::utility::convertNumber<ValueType>(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 <typename ValueType, typename RewardModelType> + std::vector<std::shared_ptr<storm::logic::Formula const>> ContinuousToDiscreteTimeModelTransformer<ValueType, RewardModelType>::checkAndTransformFormulas(std::vector<std::shared_ptr<storm::logic::Formula const>> const& formulas, std::string const& timeRewardName) { + std::vector<std::shared_ptr<storm::logic::Formula const>> 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 <typename ValueType, typename RewardModelType> std::shared_ptr<storm::models::sparse::Mdp<ValueType, RewardModelType>> ContinuousToDiscreteTimeModelTransformer<ValueType, RewardModelType>::transform(storm::models::sparse::MarkovAutomaton<ValueType, RewardModelType> const& ma, boost::optional<std::string> 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<std::shared_ptr<storm::logic::Formula const>> checkAndTransformFormulas(std::vector<std::shared_ptr<storm::logic::Formula const>> 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<storm::models::sparse::Dtmc<ValueType, RewardModelType>> transform(storm::models::sparse::Ctmc<ValueType, RewardModelType> const& ctmc, boost::optional<std::string> const& timeRewardModelName = boost::none);