← Back to branch summary

~tapaal-ltl/verifypn/scc-optimise

« back to all changes in this revision

Viewing changes to src/LTL/Algorithm/NestedDepthFirstSearch.cpp

  • Committer: Nikolaj Jensen Ulrik
  • Date: 2021-02-01 09:31:31 UTC
  • Revision ID: nikolaj@njulrik.dk-20210201093131-6xfm23r9rzyr5qht
NDFS: Replace weak test with direct SCC test

Show diffs side-by-side

added added

removed removed

Lines of Context:
src/LTL/Algorithm/NestedDepthFirstSearch.cpp
77
77
    void NestedDepthFirstSearch::ndfs(State &state) {
78
78
        std::stack<StackEntry> todo;
79
79
 
 
80
        auto seed_scc = successorGenerator->scc_id(*seed);
 
81
 
80
82
        State working = factory.newState();
81
83
        State curState = factory.newState();
82
84
 
92
94
            if (!successorGenerator->next(working, top.sucinfo)) {
93
95
                todo.pop();
94
96
            } else {
95
 
                if (is_weak && !successorGenerator->isAccepting(working)) {
 
97
                if (seed_scc != successorGenerator->scc_id(working)) {
96
98
                    continue;
97
99
                }
98
100
                if (working == *seed) {