← Back to branch summary

~tapaal-ltl/verifypn/ltl-structural-reductions

« back to all changes in this revision

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

  • Committer: Nikolaj Jensen Ulrik
  • Date: 2020-10-19 12:35:11 UTC
  • Revision ID: nikolaj@njulrik.dk-20201019123511-yhxkthos6d6u1hj2
Optimizations cleanup

Show diffs side-by-side

added added

removed removed

Lines of Context:
src/LTL/LTL_algorithm/TarjanModelChecker.cpp
36
36
        State working = factory.newState();
37
37
        while (!dstack.empty() && !violation) {
38
38
            DStack &dtop = dstack.top();
39
 
            //seen.decode(working, cstack[dtop.pos].stateid);
40
39
            if (!nexttrans(working, dtop)) {
41
40
                pop();
42
41
                continue;
43
42
            }
 
43
            // get ID of transition taken (nexttrans = lasttrans + 1)
44
44
            idx_t stateid = (*dtop.neighbors)[dtop.nexttrans - 1];
45
 
            //auto res = seen.lookup(working);
46
 
            //assert((res.first && res.second == stateid) || !res.first);
47
45
 
 
46
            // lookup successor in 'hash' table
48
47
            auto p = chash[hash(stateid)];
49
48
            while (p != std::numeric_limits<idx_t>::max() && cstack[p].stateid != stateid) {
50
49
                p = cstack[p].next;
51
50
            }
52
51
            if (p != std::numeric_limits<idx_t>::max()) {
 
52
                // we found the successor! update lowlinks etc
53
53
                update(p);
54
54
                continue;
55
55
            }
56
 
            if (!store.lookup(working).first) {
 
56
            if (store.find(stateid) == std::end(store)) {
57
57
                push(working);
58
58
            }
59
59
        }
61
61
    }
62
62
 
63
63
    void TarjanModelChecker::push(State &state) {
64
 
        const auto res = seen.lookup(state);
65
 
        assert(res.first);
 
64
        const auto res = seen.add(state);
66
65
        const auto ctop = static_cast<idx_t>(cstack.size());
67
66
        const auto h = hash(res.second);
68
67
        cstack.emplace_back(ctop, res.second, chash[h]);
77
76
        const size_t p = dstack.top().pos;
78
77
        dstack.pop();
79
78
        if (cstack[p].lowlink == p) {
80
 
            State tmp = factory.newState();
81
79
            while (cstack.size() > p) {
82
80
                auto h = hash(cstack.back().stateid);
83
 
                seen.decode(tmp, cstack.back().stateid);
84
 
                store.add(tmp);
 
81
                store.insert(cstack.back().stateid);
85
82
                chash[h] = cstack.back().next;
86
83
                cstack.pop_back();
87
84
            }
112
109
            successorGenerator.prepare(&src);
113
110
            while (successorGenerator.next(dst)) {
114
111
                auto res = seen.add(dst);
115
 
                delem.neighbors->push_back(res.second);
116
 
                continue;
117
112
#ifdef PRINTF_DEBUG
118
113
                std::cerr << "adding state\n";
119
114
                _dump_state(dst);
120
115
#endif
121
 
                res = seen.add(dst);
122
 
                assert(res.first);
123
116
                delem.neighbors->push_back(res.second);
124
117
            }
125
118
        }