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

Small fix to bisimulation options. 

Former-commit-id: 555c5ef697
main
dehnert 11 years ago
parent
ed4f1bb7cf
commit
2dae5862c8
2 changed files with 9 additions and 11 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. 8
      src/storage/DeterministicModelBisimulationDecomposition.cpp
  2. 12
      src/storage/DeterministicModelBisimulationDecomposition.h

8
src/storage/DeterministicModelBisimulationDecomposition.cpp
View File

@ -615,7 +615,7 @@ namespace storm {
} }
for (auto const& expressionFormula : atomicExpressionFormulas) { for (auto const& expressionFormula : atomicExpressionFormulas) {
std::stringstream stream; std::stringstream stream;
stream << expressionFormula;
stream << *expressionFormula;
labelsToRespect.insert(stream.str()); labelsToRespect.insert(stream.str());
} }
respectedAtomicPropositions = labelsToRespect; respectedAtomicPropositions = labelsToRespect;
@ -722,7 +722,7 @@ namespace storm {
template<typename ValueType> template<typename ValueType>
template<typename ModelType> template<typename ModelType>
void DeterministicModelBisimulationDecomposition<ValueType>::buildQuotient(ModelType const& model, boost::optional<std::set<std::string>> const& selectedAtomicPropositions, Partition const& partition, BisimulationType bisimulationType, bool keepRewards) {
void DeterministicModelBisimulationDecomposition<ValueType>::buildQuotient(ModelType const& model, std::set<std::string> const& selectedAtomicPropositions, Partition const& partition, BisimulationType bisimulationType, bool keepRewards) {
// In order to create the quotient model, we need to construct // In order to create the quotient model, we need to construct
// (a) the new transition matrix, // (a) the new transition matrix,
// (b) the new labeling, // (b) the new labeling,
@ -733,7 +733,7 @@ namespace storm {
// Prepare the new state labeling for (b). // Prepare the new state labeling for (b).
storm::models::AtomicPropositionsLabeling newLabeling(this->size(), model.getStateLabeling().getNumberOfAtomicPropositions()); storm::models::AtomicPropositionsLabeling newLabeling(this->size(), model.getStateLabeling().getNumberOfAtomicPropositions());
std::set<std::string> atomicPropositionsSet = selectedAtomicPropositions ? selectedAtomicPropositions.get() : model.getStateLabeling().getAtomicPropositions();
std::set<std::string> atomicPropositionsSet = selectedAtomicPropositions;
atomicPropositionsSet.insert("init"); atomicPropositionsSet.insert("init");
std::vector<std::string> atomicPropositions = std::vector<std::string>(atomicPropositionsSet.begin(), atomicPropositionsSet.end()); std::vector<std::string> atomicPropositions = std::vector<std::string>(atomicPropositionsSet.begin(), atomicPropositionsSet.end());
for (auto const& ap : atomicPropositions) { for (auto const& ap : atomicPropositions) {
@ -839,7 +839,7 @@ namespace storm {
template<typename ValueType> template<typename ValueType>
template<typename ModelType> template<typename ModelType>
void DeterministicModelBisimulationDecomposition<ValueType>::partitionRefinement(ModelType const& model, boost::optional<std::set<std::string>> const& atomicPropositions, storm::storage::SparseMatrix<ValueType> const& backwardTransitions, Partition& partition, BisimulationType bisimulationType, bool keepRewards, bool buildQuotient) {
void DeterministicModelBisimulationDecomposition<ValueType>::partitionRefinement(ModelType const& model, std::set<std::string> const& atomicPropositions, storm::storage::SparseMatrix<ValueType> const& backwardTransitions, Partition& partition, BisimulationType bisimulationType, bool keepRewards, bool buildQuotient) {
std::chrono::high_resolution_clock::time_point totalStart = std::chrono::high_resolution_clock::now(); std::chrono::high_resolution_clock::time_point totalStart = std::chrono::high_resolution_clock::now();
// Initially, all blocks are potential splitter, so we insert them in the splitterQueue. // Initially, all blocks are potential splitter, so we insert them in the splitterQueue.

12
src/storage/DeterministicModelBisimulationDecomposition.h
View File

@ -413,8 +413,7 @@ namespace storm {
* getQuotient(). * getQuotient().
* *
* @param model The model on whose state space to compute the coarses strong bisimulation relation. * @param model The model on whose state space to compute the coarses strong bisimulation relation.
* @param atomicPropositions The set of atomic propositions that the bisimulation considers. If not given,
* all atomic propositions are considered.
* @param atomicPropositions The set of atomic propositions that the bisimulation considers.
* @param backwardTransitions The backward transitions of the model. * @param backwardTransitions The backward transitions of the model.
* @param The initial partition. * @param The initial partition.
* @param bisimulationType The kind of bisimulation that is to be computed. * @param bisimulationType The kind of bisimulation that is to be computed.
@ -422,7 +421,7 @@ namespace storm {
* method. * method.
*/ */
template<typename ModelType> template<typename ModelType>
void partitionRefinement(ModelType const& model, boost::optional<std::set<std::string>> const& atomicPropositions, storm::storage::SparseMatrix<ValueType> const& backwardTransitions, Partition& partition, BisimulationType bisimulationType, bool keepRewards, bool buildQuotient);
void partitionRefinement(ModelType const& model, std::set<std::string> const& atomicPropositions, storm::storage::SparseMatrix<ValueType> const& backwardTransitions, Partition& partition, BisimulationType bisimulationType, bool keepRewards, bool buildQuotient);
/*! /*!
* Refines the partition based on the provided splitter. After calling this method all blocks are stable * Refines the partition based on the provided splitter. After calling this method all blocks are stable
@ -466,15 +465,14 @@ namespace storm {
* *
* @param model The model whose state space was used for computing the equivalence classes. This is used for * @param model The model whose state space was used for computing the equivalence classes. This is used for
* determining the transitions of each equivalence class. * determining the transitions of each equivalence class.
* @param selectedAtomicPropositions The set of atomic propositions that was considered by the bisimulation. The
* quotient will only have these atomic propositions. If not given, all atomic propositions will be
* considered.
* @param selectedAtomicPropositions The set of atomic propositions that was considered by the bisimulation.
* The quotient will only have these atomic propositions.
* @param partition The previously computed partition. This is used for quickly retrieving the block of a * @param partition The previously computed partition. This is used for quickly retrieving the block of a
* state. * state.
* @param bisimulationType The kind of bisimulation that is to be computed. * @param bisimulationType The kind of bisimulation that is to be computed.
*/ */
template<typename ModelType> template<typename ModelType>
void buildQuotient(ModelType const& model, boost::optional<std::set<std::string>> const& selectedAtomicPropositions, Partition const& partition, BisimulationType bisimulationType, bool keepRewards);
void buildQuotient(ModelType const& model, std::set<std::string> const& selectedAtomicPropositions, Partition const& partition, BisimulationType bisimulationType, bool keepRewards);
/*! /*!
* Creates the measure-driven initial partition for reaching psi states from phi states. * Creates the measure-driven initial partition for reaching psi states from phi states.

Write Preview
Loading…
Cancel
Save