← Back to branch summary

~tapaal-ltl/verifypn/loopInvariantReduction

« back to all changes in this revision

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

  • Committer: Simon Virenfeldt
  • Date: 2021-02-12 13:31:04 UTC
  • mfrom: (247.2.6 ltlmain)
  • Revision ID: simwir1@gmail.com-20210212133104-rnsedpg2b04307n5
Merge ltl-stubborn-set@253

Show diffs side-by-side

added added

removed removed

Lines of Context:
src/LTL/Algorithm/RandomNDFS.cpp
44
44
        }
45
45
 
46
46
        while (todo.top(curState)) {
47
 
 
48
47
            if (!call_stack.empty() && states.lookup(curState).second == call_stack.top()) {
49
48
                if (successorGenerator->isAccepting(curState)) {
50
49
                    seed = &curState;
55
54
                todo.pop(curState);
56
55
                call_stack.pop();
57
56
            } else {
 
57
                ++stats.expanded;
58
58
                call_stack.push(states.add(curState).second);
59
59
                if (!mark1.add(curState).first) {
60
60
                    continue;
61
61
                }
62
62
                successorGenerator->prepare(&curState);
63
63
                while (successorGenerator->next(working)) {
 
64
                    ++stats.explored;
64
65
                    auto r = states.add(working);
65
66
                    todo.push(r.second, ctx, formula);
66
67
                }
81
82
        todo.push(states.add(state).second, ctx, formula);
82
83
 
83
84
        while (todo.pop(curState)) {
 
85
            ++stats.expanded;
84
86
            if (!mark2.add(curState).first) {
85
87
                continue;
86
88
            }
87
89
 
88
90
            successorGenerator->prepare(&curState);
89
91
            while (successorGenerator->next(working)) {
 
92
                ++stats.explored;
90
93
                if (working == *seed) {
91
94
                    violation = true;
92
95
                    return;
97
100
        }
98
101
 
99
102
    }
 
103
 
 
104
    void RandomNDFS::printStats(ostream &os) {
 
105
        std::cout << "STATS:\n"
 
106
                  << "\tdiscovered states:          " << mark1.discovered() << std::endl
 
107
                  << "\tdiscovered states (nested): " << mark2.discovered() << std::endl
 
108
                  << "\tmax tokens:                 " << std::max(mark1.maxTokens(), mark2.maxTokens()) << std::endl
 
109
                  << "\texplored states:            " << stats.explored << std::endl
 
110
                  << "\texplored states (nested):   " << stats.expanded << std::endl;
 
111
    }
100
112
}
 
 
b'\\ No newline at end of file'