From f0f74d1d0a8d347efba8e55f10623ff844a8edd5 Mon Sep 17 00:00:00 2001 From: Jip Spel Date: Wed, 24 Oct 2018 14:08:42 +0200 Subject: [PATCH] Make use of provided methods when extending the lattice --- src/storm-pars/analysis/Lattice.cpp | 16 +++------------- 1 file changed, 3 insertions(+), 13 deletions(-) diff --git a/src/storm-pars/analysis/Lattice.cpp b/src/storm-pars/analysis/Lattice.cpp index a0dc25d47..f6c6ddb05 100644 --- a/src/storm-pars/analysis/Lattice.cpp +++ b/src/storm-pars/analysis/Lattice.cpp @@ -85,17 +85,13 @@ namespace storm { assert(!addedStates[state]); auto res = compare(above, below); assert(res == ABOVE || res == UNKNOWN); + Node *newNode = new Node(); newNode->states = storm::storage::BitVector(numberOfStates); newNode->states.set(state); - setStatesAbove(newNode, above->statesAbove | above->states, false); setStatesBelow(newNode, below->statesBelow | below->states, false); - newNode->statesAbove = above->statesAbove | above->states; - newNode->statesBelow = below->statesBelow | below->states; - newNode->recentlyAddedAbove = storm::storage::BitVector(above->statesAbove | above->states); - newNode->recentlyAddedBelow = storm::storage::BitVector(below->statesBelow | below->states); setStatesBelow(above, state); setStatesAbove(below, state); @@ -134,8 +130,8 @@ namespace storm { } void Lattice::addRelationNodes(storm::analysis::Lattice::Node *above, storm::analysis::Lattice::Node * below) { - above->statesBelow |= below->states; - below->statesAbove |= above->states; + setStatesBelow(above, below->states, true); + setStatesAbove(below, above->states, true); auto nodesBelow = getNodesBelow(below); for (auto itr = nodesBelow.begin(); itr != nodesBelow.end(); ++itr) { setStatesAbove((*itr), above->states, true); @@ -208,8 +204,6 @@ namespace storm { return addedStates; } - - void Lattice::toString(std::ostream &out) { std::vector printedNodes = std::vector({}); for (auto itr = nodes.begin(); itr != nodes.end(); ++itr) { @@ -342,9 +336,5 @@ namespace storm { node->recentlyAddedBelow = storm::storage::BitVector(states); } } - - - - } }