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

Small bugfix for bisimulation decomposition. 

Former-commit-id: eae1447df4
tempestpy_adaptions
dehnert 10 years ago
parent
72c178dd08
commit
f3048d31c2
2 changed files with 22 additions and 18 deletions
Whitespace
Show all changes Ignore whitespace when comparing lines Ignore changes in amount of whitespace Ignore changes in whitespace at EOL
Unified View
Diff Options
Show Stats Download Patch File Download Diff File
  1. 32
      src/storage/DeterministicModelBisimulationDecomposition.cpp
  2. 8
      src/storage/DeterministicModelBisimulationDecomposition.h

32
src/storage/DeterministicModelBisimulationDecomposition.cpp
View File

@ -579,16 +579,18 @@ namespace storm {
DeterministicModelBisimulationDecomposition<ValueType>::DeterministicModelBisimulationDecomposition(storm::models::Dtmc<ValueType> const& model, bool weak, bool buildQuotient) : comparator() { DeterministicModelBisimulationDecomposition<ValueType>::DeterministicModelBisimulationDecomposition(storm::models::Dtmc<ValueType> const& model, bool weak, bool buildQuotient) : comparator() {
STORM_LOG_THROW(!model.hasStateRewards() && !model.hasTransitionRewards(), storm::exceptions::IllegalFunctionCallException, "Bisimulation is currently only supported for models without reward structures."); STORM_LOG_THROW(!model.hasStateRewards() && !model.hasTransitionRewards(), storm::exceptions::IllegalFunctionCallException, "Bisimulation is currently only supported for models without reward structures.");
storm::storage::SparseMatrix<ValueType> backwardTransitions = model.getBackwardTransitions(); storm::storage::SparseMatrix<ValueType> backwardTransitions = model.getBackwardTransitions();
Partition initialPartition = getLabelBasedInitialPartition(model, backwardTransitions, weak);
partitionRefinement(model, backwardTransitions, initialPartition, weak ? BisimulationType::WeakDtmc : BisimulationType::Strong, buildQuotient);
BisimulationType bisimulationType = weak ? BisimulationType::WeakDtmc : BisimulationType::Strong;
Partition initialPartition = getLabelBasedInitialPartition(model, backwardTransitions, bisimulationType);
partitionRefinement(model, backwardTransitions, initialPartition, bisimulationType, buildQuotient);
} }
template<typename ValueType> template<typename ValueType>
DeterministicModelBisimulationDecomposition<ValueType>::DeterministicModelBisimulationDecomposition(storm::models::Ctmc<ValueType> const& model, bool weak, bool buildQuotient) { DeterministicModelBisimulationDecomposition<ValueType>::DeterministicModelBisimulationDecomposition(storm::models::Ctmc<ValueType> const& model, bool weak, bool buildQuotient) {
STORM_LOG_THROW(!model.hasStateRewards() && !model.hasTransitionRewards(), storm::exceptions::IllegalFunctionCallException, "Bisimulation is currently only supported for models without reward structures."); STORM_LOG_THROW(!model.hasStateRewards() && !model.hasTransitionRewards(), storm::exceptions::IllegalFunctionCallException, "Bisimulation is currently only supported for models without reward structures.");
storm::storage::SparseMatrix<ValueType> backwardTransitions = model.getBackwardTransitions(); storm::storage::SparseMatrix<ValueType> backwardTransitions = model.getBackwardTransitions();
Partition initialPartition = getLabelBasedInitialPartition(model, backwardTransitions, weak);
partitionRefinement(model, backwardTransitions, initialPartition, weak ? BisimulationType::WeakCtmc : BisimulationType::Strong, buildQuotient);
BisimulationType bisimulationType = weak ? BisimulationType::WeakCtmc : BisimulationType::Strong;
Partition initialPartition = getLabelBasedInitialPartition(model, backwardTransitions, bisimulationType);
partitionRefinement(model, backwardTransitions, initialPartition, bisimulationType, buildQuotient);
} }
template<typename ValueType> template<typename ValueType>
@ -596,8 +598,9 @@ namespace storm {
STORM_LOG_THROW(!model.hasStateRewards() && !model.hasTransitionRewards(), storm::exceptions::IllegalFunctionCallException, "Bisimulation is currently only supported for models without reward structures."); STORM_LOG_THROW(!model.hasStateRewards() && !model.hasTransitionRewards(), storm::exceptions::IllegalFunctionCallException, "Bisimulation is currently only supported for models without reward structures.");
STORM_LOG_THROW(!weak || !bounded, storm::exceptions::IllegalFunctionCallException, "Weak bisimulation does not preserve bounded properties."); STORM_LOG_THROW(!weak || !bounded, storm::exceptions::IllegalFunctionCallException, "Weak bisimulation does not preserve bounded properties.");
storm::storage::SparseMatrix<ValueType> backwardTransitions = model.getBackwardTransitions(); storm::storage::SparseMatrix<ValueType> backwardTransitions = model.getBackwardTransitions();
Partition initialPartition = getMeasureDrivenInitialPartition(model, backwardTransitions, phiLabel, psiLabel, weak, bounded);
partitionRefinement(model, model.getBackwardTransitions(), initialPartition, weak ? BisimulationType::WeakDtmc : BisimulationType::Strong, buildQuotient);
BisimulationType bisimulationType = weak ? BisimulationType::WeakDtmc : BisimulationType::Strong;
Partition initialPartition = getMeasureDrivenInitialPartition(model, backwardTransitions, phiLabel, psiLabel, bisimulationType, bounded);
partitionRefinement(model, model.getBackwardTransitions(), initialPartition, bisimulationType, buildQuotient);
} }
template<typename ValueType> template<typename ValueType>
@ -605,8 +608,9 @@ namespace storm {
STORM_LOG_THROW(!model.hasStateRewards() && !model.hasTransitionRewards(), storm::exceptions::IllegalFunctionCallException, "Bisimulation is currently only supported for models without reward structures."); STORM_LOG_THROW(!model.hasStateRewards() && !model.hasTransitionRewards(), storm::exceptions::IllegalFunctionCallException, "Bisimulation is currently only supported for models without reward structures.");
STORM_LOG_THROW(!weak || !bounded, storm::exceptions::IllegalFunctionCallException, "Weak bisimulation does not preserve bounded properties."); STORM_LOG_THROW(!weak || !bounded, storm::exceptions::IllegalFunctionCallException, "Weak bisimulation does not preserve bounded properties.");
storm::storage::SparseMatrix<ValueType> backwardTransitions = model.getBackwardTransitions(); storm::storage::SparseMatrix<ValueType> backwardTransitions = model.getBackwardTransitions();
Partition initialPartition = getMeasureDrivenInitialPartition(model, backwardTransitions, phiLabel, psiLabel, weak, bounded);
partitionRefinement(model, model.getBackwardTransitions(), initialPartition, weak ? BisimulationType::WeakCtmc : BisimulationType::Strong, buildQuotient);
BisimulationType bisimulationType = weak ? BisimulationType::WeakCtmc : BisimulationType::Strong;
Partition initialPartition = getMeasureDrivenInitialPartition(model, backwardTransitions, phiLabel, psiLabel, bisimulationType, bounded);
partitionRefinement(model, model.getBackwardTransitions(), initialPartition, bisimulationType, buildQuotient);
} }
template<typename ValueType> template<typename ValueType>
@ -1177,13 +1181,13 @@ namespace storm {
template<typename ValueType> template<typename ValueType>
template<typename ModelType> template<typename ModelType>
typename DeterministicModelBisimulationDecomposition<ValueType>::Partition DeterministicModelBisimulationDecomposition<ValueType>::getMeasureDrivenInitialPartition(ModelType const& model, storm::storage::SparseMatrix<ValueType> const& backwardTransitions, std::string const& phiLabel, std::string const& psiLabel, bool weak, bool bounded) {
typename DeterministicModelBisimulationDecomposition<ValueType>::Partition DeterministicModelBisimulationDecomposition<ValueType>::getMeasureDrivenInitialPartition(ModelType const& model, storm::storage::SparseMatrix<ValueType> const& backwardTransitions, std::string const& phiLabel, std::string const& psiLabel, BisimulationType bisimulationType, bool bounded) {
std::pair<storm::storage::BitVector, storm::storage::BitVector> statesWithProbability01 = storm::utility::graph::performProb01(backwardTransitions, phiLabel == "true" ? storm::storage::BitVector(model.getNumberOfStates(), true) : model.getLabeledStates(phiLabel), model.getLabeledStates(psiLabel)); std::pair<storm::storage::BitVector, storm::storage::BitVector> statesWithProbability01 = storm::utility::graph::performProb01(backwardTransitions, phiLabel == "true" ? storm::storage::BitVector(model.getNumberOfStates(), true) : model.getLabeledStates(phiLabel), model.getLabeledStates(psiLabel));
Partition partition(model.getNumberOfStates(), statesWithProbability01.first, bounded ? model.getLabeledStates(psiLabel) : statesWithProbability01.second, phiLabel, psiLabel);
Partition partition(model.getNumberOfStates(), statesWithProbability01.first, bounded ? model.getLabeledStates(psiLabel) : statesWithProbability01.second, phiLabel, psiLabel, bisimulationType == BisimulationType::WeakDtmc);
// If we are creating the initial partition for weak bisimulation, we need to (a) split off all divergent // If we are creating the initial partition for weak bisimulation, we need to (a) split off all divergent
// states of each initial block and (b) initialize the vector of silent probabilities held by the partition. // states of each initial block and (b) initialize the vector of silent probabilities held by the partition.
if (weak) {
if (bisimulationType == BisimulationType::WeakDtmc) {
this->splitOffDivergentStates(model, backwardTransitions, partition); this->splitOffDivergentStates(model, backwardTransitions, partition);
this->initializeSilentProbabilities(model, partition); this->initializeSilentProbabilities(model, partition);
} }
@ -1261,8 +1265,8 @@ namespace storm {
template<typename ValueType> template<typename ValueType>
template<typename ModelType> template<typename ModelType>
typename DeterministicModelBisimulationDecomposition<ValueType>::Partition DeterministicModelBisimulationDecomposition<ValueType>::getLabelBasedInitialPartition(ModelType const& model, storm::storage::SparseMatrix<ValueType> const& backwardTransitions, bool weak) {
Partition partition(model.getNumberOfStates(), weak);
typename DeterministicModelBisimulationDecomposition<ValueType>::Partition DeterministicModelBisimulationDecomposition<ValueType>::getLabelBasedInitialPartition(ModelType const& model, storm::storage::SparseMatrix<ValueType> const& backwardTransitions, BisimulationType bisimulationType) {
Partition partition(model.getNumberOfStates(), bisimulationType == BisimulationType::WeakDtmc);
for (auto const& label : model.getStateLabeling().getAtomicPropositions()) { for (auto const& label : model.getStateLabeling().getAtomicPropositions()) {
if (label == "init") { if (label == "init") {
continue; continue;
@ -1272,7 +1276,7 @@ namespace storm {
// If we are creating the initial partition for weak bisimulation, we need to (a) split off all divergent // If we are creating the initial partition for weak bisimulation, we need to (a) split off all divergent
// states of each initial block and (b) initialize the vector of silent probabilities held by the partition. // states of each initial block and (b) initialize the vector of silent probabilities held by the partition.
if (weak) {
if (bisimulationType == BisimulationType::WeakDtmc) {
this->splitOffDivergentStates(model, backwardTransitions, partition); this->splitOffDivergentStates(model, backwardTransitions, partition);
this->initializeSilentProbabilities(model, partition); this->initializeSilentProbabilities(model, partition);
} }

8
src/storage/DeterministicModelBisimulationDecomposition.h
View File

@ -460,24 +460,24 @@ namespace storm {
* @param backwardTransitions The backward transitions of the model. * @param backwardTransitions The backward transitions of the model.
* @param phiLabel The label that all phi states carry in the model. * @param phiLabel The label that all phi states carry in the model.
* @param psiLabel The label that all psi states carry in the model. * @param psiLabel The label that all psi states carry in the model.
* @param weak A flag indicating whether a weak bisimulation is to be computed.
* @param bisimulationType The kind of bisimulation that is to be computed.
* @param bounded If set to true, the initial partition will be chosen in such a way that preserves bounded * @param bounded If set to true, the initial partition will be chosen in such a way that preserves bounded
* reachability queries. * reachability queries.
* @return The resulting partition. * @return The resulting partition.
*/ */
template<typename ModelType> template<typename ModelType>
Partition getMeasureDrivenInitialPartition(ModelType const& model, storm::storage::SparseMatrix<ValueType> const& backwardTransitions, std::string const& phiLabel, std::string const& psiLabel, bool weak, bool bounded = false);
Partition getMeasureDrivenInitialPartition(ModelType const& model, storm::storage::SparseMatrix<ValueType> const& backwardTransitions, std::string const& phiLabel, std::string const& psiLabel, BisimulationType bisimulationType, bool bounded = false);
/*! /*!
* Creates the initial partition based on all the labels in the given model. * Creates the initial partition based on all the labels in the given model.
* *
* @param model The model whose state space is partitioned based on its labels. * @param model The model whose state space is partitioned based on its labels.
* @param backwardTransitions The backward transitions of the model. * @param backwardTransitions The backward transitions of the model.
* @param weak A flag indicating whether a weak bisimulation is to be computed.
* @param bisimulationType The kind of bisimulation that is to be computed.
* @return The resulting partition. * @return The resulting partition.
*/ */
template<typename ModelType> template<typename ModelType>
Partition getLabelBasedInitialPartition(ModelType const& model, storm::storage::SparseMatrix<ValueType> const& backwardTransitions, bool weak);
Partition getLabelBasedInitialPartition(ModelType const& model, storm::storage::SparseMatrix<ValueType> const& backwardTransitions, BisimulationType bisimulationType);
/*! /*!
* Splits all blocks of the given partition into a block that contains all divergent states and another block * Splits all blocks of the given partition into a block that contains all divergent states and another block

Write Preview
Loading…
Cancel
Save