From 8c7808b0df794e4855bc392efc0a59788055978a Mon Sep 17 00:00:00 2001 From: Jip Spel Date: Mon, 8 Oct 2018 09:09:36 +0200 Subject: [PATCH] No need to check for state breaking the SCC --- src/storm-pars/analysis/LatticeExtender.cpp | 24 +++------------------ 1 file changed, 3 insertions(+), 21 deletions(-) diff --git a/src/storm-pars/analysis/LatticeExtender.cpp b/src/storm-pars/analysis/LatticeExtender.cpp index 24058fd8a..324c8be8f 100644 --- a/src/storm-pars/analysis/LatticeExtender.cpp +++ b/src/storm-pars/analysis/LatticeExtender.cpp @@ -37,27 +37,9 @@ namespace storm { auto scc = decomposition.getBlock(i); if (scc.size() > 1) { auto states = scc.getStates(); - bool added = false; - for (auto itr = states.begin(); !added && itr != states.end(); ++itr) { - auto state = *itr; - storm::storage::BitVector subSystem = storm::storage::BitVector(model->getNumberOfStates()); - subSystem.set(states.begin(), states.end(), true); - subSystem.set(state, false); - auto subDecomposition = storm::storage::StronglyConnectedComponentDecomposition(model->getTransitionMatrix(), subSystem, false, false); - bool acyclic = true; - for (auto i = 0; acyclic && i < subDecomposition.size(); ++i) { - auto subScc = subDecomposition.getBlock(i); - acyclic = subScc.size() <= 1; - } - if (acyclic) { - initialMiddleStates.set(state); - added = true; - } - } - if (!added) { - // Add one of the states of the scc - initialMiddleStates.set(*(states.begin())); - } + // TODO: Smarter state picking + // Add one of the states of the scc + initialMiddleStates.set(*(states.begin())); } } }