sp
/
tempest
1
0
Fork 0
Code Issues Pull Requests Projects Releases Wiki Activity
Browse Source

made symbolic bisimulation work with MA and support of sparse quotient extraction for MA

main
dehnert 7 years ago
parent
9e5e1980dd
commit
8482063a16
3 changed files with 21 additions and 12 deletions
Whitespace
Show all changes Ignore whitespace when comparing lines Ignore changes in amount of whitespace Ignore changes in whitespace at EOL
Split View
Diff Options
Show Stats Download Patch File Download Diff File
  1. 16
      src/storm/builder/DdJaniModelBuilder.cpp
  2. 6
      src/storm/models/symbolic/MarkovAutomaton.cpp
  3. 11
      src/storm/storage/dd/bisimulation/QuotientExtractor.cpp

16
src/storm/builder/DdJaniModelBuilder.cpp
View File

@ -229,8 +229,8 @@ namespace storm {
std::vector<storm::expressions::Variable> localNondeterminismVariables;
// The meta variable used to distinguish Markovian from probabilistic choices in Markov automata.
storm::expressions::Variable markovNondeterminismVariable;
storm::dd::Bdd<Type> markovMarker;
storm::expressions::Variable probabilisticNondeterminismVariable;
storm::dd::Bdd<Type> probabilisticMarker;
// The meta variables used to encode the actions and nondeterminism.
std::set<storm::expressions::Variable> 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<ValueType>();
encoding *= (!variables.probabilisticMarker).template toAdd<ValueType>();
} else {
encoding *= (!variables.markovMarker).template toAdd<ValueType>();
encoding *= variables.probabilisticMarker.template toAdd<ValueType>();
}
}
@ -1712,7 +1712,7 @@ namespace storm {
} else if (modelType == storm::jani::ModelType::MDP || modelType == storm::jani::ModelType::LTS) {
result = std::make_shared<storm::models::symbolic::Mdp<Type, ValueType>>(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<storm::models::symbolic::MarkovAutomaton<Type, ValueType>>(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<storm::models::symbolic::MarkovAutomaton<Type, ValueType>>(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.");
}

6
src/storm/models/symbolic/MarkovAutomaton.cpp
View File

@ -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<storm::expressions::Variable> 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<ValueType>()).sumAbstract(columnAndNondeterminsmVariables);

11
src/storm/storage/dd/bisimulation/QuotientExtractor.cpp
View File

@ -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<uint64_t>(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<storm::models::sparse::Ctmc<ValueType>>(std::move(quotientTransitionMatrix), std::move(quotientStateLabeling), std::move(quotientRewardModels));
} else if (model.getType() == storm::models::ModelType::Mdp) {
result = std::make_shared<storm::models::sparse::Mdp<ValueType>>(std::move(quotientTransitionMatrix), std::move(quotientStateLabeling), std::move(quotientRewardModels));
} else if (model.getType() == storm::models::ModelType::MarkovAutomaton) {
storm::models::symbolic::MarkovAutomaton<DdType, ValueType> const& markovAutomaton = *model.template as<storm::models::symbolic::MarkovAutomaton<DdType, ValueType>>();
boost::optional<storm::storage::BitVector> markovianStates = sparseExtractor.extractSetExists(markovAutomaton.getMarkovianStates());
storm::storage::sparse::ModelComponents<ValueType> modelComponents(std::move(quotientTransitionMatrix), std::move(quotientStateLabeling), std::move(quotientRewardModels), false, std::move(markovianStates));
modelComponents.exitRates = sparseExtractor.extractStateVector(markovAutomaton.getExitRateVector());
result = std::make_shared<storm::models::sparse::MarkovAutomaton<ValueType>>(std::move(modelComponents));
}
return result;

Write Preview
Loading…
Cancel
Save