From 8482063a1615b1b4b18d9586f86ff6d33fb5ffc2 Mon Sep 17 00:00:00 2001 From: dehnert Date: Sun, 11 Feb 2018 19:11:18 +0100 Subject: [PATCH] made symbolic bisimulation work with MA and support of sparse quotient extraction for MA --- src/storm/builder/DdJaniModelBuilder.cpp | 16 ++++++++-------- src/storm/models/symbolic/MarkovAutomaton.cpp | 6 +++--- .../dd/bisimulation/QuotientExtractor.cpp | 11 ++++++++++- 3 files changed, 21 insertions(+), 12 deletions(-) diff --git a/src/storm/builder/DdJaniModelBuilder.cpp b/src/storm/builder/DdJaniModelBuilder.cpp index bee50923a..a6620492e 100644 --- a/src/storm/builder/DdJaniModelBuilder.cpp +++ b/src/storm/builder/DdJaniModelBuilder.cpp @@ -229,8 +229,8 @@ namespace storm { std::vector localNondeterminismVariables; // The meta variable used to distinguish Markovian from probabilistic choices in Markov automata. - storm::expressions::Variable markovNondeterminismVariable; - storm::dd::Bdd markovMarker; + storm::expressions::Variable probabilisticNondeterminismVariable; + storm::dd::Bdd probabilisticMarker; // The meta variables used to encode the actions and nondeterminism. std::set allNondeterminismVariables; @@ -322,9 +322,9 @@ namespace storm { } if (this->model.getModelType() == storm::jani::ModelType::MA) { - result.markovNondeterminismVariable = result.manager->addMetaVariable("markov").first; - result.markovMarker = result.manager->getEncoding(result.markovNondeterminismVariable, 1); - result.allNondeterminismVariables.insert(result.markovNondeterminismVariable); + result.probabilisticNondeterminismVariable = result.manager->addMetaVariable("prob").first; + result.probabilisticMarker = result.manager->getEncoding(result.probabilisticNondeterminismVariable, 1); + result.allNondeterminismVariables.insert(result.probabilisticNondeterminismVariable); } for (auto const& automatonName : this->automata) { @@ -573,9 +573,9 @@ namespace storm { if (markovian) { if (markovian.get()) { - encoding *= variables.markovMarker.template toAdd(); + encoding *= (!variables.probabilisticMarker).template toAdd(); } else { - encoding *= (!variables.markovMarker).template toAdd(); + encoding *= variables.probabilisticMarker.template toAdd(); } } @@ -1712,7 +1712,7 @@ namespace storm { } else if (modelType == storm::jani::ModelType::MDP || modelType == storm::jani::ModelType::LTS) { result = std::make_shared>(variables.manager, modelComponents.reachableStates, modelComponents.initialStates, modelComponents.deadlockStates, modelComponents.transitionMatrix, variables.rowMetaVariables, variables.rowExpressionAdapter, variables.columnMetaVariables, variables.rowColumnMetaVariablePairs, variables.allNondeterminismVariables, modelComponents.labelToExpressionMap, modelComponents.rewardModels); } else if (modelType == storm::jani::ModelType::MA) { - result = std::make_shared>(variables.manager, variables.markovMarker, modelComponents.reachableStates, modelComponents.initialStates, modelComponents.deadlockStates, modelComponents.transitionMatrix, variables.rowMetaVariables, variables.rowExpressionAdapter, variables.columnMetaVariables, variables.rowColumnMetaVariablePairs, variables.allNondeterminismVariables, modelComponents.labelToExpressionMap, modelComponents.rewardModels); + result = std::make_shared>(variables.manager, !variables.probabilisticMarker, modelComponents.reachableStates, modelComponents.initialStates, modelComponents.deadlockStates, modelComponents.transitionMatrix, variables.rowMetaVariables, variables.rowExpressionAdapter, variables.columnMetaVariables, variables.rowColumnMetaVariablePairs, variables.allNondeterminismVariables, modelComponents.labelToExpressionMap, modelComponents.rewardModels); } else { STORM_LOG_THROW(false, storm::exceptions::WrongFormatException, "Model type '" << modelType << "' not supported."); } diff --git a/src/storm/models/symbolic/MarkovAutomaton.cpp b/src/storm/models/symbolic/MarkovAutomaton.cpp index 976c11743..09b2fe7b3 100644 --- a/src/storm/models/symbolic/MarkovAutomaton.cpp +++ b/src/storm/models/symbolic/MarkovAutomaton.cpp @@ -56,13 +56,13 @@ namespace storm { // Compute the Markovian choices. this->markovianChoices = this->getQualitativeTransitionMatrix() && this->markovianMarker; - // Compute the Markovian states. - this->markovianStates = markovianChoices.existsAbstract(this->getNondeterminismVariables()); - // Compute the probabilistic states. std::set columnAndNondeterminsmVariables; std::set_union(this->getColumnVariables().begin(), this->getColumnVariables().end(), this->getNondeterminismVariables().begin(), this->getNondeterminismVariables().end(), std::inserter(columnAndNondeterminsmVariables, columnAndNondeterminsmVariables.begin())); this->probabilisticStates = (this->getQualitativeTransitionMatrix() && !markovianMarker).existsAbstract(columnAndNondeterminsmVariables); + + // Compute the Markovian states. + this->markovianStates = markovianChoices.existsAbstract(columnAndNondeterminsmVariables); // Compute the vector of exit rates. this->exitRateVector = (this->getTransitionMatrix() * this->markovianMarker.template toAdd()).sumAbstract(columnAndNondeterminsmVariables); diff --git a/src/storm/storage/dd/bisimulation/QuotientExtractor.cpp b/src/storm/storage/dd/bisimulation/QuotientExtractor.cpp index 6645edeae..340b191fe 100644 --- a/src/storm/storage/dd/bisimulation/QuotientExtractor.cpp +++ b/src/storm/storage/dd/bisimulation/QuotientExtractor.cpp @@ -13,6 +13,7 @@ #include "storm/models/sparse/Dtmc.h" #include "storm/models/sparse/Ctmc.h" #include "storm/models/sparse/Mdp.h" +#include "storm/models/sparse/MarkovAutomaton.h" #include "storm/models/sparse/StandardRewardModel.h" #include "storm/storage/dd/bisimulation/PreservationInformation.h" @@ -306,7 +307,7 @@ namespace storm { rowPermutation = std::vector(matrixEntries.size()); std::iota(rowPermutation.begin(), rowPermutation.end(), 0ull); if (this->isNondeterministic) { - std::sort(rowPermutation.begin(), rowPermutation.end(), [this] (uint64_t first, uint64_t second) { return this->rowToState[first] < this->rowToState[second]; } ); + std::stable_sort(rowPermutation.begin(), rowPermutation.end(), [this] (uint64_t first, uint64_t second) { return this->rowToState[first] < this->rowToState[second]; } ); } uint64_t rowCounter = 0; @@ -905,6 +906,14 @@ namespace storm { result = std::make_shared>(std::move(quotientTransitionMatrix), std::move(quotientStateLabeling), std::move(quotientRewardModels)); } else if (model.getType() == storm::models::ModelType::Mdp) { result = std::make_shared>(std::move(quotientTransitionMatrix), std::move(quotientStateLabeling), std::move(quotientRewardModels)); + } else if (model.getType() == storm::models::ModelType::MarkovAutomaton) { + storm::models::symbolic::MarkovAutomaton const& markovAutomaton = *model.template as>(); + + boost::optional markovianStates = sparseExtractor.extractSetExists(markovAutomaton.getMarkovianStates()); + storm::storage::sparse::ModelComponents modelComponents(std::move(quotientTransitionMatrix), std::move(quotientStateLabeling), std::move(quotientRewardModels), false, std::move(markovianStates)); + modelComponents.exitRates = sparseExtractor.extractStateVector(markovAutomaton.getExitRateVector()); + + result = std::make_shared>(std::move(modelComponents)); } return result;