← Back to branch summary

~tapaal-ltl/verifypn/scc-optimise

« back to all changes in this revision

Viewing changes to src/CTL/SearchStrategy/SearchStrategy.cpp

  • Committer: srba.jiri at gmail
  • Date: 2020-09-11 14:23:39 UTC
  • mfrom: (213.1.151 interval_tar)
  • Revision ID: srba.jiri@gmail.com-20200911142339-bq9328s1gppw24uj
merged in lp:~verifypn-maintainers/verifypn/interval_tar doing 
- Implements TAR w/o z3, but using a simple integer inference engine for Hoare logic.
 - Replaces LP-Solve with GLPK, reduces computation-time and memory overhead
 - Implements new global properties, translated into CTL formulae.

Show diffs side-by-side

added added

removed removed

Lines of Context:
src/CTL/SearchStrategy/SearchStrategy.cpp
 
1
 
 
2
#include "CTL/DependencyGraph/Configuration.h"
 
3
#include "CTL/SearchStrategy/SearchStrategy.h"
 
4
 
 
5
#include <iostream>
 
6
#include <cassert>
 
7
 
 
8
namespace SearchStrategy{
 
9
 
 
10
    bool SearchStrategy::empty() const
 
11
    {
 
12
        return Wsize() == 0 && N.empty() && D.empty();
 
13
    }
 
14
 
 
15
    void SearchStrategy::pushNegation(DependencyGraph::Edge* edge)
 
16
    {
 
17
        edge->status = 3;
 
18
        ++edge->refcnt;
 
19
        bool allOne = true;
 
20
        bool hasCZero = false;
 
21
 
 
22
        for (DependencyGraph::Configuration *c : edge->targets) {
 
23
            if (c->assignment == DependencyGraph::Assignment::CZERO) {
 
24
                hasCZero = true;
 
25
                break;
 
26
            }
 
27
            if (c->assignment != DependencyGraph::Assignment::ONE) {
 
28
                allOne = false;
 
29
            }
 
30
        }
 
31
 
 
32
        if(allOne || hasCZero)
 
33
        {
 
34
            D.push_back(edge);
 
35
        }
 
36
        else
 
37
        {
 
38
            N.push_back(edge);
 
39
        }
 
40
    }
 
41
 
 
42
    void SearchStrategy::pushEdge(DependencyGraph::Edge *edge)
 
43
    {
 
44
        if(edge->status > 0 || edge->source->isDone()) return;
 
45
        if(edge->processed && edge->is_negated)
 
46
        {
 
47
            pushNegation(edge);
 
48
            return;
 
49
        }
 
50
        edge->status = 1;
 
51
        ++edge->refcnt;
 
52
        pushToW(edge);
 
53
    }
 
54
 
 
55
    void SearchStrategy::pushDependency(DependencyGraph::Edge* edge)
 
56
    {
 
57
        if(edge->source->isDone()) return;
 
58
        edge->status = 2;
 
59
        ++edge->refcnt;
 
60
        D.push_back(edge);
 
61
    }
 
62
 
 
63
    DependencyGraph::Edge* SearchStrategy::popEdge(bool saturate)
 
64
    {
 
65
        if(saturate && D.empty()) return nullptr;
 
66
 
 
67
        if (Wsize() == 0 && D.empty()) {
 
68
            return nullptr;
 
69
        }
 
70
 
 
71
        auto edge = D.empty() ? popFromW() : D.back();
 
72
 
 
73
        if(!D.empty())
 
74
            D.pop_back();
 
75
 
 
76
        assert(edge->refcnt >= 0);
 
77
        --edge->refcnt;
 
78
        edge->status = 0;
 
79
        return edge;
 
80
    }
 
81
 
 
82
    uint32_t SearchStrategy::maxDistance() const
 
83
    {
 
84
        uint32_t m = 0;
 
85
        for(DependencyGraph::Edge* e : N)
 
86
        {
 
87
            if(!e->source->isDone())
 
88
                m = std::max(m, e->source->getDistance());
 
89
        }
 
90
        return m;
 
91
    }
 
92
 
 
93
    bool SearchStrategy::available() const
 
94
    {
 
95
        return Wsize() > 0 || !D.empty();
 
96
    }
 
97
 
 
98
    void SearchStrategy::releaseNegationEdges(uint32_t dist)
 
99
    {
 
100
        for(auto it = N.begin(); it != N.end(); ++it)
 
101
        {
 
102
            assert(*it);
 
103
            if((*it)->source->getDistance() >= dist || (*it)->source->isDone())
 
104
            {
 
105
                pushToW(*it);
 
106
                it = N.erase(it);
 
107
                if(N.empty() || it == N.end()) break;
 
108
            }
 
109
        }
 
110
    }
 
111
 
 
112
    bool SearchStrategy::trivialNegation()
 
113
    {
 
114
        for(auto it = N.begin(); it != N.end(); ++it)
 
115
        {
 
116
            bool allOne = true;
 
117
            bool hasCZero = false;
 
118
            auto e = *it;
 
119
            for (DependencyGraph::Configuration *c : e->targets) {
 
120
                if (c->assignment == DependencyGraph::Assignment::CZERO) {
 
121
                    hasCZero = true;
 
122
                    break;
 
123
                }
 
124
                if (c->assignment != DependencyGraph::Assignment::ONE) {
 
125
                    allOne = false;
 
126
                }
 
127
            }
 
128
 
 
129
            if(allOne || hasCZero)
 
130
            {
 
131
                D.push_back(*it);
 
132
                it = N.erase(it);
 
133
                if(N.empty() || it == N.end()) break;
 
134
            }
 
135
        }
 
136
        return !D.empty();
 
137
    }
 
138
}