From cc7d44dd157ea3c59d2b3831dee72e1813e81d2a Mon Sep 17 00:00:00 2001
From: dehnert <dehnert@cs.rwth-aachen.de>
Date: Thu, 29 Jan 2015 21:19:49 +0100
Subject: [PATCH 1/5] Added proper canHandle method to propositional model
checker.
Former-commit-id: 4af714e31a33e6c967823915f6d00027f1005537
---
.../propositional/SparsePropositionalModelChecker.cpp | 5 +++++
.../propositional/SparsePropositionalModelChecker.h | 1 +
2 files changed, 6 insertions(+)
diff --git a/src/modelchecker/propositional/SparsePropositionalModelChecker.cpp b/src/modelchecker/propositional/SparsePropositionalModelChecker.cpp
index 565546adf..aa8c4e058 100644
--- a/src/modelchecker/propositional/SparsePropositionalModelChecker.cpp
+++ b/src/modelchecker/propositional/SparsePropositionalModelChecker.cpp
@@ -15,6 +15,11 @@ namespace storm {
// Intentionally left empty.
}
+ template<typename ValueType>
+ bool SparsePropositionalModelChecker<ValueType>::canHandle(storm::logic::Formula const& formula) const {
+ return formula.isPropositionalFormula();
+ }
+
template<typename ValueType>
std::unique_ptr<CheckResult> SparsePropositionalModelChecker<ValueType>::checkBooleanLiteralFormula(storm::logic::BooleanLiteralFormula const& stateFormula) {
if (stateFormula.isTrueFormula()) {
diff --git a/src/modelchecker/propositional/SparsePropositionalModelChecker.h b/src/modelchecker/propositional/SparsePropositionalModelChecker.h
index c6309e4f0..d3a9011ce 100644
--- a/src/modelchecker/propositional/SparsePropositionalModelChecker.h
+++ b/src/modelchecker/propositional/SparsePropositionalModelChecker.h
@@ -14,6 +14,7 @@ namespace storm {
explicit SparsePropositionalModelChecker(storm::models::AbstractModel<ValueType> const& model);
// The implemented methods of the AbstractModelChecker interface.
+ virtual bool canHandle(storm::logic::Formula const& formula) const override;
virtual std::unique_ptr<CheckResult> checkBooleanLiteralFormula(storm::logic::BooleanLiteralFormula const& stateFormula) override;
virtual std::unique_ptr<CheckResult> checkAtomicLabelFormula(storm::logic::AtomicLabelFormula const& stateFormula) override;
From 9cf82bcd98ff23c9c63c54a615b3468a76c9f4ed Mon Sep 17 00:00:00 2001
From: dehnert <dehnert@cs.rwth-aachen.de>
Date: Fri, 30 Jan 2015 10:59:11 +0100
Subject: [PATCH 2/5] Added conversion from transition-based rewards to
state-based rewards to enable proper treatment in bisimulation minimization
Former-commit-id: d0c31094bdc5d781b070e91c743416ca7b40fa73
---
src/models/AbstractModel.h | 13 +++++++++++++
src/utility/cli.h | 4 ++++
2 files changed, 17 insertions(+)
diff --git a/src/models/AbstractModel.h b/src/models/AbstractModel.h
index b115e2551..76efcdb07 100644
--- a/src/models/AbstractModel.h
+++ b/src/models/AbstractModel.h
@@ -11,7 +11,11 @@
#include "src/storage/SparseMatrix.h"
#include "src/storage/Scheduler.h"
#include "src/storage/StronglyConnectedComponentDecomposition.h"
+#include "src/utility/macros.h"
#include "src/utility/Hash.h"
+#include "src/utility/vector.h"
+
+#include "src/exceptions/InvalidOperationException.h"
namespace storm {
namespace models {
@@ -329,6 +333,15 @@ class AbstractModel: public std::enable_shared_from_this<AbstractModel<T>> {
return static_cast<bool>(choiceLabeling);
}
+ void convertTransitionRewardsToStateRewards() {
+ STORM_LOG_THROW(this->hasTransitionRewards(), storm::exceptions::InvalidOperationException, "Cannot reduce non-existant transition rewards to state rewards.");
+ if (this->hasStateRewards()) {
+ storm::utility::vector::addVectorsInPlace(stateRewardVector.get(), transitionMatrix.getPointwiseProductRowSumVector(transitionRewardMatrix.get()));
+ } else {
+ this->stateRewardVector = transitionMatrix.getPointwiseProductRowSumVector(transitionRewardMatrix.get());
+ }
+ }
+
/*!
* Retrieves the size of the internal representation of the model in memory.
* @return the size of the internal representation of the model in memory
diff --git a/src/utility/cli.h b/src/utility/cli.h
index de987e365..07fb2fbd5 100644
--- a/src/utility/cli.h
+++ b/src/utility/cli.h
@@ -288,6 +288,10 @@ namespace storm {
STORM_LOG_THROW(model->getType() == storm::models::DTMC, storm::exceptions::InvalidSettingsException, "Bisimulation minimization is currently only available for DTMCs.");
std::shared_ptr<storm::models::Dtmc<double>> dtmc = model->template as<storm::models::Dtmc<double>>();
+ if (dtmc->hasTransitionRewards()) {
+ dtmc->convertTransitionRewardsToStateRewards();
+ }
+
std::cout << "Performing bisimulation minimization... ";
storm::storage::DeterministicModelBisimulationDecomposition<double> bisimulationDecomposition(*dtmc, boost::optional<std::set<std::string>>(), true, storm::settings::bisimulationSettings().isWeakBisimulationSet(), true);
model = bisimulationDecomposition.getQuotient();
From 700703140f2ac46e027b9449ba34902e4e2b3a4a Mon Sep 17 00:00:00 2001
From: dehnert <dehnert@cs.rwth-aachen.de>
Date: Fri, 30 Jan 2015 11:33:48 +0100
Subject: [PATCH 3/5] Fixed minor issue.
Former-commit-id: 9799a0cb3095bf8d978b167bfb7111e5c6acb3c2
---
src/models/AbstractModel.h | 1 +
1 file changed, 1 insertion(+)
diff --git a/src/models/AbstractModel.h b/src/models/AbstractModel.h
index 76efcdb07..958f248aa 100644
--- a/src/models/AbstractModel.h
+++ b/src/models/AbstractModel.h
@@ -340,6 +340,7 @@ class AbstractModel: public std::enable_shared_from_this<AbstractModel<T>> {
} else {
this->stateRewardVector = transitionMatrix.getPointwiseProductRowSumVector(transitionRewardMatrix.get());
}
+ this->transitionRewardMatrix.reset();
}
/*!
From 495230609247fda9f9a9a8dc69c35fd034471337 Mon Sep 17 00:00:00 2001
From: dehnert <dehnert@cs.rwth-aachen.de>
Date: Fri, 30 Jan 2015 17:43:56 +0100
Subject: [PATCH 4/5] Worked on making bisimulation decomposition a bit easier
to use.
Former-commit-id: 0fe6b2af6a3ebc7611e54466ab1d5c24c29fb507
---
src/exceptions/InvalidOptionException.h | 15 ++
src/logic/BinaryPathFormula.cpp | 8 +
src/logic/BinaryPathFormula.h | 2 +
src/logic/BinaryStateFormula.cpp | 8 +
src/logic/BinaryStateFormula.h | 2 +
src/logic/BoundedUntilFormula.cpp | 4 +
src/logic/BoundedUntilFormula.h | 2 +
src/logic/Formula.cpp | 8 +
src/logic/Formula.h | 2 +
src/logic/NextFormula.cpp | 4 +
src/logic/NextFormula.h | 2 +
src/logic/UnaryPathFormula.cpp | 8 +
src/logic/UnaryPathFormula.h | 2 +
src/logic/UnaryStateFormula.cpp | 8 +
src/logic/UnaryStateFormula.h | 2 +
src/models/AbstractModel.h | 2 +-
...ministicModelBisimulationDecomposition.cpp | 245 +++++++++++-------
...erministicModelBisimulationDecomposition.h | 106 ++++----
src/utility/cli.h | 5 +-
...sticModelBisimulationDecompositionTest.cpp | 24 +-
20 files changed, 305 insertions(+), 154 deletions(-)
create mode 100644 src/exceptions/InvalidOptionException.h
diff --git a/src/exceptions/InvalidOptionException.h b/src/exceptions/InvalidOptionException.h
new file mode 100644
index 000000000..ec94cf8a9
--- /dev/null
+++ b/src/exceptions/InvalidOptionException.h
@@ -0,0 +1,15 @@
+#ifndef STORM_EXCEPTIONS_INVALIDOPTIONEXCEPTION_H_
+#define STORM_EXCEPTIONS_INVALIDOPTIONEXCEPTION_H_
+
+#include "src/exceptions/BaseException.h"
+#include "src/exceptions/ExceptionMacros.h"
+
+namespace storm {
+ namespace exceptions {
+
+ STORM_NEW_EXCEPTION(InvalidOptionException)
+
+ } // namespace exceptions
+} // namespace storm
+
+#endif /* STORM_EXCEPTIONS_INVALIDOPTIONEXCEPTION_H_ */
diff --git a/src/logic/BinaryPathFormula.cpp b/src/logic/BinaryPathFormula.cpp
index fb2e77687..a8e30ec4c 100644
--- a/src/logic/BinaryPathFormula.cpp
+++ b/src/logic/BinaryPathFormula.cpp
@@ -18,6 +18,14 @@ namespace storm {
return this->getLeftSubformula().isLtlFormula() && this->getRightSubformula().isLtlFormula();
}
+ bool BinaryPathFormula::containsBoundedUntilFormula() const {
+ return this->getLeftSubformula().containsBoundedUntilFormula() || this->getRightSubformula().containsBoundedUntilFormula();
+ }
+
+ bool BinaryPathFormula::containsNextFormula() const {
+ return this->getLeftSubformula().containsNextFormula() || this->getRightSubformula().containsNextFormula();
+ }
+
bool BinaryPathFormula::containsProbabilityOperator() const {
return this->getLeftSubformula().containsProbabilityOperator() || this->getRightSubformula().containsProbabilityOperator();
}
diff --git a/src/logic/BinaryPathFormula.h b/src/logic/BinaryPathFormula.h
index 8ce897168..3d9ce2a00 100644
--- a/src/logic/BinaryPathFormula.h
+++ b/src/logic/BinaryPathFormula.h
@@ -19,6 +19,8 @@ namespace storm {
virtual bool isPctlPathFormula() const override;
virtual bool isLtlFormula() const override;
+ virtual bool containsBoundedUntilFormula() const override;
+ virtual bool containsNextFormula() const override;
virtual bool containsProbabilityOperator() const override;
virtual bool containsNestedProbabilityOperators() const override;
virtual bool containsRewardOperator() const override;
diff --git a/src/logic/BinaryStateFormula.cpp b/src/logic/BinaryStateFormula.cpp
index fb9a7560e..bf11df80b 100644
--- a/src/logic/BinaryStateFormula.cpp
+++ b/src/logic/BinaryStateFormula.cpp
@@ -18,6 +18,14 @@ namespace storm {
return this->getLeftSubformula().isLtlFormula() && this->getRightSubformula().isLtlFormula();
}
+ bool BinaryStateFormula::containsBoundedUntilFormula() const {
+ return this->getLeftSubformula().containsBoundedUntilFormula() || this->getRightSubformula().containsBoundedUntilFormula();
+ }
+
+ bool BinaryStateFormula::containsNextFormula() const {
+ return this->getLeftSubformula().containsNextFormula() || this->getRightSubformula().containsNextFormula();
+ }
+
bool BinaryStateFormula::containsProbabilityOperator() const {
return this->getLeftSubformula().containsProbabilityOperator() || this->getRightSubformula().containsProbabilityOperator();
}
diff --git a/src/logic/BinaryStateFormula.h b/src/logic/BinaryStateFormula.h
index 409c5b969..075ae236a 100644
--- a/src/logic/BinaryStateFormula.h
+++ b/src/logic/BinaryStateFormula.h
@@ -17,6 +17,8 @@ namespace storm {
virtual bool isPctlStateFormula() const override;
virtual bool isLtlFormula() const override;
+ virtual bool containsBoundedUntilFormula() const override;
+ virtual bool containsNextFormula() const override;
virtual bool containsProbabilityOperator() const override;
virtual bool containsNestedProbabilityOperators() const override;
virtual bool containsRewardOperator() const override;
diff --git a/src/logic/BoundedUntilFormula.cpp b/src/logic/BoundedUntilFormula.cpp
index 3efb6af82..5c148bc1f 100644
--- a/src/logic/BoundedUntilFormula.cpp
+++ b/src/logic/BoundedUntilFormula.cpp
@@ -18,6 +18,10 @@ namespace storm {
return true;
}
+ bool BoundedUntilFormula::containsBoundedUntilFormula() const {
+ return true;
+ }
+
bool BoundedUntilFormula::isIntervalBounded() const {
return bounds.which() == 1;
}
diff --git a/src/logic/BoundedUntilFormula.h b/src/logic/BoundedUntilFormula.h
index e79451f0f..0ed97524a 100644
--- a/src/logic/BoundedUntilFormula.h
+++ b/src/logic/BoundedUntilFormula.h
@@ -14,6 +14,8 @@ namespace storm {
virtual bool isBoundedUntilFormula() const override;
+ virtual bool containsBoundedUntilFormula() const override;
+
bool isIntervalBounded() const;
bool isIntegerUpperBounded() const;
diff --git a/src/logic/Formula.cpp b/src/logic/Formula.cpp
index 715c3f502..6cf27dfdd 100644
--- a/src/logic/Formula.cpp
+++ b/src/logic/Formula.cpp
@@ -138,6 +138,14 @@ namespace storm {
return false;
}
+ bool Formula::containsBoundedUntilFormula() const {
+ return false;
+ }
+
+ bool Formula::containsNextFormula() const {
+ return false;
+ }
+
bool Formula::containsProbabilityOperator() const {
return false;
}
diff --git a/src/logic/Formula.h b/src/logic/Formula.h
index ba6dedd67..bb2e74a7c 100644
--- a/src/logic/Formula.h
+++ b/src/logic/Formula.h
@@ -83,6 +83,8 @@ namespace storm {
virtual bool isPltlFormula() const;
virtual bool isLtlFormula() const;
virtual bool isPropositionalFormula() const;
+ virtual bool containsBoundedUntilFormula() const;
+ virtual bool containsNextFormula() const;
virtual bool containsProbabilityOperator() const;
virtual bool containsNestedProbabilityOperators() const;
virtual bool containsRewardOperator() const;
diff --git a/src/logic/NextFormula.cpp b/src/logic/NextFormula.cpp
index 37f4c4b3f..4bdf98d1f 100644
--- a/src/logic/NextFormula.cpp
+++ b/src/logic/NextFormula.cpp
@@ -10,6 +10,10 @@ namespace storm {
return true;
}
+ bool NextFormula::containsNextFormula() const {
+ return true;
+ }
+
std::ostream& NextFormula::writeToStream(std::ostream& out) const {
out << "X ";
this->getSubformula().writeToStream(out);
diff --git a/src/logic/NextFormula.h b/src/logic/NextFormula.h
index 186f81e51..179185f48 100644
--- a/src/logic/NextFormula.h
+++ b/src/logic/NextFormula.h
@@ -15,6 +15,8 @@ namespace storm {
virtual bool isNextFormula() const override;
+ virtual bool containsNextFormula() const override;
+
virtual std::ostream& writeToStream(std::ostream& out) const override;
};
}
diff --git a/src/logic/UnaryPathFormula.cpp b/src/logic/UnaryPathFormula.cpp
index a30979311..d6d6dd01d 100644
--- a/src/logic/UnaryPathFormula.cpp
+++ b/src/logic/UnaryPathFormula.cpp
@@ -18,6 +18,14 @@ namespace storm {
return this->getSubformula().isLtlFormula();
}
+ bool UnaryPathFormula::containsBoundedUntilFormula() const {
+ return this->getSubformula().containsBoundedUntilFormula();
+ }
+
+ bool UnaryPathFormula::containsNextFormula() const {
+ return this->getSubformula().containsNextFormula();
+ }
+
bool UnaryPathFormula::containsProbabilityOperator() const {
return this->getSubformula().containsProbabilityOperator();
}
diff --git a/src/logic/UnaryPathFormula.h b/src/logic/UnaryPathFormula.h
index faabd4a25..f02c7a830 100644
--- a/src/logic/UnaryPathFormula.h
+++ b/src/logic/UnaryPathFormula.h
@@ -19,6 +19,8 @@ namespace storm {
virtual bool isPctlPathFormula() const override;
virtual bool isLtlFormula() const override;
+ virtual bool containsBoundedUntilFormula() const override;
+ virtual bool containsNextFormula() const override;
virtual bool containsProbabilityOperator() const override;
virtual bool containsNestedProbabilityOperators() const override;
virtual bool containsRewardOperator() const override;
diff --git a/src/logic/UnaryStateFormula.cpp b/src/logic/UnaryStateFormula.cpp
index 9dfd1286d..ab2718d69 100644
--- a/src/logic/UnaryStateFormula.cpp
+++ b/src/logic/UnaryStateFormula.cpp
@@ -22,6 +22,14 @@ namespace storm {
return this->getSubformula().isLtlFormula();
}
+ bool UnaryStateFormula::containsBoundedUntilFormula() const {
+ return this->getSubformula().containsBoundedUntilFormula();
+ }
+
+ bool UnaryStateFormula::containsNextFormula() const {
+ return this->getSubformula().containsNextFormula();
+ }
+
bool UnaryStateFormula::containsProbabilityOperator() const {
return getSubformula().containsProbabilityOperator();
}
diff --git a/src/logic/UnaryStateFormula.h b/src/logic/UnaryStateFormula.h
index cac202275..f604262e8 100644
--- a/src/logic/UnaryStateFormula.h
+++ b/src/logic/UnaryStateFormula.h
@@ -18,6 +18,8 @@ namespace storm {
virtual bool isPropositionalFormula() const override;
virtual bool isPctlStateFormula() const override;
virtual bool isLtlFormula() const override;
+ virtual bool containsBoundedUntilFormula() const override;
+ virtual bool containsNextFormula() const override;
virtual bool containsProbabilityOperator() const override;
virtual bool containsNestedProbabilityOperators() const override;
virtual bool containsRewardOperator() const override;
diff --git a/src/models/AbstractModel.h b/src/models/AbstractModel.h
index 958f248aa..c6c2e7e3d 100644
--- a/src/models/AbstractModel.h
+++ b/src/models/AbstractModel.h
@@ -340,7 +340,7 @@ class AbstractModel: public std::enable_shared_from_this<AbstractModel<T>> {
} else {
this->stateRewardVector = transitionMatrix.getPointwiseProductRowSumVector(transitionRewardMatrix.get());
}
- this->transitionRewardMatrix.reset();
+ this->transitionRewardMatrix = boost::optional<storm::storage::SparseMatrix<T>>();
}
/*!
diff --git a/src/storage/DeterministicModelBisimulationDecomposition.cpp b/src/storage/DeterministicModelBisimulationDecomposition.cpp
index 8455825f2..1134d8904 100644
--- a/src/storage/DeterministicModelBisimulationDecomposition.cpp
+++ b/src/storage/DeterministicModelBisimulationDecomposition.cpp
@@ -6,14 +6,18 @@
#include <iomanip>
#include <boost/iterator/transform_iterator.hpp>
+#include "src/modelchecker/propositional/SparsePropositionalModelChecker.h"
+#include "src/modelchecker/results/ExplicitQualitativeCheckResult.h"
+
#include "src/utility/graph.h"
#include "src/exceptions/IllegalFunctionCallException.h"
+#include "src/exceptions/InvalidOptionException.h"
namespace storm {
namespace storage {
template<typename ValueType>
- DeterministicModelBisimulationDecomposition<ValueType>::Block::Block(storm::storage::sparse::state_type begin, storm::storage::sparse::state_type end, Block* prev, Block* next, std::size_t id, std::shared_ptr<std::string> const& label) : next(next), prev(prev), begin(begin), end(end), markedAsSplitter(false), markedAsPredecessorBlock(false), markedPosition(begin), absorbing(false), id(id), label(label) {
+ DeterministicModelBisimulationDecomposition<ValueType>::Block::Block(storm::storage::sparse::state_type begin, storm::storage::sparse::state_type end, Block* prev, Block* next, std::size_t id) : next(next), prev(prev), begin(begin), end(end), markedAsSplitter(false), markedAsPredecessorBlock(false), markedPosition(begin), absorbing(false), id(id) {
if (next != nullptr) {
next->prev = this;
}
@@ -130,12 +134,12 @@ namespace storm {
typename DeterministicModelBisimulationDecomposition<ValueType>::Block* DeterministicModelBisimulationDecomposition<ValueType>::Block::getPreviousBlockPointer() {
return this->prev;
}
-
+
template<typename ValueType>
typename DeterministicModelBisimulationDecomposition<ValueType>::Block* DeterministicModelBisimulationDecomposition<ValueType>::Block::getNextBlockPointer() {
return this->next;
}
-
+
template<typename ValueType>
typename DeterministicModelBisimulationDecomposition<ValueType>::Block const& DeterministicModelBisimulationDecomposition<ValueType>::Block::getPreviousBlock() const {
return *this->prev;
@@ -169,12 +173,12 @@ namespace storm {
void DeterministicModelBisimulationDecomposition<ValueType>::Block::markAsSplitter() {
this->markedAsSplitter = true;
}
-
+
template<typename ValueType>
void DeterministicModelBisimulationDecomposition<ValueType>::Block::unmarkAsSplitter() {
this->markedAsSplitter = false;
}
-
+
template<typename ValueType>
std::size_t DeterministicModelBisimulationDecomposition<ValueType>::Block::getId() const {
return this->id;
@@ -225,22 +229,6 @@ namespace storm {
return markedAsPredecessorBlock;
}
- template<typename ValueType>
- bool DeterministicModelBisimulationDecomposition<ValueType>::Block::hasLabel() const {
- return this->label != nullptr;
- }
-
- template<typename ValueType>
- std::string const& DeterministicModelBisimulationDecomposition<ValueType>::Block::getLabel() const {
- STORM_LOG_THROW(this->label != nullptr, storm::exceptions::IllegalFunctionCallException, "Unable to retrieve label of block that has none.");
- return *this->label;
- }
-
- template<typename ValueType>
- std::shared_ptr<std::string> const& DeterministicModelBisimulationDecomposition<ValueType>::Block::getLabelPtr() const {
- return this->label;
- }
-
template<typename ValueType>
DeterministicModelBisimulationDecomposition<ValueType>::Partition::Partition(std::size_t numberOfStates, bool keepSilentProbabilities) : numberOfBlocks(0), stateToBlockMapping(numberOfStates), statesAndValues(numberOfStates), positions(numberOfStates), keepSilentProbabilities(keepSilentProbabilities), silentProbabilities() {
// Create the block and give it an iterator to itself.
@@ -261,7 +249,7 @@ namespace storm {
}
template<typename ValueType>
- DeterministicModelBisimulationDecomposition<ValueType>::Partition::Partition(std::size_t numberOfStates, storm::storage::BitVector const& prob0States, storm::storage::BitVector const& prob1States, std::string const& otherLabel, std::string const& prob1Label, bool keepSilentProbabilities) : numberOfBlocks(0), stateToBlockMapping(numberOfStates), statesAndValues(numberOfStates), positions(numberOfStates), keepSilentProbabilities(keepSilentProbabilities), silentProbabilities() {
+ DeterministicModelBisimulationDecomposition<ValueType>::Partition::Partition(std::size_t numberOfStates, storm::storage::BitVector const& prob0States, storm::storage::BitVector const& prob1States, bool keepSilentProbabilities) : numberOfBlocks(0), stateToBlockMapping(numberOfStates), statesAndValues(numberOfStates), positions(numberOfStates), keepSilentProbabilities(keepSilentProbabilities), silentProbabilities() {
storm::storage::sparse::state_type position = 0;
Block* firstBlock = nullptr;
Block* secondBlock = nullptr;
@@ -270,7 +258,7 @@ namespace storm {
typename std::list<Block>::iterator firstIt = blocks.emplace(this->blocks.end(), 0, prob0States.getNumberOfSetBits(), nullptr, nullptr, numberOfBlocks++);
firstBlock = &(*firstIt);
firstBlock->setIterator(firstIt);
-
+
for (auto state : prob0States) {
statesAndValues[position] = std::make_pair(state, storm::utility::zero<ValueType>());
positions[state] = position;
@@ -279,9 +267,9 @@ namespace storm {
}
firstBlock->setAbsorbing(true);
}
-
+
if (!prob1States.empty()) {
- typename std::list<Block>::iterator secondIt = blocks.emplace(this->blocks.end(), position, position + prob1States.getNumberOfSetBits(), firstBlock, nullptr, numberOfBlocks++, std::shared_ptr<std::string>(new std::string(prob1Label)));
+ typename std::list<Block>::iterator secondIt = blocks.emplace(this->blocks.end(), position, position + prob1States.getNumberOfSetBits(), firstBlock, nullptr, numberOfBlocks++);
secondBlock = &(*secondIt);
secondBlock->setIterator(secondIt);
@@ -296,7 +284,7 @@ namespace storm {
storm::storage::BitVector otherStates = ~(prob0States | prob1States);
if (!otherStates.empty()) {
- typename std::list<Block>::iterator thirdIt = blocks.emplace(this->blocks.end(), position, numberOfStates, secondBlock, nullptr, numberOfBlocks++, otherLabel == "true" ? std::shared_ptr<std::string>(nullptr) : std::shared_ptr<std::string>(new std::string(otherLabel)));
+ typename std::list<Block>::iterator thirdIt = blocks.emplace(this->blocks.end(), position, numberOfStates, secondBlock, nullptr, numberOfBlocks++);
thirdBlock = &(*thirdIt);
thirdBlock->setIterator(thirdIt);
@@ -319,7 +307,7 @@ namespace storm {
std::swap(this->statesAndValues[this->positions[state1]], this->statesAndValues[this->positions[state2]]);
std::swap(this->positions[state1], this->positions[state2]);
}
-
+
template<typename ValueType>
void DeterministicModelBisimulationDecomposition<ValueType>::Partition::swapStatesAtPositions(storm::storage::sparse::state_type position1, storm::storage::sparse::state_type position2) {
storm::storage::sparse::state_type state1 = this->statesAndValues[position1].first;
@@ -365,7 +353,7 @@ namespace storm {
void DeterministicModelBisimulationDecomposition<ValueType>::Partition::increaseValue(storm::storage::sparse::state_type state, ValueType value) {
this->statesAndValues[this->positions[state]].second += value;
}
-
+
template<typename ValueType>
void DeterministicModelBisimulationDecomposition<ValueType>::Partition::updateBlockMapping(Block& block, typename std::vector<std::pair<storm::storage::sparse::state_type, ValueType>>::iterator first, typename std::vector<std::pair<storm::storage::sparse::state_type, ValueType>>::iterator last) {
for (; first != last; ++first) {
@@ -382,12 +370,12 @@ namespace storm {
typename DeterministicModelBisimulationDecomposition<ValueType>::Block& DeterministicModelBisimulationDecomposition<ValueType>::Partition::getBlock(storm::storage::sparse::state_type state) {
return *this->stateToBlockMapping[state];
}
-
+
template<typename ValueType>
typename DeterministicModelBisimulationDecomposition<ValueType>::Block const& DeterministicModelBisimulationDecomposition<ValueType>::Partition::getBlock(storm::storage::sparse::state_type state) const {
return *this->stateToBlockMapping[state];
}
-
+
template<typename ValueType>
typename std::vector<std::pair<storm::storage::sparse::state_type, ValueType>>::iterator DeterministicModelBisimulationDecomposition<ValueType>::Partition::getBegin(Block const& block) {
return this->statesAndValues.begin() + block.getBegin();
@@ -397,7 +385,7 @@ namespace storm {
typename std::vector<std::pair<storm::storage::sparse::state_type, ValueType>>::iterator DeterministicModelBisimulationDecomposition<ValueType>::Partition::getEnd(Block const& block) {
return this->statesAndValues.begin() + block.getEnd();
}
-
+
template<typename ValueType>
typename std::vector<std::pair<storm::storage::sparse::state_type, ValueType>>::const_iterator DeterministicModelBisimulationDecomposition<ValueType>::Partition::getBegin(Block const& block) const {
return this->statesAndValues.begin() + block.getBegin();
@@ -417,7 +405,7 @@ namespace storm {
}
// Actually create the new block and insert it at the correct position.
- typename std::list<Block>::iterator selfIt = this->blocks.emplace(block.getIterator(), block.getBegin(), position, block.getPreviousBlockPointer(), &block, numberOfBlocks++, block.getLabelPtr());
+ typename std::list<Block>::iterator selfIt = this->blocks.emplace(block.getIterator(), block.getBegin(), position, block.getPreviousBlockPointer(), &block, numberOfBlocks++);
selfIt->setIterator(selfIt);
Block& newBlock = *selfIt;
@@ -589,41 +577,121 @@ namespace storm {
}
template<typename ValueType>
- DeterministicModelBisimulationDecomposition<ValueType>::DeterministicModelBisimulationDecomposition(storm::models::Dtmc<ValueType> const& model, boost::optional<std::set<std::string>> const& atomicPropositions, bool keepRewards, bool weak, bool buildQuotient) : comparator() {
- STORM_LOG_THROW(!model.hasTransitionRewards(), storm::exceptions::IllegalFunctionCallException, "Bisimulation is currently only supported for models without transition rewards.");
- storm::storage::SparseMatrix<ValueType> backwardTransitions = model.getBackwardTransitions();
- BisimulationType bisimulationType = weak ? BisimulationType::WeakDtmc : BisimulationType::Strong;
- Partition initialPartition = getLabelBasedInitialPartition(model, backwardTransitions, bisimulationType, atomicPropositions, keepRewards);
- partitionRefinement(model, atomicPropositions, backwardTransitions, initialPartition, bisimulationType, keepRewards, buildQuotient);
+ DeterministicModelBisimulationDecomposition<ValueType>::Options::Options(storm::logic::Formula const& formula) : Options() {
+ if (!formula.containsRewardOperator()) {
+ this->keepRewards = false;
+ }
+
+ // As a tradeoff, we compute a strong bisimulation, because that is typically much faster. If the number of
+ // states is to be minimized, this should be set to weak by the calling site.
+ weak = false;
+
+ // We need to preserve bounded properties iff the formula contains a bounded until or a next subformula.
+ bounded = formula.containsBoundedUntilFormula() || formula.containsNextFormula();
+
+ std::vector<std::shared_ptr<storm::logic::AtomicExpressionFormula const>> atomicExpressionFormulas = formula.getAtomicExpressionFormulas();
+ std::vector<std::shared_ptr<storm::logic::AtomicLabelFormula const>> atomicLabelFormulas = formula.getAtomicLabelFormulas();
+
+ std::set<std::string> labelsToRespect;
+ for (auto const& labelFormula : atomicLabelFormulas) {
+ labelsToRespect.insert(labelFormula->getLabel());
+ }
+ for (auto const& expressionFormula : atomicExpressionFormulas) {
+ std::stringstream stream;
+ stream << expressionFormula;
+ labelsToRespect.insert(stream.str());
+ }
+ respectedAtomicPropositions = labelsToRespect;
+
+ std::shared_ptr<storm::logic::Formula const> newFormula = formula.asSharedPointer();
+
+ if (formula.isProbabilityOperatorFormula()) {
+ newFormula = formula.asProbabilityOperatorFormula().getSubformula().asSharedPointer();
+ } else if (formula.isRewardOperatorFormula()) {
+ newFormula = formula.asRewardOperatorFormula().getSubformula().asSharedPointer();
+ }
+
+ std::shared_ptr<storm::logic::Formula const> leftSubformula = std::make_shared<storm::logic::BooleanLiteralFormula>(true);
+ std::shared_ptr<storm::logic::Formula const> rightSubformula;
+ if (newFormula->isUntilFormula()) {
+ leftSubformula = newFormula->asUntilFormula().getLeftSubformula().asSharedPointer();
+ rightSubformula = newFormula->asUntilFormula().getRightSubformula().asSharedPointer();
+ if (leftSubformula->isPropositionalFormula() && rightSubformula->isPropositionalFormula()) {
+ measureDrivenInitialPartition = true;
+ }
+ } else if (newFormula->isEventuallyFormula()) {
+ rightSubformula = newFormula->asEventuallyFormula().getSubformula().asSharedPointer();
+ if (rightSubformula->isPropositionalFormula()) {
+ measureDrivenInitialPartition = true;
+ }
+ } else if (newFormula->isReachabilityRewardFormula()) {
+ rightSubformula = newFormula->asEventuallyFormula().getSubformula().asSharedPointer();
+ if (rightSubformula->isPropositionalFormula()) {
+ measureDrivenInitialPartition = true;
+ }
+ }
+
+ if (measureDrivenInitialPartition) {
+ phiStateFormula = leftSubformula;
+ psiStateFormula = rightSubformula;
+ }
}
-
+
template<typename ValueType>
- DeterministicModelBisimulationDecomposition<ValueType>::DeterministicModelBisimulationDecomposition(storm::models::Ctmc<ValueType> const& model, boost::optional<std::set<std::string>> const& atomicPropositions, bool keepRewards, bool weak, bool buildQuotient) {
- STORM_LOG_THROW(!keepRewards || !model.hasTransitionRewards(), storm::exceptions::IllegalFunctionCallException, "Bisimulation is currently only supported for models without transition rewards.");
- storm::storage::SparseMatrix<ValueType> backwardTransitions = model.getBackwardTransitions();
- BisimulationType bisimulationType = weak ? BisimulationType::WeakCtmc : BisimulationType::Strong;
- Partition initialPartition = getLabelBasedInitialPartition(model, backwardTransitions, bisimulationType, atomicPropositions, keepRewards);
- partitionRefinement(model, atomicPropositions, backwardTransitions, initialPartition, bisimulationType, keepRewards,buildQuotient);
+ DeterministicModelBisimulationDecomposition<ValueType>::Options::Options() : measureDrivenInitialPartition(false), phiStateFormula(), psiStateFormula(), respectedAtomicPropositions(), keepRewards(true), weak(false), bounded(true), buildQuotient(true) {
+ // Intentionally left empty.
}
template<typename ValueType>
- DeterministicModelBisimulationDecomposition<ValueType>::DeterministicModelBisimulationDecomposition(storm::models::Dtmc<ValueType> const& model, std::string const& phiLabel, std::string const& psiLabel, bool keepRewards, bool weak, bool bounded, bool buildQuotient) {
- STORM_LOG_THROW(!keepRewards || !model.hasTransitionRewards(), storm::exceptions::IllegalFunctionCallException, "Bisimulation is currently only supported for models without transition rewards.");
- STORM_LOG_THROW(!weak || !bounded, storm::exceptions::IllegalFunctionCallException, "Weak bisimulation does not preserve bounded properties.");
+ DeterministicModelBisimulationDecomposition<ValueType>::DeterministicModelBisimulationDecomposition(storm::models::Dtmc<ValueType> const& model, Options const& options) {
+ STORM_LOG_THROW(!model.hasTransitionRewards(), storm::exceptions::IllegalFunctionCallException, "Bisimulation is currently only supported for models without transition rewards. Consider converting the transition rewards to state rewards (via suitable function calls).");
+ STORM_LOG_THROW(!options.weak || !options.bounded, storm::exceptions::IllegalFunctionCallException, "Weak bisimulation cannot preserve bounded properties.");
storm::storage::SparseMatrix<ValueType> backwardTransitions = model.getBackwardTransitions();
- BisimulationType bisimulationType = weak ? BisimulationType::WeakDtmc : BisimulationType::Strong;
- Partition initialPartition = getMeasureDrivenInitialPartition(model, backwardTransitions, phiLabel, psiLabel, bisimulationType, keepRewards, bounded);
- partitionRefinement(model, std::set<std::string>({phiLabel, psiLabel}), model.getBackwardTransitions(), initialPartition, bisimulationType, keepRewards, buildQuotient);
+ BisimulationType bisimulationType = options.weak ? BisimulationType::WeakDtmc : BisimulationType::Strong;
+
+ std::set<std::string> atomicPropositions;
+ if (options.respectedAtomicPropositions) {
+ atomicPropositions = options.respectedAtomicPropositions.get();
+ } else {
+ atomicPropositions = model.getStateLabeling().getAtomicPropositions();
+ }
+
+ Partition initialPartition;
+ if (options.measureDrivenInitialPartition) {
+ STORM_LOG_THROW(options.phiStateFormula, storm::exceptions::InvalidOptionException, "Unable to compute measure-driven initial partition without phi and psi states.");
+ STORM_LOG_THROW(options.psiStateFormula, storm::exceptions::InvalidOptionException, "Unable to compute measure-driven initial partition without phi and psi states.");
+ initialPartition = getMeasureDrivenInitialPartition(model, backwardTransitions, options.phiStateFormula.get(), options.psiStateFormula.get(), bisimulationType, options.keepRewards, options.bounded);
+ } else {
+ initialPartition = getLabelBasedInitialPartition(model, backwardTransitions, bisimulationType, atomicPropositions, options.keepRewards);
+ }
+
+ partitionRefinement(model, atomicPropositions, backwardTransitions, initialPartition, bisimulationType, options.keepRewards, options.buildQuotient);
}
template<typename ValueType>
- DeterministicModelBisimulationDecomposition<ValueType>::DeterministicModelBisimulationDecomposition(storm::models::Ctmc<ValueType> const& model, std::string const& phiLabel, std::string const& psiLabel, bool keepRewards, bool weak, bool bounded, bool buildQuotient) {
- STORM_LOG_THROW(!keepRewards || !model.hasTransitionRewards(), storm::exceptions::IllegalFunctionCallException, "Bisimulation is currently only supported for models without transition rewards.");
- STORM_LOG_THROW(!weak || !bounded, storm::exceptions::IllegalFunctionCallException, "Weak bisimulation does not preserve bounded properties.");
+ DeterministicModelBisimulationDecomposition<ValueType>::DeterministicModelBisimulationDecomposition(storm::models::Ctmc<ValueType> const& model, Options const& options) {
+ STORM_LOG_THROW(!model.hasTransitionRewards(), storm::exceptions::IllegalFunctionCallException, "Bisimulation is currently only supported for models without transition rewards. Consider converting the transition rewards to state rewards (via suitable function calls).");
+ STORM_LOG_THROW(!options.weak || !options.bounded, storm::exceptions::IllegalFunctionCallException, "Weak bisimulation cannot preserve bounded properties.");
storm::storage::SparseMatrix<ValueType> backwardTransitions = model.getBackwardTransitions();
- BisimulationType bisimulationType = weak ? BisimulationType::WeakCtmc : BisimulationType::Strong;
- Partition initialPartition = getMeasureDrivenInitialPartition(model, backwardTransitions, phiLabel, psiLabel, bisimulationType, keepRewards, bounded);
- partitionRefinement(model, std::set<std::string>({phiLabel, psiLabel}), model.getBackwardTransitions(), initialPartition, bisimulationType, keepRewards, buildQuotient);
+ BisimulationType bisimulationType = options.weak ? BisimulationType::WeakCtmc : BisimulationType::Strong;
+
+ std::set<std::string> atomicPropositions;
+ if (options.respectedAtomicPropositions) {
+ atomicPropositions = options.respectedAtomicPropositions.get();
+ } else {
+ atomicPropositions = model.getStateLabeling().getAtomicPropositions();
+ }
+
+ Partition initialPartition;
+ if (options.measureDrivenInitialPartition) {
+ STORM_LOG_THROW(options.phiStateFormula, storm::exceptions::InvalidOptionException, "Unable to compute measure-driven initial partition without phi and psi states.");
+ STORM_LOG_THROW(options.psiStateFormula, storm::exceptions::InvalidOptionException, "Unable to compute measure-driven initial partition without phi and psi states.");
+ initialPartition = getMeasureDrivenInitialPartition(model, backwardTransitions, options.phiStateFormula.get(), options.psiStateFormula.get(), bisimulationType, options.keepRewards, options.bounded);
+ } else {
+ initialPartition = getLabelBasedInitialPartition(model, backwardTransitions, bisimulationType, atomicPropositions, options.keepRewards);
+ }
+
+ partitionRefinement(model, atomicPropositions, backwardTransitions, initialPartition, bisimulationType, options.keepRewards, options.buildQuotient);
}
template<typename ValueType>
@@ -683,15 +751,11 @@ namespace storm {
if (oldBlock.isAbsorbing()) {
builder.addNextValue(blockIndex, blockIndex, storm::utility::constantOne<ValueType>());
- if (oldBlock.hasLabel()) {
- newLabeling.addAtomicPropositionToState(oldBlock.getLabel(), blockIndex);
- } else {
- // Otherwise add all atomic propositions to the equivalence class that the representative state
- // satisfies.
- for (auto const& ap : atomicPropositions) {
- if (model.getStateLabeling().getStateHasAtomicProposition(ap, representativeState)) {
- newLabeling.addAtomicPropositionToState(ap, blockIndex);
- }
+ // Otherwise add all atomic propositions to the equivalence class that the representative state
+ // satisfies.
+ for (auto const& ap : atomicPropositions) {
+ if (model.getStateLabeling().getStateHasAtomicProposition(ap, representativeState)) {
+ newLabeling.addAtomicPropositionToState(ap, blockIndex);
}
}
} else {
@@ -722,16 +786,11 @@ namespace storm {
}
}
- // If the block has a special label, we only add that to the block.
- if (oldBlock.hasLabel()) {
- newLabeling.addAtomicPropositionToState(oldBlock.getLabel(), blockIndex);
- } else {
- // Otherwise add all atomic propositions to the equivalence class that the representative state
- // satisfies.
- for (auto const& ap : atomicPropositions) {
- if (model.getStateLabeling().getStateHasAtomicProposition(ap, representativeState)) {
- newLabeling.addAtomicPropositionToState(ap, blockIndex);
- }
+ // Otherwise add all atomic propositions to the equivalence class that the representative state
+ // satisfies.
+ for (auto const& ap : atomicPropositions) {
+ if (model.getStateLabeling().getStateHasAtomicProposition(ap, representativeState)) {
+ newLabeling.addAtomicPropositionToState(ap, blockIndex);
}
}
}
@@ -757,17 +816,17 @@ namespace storm {
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) {
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.
std::chrono::high_resolution_clock::time_point refinementStart = std::chrono::high_resolution_clock::now();
std::deque<Block*> splitterQueue;
std::for_each(partition.getBlocks().begin(), partition.getBlocks().end(), [&] (Block& a) { splitterQueue.push_back(&a); a.markAsSplitter(); });
-
+
// Then perform the actual splitting until there are no more splitters.
while (!splitterQueue.empty()) {
// Optionally: sort the splitter queue according to some criterion (here: prefer small splitters).
std::sort(splitterQueue.begin(), splitterQueue.end(), [] (Block const* b1, Block const* b2) { return b1->getNumberOfStates() < b2->getNumberOfStates(); } );
-
+
// Get and prepare the next splitter.
Block* splitter = splitterQueue.front();
splitterQueue.pop_front();
@@ -777,7 +836,7 @@ namespace storm {
refinePartition(model.getTransitionMatrix(), backwardTransitions, *splitter, partition, bisimulationType, splitterQueue);
}
std::chrono::high_resolution_clock::duration refinementTime = std::chrono::high_resolution_clock::now() - refinementStart;
-
+
// Now move the states from the internal partition into their final place in the decomposition. We do so in
// a way that maintains the block IDs as indices.
std::chrono::high_resolution_clock::time_point extractionStart = std::chrono::high_resolution_clock::now();
@@ -790,12 +849,12 @@ namespace storm {
std::function<storm::storage::sparse::state_type(std::pair<storm::storage::sparse::state_type, ValueType> const&)> projection = [](std::pair<storm::storage::sparse::state_type, ValueType> const& a) -> storm::storage::sparse::state_type { return a.first; };
this->blocks[block.getId()] = block_type(boost::make_transform_iterator(partition.getBegin(block), projection), boost::make_transform_iterator(partition.getEnd(block), projection), true);
}
-
+
// If we are required to build the quotient model, do so now.
if (buildQuotient) {
this->buildQuotient(model, atomicPropositions, partition, bisimulationType, keepRewards);
}
-
+
std::chrono::high_resolution_clock::duration extractionTime = std::chrono::high_resolution_clock::now() - extractionStart;
std::chrono::high_resolution_clock::duration totalTime = std::chrono::high_resolution_clock::now() - totalStart;
@@ -1007,7 +1066,7 @@ namespace storm {
typename std::vector<std::pair<storm::storage::sparse::state_type, ValueType>>::const_iterator end = partition.getStatesAndValues().begin() + block.getBegin() - 1;
storm::storage::sparse::state_type currentIndex = block.getOriginalBegin();
result.push_back(currentIndex);
-
+
// Now we can check whether the block needs to be split, which is the case iff the probabilities for the
// first and the last state are different.
while (!comparator.isEqual(begin->second, end->second)) {
@@ -1022,7 +1081,7 @@ namespace storm {
++begin;
++currentIndex;
}
-
+
// Remember the index at which the probabilities were different.
result.push_back(currentIndex);
}
@@ -1115,7 +1174,7 @@ namespace storm {
storm::storage::sparse::state_type predecessor = predecessorEntry.getColumn();
Block& predecessorBlock = partition.getBlock(predecessor);
storm::storage::sparse::state_type predecessorPosition = partition.getPosition(predecessor);
-
+
if (predecessorPosition >= predecessorBlock.getBegin()) {
partition.swapStatesAtPositions(predecessorPosition, predecessorBlock.getBegin());
predecessorBlock.incrementBegin();
@@ -1130,7 +1189,7 @@ namespace storm {
}
}
}
-
+
if (bisimulationType == BisimulationType::Strong || bisimulationType == BisimulationType::WeakCtmc) {
std::list<Block*> blocksToSplit;
@@ -1181,7 +1240,7 @@ namespace storm {
partition.setSilentProbabilities(partition.getStatesAndValues().begin() + splitter.getOriginalBegin(), partition.getStatesAndValues().begin() + splitter.getBegin());
partition.setSilentProbabilitiesToZero(partition.getStatesAndValues().begin() + splitter.getBegin(), partition.getStatesAndValues().begin() + splitter.getEnd());
}
-
+
// Now refine all predecessor blocks in a weak manner. That is, we split according to the criterion of
// weak bisimulation.
for (auto blockPtr : predecessorBlocks) {
@@ -1194,7 +1253,7 @@ namespace storm {
// Restore the begin of the block.
block.setBegin(block.getOriginalBegin());
}
-
+
block.unmarkAsPredecessorBlock();
block.resetMarkedPosition();
}
@@ -1205,9 +1264,13 @@ namespace storm {
template<typename ValueType>
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, BisimulationType bisimulationType, bool keepRewards, 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));
- Partition partition(model.getNumberOfStates(), statesWithProbability01.first, bounded || keepRewards ? model.getLabeledStates(psiLabel) : statesWithProbability01.second, phiLabel, psiLabel, bisimulationType == BisimulationType::WeakDtmc);
+ typename DeterministicModelBisimulationDecomposition<ValueType>::Partition DeterministicModelBisimulationDecomposition<ValueType>::getMeasureDrivenInitialPartition(ModelType const& model, storm::storage::SparseMatrix<ValueType> const& backwardTransitions, std::shared_ptr<storm::logic::Formula const> const& phiStateFormula, std::shared_ptr<storm::logic::Formula const> const& psiStateFormula, BisimulationType bisimulationType, bool keepRewards, bool bounded) {
+ storm::modelchecker::SparsePropositionalModelChecker<ValueType> checker(model);
+ std::unique_ptr<storm::modelchecker::CheckResult> phiStates = checker.check(*phiStateFormula);
+ std::unique_ptr<storm::modelchecker::CheckResult> psiStates = checker.check(*psiStateFormula);
+
+ std::pair<storm::storage::BitVector, storm::storage::BitVector> statesWithProbability01 = storm::utility::graph::performProb01(backwardTransitions, phiStates->asExplicitQualitativeCheckResult().getTruthValuesVector(), psiStates->asExplicitQualitativeCheckResult().getTruthValuesVector());
+ Partition partition(model.getNumberOfStates(), statesWithProbability01.first, bounded || keepRewards ? psiStates->asExplicitQualitativeCheckResult().getTruthValuesVector() : statesWithProbability01.second, bisimulationType == BisimulationType::WeakDtmc);
// If the model has state rewards, we need to consider them, because otherwise reward properties are not
// preserved.
diff --git a/src/storage/DeterministicModelBisimulationDecomposition.h b/src/storage/DeterministicModelBisimulationDecomposition.h
index 3fb4331fd..03dc4f444 100644
--- a/src/storage/DeterministicModelBisimulationDecomposition.h
+++ b/src/storage/DeterministicModelBisimulationDecomposition.h
@@ -6,6 +6,7 @@
#include "src/storage/sparse/StateType.h"
#include "src/storage/Decomposition.h"
+#include "src/logic/Formulas.h"
#include "src/models/Dtmc.h"
#include "src/models/Ctmc.h"
#include "src/storage/Distribution.h"
@@ -21,53 +22,62 @@ namespace storm {
template <typename ValueType>
class DeterministicModelBisimulationDecomposition : public Decomposition<StateBlock> {
public:
- /*!
- * Decomposes the given DTMC into equivalence classes under weak or strong bisimulation.
- *
- * @param model The model to decompose.
- * @param A set of atomic propositions that is to be respected. If not given, all atomic propositions of the
- * model will be respected. If built, the quotient model will only contain the respected atomic propositions.
- * @param weak A flag indication whether a weak bisimulation is to be computed.
- * @param buildQuotient Sets whether or not the quotient model is to be built.
- */
- DeterministicModelBisimulationDecomposition(storm::models::Dtmc<ValueType> const& model, boost::optional<std::set<std::string>> const& atomicPropositions = boost::optional<std::set<std::string>>(), bool keepRewards = true, bool weak = false, bool buildQuotient = false);
+ // A class that offers the possibility to customize the bisimulation.
+ struct Options {
+ // Creates an object representing the default values for all options.
+ Options();
- /*!
- * Decomposes the given CTMC into equivalence classes under weak or strong bisimulation.
- *
- * @param model The model to decompose.
- * @param A set of atomic propositions that is to be respected. If not given, all atomic propositions of the
- * model will be respected. If built, the quotient model will only contain the respected atomic propositions.
- * @param weak A flag indication whether a weak bisimulation is to be computed.
- * @param buildQuotient Sets whether or not the quotient model is to be built.
- */
- DeterministicModelBisimulationDecomposition(storm::models::Ctmc<ValueType> const& model, boost::optional<std::set<std::string>> const& atomicPropositions = boost::optional<std::set<std::string>>(), bool keepRewards = true, bool weak = false, bool buildQuotient = false);
+ /*!
+ * Creates an object representing the options necessary to obtain the smallest quotient while still
+ * preserving the given formula.
+ *
+ * @param formula The formula that is to be preserved.
+ */
+ Options(storm::logic::Formula const& formula);
+
+ // 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
+ // measure driven initial partition wrt. to the states phi and psi is taken.
+ bool measureDrivenInitialPartition;
+ boost::optional<std::shared_ptr<storm::logic::Formula const>> phiStateFormula;
+ boost::optional<std::shared_ptr<storm::logic::Formula const>> psiStateFormula;
+
+ // 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;
+
+ // 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;
+
+ // A flag that indicates whether a strong or a weak bisimulation is to be computed.
+ bool weak;
+
+ // 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;
+
+ // A flag that governs whether the quotient model is actually built or only the decomposition is computed.
+ bool buildQuotient;
+ };
/*!
- * Decomposes the given DTMC into equivalence classes under strong bisimulation in a way that onle safely
- * preserves formulas of the form phi until psi.
+ * Decomposes the given DTMC into equivalance classes of a bisimulation. Which kind of bisimulation is
+ * computed, is customizable via the given options.
*
* @param model The model to decompose.
- * @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 weak A flag indication whether a weak bisimulation is to be computed.
- * @param bounded If set to true, also bounded until formulas are preserved.
- * @param buildQuotient Sets whether or not the quotient model is to be built.
+ * @param options The options that customize the computed bisimulation.
*/
- DeterministicModelBisimulationDecomposition(storm::models::Dtmc<ValueType> const& model, std::string const& phiLabel, std::string const& psiLabel, bool keepRewards, bool weak, bool bounded, bool buildQuotient = false);
+ DeterministicModelBisimulationDecomposition(storm::models::Dtmc<ValueType> const& model, Options const& options = Options());
/*!
- * Decomposes the given CTMC into equivalence classes under strong bisimulation in a way that onle safely
- * preserves formulas of the form phi until psi.
+ * Decomposes the given CTMC into equivalance classes of a bisimulation. Which kind of bisimulation is
+ * computed, is customizable via the given options.
*
* @param model The model to decompose.
- * @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 weak A flag indication whether a weak bisimulation is to be computed.
- * @param bounded If set to true, also bounded until formulas are preserved.
- * @param buildQuotient Sets whether or not the quotient model is to be built.
+ * @param options The options that customize the computed bisimulation.
*/
- DeterministicModelBisimulationDecomposition(storm::models::Ctmc<ValueType> const& model, std::string const& phiLabel, std::string const& psiLabel, bool keepRewards, bool weak, bool bounded, bool buildQuotient = false);
+ DeterministicModelBisimulationDecomposition(storm::models::Ctmc<ValueType> const& model, Options const& options = Options());
/*!
* Retrieves the quotient of the model under the previously computed bisimulation.
@@ -87,7 +97,7 @@ namespace storm {
typedef typename std::list<Block>::const_iterator const_iterator;
// Creates a new block with the given begin and end.
- Block(storm::storage::sparse::state_type begin, storm::storage::sparse::state_type end, Block* prev, Block* next, std::size_t id, std::shared_ptr<std::string> const& label = nullptr);
+ Block(storm::storage::sparse::state_type begin, storm::storage::sparse::state_type end, Block* prev, Block* next, std::size_t id);
// Prints the block.
void print(Partition const& partition) const;
@@ -191,15 +201,6 @@ namespace storm {
// Retrieves whether the block is to be interpreted as absorbing.
bool isAbsorbing() const;
- // Retrieves whether the block has a special label.
- bool hasLabel() const;
-
- // Retrieves the special label of the block if it has one.
- std::string const& getLabel() const;
-
- // Retrieves a pointer to the label of the block (which is the nullptr if there is none).
- std::shared_ptr<std::string> const& getLabelPtr() const;
-
private:
// An iterator to itself. This is needed to conveniently insert elements in the overall list of blocks
// kept by the partition.
@@ -227,9 +228,6 @@ namespace storm {
// The ID of the block. This is only used for debugging purposes.
std::size_t id;
-
- // The label of the block or nullptr if it has none.
- std::shared_ptr<std::string> label;
};
class Partition {
@@ -252,11 +250,9 @@ namespace storm {
* @param numberOfStates The number of states the partition holds.
* @param prob0States The states which have probability 0 of satisfying phi until psi.
* @param prob1States The states which have probability 1 of satisfying phi until psi.
- * @param otherLabel The label that is to be attached to all other states.
- * @param prob1Label The label that is to be attached to all states with probability 1.
* @param keepSilentProbabilities A flag indicating whether or not silent probabilities are to be tracked.
*/
- Partition(std::size_t numberOfStates, storm::storage::BitVector const& prob0States, storm::storage::BitVector const& prob1States, std::string const& otherLabel, std::string const& prob1Label, bool keepSilentProbabilities = false);
+ Partition(std::size_t numberOfStates, storm::storage::BitVector const& prob0States, storm::storage::BitVector const& prob1States, bool keepSilentProbabilities = false);
Partition() = default;
Partition(Partition const& other) = default;
@@ -468,15 +464,15 @@ namespace storm {
* @param model The model whose state space is partitioned based on reachability of psi states from phi
* states.
* @param backwardTransitions The backward transitions of 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 phiStateFormula The formula that defines the phi states in the model.
+ * @param psiStateFormula The formula that defines the psi states in the model.
* @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
* reachability queries.
* @return The resulting partition.
*/
template<typename ModelType>
- Partition getMeasureDrivenInitialPartition(ModelType const& model, storm::storage::SparseMatrix<ValueType> const& backwardTransitions, std::string const& phiLabel, std::string const& psiLabel, BisimulationType bisimulationType, bool keepRewards = true, bool bounded = false);
+ Partition getMeasureDrivenInitialPartition(ModelType const& model, storm::storage::SparseMatrix<ValueType> const& backwardTransitions, std::shared_ptr<storm::logic::Formula const> const& phiStateFormula, std::shared_ptr<storm::logic::Formula const> const& psiStateFormula, BisimulationType bisimulationType, bool keepRewards = true, bool bounded = false);
/*!
* Creates the initial partition based on all the labels in the given model.
diff --git a/src/utility/cli.h b/src/utility/cli.h
index 07fb2fbd5..195a4c0be 100644
--- a/src/utility/cli.h
+++ b/src/utility/cli.h
@@ -293,7 +293,10 @@ namespace storm {
}
std::cout << "Performing bisimulation minimization... ";
- storm::storage::DeterministicModelBisimulationDecomposition<double> bisimulationDecomposition(*dtmc, boost::optional<std::set<std::string>>(), true, storm::settings::bisimulationSettings().isWeakBisimulationSet(), true);
+ typename storm::storage::DeterministicModelBisimulationDecomposition<double>::Options options;
+ options.weak = storm::settings::bisimulationSettings().isWeakBisimulationSet();
+
+ storm::storage::DeterministicModelBisimulationDecomposition<double> bisimulationDecomposition(*dtmc, options);
model = bisimulationDecomposition.getQuotient();
std::cout << "done." << std::endl << std::endl;
}
diff --git a/test/functional/storage/DeterministicModelBisimulationDecompositionTest.cpp b/test/functional/storage/DeterministicModelBisimulationDecompositionTest.cpp
index ffe337d31..4a8f5f143 100644
--- a/test/functional/storage/DeterministicModelBisimulationDecompositionTest.cpp
+++ b/test/functional/storage/DeterministicModelBisimulationDecompositionTest.cpp
@@ -9,7 +9,7 @@ TEST(DeterministicModelBisimulationDecomposition, Die) {
ASSERT_EQ(abstractModel->getType(), storm::models::DTMC);
std::shared_ptr<storm::models::Dtmc<double>> dtmc = abstractModel->as<storm::models::Dtmc<double>>();
- storm::storage::DeterministicModelBisimulationDecomposition<double> bisim(*dtmc, boost::optional<std::set<std::string>>(), true, false, true);
+ storm::storage::DeterministicModelBisimulationDecomposition<double> bisim(*dtmc);
std::shared_ptr<storm::models::AbstractModel<double>> result;
ASSERT_NO_THROW(result = bisim.getQuotient());
@@ -17,14 +17,20 @@ TEST(DeterministicModelBisimulationDecomposition, Die) {
EXPECT_EQ(13, result->getNumberOfStates());
EXPECT_EQ(20, result->getNumberOfTransitions());
- storm::storage::DeterministicModelBisimulationDecomposition<double> bisim2(*dtmc, std::set<std::string>({"one"}), true, false, true);
+ typename storm::storage::DeterministicModelBisimulationDecomposition<double>::Options options;
+ options.respectedAtomicPropositions = std::set<std::string>({"one"});
+
+ storm::storage::DeterministicModelBisimulationDecomposition<double> bisim2(*dtmc, options);
ASSERT_NO_THROW(result = bisim2.getQuotient());
EXPECT_EQ(storm::models::DTMC, result->getType());
EXPECT_EQ(5, result->getNumberOfStates());
EXPECT_EQ(8, result->getNumberOfTransitions());
+
+ options.bounded = false;
+ options.weak = true;
- storm::storage::DeterministicModelBisimulationDecomposition<double> bisim3(*dtmc, std::set<std::string>({"one"}), true, true, true);
+ storm::storage::DeterministicModelBisimulationDecomposition<double> bisim3(*dtmc, options);
ASSERT_NO_THROW(result = bisim3.getQuotient());
EXPECT_EQ(storm::models::DTMC, result->getType());
@@ -38,7 +44,7 @@ TEST(DeterministicModelBisimulationDecomposition, Crowds) {
ASSERT_EQ(abstractModel->getType(), storm::models::DTMC);
std::shared_ptr<storm::models::Dtmc<double>> dtmc = abstractModel->as<storm::models::Dtmc<double>>();
- storm::storage::DeterministicModelBisimulationDecomposition<double> bisim(*dtmc, boost::optional<std::set<std::string>>(), true, false, true);
+ storm::storage::DeterministicModelBisimulationDecomposition<double> bisim(*dtmc);
std::shared_ptr<storm::models::AbstractModel<double>> result;
ASSERT_NO_THROW(result = bisim.getQuotient());
@@ -46,14 +52,20 @@ TEST(DeterministicModelBisimulationDecomposition, Crowds) {
EXPECT_EQ(334, result->getNumberOfStates());
EXPECT_EQ(546, result->getNumberOfTransitions());
- storm::storage::DeterministicModelBisimulationDecomposition<double> bisim2(*dtmc, std::set<std::string>({"observe0Greater1"}), true, false, true);
+ typename storm::storage::DeterministicModelBisimulationDecomposition<double>::Options options;
+ options.respectedAtomicPropositions = std::set<std::string>({"observe0Greater1"});
+
+ storm::storage::DeterministicModelBisimulationDecomposition<double> bisim2(*dtmc, options);
ASSERT_NO_THROW(result = bisim2.getQuotient());
EXPECT_EQ(storm::models::DTMC, result->getType());
EXPECT_EQ(65, result->getNumberOfStates());
EXPECT_EQ(105, result->getNumberOfTransitions());
- storm::storage::DeterministicModelBisimulationDecomposition<double> bisim3(*dtmc, std::set<std::string>({"observe0Greater1"}), true, true, true);
+ options.bounded = false;
+ options.weak = true;
+
+ storm::storage::DeterministicModelBisimulationDecomposition<double> bisim3(*dtmc, options);
ASSERT_NO_THROW(result = bisim3.getQuotient());
EXPECT_EQ(storm::models::DTMC, result->getType());
From ed4f1bb7cfc185da79c361e2f8eee4075fbd04a3 Mon Sep 17 00:00:00 2001
From: dehnert <dehnert@cs.rwth-aachen.de>
Date: Fri, 30 Jan 2015 22:59:26 +0100
Subject: [PATCH 5/5] Added the possibility to build the bisimulation options
from a formula in the sense that it automatically picks suitable settings for
the formula.
Former-commit-id: 932c7d899a2a70a5a631b63fe7122a599adc67c3
---
...ministicModelBisimulationDecomposition.cpp | 65 +++++++++++++------
...erministicModelBisimulationDecomposition.h | 32 +++++++--
...sticModelBisimulationDecompositionTest.cpp | 41 ++++++++++++
3 files changed, 112 insertions(+), 26 deletions(-)
diff --git a/src/storage/DeterministicModelBisimulationDecomposition.cpp b/src/storage/DeterministicModelBisimulationDecomposition.cpp
index 1134d8904..6c8641211 100644
--- a/src/storage/DeterministicModelBisimulationDecomposition.cpp
+++ b/src/storage/DeterministicModelBisimulationDecomposition.cpp
@@ -194,6 +194,22 @@ namespace storm {
return this->absorbing;
}
+ template<typename ValueType>
+ void DeterministicModelBisimulationDecomposition<ValueType>::Block::setRepresentativeState(storm::storage::sparse::state_type representativeState) {
+ this->representativeState = representativeState;
+ }
+
+ template<typename ValueType>
+ bool DeterministicModelBisimulationDecomposition<ValueType>::Block::hasRepresentativeState() const {
+ return static_cast<bool>(representativeState);
+ }
+
+ template<typename ValueType>
+ storm::storage::sparse::state_type DeterministicModelBisimulationDecomposition<ValueType>::Block::getRepresentativeState() const {
+ STORM_LOG_THROW(representativeState, storm::exceptions::InvalidOperationException, "Unable to retrieve representative state for block.");
+ return representativeState.get();
+ }
+
template<typename ValueType>
storm::storage::sparse::state_type DeterministicModelBisimulationDecomposition<ValueType>::Block::getMarkedPosition() const {
return this->markedPosition;
@@ -249,7 +265,7 @@ namespace storm {
}
template<typename ValueType>
- DeterministicModelBisimulationDecomposition<ValueType>::Partition::Partition(std::size_t numberOfStates, storm::storage::BitVector const& prob0States, storm::storage::BitVector const& prob1States, bool keepSilentProbabilities) : numberOfBlocks(0), stateToBlockMapping(numberOfStates), statesAndValues(numberOfStates), positions(numberOfStates), keepSilentProbabilities(keepSilentProbabilities), silentProbabilities() {
+ DeterministicModelBisimulationDecomposition<ValueType>::Partition::Partition(std::size_t numberOfStates, storm::storage::BitVector const& prob0States, storm::storage::BitVector const& prob1States, boost::optional<storm::storage::sparse::state_type> representativeProb1State, bool keepSilentProbabilities) : numberOfBlocks(0), stateToBlockMapping(numberOfStates), statesAndValues(numberOfStates), positions(numberOfStates), keepSilentProbabilities(keepSilentProbabilities), silentProbabilities() {
storm::storage::sparse::state_type position = 0;
Block* firstBlock = nullptr;
Block* secondBlock = nullptr;
@@ -280,6 +296,7 @@ namespace storm {
++position;
}
secondBlock->setAbsorbing(true);
+ secondBlock->setRepresentativeState(representativeProb1State.get());
}
storm::storage::BitVector otherStates = ~(prob0States | prob1States);
@@ -577,7 +594,7 @@ namespace storm {
}
template<typename ValueType>
- DeterministicModelBisimulationDecomposition<ValueType>::Options::Options(storm::logic::Formula const& formula) : Options() {
+ DeterministicModelBisimulationDecomposition<ValueType>::Options::Options(storm::models::AbstractModel<ValueType> const& model, storm::logic::Formula const& formula) : Options() {
if (!formula.containsRewardOperator()) {
this->keepRewards = false;
}
@@ -632,13 +649,16 @@ namespace storm {
}
if (measureDrivenInitialPartition) {
- phiStateFormula = leftSubformula;
- psiStateFormula = rightSubformula;
+ storm::modelchecker::SparsePropositionalModelChecker<ValueType> checker(model);
+ std::unique_ptr<storm::modelchecker::CheckResult> phiStatesCheckResult = checker.check(*leftSubformula);
+ std::unique_ptr<storm::modelchecker::CheckResult> psiStatesCheckResult = checker.check(*rightSubformula);
+ phiStates = phiStatesCheckResult->asExplicitQualitativeCheckResult().getTruthValuesVector();
+ psiStates = psiStatesCheckResult->asExplicitQualitativeCheckResult().getTruthValuesVector();
}
}
template<typename ValueType>
- DeterministicModelBisimulationDecomposition<ValueType>::Options::Options() : measureDrivenInitialPartition(false), phiStateFormula(), psiStateFormula(), respectedAtomicPropositions(), keepRewards(true), weak(false), bounded(true), buildQuotient(true) {
+ DeterministicModelBisimulationDecomposition<ValueType>::Options::Options() : measureDrivenInitialPartition(false), phiStates(), psiStates(), respectedAtomicPropositions(), keepRewards(true), weak(false), bounded(true), buildQuotient(true) {
// Intentionally left empty.
}
@@ -658,9 +678,9 @@ namespace storm {
Partition initialPartition;
if (options.measureDrivenInitialPartition) {
- STORM_LOG_THROW(options.phiStateFormula, storm::exceptions::InvalidOptionException, "Unable to compute measure-driven initial partition without phi and psi states.");
- STORM_LOG_THROW(options.psiStateFormula, storm::exceptions::InvalidOptionException, "Unable to compute measure-driven initial partition without phi and psi states.");
- initialPartition = getMeasureDrivenInitialPartition(model, backwardTransitions, options.phiStateFormula.get(), options.psiStateFormula.get(), bisimulationType, options.keepRewards, options.bounded);
+ STORM_LOG_THROW(options.phiStates, storm::exceptions::InvalidOptionException, "Unable to compute measure-driven initial partition without phi and psi states.");
+ STORM_LOG_THROW(options.psiStates, storm::exceptions::InvalidOptionException, "Unable to compute measure-driven initial partition without phi and psi states.");
+ initialPartition = getMeasureDrivenInitialPartition(model, backwardTransitions, options.phiStates.get(), options.psiStates.get(), bisimulationType, options.keepRewards, options.bounded);
} else {
initialPartition = getLabelBasedInitialPartition(model, backwardTransitions, bisimulationType, atomicPropositions, options.keepRewards);
}
@@ -684,9 +704,9 @@ namespace storm {
Partition initialPartition;
if (options.measureDrivenInitialPartition) {
- STORM_LOG_THROW(options.phiStateFormula, storm::exceptions::InvalidOptionException, "Unable to compute measure-driven initial partition without phi and psi states.");
- STORM_LOG_THROW(options.psiStateFormula, storm::exceptions::InvalidOptionException, "Unable to compute measure-driven initial partition without phi and psi states.");
- initialPartition = getMeasureDrivenInitialPartition(model, backwardTransitions, options.phiStateFormula.get(), options.psiStateFormula.get(), bisimulationType, options.keepRewards, options.bounded);
+ STORM_LOG_THROW(options.phiStates, storm::exceptions::InvalidOptionException, "Unable to compute measure-driven initial partition without phi and psi states.");
+ STORM_LOG_THROW(options.psiStates, storm::exceptions::InvalidOptionException, "Unable to compute measure-driven initial partition without phi and psi states.");
+ initialPartition = getMeasureDrivenInitialPartition(model, backwardTransitions, options.phiStates.get(), options.psiStates.get(), bisimulationType, options.keepRewards, options.bounded);
} else {
initialPartition = getLabelBasedInitialPartition(model, backwardTransitions, bisimulationType, atomicPropositions, options.keepRewards);
}
@@ -751,8 +771,13 @@ namespace storm {
if (oldBlock.isAbsorbing()) {
builder.addNextValue(blockIndex, blockIndex, storm::utility::constantOne<ValueType>());
- // Otherwise add all atomic propositions to the equivalence class that the representative state
- // satisfies.
+ // If the block has a special representative state, we retrieve it now.
+ if (oldBlock.hasRepresentativeState()) {
+ representativeState = oldBlock.getRepresentativeState();
+ }
+
+ // Add all of the selected atomic propositions that hold in the representative state to the state
+ // representing the block.
for (auto const& ap : atomicPropositions) {
if (model.getStateLabeling().getStateHasAtomicProposition(ap, representativeState)) {
newLabeling.addAtomicPropositionToState(ap, blockIndex);
@@ -1264,13 +1289,15 @@ namespace storm {
template<typename ValueType>
template<typename ModelType>
- typename DeterministicModelBisimulationDecomposition<ValueType>::Partition DeterministicModelBisimulationDecomposition<ValueType>::getMeasureDrivenInitialPartition(ModelType const& model, storm::storage::SparseMatrix<ValueType> const& backwardTransitions, std::shared_ptr<storm::logic::Formula const> const& phiStateFormula, std::shared_ptr<storm::logic::Formula const> const& psiStateFormula, BisimulationType bisimulationType, bool keepRewards, bool bounded) {
- storm::modelchecker::SparsePropositionalModelChecker<ValueType> checker(model);
- std::unique_ptr<storm::modelchecker::CheckResult> phiStates = checker.check(*phiStateFormula);
- std::unique_ptr<storm::modelchecker::CheckResult> psiStates = checker.check(*psiStateFormula);
+ typename DeterministicModelBisimulationDecomposition<ValueType>::Partition DeterministicModelBisimulationDecomposition<ValueType>::getMeasureDrivenInitialPartition(ModelType const& model, storm::storage::SparseMatrix<ValueType> const& backwardTransitions, storm::storage::BitVector const& phiStates, storm::storage::BitVector const& psiStates, BisimulationType bisimulationType, bool keepRewards, bool bounded) {
+ std::pair<storm::storage::BitVector, storm::storage::BitVector> statesWithProbability01 = storm::utility::graph::performProb01(backwardTransitions, phiStates, psiStates);
+
+ boost::optional<storm::storage::sparse::state_type> representativePsiState;
+ if (!psiStates.empty()) {
+ representativePsiState = *psiStates.begin();
+ }
- std::pair<storm::storage::BitVector, storm::storage::BitVector> statesWithProbability01 = storm::utility::graph::performProb01(backwardTransitions, phiStates->asExplicitQualitativeCheckResult().getTruthValuesVector(), psiStates->asExplicitQualitativeCheckResult().getTruthValuesVector());
- Partition partition(model.getNumberOfStates(), statesWithProbability01.first, bounded || keepRewards ? psiStates->asExplicitQualitativeCheckResult().getTruthValuesVector() : statesWithProbability01.second, bisimulationType == BisimulationType::WeakDtmc);
+ Partition partition(model.getNumberOfStates(), statesWithProbability01.first, bounded || keepRewards ? psiStates : statesWithProbability01.second, representativePsiState, bisimulationType == BisimulationType::WeakDtmc);
// If the model has state rewards, we need to consider them, because otherwise reward properties are not
// preserved.
diff --git a/src/storage/DeterministicModelBisimulationDecomposition.h b/src/storage/DeterministicModelBisimulationDecomposition.h
index 03dc4f444..255e2c22a 100644
--- a/src/storage/DeterministicModelBisimulationDecomposition.h
+++ b/src/storage/DeterministicModelBisimulationDecomposition.h
@@ -31,16 +31,18 @@ namespace storm {
* Creates an object representing the options necessary to obtain the smallest quotient while still
* preserving the given formula.
*
+ * @param The model for which the quotient model shall be computed. This needs to be given in order to
+ * derive a suitable initial partition.
* @param formula The formula that is to be preserved.
*/
- Options(storm::logic::Formula const& formula);
+ Options(storm::models::AbstractModel<ValueType> const& model, storm::logic::Formula const& formula);
// 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
// measure driven initial partition wrt. to the states phi and psi is taken.
bool measureDrivenInitialPartition;
- boost::optional<std::shared_ptr<storm::logic::Formula const>> phiStateFormula;
- boost::optional<std::shared_ptr<storm::logic::Formula const>> psiStateFormula;
+ boost::optional<storm::storage::BitVector> phiStates;
+ boost::optional<storm::storage::BitVector> psiStates;
// 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.
@@ -201,6 +203,15 @@ namespace storm {
// Retrieves whether the block is to be interpreted as absorbing.
bool isAbsorbing() const;
+ // Sets the representative state of this block
+ void setRepresentativeState(storm::storage::sparse::state_type representativeState);
+
+ // Retrieves the representative state for this block.
+ bool hasRepresentativeState() const;
+
+ // Retrieves the representative state for this block.
+ storm::storage::sparse::state_type getRepresentativeState() const;
+
private:
// An iterator to itself. This is needed to conveniently insert elements in the overall list of blocks
// kept by the partition.
@@ -228,6 +239,10 @@ namespace storm {
// The ID of the block. This is only used for debugging purposes.
std::size_t id;
+
+ // An optional representative state for the block. If this is set, this state is used to derive the
+ // atomic propositions of the meta state in the quotient model.
+ boost::optional<storm::storage::sparse::state_type> representativeState;
};
class Partition {
@@ -250,9 +265,12 @@ namespace storm {
* @param numberOfStates The number of states the partition holds.
* @param prob0States The states which have probability 0 of satisfying phi until psi.
* @param prob1States The states which have probability 1 of satisfying phi until psi.
+ * @param representativeProb1State If the set of prob1States is non-empty, this needs to be a state
+ * that is representative for this block in the sense that the state representing this block in the quotient
+ * model will receive exactly the atomic propositions of the representative state.
* @param keepSilentProbabilities A flag indicating whether or not silent probabilities are to be tracked.
*/
- Partition(std::size_t numberOfStates, storm::storage::BitVector const& prob0States, storm::storage::BitVector const& prob1States, bool keepSilentProbabilities = false);
+ Partition(std::size_t numberOfStates, storm::storage::BitVector const& prob0States, storm::storage::BitVector const& prob1States, boost::optional<storm::storage::sparse::state_type> representativeProb1State, bool keepSilentProbabilities = false);
Partition() = default;
Partition(Partition const& other) = default;
@@ -464,15 +482,15 @@ namespace storm {
* @param model The model whose state space is partitioned based on reachability of psi states from phi
* states.
* @param backwardTransitions The backward transitions of the model.
- * @param phiStateFormula The formula that defines the phi states in the model.
- * @param psiStateFormula The formula that defines the psi states in the model.
+ * @param phiStates The phi states in the model.
+ * @param psiStates The psi states in the model.
* @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
* reachability queries.
* @return The resulting partition.
*/
template<typename ModelType>
- Partition getMeasureDrivenInitialPartition(ModelType const& model, storm::storage::SparseMatrix<ValueType> const& backwardTransitions, std::shared_ptr<storm::logic::Formula const> const& phiStateFormula, std::shared_ptr<storm::logic::Formula const> const& psiStateFormula, BisimulationType bisimulationType, bool keepRewards = true, bool bounded = false);
+ Partition getMeasureDrivenInitialPartition(ModelType const& model, storm::storage::SparseMatrix<ValueType> const& backwardTransitions, storm::storage::BitVector const& phiStates, storm::storage::BitVector const& psiStates, BisimulationType bisimulationType, bool keepRewards = true, bool bounded = false);
/*!
* Creates the initial partition based on all the labels in the given model.
diff --git a/test/functional/storage/DeterministicModelBisimulationDecompositionTest.cpp b/test/functional/storage/DeterministicModelBisimulationDecompositionTest.cpp
index 4a8f5f143..196cde5b8 100644
--- a/test/functional/storage/DeterministicModelBisimulationDecompositionTest.cpp
+++ b/test/functional/storage/DeterministicModelBisimulationDecompositionTest.cpp
@@ -36,6 +36,16 @@ TEST(DeterministicModelBisimulationDecomposition, Die) {
EXPECT_EQ(storm::models::DTMC, result->getType());
EXPECT_EQ(5, result->getNumberOfStates());
EXPECT_EQ(8, result->getNumberOfTransitions());
+
+ auto labelFormula = std::make_shared<storm::logic::AtomicLabelFormula>("one");
+ auto eventuallyFormula = std::make_shared<storm::logic::EventuallyFormula>(labelFormula);
+
+ typename storm::storage::DeterministicModelBisimulationDecomposition<double>::Options options2(*dtmc, *eventuallyFormula);
+ storm::storage::DeterministicModelBisimulationDecomposition<double> bisim4(*dtmc, options2);
+ ASSERT_NO_THROW(result = bisim4.getQuotient());
+ EXPECT_EQ(storm::models::DTMC, result->getType());
+ EXPECT_EQ(5, result->getNumberOfStates());
+ EXPECT_EQ(8, result->getNumberOfTransitions());
}
TEST(DeterministicModelBisimulationDecomposition, Crowds) {
@@ -71,4 +81,35 @@ TEST(DeterministicModelBisimulationDecomposition, Crowds) {
EXPECT_EQ(storm::models::DTMC, result->getType());
EXPECT_EQ(43, result->getNumberOfStates());
EXPECT_EQ(83, result->getNumberOfTransitions());
+
+ auto labelFormula = std::make_shared<storm::logic::AtomicLabelFormula>("observe0Greater1");
+ auto eventuallyFormula = std::make_shared<storm::logic::EventuallyFormula>(labelFormula);
+
+ typename storm::storage::DeterministicModelBisimulationDecomposition<double>::Options options2(*dtmc, *eventuallyFormula);
+ storm::storage::DeterministicModelBisimulationDecomposition<double> bisim4(*dtmc, options2);
+ ASSERT_NO_THROW(result = bisim4.getQuotient());
+
+ EXPECT_EQ(storm::models::DTMC, result->getType());
+ EXPECT_EQ(64, result->getNumberOfStates());
+ EXPECT_EQ(104, result->getNumberOfTransitions());
+
+ auto probabilityOperatorFormula = std::make_shared<storm::logic::ProbabilityOperatorFormula>(eventuallyFormula);
+
+ typename storm::storage::DeterministicModelBisimulationDecomposition<double>::Options options3(*dtmc, *probabilityOperatorFormula);
+ storm::storage::DeterministicModelBisimulationDecomposition<double> bisim5(*dtmc, options3);
+ ASSERT_NO_THROW(result = bisim5.getQuotient());
+
+ EXPECT_EQ(storm::models::DTMC, result->getType());
+ EXPECT_EQ(64, result->getNumberOfStates());
+ EXPECT_EQ(104, result->getNumberOfTransitions());
+
+ auto boundedUntilFormula = std::make_shared<storm::logic::BoundedUntilFormula>(std::make_shared<storm::logic::BooleanLiteralFormula>(true), labelFormula, 50);
+
+ typename storm::storage::DeterministicModelBisimulationDecomposition<double>::Options options4(*dtmc, *boundedUntilFormula);
+ storm::storage::DeterministicModelBisimulationDecomposition<double> bisim6(*dtmc, options4);
+ ASSERT_NO_THROW(result = bisim6.getQuotient());
+
+ EXPECT_EQ(storm::models::DTMC, result->getType());
+ EXPECT_EQ(65, result->getNumberOfStates());
+ EXPECT_EQ(105, result->getNumberOfTransitions());
}