From 2484a515a0112cd26a8c6089eb3dd1ee7ae294e8 Mon Sep 17 00:00:00 2001
From: dehnert <dehnert@cs.rwth-aachen.de>
Date: Tue, 27 Oct 2015 23:30:51 +0100
Subject: [PATCH] some more work on bisim
Former-commit-id: aaa8088b009de8b1f0469cc2171b2821f1c6656e
---
src/models/sparse/StandardRewardModel.cpp | 4 +++-
.../bisimulation/BisimulationDecomposition.cpp | 15 +++++++++------
src/storage/bisimulation/Block.cpp | 2 +-
...terministicModelBisimulationDecomposition.cpp | 16 ++++++++--------
src/storage/bisimulation/Partition.cpp | 6 +++---
src/utility/storm.h | 1 +
6 files changed, 25 insertions(+), 19 deletions(-)
diff --git a/src/models/sparse/StandardRewardModel.cpp b/src/models/sparse/StandardRewardModel.cpp
index 1f7db2b79..fe63c4b78 100644
--- a/src/models/sparse/StandardRewardModel.cpp
+++ b/src/models/sparse/StandardRewardModel.cpp
@@ -147,6 +147,7 @@ namespace storm {
if (this->hasTransitionRewards()) {
if (this->hasStateActionRewards()) {
storm::utility::vector::addVectors<ValueType>(this->getStateActionRewardVector(), transitionMatrix.getPointwiseProductRowSumVector(this->getTransitionRewardMatrix()), this->getStateActionRewardVector());
+ optionalStateActionRewardVector = boost::none;
} else {
this->optionalStateActionRewardVector = transitionMatrix.getPointwiseProductRowSumVector(this->getTransitionRewardMatrix());
}
@@ -157,8 +158,9 @@ namespace storm {
STORM_LOG_THROW(this->getStateRewardVector().size() == this->getStateActionRewardVector().size(), storm::exceptions::InvalidOperationException, "The reduction to state rewards is only possible of both the state and the state-action rewards have the same dimension.");
storm::utility::vector::addVectors<ValueType>(this->getStateActionRewardVector(), this->getStateRewardVector(), this->getStateRewardVector());
} else {
- this->optionalStateRewardVector = std::move(this->optionalStateRewardVector);
+ this->optionalStateRewardVector = std::move(this->optionalStateActionRewardVector);
}
+ optionalStateActionRewardVector = boost::none;
}
}
diff --git a/src/storage/bisimulation/BisimulationDecomposition.cpp b/src/storage/bisimulation/BisimulationDecomposition.cpp
index 120f88f88..d550c510c 100644
--- a/src/storage/bisimulation/BisimulationDecomposition.cpp
+++ b/src/storage/bisimulation/BisimulationDecomposition.cpp
@@ -28,7 +28,10 @@ namespace storm {
template<typename ModelType>
BisimulationDecomposition<ModelType>::Options::Options(ModelType const& model, std::vector<std::shared_ptr<storm::logic::Formula>> const& formulas) : Options() {
- if (formulas.size() == 1) {
+ if (formulas.empty()) {
+ this->respectedAtomicPropositions = model.getStateLabeling().getLabels();
+ this->keepRewards = true;
+ } if (formulas.size() == 1) {
this->preserveSingleFormula(model, *formulas.front());
} else {
for (auto const& formula : formulas) {
@@ -202,7 +205,7 @@ namespace storm {
splitter->unmarkAsSplitter();
// Now refine the partition using the current splitter.
- std::cout << "refining based on splitter " << splitter->getId() << std::endl;
+// std::cout << "refining based on splitter " << splitter->getId() << std::endl;
refinePartitionBasedOnSplitter(*splitter, splitterQueue);
}
}
@@ -236,8 +239,8 @@ namespace storm {
this->splitInitialPartitionBasedOnStateRewards();
}
- std::cout << "successfully built (label) initial partition" << std::endl;
- partition.print();
+// std::cout << "successfully built (label) initial partition" << std::endl;
+// partition.print();
}
template<typename ModelType>
@@ -257,8 +260,8 @@ namespace storm {
this->splitInitialPartitionBasedOnStateRewards();
}
- std::cout << "successfully built (measure-driven) initial partition" << std::endl;
- partition.print();
+// std::cout << "successfully built (measure-driven) initial partition" << std::endl;
+// partition.print();
}
template<typename ModelType>
diff --git a/src/storage/bisimulation/Block.cpp b/src/storage/bisimulation/Block.cpp
index 2157baeb3..2de49e62a 100644
--- a/src/storage/bisimulation/Block.cpp
+++ b/src/storage/bisimulation/Block.cpp
@@ -35,7 +35,7 @@ namespace storm {
}
void Block::setBeginIndex(storm::storage::sparse::state_type beginIndex) {
- std::cout << "setting beg index to " << beginIndex << " [" << this << "]" << std::endl;
+// std::cout << "setting beg index to " << beginIndex << " [" << this << "]" << std::endl;
this->beginIndex = beginIndex;
STORM_LOG_ASSERT(beginIndex < endIndex, "Unable to resize block to illegal size.");
}
diff --git a/src/storage/bisimulation/DeterministicModelBisimulationDecomposition.cpp b/src/storage/bisimulation/DeterministicModelBisimulationDecomposition.cpp
index 9a739cea3..565dfef91 100644
--- a/src/storage/bisimulation/DeterministicModelBisimulationDecomposition.cpp
+++ b/src/storage/bisimulation/DeterministicModelBisimulationDecomposition.cpp
@@ -29,8 +29,8 @@ namespace storm {
template<typename ModelType>
DeterministicModelBisimulationDecomposition<ModelType>::DeterministicModelBisimulationDecomposition(ModelType const& model, typename BisimulationDecomposition<ModelType>::Options const& options) : BisimulationDecomposition<ModelType>(model, options), probabilitiesToCurrentSplitter(model.getNumberOfStates(), storm::utility::zero<ValueType>()), predecessorsOfCurrentSplitter(model.getNumberOfStates()) {
- STORM_LOG_THROW(!model.hasRewardModel() || model.hasUniqueRewardModel(), storm::exceptions::IllegalFunctionCallException, "Bisimulation currently only supports models with at most one reward model.");
- STORM_LOG_THROW(!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.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.");
}
@@ -160,7 +160,7 @@ namespace storm {
template<typename ModelType>
void DeterministicModelBisimulationDecomposition<ModelType>::refinePredecessorBlocksOfSplitter(std::list<Block*>& predecessorBlocks, std::deque<bisimulation::Block*>& splitterQueue) {
for (auto block : predecessorBlocks) {
- std::cout << "splitting predecessor block " << block->getId() << " of splitter" << std::endl;
+// std::cout << "splitting predecessor block " << block->getId() << " of splitter" << std::endl;
this->partition.splitBlock(*block, [this] (storm::storage::sparse::state_type const& state1, storm::storage::sparse::state_type const& state2) {
bool firstIsPredecessor = isPredecessorOfCurrentSplitter(state1);
bool secondIsPredecessor = isPredecessorOfCurrentSplitter(state2);
@@ -175,7 +175,7 @@ namespace storm {
splitterQueue.emplace_back(&block);
});
// this->partition.print();
- std::cout << "size: " << this->partition.size() << std::endl;
+// std::cout << "size: " << this->partition.size() << std::endl;
// Remember that we have refined the block.
block->setNeedsRefinement(false);
@@ -227,10 +227,10 @@ namespace storm {
}
}
- std::cout << "probs of splitter predecessors: " << std::endl;
- for (auto state : predecessorsOfCurrentSplitter) {
- std::cout << state << " [" << this->partition.getBlock(state).getId() << "]" << " -> " << probabilitiesToCurrentSplitter[state] << std::endl;
- }
+// std::cout << "probs of splitter predecessors: " << std::endl;
+// for (auto state : predecessorsOfCurrentSplitter) {
+// std::cout << state << " [" << this->partition.getBlock(state).getId() << "]" << " -> " << probabilitiesToCurrentSplitter[state] << std::endl;
+// }
if (this->options.type == BisimulationType::Strong || this->model.getType() == storm::models::ModelType::Ctmc) {
refinePredecessorBlocksOfSplitter(predecessorBlocks, splitterQueue);
diff --git a/src/storage/bisimulation/Partition.cpp b/src/storage/bisimulation/Partition.cpp
index cf9dfa8aa..bbe45fc0a 100644
--- a/src/storage/bisimulation/Partition.cpp
+++ b/src/storage/bisimulation/Partition.cpp
@@ -142,7 +142,7 @@ namespace storm {
std::pair<std::vector<std::unique_ptr<Block>>::iterator, bool> Partition::splitBlock(Block& block, storm::storage::sparse::state_type position) {
STORM_LOG_THROW(position >= block.getBeginIndex() && position <= block.getEndIndex(), storm::exceptions::InvalidArgumentException, "Cannot split block at illegal position.");
- std::cout << "splitting " << block.getId() << " at pos " << position << " (was " << block.getBeginIndex() << " to " << block.getEndIndex() << ")" << std::endl;
+// std::cout << "splitting " << block.getId() << " at pos " << position << " (was " << block.getBeginIndex() << " to " << block.getEndIndex() << ")" << std::endl;
// In case one of the resulting blocks would be empty, we simply return the current block and do not create
// a new one.
@@ -157,7 +157,7 @@ namespace storm {
auto newBlockIt = std::prev(blocks.end());
// Resize the current block appropriately.
- std::cout << "setting begin pos of block " << block.getId() << " to " << position << std::endl;
+// std::cout << "setting begin pos of block " << block.getId() << " to " << position << std::endl;
block.setBeginIndex(position);
// Mark both blocks as splitters.
@@ -171,7 +171,7 @@ namespace storm {
}
bool Partition::splitBlock(Block& block, std::function<bool (storm::storage::sparse::state_type, storm::storage::sparse::state_type)> const& less, std::function<void (Block&)> const& newBlockCallback) {
- std::cout << "sorting the block [" << block.getId() << "]" << std::endl;
+// std::cout << "sorting the block [" << block.getId() << "]" << std::endl;
// Sort the range of the block such that all states that have the label are moved to the front.
std::sort(this->begin(block), this->end(block), less);
diff --git a/src/utility/storm.h b/src/utility/storm.h
index 2eea34738..221545743 100644
--- a/src/utility/storm.h
+++ b/src/utility/storm.h
@@ -126,6 +126,7 @@ namespace storm {
}
storm::storage::DeterministicModelBisimulationDecomposition<ModelType> bisimulationDecomposition(*model, options);
+ bisimulationDecomposition.computeBisimulationDecomposition();
model = bisimulationDecomposition.getQuotient();
std::cout << "done." << std::endl << std::endl;
return model;