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

refactored bisimulation a bit (mainly the entry point as well as hidden some options) 

Former-commit-id: 5405a14930
tempestpy_adaptions
sjunges 9 years ago
parent
3bdd87e7a7
commit
ad01dfa611
6 changed files with 121 additions and 59 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. 14
      src/storage/bisimulation/BisimulationDecomposition.cpp
  2. 84
      src/storage/bisimulation/BisimulationDecomposition.h
  3. 18
      src/storage/bisimulation/DeterministicModelBisimulationDecomposition.cpp
  4. 12
      src/storage/bisimulation/NondeterministicModelBisimulationDecomposition.cpp
  5. 46
      src/utility/storm.h
  6. 6
      test/functional/storage/DeterministicModelBisimulationDecompositionTest.cpp

14
src/storage/bisimulation/BisimulationDecomposition.cpp
View File

@ -44,7 +44,7 @@ namespace storm {
} }
template<typename ModelType, typename BlockDataType> template<typename ModelType, typename BlockDataType>
BisimulationDecomposition<ModelType, BlockDataType>::Options::Options() : measureDrivenInitialPartition(false), phiStates(), psiStates(), respectedAtomicPropositions(), keepRewards(false), type(BisimulationType::Strong), bounded(false), buildQuotient(true) {
BisimulationDecomposition<ModelType, BlockDataType>::Options::Options() : measureDrivenInitialPartition(false), phiStates(), psiStates(), respectedAtomicPropositions(), buildQuotient(true), keepRewards(false), type(BisimulationType::Strong), bounded(false) {
// Intentionally left empty. // Intentionally left empty.
} }
@ -163,9 +163,9 @@ namespace storm {
template<typename ModelType, typename BlockDataType> template<typename ModelType, typename BlockDataType>
BisimulationDecomposition<ModelType, BlockDataType>::BisimulationDecomposition(ModelType const& model, storm::storage::SparseMatrix<ValueType> const& backwardTransitions, Options const& options) : model(model), backwardTransitions(backwardTransitions), options(options), partition(), comparator(), quotient(nullptr) { BisimulationDecomposition<ModelType, BlockDataType>::BisimulationDecomposition(ModelType const& model, storm::storage::SparseMatrix<ValueType> const& backwardTransitions, Options const& options) : model(model), backwardTransitions(backwardTransitions), options(options), partition(), comparator(), quotient(nullptr) {
STORM_LOG_THROW(!options.keepRewards || !model.hasRewardModel() || model.hasUniqueRewardModel(), storm::exceptions::IllegalFunctionCallException, "Bisimulation currently only supports models with at most one reward model.");
STORM_LOG_THROW(!options.keepRewards || !model.hasRewardModel() || model.getUniqueRewardModel()->second.hasOnlyStateRewards(), storm::exceptions::IllegalFunctionCallException, "Bisimulation is currently supported for models with state rewards only. Consider converting the transition rewards to state rewards (via suitable function calls).");
STORM_LOG_THROW(options.type != BisimulationType::Weak || !options.bounded, storm::exceptions::IllegalFunctionCallException, "Weak bisimulation cannot preserve bounded properties.");
STORM_LOG_THROW(!options.getKeepRewards() || !model.hasRewardModel() || model.hasUniqueRewardModel(), storm::exceptions::IllegalFunctionCallException, "Bisimulation currently only supports models with at most one reward model.");
STORM_LOG_THROW(!options.getKeepRewards() || !model.hasRewardModel() || model.getUniqueRewardModel()->second.hasOnlyStateRewards(), storm::exceptions::IllegalFunctionCallException, "Bisimulation is currently supported for models with state rewards only. Consider converting the transition rewards to state rewards (via suitable function calls).");
STORM_LOG_THROW(options.getType() != BisimulationType::Weak || !options.getBounded(), storm::exceptions::IllegalFunctionCallException, "Weak bisimulation cannot preserve bounded properties.");
// Fix the respected atomic propositions if they were not explicitly given. // Fix the respected atomic propositions if they were not explicitly given.
if (!this->options.respectedAtomicPropositions) { if (!this->options.respectedAtomicPropositions) {
@ -270,7 +270,7 @@ namespace storm {
// If the model has state rewards, we need to consider them, because otherwise reward properties are not // If the model has state rewards, we need to consider them, because otherwise reward properties are not
// preserved. // preserved.
if (options.keepRewards && model.hasRewardModel()) {
if (options.getKeepRewards() && model.hasRewardModel()) {
this->splitInitialPartitionBasedOnStateRewards(); this->splitInitialPartitionBasedOnStateRewards();
} }
} }
@ -284,11 +284,11 @@ namespace storm {
representativePsiState = *options.psiStates.get().begin(); representativePsiState = *options.psiStates.get().begin();
} }
partition = storm::storage::bisimulation::Partition<BlockDataType>(model.getNumberOfStates(), statesWithProbability01.first, options.bounded || options.keepRewards ? options.psiStates.get() : statesWithProbability01.second, representativePsiState);
partition = storm::storage::bisimulation::Partition<BlockDataType>(model.getNumberOfStates(), statesWithProbability01.first, options.getBounded() || options.getKeepRewards() ? options.psiStates.get() : statesWithProbability01.second, representativePsiState);
// If the model has state rewards, we need to consider them, because otherwise reward properties are not // If the model has state rewards, we need to consider them, because otherwise reward properties are not
// preserved. // preserved.
if (options.keepRewards && model.hasRewardModel()) {
if (options.getKeepRewards() && model.hasRewardModel()) {
this->splitInitialPartitionBasedOnStateRewards(); this->splitInitialPartitionBasedOnStateRewards();
} }
} }

84
src/storage/bisimulation/BisimulationDecomposition.h
View File

@ -3,6 +3,8 @@
#include <deque> #include <deque>
#include "src/settings/SettingsManager.h"
#include "src/settings/modules/BisimulationSettings.h"
#include "src/storage/sparse/StateType.h" #include "src/storage/sparse/StateType.h"
#include "src/storage/Decomposition.h" #include "src/storage/Decomposition.h"
#include "src/storage/StateBlock.h" #include "src/storage/StateBlock.h"
@ -25,6 +27,23 @@ namespace storm {
namespace storage { namespace storage {
enum class BisimulationType { Strong, Weak }; enum class BisimulationType { Strong, Weak };
enum class BisimulationTypeChoice { Strong, Weak, FromSettings };
inline BisimulationType resolveBisimulationTypeChoice(BisimulationTypeChoice c) {
switch(c) {
case BisimulationTypeChoice::Strong:
return BisimulationType::Strong;
case BisimulationTypeChoice::Weak:
return BisimulationType::Weak;
case BisimulationTypeChoice::FromSettings:
if (storm::settings::bisimulationSettings().isWeakBisimulationSet()) {
return BisimulationType::Weak;
} else {
return BisimulationType::Strong;
}
}
}
/*! /*!
* This class is the superclass of all decompositions of a sparse model into its bisimulation quotient. * This class is the superclass of all decompositions of a sparse model into its bisimulation quotient.
@ -37,6 +56,8 @@ namespace storm {
// A class that offers the possibility to customize the bisimulation. // A class that offers the possibility to customize the bisimulation.
struct Options { struct Options {
// Creates an object representing the default values for all options. // Creates an object representing the default values for all options.
Options(); Options();
@ -68,33 +89,74 @@ namespace storm {
*/ */
void preserveFormula(ModelType const& model, storm::logic::Formula const& formula); void preserveFormula(ModelType const& model, storm::logic::Formula const& formula);
/**
* Sets the bisimulation type. If the bisimulation type is set to weak,
* we also change the bounded flag (as bounded properties are not preserved under
* weak bisimulation).
*/
void setType(BisimulationType t) {
if(t == BisimulationType::Weak) {
bounded = false;
}
type = t;
}
BisimulationType getType() const {
return this->type;
}
bool getBounded() const {
return this->bounded;
}
bool getKeepRewards() const {
return this->keepRewards;
}
bool isOptimizationDirectionSet() const {
return static_cast<bool>(optimalityType);
}
OptimizationDirection getOptimizationDirection() const {
assert(optimalityType);
return optimalityType.get();
}
// A flag that indicates whether a measure driven initial partition is to be used. If this flag is set // A flag that indicates whether a measure driven initial partition is to be used. If this flag is set
// to true, the two optional pairs phiStatesAndLabel and psiStatesAndLabel must be set. Then, the // to true, the two optional pairs phiStatesAndLabel and psiStatesAndLabel must be set. Then, the
// measure driven initial partition wrt. to the states phi and psi is taken. // measure driven initial partition wrt. to the states phi and psi is taken.
bool measureDrivenInitialPartition; bool measureDrivenInitialPartition;
boost::optional<storm::storage::BitVector> phiStates; boost::optional<storm::storage::BitVector> phiStates;
boost::optional<storm::storage::BitVector> psiStates; boost::optional<storm::storage::BitVector> psiStates;
boost::optional<OptimizationDirection> optimalityType;
// An optional set of strings that indicate which of the atomic propositions of the model are to be
// respected and which may be ignored. If not given, all atomic propositions of the model are respected.
/// An optional set of strings that indicate which of the atomic propositions of the model are to be
/// respected and which may be ignored. If not given, all atomic propositions of the model are respected.
boost::optional<std::set<std::string>> respectedAtomicPropositions; boost::optional<std::set<std::string>> respectedAtomicPropositions;
// A flag that indicates whether or not the state-rewards of the model are to be respected (and should
// be kept in the quotient model, if one is built).
/// A flag that governs whether the quotient model is actually built or only the decomposition is computed.
bool buildQuotient;
private:
boost::optional<OptimizationDirection> optimalityType;
/// A flag that indicates whether or not the state-rewards of the model are to be respected (and should
/// be kept in the quotient model, if one is built).
bool keepRewards; bool keepRewards;
// A flag that indicates whether a strong or a weak bisimulation is to be computed.
/// A flag that indicates whether a strong or a weak bisimulation is to be computed.
BisimulationType type; BisimulationType type;
// A flag that indicates whether step-bounded properties are to be preserved. This may only be set to tru
// when computing strong bisimulation equivalence.
/// A flag that indicates whether step-bounded properties are to be preserved. This may only be set to tru
/// when computing strong bisimulation equivalence.
bool bounded; bool bounded;
// A flag that governs whether the quotient model is actually built or only the decomposition is computed.
bool buildQuotient;
private:
/*! /*!
* Sets the options under the assumption that the given formula is the only one that is to be checked. * Sets the options under the assumption that the given formula is the only one that is to be checked.
* *

18
src/storage/bisimulation/DeterministicModelBisimulationDecomposition.cpp
View File

@ -122,7 +122,7 @@ namespace storm {
void DeterministicModelBisimulationDecomposition<ModelType>::initializeMeasureDrivenPartition() { void DeterministicModelBisimulationDecomposition<ModelType>::initializeMeasureDrivenPartition() {
BisimulationDecomposition<ModelType, BlockDataType>::initializeMeasureDrivenPartition(); BisimulationDecomposition<ModelType, BlockDataType>::initializeMeasureDrivenPartition();
if (this->options.type == BisimulationType::Weak && this->model.getType() == storm::models::ModelType::Dtmc) {
if (this->options.getType() == BisimulationType::Weak && this->model.getType() == storm::models::ModelType::Dtmc) {
this->initializeWeakDtmcBisimulation(); this->initializeWeakDtmcBisimulation();
} }
} }
@ -131,7 +131,7 @@ namespace storm {
void DeterministicModelBisimulationDecomposition<ModelType>::initializeLabelBasedPartition() { void DeterministicModelBisimulationDecomposition<ModelType>::initializeLabelBasedPartition() {
BisimulationDecomposition<ModelType, BlockDataType>::initializeLabelBasedPartition(); BisimulationDecomposition<ModelType, BlockDataType>::initializeLabelBasedPartition();
if (this->options.type == BisimulationType::Weak && this->model.getType() == storm::models::ModelType::Dtmc) {
if (this->options.getType() == BisimulationType::Weak && this->model.getType() == storm::models::ModelType::Dtmc) {
this->initializeWeakDtmcBisimulation(); this->initializeWeakDtmcBisimulation();
} }
} }
@ -494,7 +494,7 @@ namespace storm {
} }
// Finally, we split the block based on the precomputed probabilities and the chosen bisimulation type. // Finally, we split the block based on the precomputed probabilities and the chosen bisimulation type.
if (this->options.type == BisimulationType::Strong || this->model.getType() == storm::models::ModelType::Ctmc) {
if (this->options.getType() == BisimulationType::Strong || this->model.getType() == storm::models::ModelType::Ctmc) {
refinePredecessorBlocksOfSplitterStrong(predecessorBlocks, splitterQueue); refinePredecessorBlocksOfSplitterStrong(predecessorBlocks, splitterQueue);
} else { } else {
// If the splitter is a predecessor of we can use the computed probabilities to update the silent // If the splitter is a predecessor of we can use the computed probabilities to update the silent
@ -528,7 +528,7 @@ namespace storm {
// If the model had state rewards, we need to build the state rewards for the quotient as well. // If the model had state rewards, we need to build the state rewards for the quotient as well.
boost::optional<std::vector<ValueType>> stateRewards; boost::optional<std::vector<ValueType>> stateRewards;
if (this->options.keepRewards && this->model.hasRewardModel()) {
if (this->options.getKeepRewards() && this->model.hasRewardModel()) {
stateRewards = std::vector<ValueType>(this->blocks.size()); stateRewards = std::vector<ValueType>(this->blocks.size());
} }
@ -542,7 +542,7 @@ namespace storm {
// However, for weak bisimulation, we need to make sure the representative state is a non-silent one (if // However, for weak bisimulation, we need to make sure the representative state is a non-silent one (if
// there is any such state). // there is any such state).
if (this->options.type == BisimulationType::Weak) {
if (this->options.getType() == BisimulationType::Weak) {
for (auto const& state : block) { for (auto const& state : block) {
if (!isSilent(state)) { if (!isSilent(state)) {
representativeState = state; representativeState = state;
@ -576,7 +576,7 @@ namespace storm {
storm::storage::sparse::state_type targetBlock = this->partition.getBlock(entry.getColumn()).getId(); storm::storage::sparse::state_type targetBlock = this->partition.getBlock(entry.getColumn()).getId();
// If we are computing a weak bisimulation quotient, there is no need to add self-loops. // If we are computing a weak bisimulation quotient, there is no need to add self-loops.
if ((this->options.type == BisimulationType::Weak) && targetBlock == blockIndex) {
if ((this->options.getType() == BisimulationType::Weak) && targetBlock == blockIndex) {
continue; continue;
} }
@ -590,7 +590,7 @@ namespace storm {
// Now add them to the actual matrix. // Now add them to the actual matrix.
for (auto const& probabilityEntry : blockProbability) { for (auto const& probabilityEntry : blockProbability) {
if (this->options.type == BisimulationType::Weak && this->model.getType() == storm::models::ModelType::Dtmc) {
if (this->options.getType() == BisimulationType::Weak && this->model.getType() == storm::models::ModelType::Dtmc) {
builder.addNextValue(blockIndex, probabilityEntry.first, probabilityEntry.second / (storm::utility::one<ValueType>() - getSilentProbability(representativeState))); builder.addNextValue(blockIndex, probabilityEntry.first, probabilityEntry.second / (storm::utility::one<ValueType>() - getSilentProbability(representativeState)));
} else { } else {
builder.addNextValue(blockIndex, probabilityEntry.first, probabilityEntry.second); builder.addNextValue(blockIndex, probabilityEntry.first, probabilityEntry.second);
@ -608,7 +608,7 @@ namespace storm {
// If the model has state rewards, we simply copy the state reward of the representative state, because // If the model has state rewards, we simply copy the state reward of the representative state, because
// all states in a block are guaranteed to have the same state reward. // all states in a block are guaranteed to have the same state reward.
if (this->options.keepRewards && this->model.hasRewardModel()) {
if (this->options.getKeepRewards() && this->model.hasRewardModel()) {
typename std::unordered_map<std::string, typename ModelType::RewardModelType>::const_iterator nameRewardModelPair = this->model.getUniqueRewardModel(); typename std::unordered_map<std::string, typename ModelType::RewardModelType>::const_iterator nameRewardModelPair = this->model.getUniqueRewardModel();
stateRewards.get()[blockIndex] = nameRewardModelPair->second.getStateRewardVector()[representativeState]; stateRewards.get()[blockIndex] = nameRewardModelPair->second.getStateRewardVector()[representativeState];
} }
@ -622,7 +622,7 @@ namespace storm {
// Construct the reward model mapping. // Construct the reward model mapping.
std::unordered_map<std::string, typename ModelType::RewardModelType> rewardModels; std::unordered_map<std::string, typename ModelType::RewardModelType> rewardModels;
if (this->options.keepRewards && this->model.hasRewardModel()) {
if (this->options.getKeepRewards() && this->model.hasRewardModel()) {
typename std::unordered_map<std::string, typename ModelType::RewardModelType>::const_iterator nameRewardModelPair = this->model.getUniqueRewardModel(); typename std::unordered_map<std::string, typename ModelType::RewardModelType>::const_iterator nameRewardModelPair = this->model.getUniqueRewardModel();
rewardModels.insert(std::make_pair(nameRewardModelPair->first, typename ModelType::RewardModelType(stateRewards))); rewardModels.insert(std::make_pair(nameRewardModelPair->first, typename ModelType::RewardModelType(stateRewards)));
} }

12
src/storage/bisimulation/NondeterministicModelBisimulationDecomposition.cpp
View File

@ -17,13 +17,13 @@ namespace storm {
template<typename ModelType> template<typename ModelType>
NondeterministicModelBisimulationDecomposition<ModelType>::NondeterministicModelBisimulationDecomposition(ModelType const& model, typename BisimulationDecomposition<ModelType, NondeterministicModelBisimulationDecomposition::BlockDataType>::Options const& options) : BisimulationDecomposition<ModelType, NondeterministicModelBisimulationDecomposition::BlockDataType>(model, model.getTransitionMatrix().transpose(false), options), choiceToStateMapping(model.getNumberOfChoices()), quotientDistributions(model.getNumberOfChoices()), orderedQuotientDistributions(model.getNumberOfChoices()) { NondeterministicModelBisimulationDecomposition<ModelType>::NondeterministicModelBisimulationDecomposition(ModelType const& model, typename BisimulationDecomposition<ModelType, NondeterministicModelBisimulationDecomposition::BlockDataType>::Options const& options) : BisimulationDecomposition<ModelType, NondeterministicModelBisimulationDecomposition::BlockDataType>(model, model.getTransitionMatrix().transpose(false), options), choiceToStateMapping(model.getNumberOfChoices()), quotientDistributions(model.getNumberOfChoices()), orderedQuotientDistributions(model.getNumberOfChoices()) {
STORM_LOG_THROW(options.type == BisimulationType::Strong, storm::exceptions::IllegalFunctionCallException, "Weak bisimulation is currently not supported for nondeterministic models.");
STORM_LOG_THROW(options.getType() == BisimulationType::Strong, storm::exceptions::IllegalFunctionCallException, "Weak bisimulation is currently not supported for nondeterministic models.");
} }
template<typename ModelType> template<typename ModelType>
std::pair<storm::storage::BitVector, storm::storage::BitVector> NondeterministicModelBisimulationDecomposition<ModelType>::getStatesWithProbability01() { std::pair<storm::storage::BitVector, storm::storage::BitVector> NondeterministicModelBisimulationDecomposition<ModelType>::getStatesWithProbability01() {
STORM_LOG_THROW(static_cast<bool>(this->options.optimalityType), storm::exceptions::IllegalFunctionCallException, "Can only compute states with probability 0/1 with an optimization direction (min/max).");
if (this->options.optimalityType.get() == OptimizationDirection::Minimize) {
STORM_LOG_THROW(this->options.isOptimizationDirectionSet(), storm::exceptions::IllegalFunctionCallException, "Can only compute states with probability 0/1 with an optimization direction (min/max).");
if (this->options.getOptimizationDirection() == OptimizationDirection::Minimize) {
return storm::utility::graph::performProb01Min(this->model.getTransitionMatrix(), this->model.getTransitionMatrix().getRowGroupIndices(), this->model.getBackwardTransitions(), this->options.phiStates.get(), this->options.psiStates.get()); return storm::utility::graph::performProb01Min(this->model.getTransitionMatrix(), this->model.getTransitionMatrix().getRowGroupIndices(), this->model.getBackwardTransitions(), this->options.phiStates.get(), this->options.psiStates.get());
} else { } else {
return storm::utility::graph::performProb01Max(this->model.getTransitionMatrix(), this->model.getTransitionMatrix().getRowGroupIndices(), this->model.getBackwardTransitions(), this->options.phiStates.get(), this->options.psiStates.get()); return storm::utility::graph::performProb01Max(this->model.getTransitionMatrix(), this->model.getTransitionMatrix().getRowGroupIndices(), this->model.getBackwardTransitions(), this->options.phiStates.get(), this->options.psiStates.get());
@ -109,7 +109,7 @@ namespace storm {
// If the model had state rewards, we need to build the state rewards for the quotient as well. // If the model had state rewards, we need to build the state rewards for the quotient as well.
boost::optional<std::vector<ValueType>> stateRewards; boost::optional<std::vector<ValueType>> stateRewards;
if (this->options.keepRewards && this->model.hasRewardModel()) {
if (this->options.getKeepRewards() && this->model.hasRewardModel()) {
stateRewards = std::vector<ValueType>(this->blocks.size()); stateRewards = std::vector<ValueType>(this->blocks.size());
} }
@ -169,7 +169,7 @@ namespace storm {
// If the model has state rewards, we simply copy the state reward of the representative state, because // If the model has state rewards, we simply copy the state reward of the representative state, because
// all states in a block are guaranteed to have the same state reward. // all states in a block are guaranteed to have the same state reward.
if (this->options.keepRewards && this->model.hasRewardModel()) {
if (this->options.getKeepRewards() && this->model.hasRewardModel()) {
typename std::unordered_map<std::string, typename ModelType::RewardModelType>::const_iterator nameRewardModelPair = this->model.getUniqueRewardModel(); typename std::unordered_map<std::string, typename ModelType::RewardModelType>::const_iterator nameRewardModelPair = this->model.getUniqueRewardModel();
stateRewards.get()[blockIndex] = nameRewardModelPair->second.getStateRewardVector()[representativeState]; stateRewards.get()[blockIndex] = nameRewardModelPair->second.getStateRewardVector()[representativeState];
} }
@ -183,7 +183,7 @@ namespace storm {
// Construct the reward model mapping. // Construct the reward model mapping.
std::unordered_map<std::string, typename ModelType::RewardModelType> rewardModels; std::unordered_map<std::string, typename ModelType::RewardModelType> rewardModels;
if (this->options.keepRewards && this->model.hasRewardModel()) {
if (this->options.getKeepRewards() && this->model.hasRewardModel()) {
typename std::unordered_map<std::string, typename ModelType::RewardModelType>::const_iterator nameRewardModelPair = this->model.getUniqueRewardModel(); typename std::unordered_map<std::string, typename ModelType::RewardModelType>::const_iterator nameRewardModelPair = this->model.getUniqueRewardModel();
rewardModels.insert(std::make_pair(nameRewardModelPair->first, typename ModelType::RewardModelType(stateRewards))); rewardModels.insert(std::make_pair(nameRewardModelPair->first, typename ModelType::RewardModelType(stateRewards)));
} }

46
src/utility/storm.h
View File

@ -137,16 +137,13 @@ namespace storm {
} }
template<typename ModelType> template<typename ModelType>
std::shared_ptr<ModelType> performDeterministicSparseBisimulationMinimization(std::shared_ptr<ModelType> model, std::vector<std::shared_ptr<storm::logic::Formula>> const& formulas) {
std::shared_ptr<ModelType> performDeterministicSparseBisimulationMinimization(std::shared_ptr<ModelType> model, std::vector<std::shared_ptr<storm::logic::Formula>> const& formulas, storm::storage::BisimulationType type) {
std::cout << "Performing bisimulation minimization... "; std::cout << "Performing bisimulation minimization... ";
typename storm::storage::DeterministicModelBisimulationDecomposition<ModelType>::Options options; typename storm::storage::DeterministicModelBisimulationDecomposition<ModelType>::Options options;
if (!formulas.empty()) { if (!formulas.empty()) {
options = typename storm::storage::DeterministicModelBisimulationDecomposition<ModelType>::Options(*model, formulas); options = typename storm::storage::DeterministicModelBisimulationDecomposition<ModelType>::Options(*model, formulas);
} }
if (storm::settings::bisimulationSettings().isWeakBisimulationSet()) {
options.type = storm::storage::BisimulationType::Weak;
options.bounded = false;
}
options.setType(type);
storm::storage::DeterministicModelBisimulationDecomposition<ModelType> bisimulationDecomposition(*model, options); storm::storage::DeterministicModelBisimulationDecomposition<ModelType> bisimulationDecomposition(*model, options);
bisimulationDecomposition.computeBisimulationDecomposition(); bisimulationDecomposition.computeBisimulationDecomposition();
@ -156,16 +153,14 @@ namespace storm {
} }
template<typename ModelType> template<typename ModelType>
std::shared_ptr<ModelType> performNondeterministicSparseBisimulationMinimization(std::shared_ptr<ModelType> model, std::vector<std::shared_ptr<storm::logic::Formula>> const& formulas) {
std::shared_ptr<ModelType> performNondeterministicSparseBisimulationMinimization(std::shared_ptr<ModelType> model, std::vector<std::shared_ptr<storm::logic::Formula>> const& formulas, storm::storage::BisimulationType type) {
std::cout << "Performing bisimulation minimization... "; std::cout << "Performing bisimulation minimization... ";
typename storm::storage::DeterministicModelBisimulationDecomposition<ModelType>::Options options; typename storm::storage::DeterministicModelBisimulationDecomposition<ModelType>::Options options;
if (!formulas.empty()) { if (!formulas.empty()) {
options = typename storm::storage::NondeterministicModelBisimulationDecomposition<ModelType>::Options(*model, formulas); options = typename storm::storage::NondeterministicModelBisimulationDecomposition<ModelType>::Options(*model, formulas);
} }
if (storm::settings::bisimulationSettings().isWeakBisimulationSet()) {
options.type = storm::storage::BisimulationType::Weak;
options.bounded = false;
}
options.setType(type);
storm::storage::NondeterministicModelBisimulationDecomposition<ModelType> bisimulationDecomposition(*model, options); storm::storage::NondeterministicModelBisimulationDecomposition<ModelType> bisimulationDecomposition(*model, options);
bisimulationDecomposition.computeBisimulationDecomposition(); bisimulationDecomposition.computeBisimulationDecomposition();
@ -174,23 +169,30 @@ namespace storm {
return model; return model;
} }
template<typename ModelType, typename ValueType = typename ModelType::ValueType, typename std::enable_if<std::is_base_of<storm::models::sparse::Model<ValueType>, ModelType>::value, bool>::type = 0>
std::shared_ptr<storm::models::ModelBase> performBisimulationMinimization(std::shared_ptr<ModelType> model, std::vector<std::shared_ptr<storm::logic::Formula>> const& formulas, storm::storage::BisimulationType type) {
STORM_LOG_THROW(model->isOfType(storm::models::ModelType::Dtmc) || model->isOfType(storm::models::ModelType::Ctmc) || model->isOfType(storm::models::ModelType::Mdp), storm::exceptions::InvalidSettingsException, "Bisimulation minimization is currently only available for DTMCs, CTMCs and MDPs.");
model->reduceToStateBasedRewards();
if (model->isOfType(storm::models::ModelType::Dtmc)) {
return performDeterministicSparseBisimulationMinimization<storm::models::sparse::Dtmc<ValueType>>(model->template as<storm::models::sparse::Dtmc<ValueType>>(), formulas, type);
} else if (model->isOfType(storm::models::ModelType::Ctmc)) {
return performDeterministicSparseBisimulationMinimization<storm::models::sparse::Ctmc<ValueType>>(model->template as<storm::models::sparse::Ctmc<ValueType>>(), formulas, type);
} else {
return performNondeterministicSparseBisimulationMinimization<storm::models::sparse::Mdp<ValueType>>(model->template as<storm::models::sparse::Mdp<ValueType>>(), formulas, type);
}
}
template<typename ModelType, typename ValueType = typename ModelType::ValueType, typename std::enable_if<std::is_base_of<storm::models::sparse::Model<ValueType>, ModelType>::value, bool>::type = 0> template<typename ModelType, typename ValueType = typename ModelType::ValueType, typename std::enable_if<std::is_base_of<storm::models::sparse::Model<ValueType>, ModelType>::value, bool>::type = 0>
std::shared_ptr<storm::models::ModelBase> preprocessModel(std::shared_ptr<ModelType> model, std::vector<std::shared_ptr<storm::logic::Formula>> const& formulas) { std::shared_ptr<storm::models::ModelBase> preprocessModel(std::shared_ptr<ModelType> model, std::vector<std::shared_ptr<storm::logic::Formula>> const& formulas) {
if (storm::settings::generalSettings().isBisimulationSet()) { if (storm::settings::generalSettings().isBisimulationSet()) {
STORM_LOG_THROW(model->isSparseModel(), storm::exceptions::InvalidSettingsException, "Bisimulation minimization is currently only available for sparse models.");
STORM_LOG_THROW(model->isOfType(storm::models::ModelType::Dtmc) || model->isOfType(storm::models::ModelType::Ctmc) || model->isOfType(storm::models::ModelType::Mdp), storm::exceptions::InvalidSettingsException, "Bisimulation minimization is currently only available for DTMCs, CTMCs and MDPs.");
model->reduceToStateBasedRewards();
if (model->isOfType(storm::models::ModelType::Dtmc)) {
return performDeterministicSparseBisimulationMinimization<storm::models::sparse::Dtmc<ValueType>>(model->template as<storm::models::sparse::Dtmc<ValueType>>(), formulas);
} else if (model->isOfType(storm::models::ModelType::Ctmc)) {
return performDeterministicSparseBisimulationMinimization<storm::models::sparse::Ctmc<ValueType>>(model->template as<storm::models::sparse::Ctmc<ValueType>>(), formulas);
} else {
return performNondeterministicSparseBisimulationMinimization<storm::models::sparse::Mdp<ValueType>>(model->template as<storm::models::sparse::Mdp<ValueType>>(), formulas);
storm::storage::BisimulationType bisimType = storm::storage::BisimulationType::Strong;
if (storm::settings::bisimulationSettings().isWeakBisimulationSet()) {
bisimType = storm::storage::BisimulationType::Weak;
} }
STORM_LOG_THROW(model->isSparseModel(), storm::exceptions::InvalidSettingsException, "Bisimulation minimization is currently only available for sparse models.");
return performBisimulationMinimization(model, formulas, bisimType);
} }
return model; return model;
} }

6
test/functional/storage/DeterministicModelBisimulationDecompositionTest.cpp
View File

@ -35,8 +35,7 @@ TEST(DeterministicModelBisimulationDecomposition, Die) {
EXPECT_EQ(5ul, result->getNumberOfStates()); EXPECT_EQ(5ul, result->getNumberOfStates());
EXPECT_EQ(8ul, result->getNumberOfTransitions()); EXPECT_EQ(8ul, result->getNumberOfTransitions());
options.bounded = false;
options.type = storm::storage::BisimulationType::Weak;
options.setType(storm::storage::BisimulationType::Weak);
storm::storage::DeterministicModelBisimulationDecomposition<storm::models::sparse::Dtmc<double>> bisim3(*dtmc, options); storm::storage::DeterministicModelBisimulationDecomposition<storm::models::sparse::Dtmc<double>> bisim3(*dtmc, options);
ASSERT_NO_THROW(bisim3.computeBisimulationDecomposition()); ASSERT_NO_THROW(bisim3.computeBisimulationDecomposition());
@ -93,8 +92,7 @@ TEST(DeterministicModelBisimulationDecomposition, Crowds) {
EXPECT_EQ(65ul, result->getNumberOfStates()); EXPECT_EQ(65ul, result->getNumberOfStates());
EXPECT_EQ(105ul, result->getNumberOfTransitions()); EXPECT_EQ(105ul, result->getNumberOfTransitions());
options.bounded = false;
options.type = storm::storage::BisimulationType::Weak;
options.setType(storm::storage::BisimulationType::Weak);
storm::storage::DeterministicModelBisimulationDecomposition<storm::models::sparse::Dtmc<double>> bisim3(*dtmc, options); storm::storage::DeterministicModelBisimulationDecomposition<storm::models::sparse::Dtmc<double>> bisim3(*dtmc, options);
ASSERT_NO_THROW(bisim3.computeBisimulationDecomposition()); ASSERT_NO_THROW(bisim3.computeBisimulationDecomposition());

Write Preview
Loading…
Cancel
Save