Skip to content

Commit 87f77fd

Browse files
plindnercsplindnercs
committed
changed bookkeeping to BlockSets + some minor changes
1 parent b3bf878 commit 87f77fd

9 files changed

Lines changed: 39 additions & 26 deletions

‎resources/examples/testfiles/dtmc/nand-20-4.pm‎

Lines changed: 2 additions & 2 deletions
Original file line numberDiff line numberDiff line change
@@ -5,8 +5,8 @@
55

66
dtmc
77

8-
const int N = 4; // number of inputs in each bundle
9-
const int K = 1; // number of restorative stages
8+
const int N = 20; // number of inputs in each bundle
9+
const int K = 4; // number of restorative stages
1010

1111
const int M = 2*K+1; // total number of multiplexing units
1212

‎src/storm/storage/bisimulation/BisimulationDecomposition.cpp‎

Lines changed: 3 additions & 4 deletions
Original file line numberDiff line numberDiff line change
@@ -260,13 +260,12 @@ void BisimulationDecomposition<ModelType>::computeBisimulationDecomposition() {
260260
template<typename ModelType>
261261
void BisimulationDecomposition<ModelType>::performPartitionRefinement() {
262262
std::deque<typename Partition::Block> splitterQueue;
263-
std::unordered_set<uint64_t> enqueuedSplitterBlocks;
263+
bisimulation::Partition::BlockSet enqueuedSplitterBlocks;
264264

265265
// Initially, add all current blocks to the queue
266266
this->partition.forEachBlock([&](auto const& block) {
267267
splitterQueue.push_back(block);
268-
// TODO: enqueuedSplitterBlocks mit BlockSet anstatt erstem representativen Zustand
269-
enqueuedSplitterBlocks.insert(block.front());
268+
enqueuedSplitterBlocks.insert(block);
270269
});
271270

272271
uint_fast64_t iterations = 0;
@@ -275,7 +274,7 @@ void BisimulationDecomposition<ModelType>::performPartitionRefinement() {
275274

276275
auto splitterBlock = splitterQueue.front();
277276
splitterQueue.pop_front();
278-
enqueuedSplitterBlocks.erase(splitterBlock.front());
277+
enqueuedSplitterBlocks.erase(splitterBlock);
279278

280279
refinePartitionBasedOnSplitter(splitterBlock, splitterQueue, enqueuedSplitterBlocks);
281280
}

‎src/storm/storage/bisimulation/BisimulationDecomposition.h‎

Lines changed: 1 addition & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -243,7 +243,7 @@ class BisimulationDecomposition {
243243
* @param splitterBlock The splitter to use.
244244
*/
245245
virtual void refinePartitionBasedOnSplitter(std::span<uint64_t const> splitterBlock, std::deque<typename bisimulation::Partition::Block>& splitterQueue,
246-
std::unordered_set<uint64_t>& enqueuedSplitterBlocks) = 0;
246+
bisimulation::Partition::BlockSet& enqueuedSplitterBlocks) = 0;
247247

248248
/*!
249249
* Builds the quotient model based on the previously computed equivalence classes (stored in the blocks

‎src/storm/storage/bisimulation/DeterministicModelBisimulationDecomposition.cpp‎

Lines changed: 9 additions & 6 deletions
Original file line numberDiff line numberDiff line change
@@ -100,7 +100,7 @@ typename DeterministicModelBisimulationDecomposition<ModelType>::ValueType Deter
100100

101101
template<typename ModelType>
102102
void DeterministicModelBisimulationDecomposition<ModelType>::refinePartitionBasedOnSplitter(std::span<uint64_t const> splitterBlock, std::deque<typename bisimulation::Partition::Block>& splitterQueue,
103-
std::unordered_set<uint64_t>& enqueuedSplitterBlocks) {
103+
bisimulation::Partition::BlockSet& enqueuedSplitterBlocks) {
104104
storm::storage::bisimulation::Partition::BlockSet blocksToSplit;
105105

106106
// std::fill(probabilitiesToCurrentSplitter.begin(), probabilitiesToCurrentSplitter.end(), storm::utility::zero<ValueType>());
@@ -133,9 +133,11 @@ void DeterministicModelBisimulationDecomposition<ModelType>::refinePartitionBase
133133
this->partition.splitBlockByPredicate(predecessorBlockToSplit, [this]
134134
(auto const& state) { return touchedProbabilitiesToSplitter.get(state); });
135135

136-
// TODO: Change check to BlockSet (enqueuedBlocks)
137136
if (noPredecessors.size() > 0) {
138-
splitterQueue.push_back(noPredecessors);
137+
if (!enqueuedSplitterBlocks.contains(noPredecessors)) {
138+
splitterQueue.push_back(noPredecessors);
139+
enqueuedSplitterBlocks.insert(noPredecessors);
140+
}
139141
}
140142

141143
if (predecessors.size() > 0) {
@@ -147,9 +149,10 @@ void DeterministicModelBisimulationDecomposition<ModelType>::refinePartitionBase
147149
// Add all blocks that were split to splitter queue
148150
if (wasSplit) {
149151
this->partition.forEachSubBlock(predecessors, [&splitterQueue, &enqueuedSplitterBlocks](auto const& block) {
150-
// TODO: Change check to BlockSet (enqueuedBlocks)
151-
splitterQueue.push_back(block);
152-
enqueuedSplitterBlocks.insert(block.front());
152+
if (!enqueuedSplitterBlocks.contains(block)) {
153+
splitterQueue.push_back(block);
154+
enqueuedSplitterBlocks.insert(block);
155+
}
153156
});
154157
}
155158
}

‎src/storm/storage/bisimulation/DeterministicModelBisimulationDecomposition.h‎

Lines changed: 1 addition & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -38,7 +38,7 @@ class DeterministicModelBisimulationDecomposition : public BisimulationDecomposi
3838
virtual void buildQuotient() override;
3939

4040
virtual void refinePartitionBasedOnSplitter(std::span<uint64_t const> splitterBlock, std::deque<typename bisimulation::Partition::Block>& splitterQueue,
41-
std::unordered_set<uint64_t>& enqueuedSplitterBlocks) override;
41+
bisimulation::Partition::BlockSet& enqueuedSplitterBlocks) override;
4242

4343
private:
4444
// Post-processes the initial partition to properly initialize it.

‎src/storm/storage/bisimulation/NondeterministicModelBisimulationDecomposition.cpp‎

Lines changed: 1 addition & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -138,7 +138,7 @@ bool NondeterministicModelBisimulationDecomposition<ModelType>::quotientDistribu
138138

139139
template<typename ModelType>
140140
void NondeterministicModelBisimulationDecomposition<ModelType>::refinePartitionBasedOnSplitter(std::span<uint64_t const> splitterBlock, std::deque<typename bisimulation::Partition::Block>& splitterQueue,
141-
std::unordered_set<uint64_t>& enqueuedSplitterBlocks) {
141+
bisimulation::Partition::BlockSet& enqueuedSplitterBlocks) {
142142

143143
}
144144

‎src/storm/storage/bisimulation/NondeterministicModelBisimulationDecomposition.h‎

Lines changed: 1 addition & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -35,7 +35,7 @@ class NondeterministicModelBisimulationDecomposition : public BisimulationDecomp
3535
virtual void buildQuotient() override;
3636

3737
virtual void refinePartitionBasedOnSplitter(std::span<uint64_t const> splitterBlock, std::deque<typename bisimulation::Partition::Block>& splitterQueue,
38-
std::unordered_set<uint64_t>& enqueuedSplitterBlocks) override;
38+
bisimulation::Partition::BlockSet& enqueuedSplitterBlocks) override;
3939

4040
virtual void initialize() override;
4141

‎src/storm/storage/bisimulation/Partition.h‎

Lines changed: 19 additions & 8 deletions
Original file line numberDiff line numberDiff line change
@@ -26,16 +26,27 @@ class Partition {
2626
// Typedefs for readability
2727
using ElementIndex = uint64_t;
2828
using Block = std::span<ElementIndex const>;
29-
static constexpr auto BlockCompare = [](Block const& lhs, Block const& rhs) {
30-
if (lhs.data() < rhs.data()) {
31-
return true;
32-
}
33-
if (lhs.data() > rhs.data()) {
34-
return false;
29+
struct BlockCompare {
30+
bool operator()(Block const& lhs, Block const& rhs) const {
31+
if (lhs.data() < rhs.data()) {
32+
return true;
33+
}
34+
if (lhs.data() > rhs.data()) {
35+
return false;
36+
}
37+
return lhs.size() < rhs.size();
3538
}
36-
return lhs.size() < rhs.size();
3739
};
38-
using BlockSet = std::set<Block, decltype(BlockCompare)>;
40+
// static constexpr auto BlockCompare = [](Block const& lhs, Block const& rhs) {
41+
// if (lhs.data() < rhs.data()) {
42+
// return true;
43+
// }
44+
// if (lhs.data() > rhs.data()) {
45+
// return false;
46+
// }
47+
// return lhs.size() < rhs.size();
48+
// };
49+
using BlockSet = std::set<Block, BlockCompare>;
3950

4051
Partition(Partition const& other) = default;
4152
Partition& operator=(Partition const& other) = default;

‎src/test/storm/storage/DeterministicModelBisimulationDecompositionTest.cpp‎

Lines changed: 2 additions & 2 deletions
Original file line numberDiff line numberDiff line change
@@ -63,11 +63,11 @@ TEST(DeterministicModelBisimulationDecomposition, Die) {
6363
EXPECT_EQ(8ul, result->getNumberOfTransitions());
6464
}
6565

66-
TEST(DeterministicModelBisimulationDecomposition, Nand4) {
66+
TEST(DeterministicModelBisimulationDecomposition, Nand3) {
6767
std::string programFile = STORM_TEST_RESOURCES_DIR "/dtmc/nand-20-4.pm";
6868
storm::prism::Program program = storm::api::parseProgram(programFile);
6969
program = storm::utility::prism::preprocess(program, "");
70-
std::string formulasAsString = "Pmin=? [F ((s = 4) & ((z / 40) < 1/10))]";
70+
std::string formulasAsString = "Pmin=? [F ((s = 4) & ((z / 20) < 1/10))]";
7171
std::vector<std::shared_ptr<storm::logic::Formula const>> formulas =
7272
storm::api::extractFormulasFromProperties(storm::api::parsePropertiesForPrismProgram(formulasAsString, program));
7373
std::shared_ptr<storm::models::sparse::Dtmc<double>> dtmc =

0 commit comments

Comments
 (0)