From 8bded41867ae39c57902f052c4fca59702b9571e Mon Sep 17 00:00:00 2001 From: Jip Spel Date: Fri, 14 Sep 2018 13:00:12 +0200 Subject: [PATCH] Add state to lattice when there are more than 2 outgoing transitions --- src/storm-pars/analysis/LatticeExtender.cpp | 20 +++++++++++++++++++- 1 file changed, 19 insertions(+), 1 deletion(-) diff --git a/src/storm-pars/analysis/LatticeExtender.cpp b/src/storm-pars/analysis/LatticeExtender.cpp index d62a0a696..a0448ce42 100644 --- a/src/storm-pars/analysis/LatticeExtender.cpp +++ b/src/storm-pars/analysis/LatticeExtender.cpp @@ -147,7 +147,25 @@ namespace storm { return std::make_tuple(lattice, successor1, successor2); } } else if (check && successors.getNumberOfSetBits() > 2) { - // TODO + for (auto i = successors.getNextSetIndex(0); i < successors.size(); i = successors.getNextSetIndex(i+1)) { + for (auto j = successors.getNextSetIndex(i+1); j < successors.size(); j = successors.getNextSetIndex(j+1)) { + if (lattice->compare(i,j) == storm::analysis::Lattice::UNKNOWN) { + return std::make_tuple(lattice, i, j); + } + } + } + + auto highest = successors.getNextSetIndex(0); + auto lowest = highest; + for (auto i = successors.getNextSetIndex(highest+1); i < successors.size(); i = successors.getNextSetIndex(i+1)) { + if (lattice->compare(i, highest) == storm::analysis::Lattice::ABOVE) { + highest = i; + } + if (lattice->compare(lowest, i) == storm::analysis::Lattice::ABOVE) { + lowest = i; + } + } + lattice->addBetween(stateNumber, lattice->getNode(highest), lattice->getNode(lowest)); } } // Nothing changed and not done yet