Browse Source

No need to check for state breaking the SCC

tempestpy_adaptions
Jip Spel 6 years ago
parent
commit
8c7808b0df
  1. 20
      src/storm-pars/analysis/LatticeExtender.cpp

20
src/storm-pars/analysis/LatticeExtender.cpp

@ -37,30 +37,12 @@ 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<ValueType>(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) {
// TODO: Smarter state picking
// Add one of the states of the scc
initialMiddleStates.set(*(states.begin()));
}
}
}
}
template <typename ValueType>
std::tuple<storm::analysis::Lattice*, uint_fast64_t, uint_fast64_t> LatticeExtender<ValueType>::toLattice(std::vector<std::shared_ptr<storm::logic::Formula const>> formulas) {

Loading…
Cancel
Save