← Back to branch summary

~tapaal-ltl/verifypn/fire-count-heuristic

« back to all changes in this revision

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

  • Committer: Nikolaj Jensen Ulrik
  • Date: 2021-03-19 12:45:08 UTC
  • Revision ID: nikolaj@njulrik.dk-20210319124508-xztoihw9nhyx7z0v
LTL engine now allows combination of stubborn sets and heuristics

Show diffs side-by-side

added added

removed removed

Lines of Context:
src/LTL/Algorithm/TarjanModelChecker.cpp
60
60
                dtop.sucinfo.last_state = stateid;
61
61
 
62
62
                // lookup successor in 'hash' table
63
 
                auto p = chash[hash(stateid)];
64
 
                while (p != std::numeric_limits<idx_t>::max() && cstack[p].stateid != stateid) {
65
 
                    p = cstack[p].next;
 
63
                auto suc_pos = chash[hash(stateid)];
 
64
                auto marking = seen.getMarkingId(stateid);
 
65
                while (suc_pos != std::numeric_limits<idx_t>::max() && cstack[suc_pos].stateid != stateid) {
 
66
                    if constexpr (IsSpooling) {
 
67
                        if (seen.getMarkingId(cstack[suc_pos].stateid) == marking) {
 
68
                            if (extstack.empty() || suc_pos > extstack.top()) {
 
69
                                this->successorGenerator->generateAll();
 
70
                                extstack.push(cstack.size() - 1);
 
71
                            }
 
72
                        }
 
73
                    }
 
74
                    suc_pos = cstack[suc_pos].next;
66
75
                }
67
 
                if (p != std::numeric_limits<idx_t>::max()) {
 
76
                if (suc_pos != std::numeric_limits<idx_t>::max()) {
 
77
                    if constexpr (IsSpooling) {
 
78
                        if (extstack.empty() || suc_pos > extstack.top()) {
 
79
                            this->successorGenerator->generateAll();
 
80
                            extstack.push(cstack.size() - 1);
 
81
                        }
 
82
                    }
68
83
                    // we found the successor, i.e. there's a loop!
69
84
                    // now update lowlinks and check whether the loop contains an accepting state
70
 
                    update(p);
 
85
                    update(suc_pos);
71
86
                    continue;
72
87
                }
73
88
                if (store.find(stateid) == std::end(store)) {
125
140
        if (!astack.empty() && p == astack.top()) {
126
141
            astack.pop();
127
142
        }
 
143
        if (!extstack.empty() && p == extstack.top()) {
 
144
            extstack.pop();
 
145
        }
128
146
        if (!dstack.empty()) {
129
147
            update(p);
130
148
        }