← Back to branch summary

~tapaal-ltl/verifypn/scc-optimise

« back to all changes in this revision

Viewing changes to src/CTL/Algorithm/CertainZeroFPA.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/Algorithm/CertainZeroFPA.cpp
 
1
#include "CTL/Algorithm/CertainZeroFPA.h"
 
2
 
 
3
#include <cassert>
 
4
#include <iostream>
 
5
 
 
6
using namespace DependencyGraph;
 
7
using namespace SearchStrategy;
 
8
 
 
9
bool Algorithm::CertainZeroFPA::search(DependencyGraph::BasicDependencyGraph &t_graph)
 
10
{
 
11
    graph = &t_graph;
 
12
 
 
13
 
 
14
    vertex = graph->initialConfiguration();
 
15
    {
 
16
        explore(vertex);
 
17
    }
 
18
 
 
19
    size_t cnt = 0;
 
20
    while(!strategy->empty())
 
21
    {
 
22
        while (auto e = strategy->popEdge(false)) 
 
23
        {
 
24
            ++e->refcnt;
 
25
            assert(e->refcnt >= 1);
 
26
            checkEdge(e);
 
27
            assert(e->refcnt >= -1);
 
28
            if(e->refcnt > 0) --e->refcnt;
 
29
            if(e->refcnt == 0) graph->release(e);            
 
30
            ++cnt;
 
31
            if((cnt % 1000) == 0) strategy->trivialNegation();
 
32
            if(vertex->isDone()) return vertex->assignment == ONE;
 
33
        }
 
34
        
 
35
        if(vertex->isDone()) return vertex->assignment == ONE;
 
36
        
 
37
        if(!strategy->trivialNegation())
 
38
        {
 
39
            cnt = 0;
 
40
            strategy->releaseNegationEdges(strategy->maxDistance());
 
41
            continue;
 
42
        }
 
43
    }
 
44
 
 
45
    return vertex->assignment == ONE;
 
46
}
 
47
 
 
48
void Algorithm::CertainZeroFPA::checkEdge(Edge* e, bool only_assign)
 
49
{
 
50
    if(e->handled) return;
 
51
    if(e->source->isDone())
 
52
    {
 
53
        if(e->refcnt == 0) graph->release(e);
 
54
        return;
 
55
    }
 
56
    
 
57
    bool allOne = true;
 
58
    bool hasCZero = false;
 
59
    Configuration *lastUndecided = nullptr;
 
60
    for (auto c : e->targets) {
 
61
        if (c->assignment == ONE)
 
62
        {
 
63
            continue;
 
64
        }
 
65
        else
 
66
        {
 
67
            allOne = false;
 
68
 
 
69
            if (c->assignment == CZERO) {
 
70
                hasCZero = true;
 
71
            }
 
72
            else if(lastUndecided == nullptr)
 
73
            {
 
74
                lastUndecided = c;
 
75
            }
 
76
        }
 
77
        if(lastUndecided  != nullptr && hasCZero) break;
 
78
    }
 
79
 
 
80
    if (e->is_negated) {
 
81
        _processedNegationEdges += 1;
 
82
        //Process negation edge
 
83
        if (allOne) {
 
84
            --e->source->nsuccs;
 
85
            e->handled = true;
 
86
            assert(e->refcnt > 0);
 
87
            if(only_assign) --e->refcnt;
 
88
            if (e->source->nsuccs == 0) {
 
89
                finalAssign(e->source, CZERO);
 
90
            }
 
91
            if(e->refcnt == 0) { graph->release(e);}
 
92
        } else if (hasCZero) {
 
93
            finalAssign(e->source, ONE);
 
94
        } else {
 
95
            assert(lastUndecided != nullptr);
 
96
            if(only_assign) return;
 
97
            if (lastUndecided->assignment == ZERO && e->processed) {
 
98
                finalAssign(e->source, ONE);
 
99
            } else {
 
100
                if(!e->processed)
 
101
                {
 
102
                    strategy->pushNegation(e);
 
103
                }
 
104
                addDependency(e, lastUndecided);
 
105
                if (lastUndecided->assignment == UNKNOWN) {
 
106
                    explore(lastUndecided);
 
107
                }
 
108
            }
 
109
        }
 
110
    } else {
 
111
        _processedEdges += 1;
 
112
        //Process hyper edge
 
113
        if (allOne) {
 
114
            finalAssign(e->source, ONE);
 
115
        } else if (hasCZero) {
 
116
            --e->source->nsuccs;
 
117
            e->handled = true;
 
118
            assert(e->refcnt > 0);
 
119
            if(only_assign) --e->refcnt;
 
120
            if (e->source->nsuccs == 0) {
 
121
                finalAssign(e->source, CZERO);
 
122
            }
 
123
            if(e->refcnt == 0) {graph->release(e);}
 
124
 
 
125
        } else if (lastUndecided != nullptr) {
 
126
            if(only_assign) return;
 
127
            if(!e->processed) {
 
128
                for (auto t : e->targets)
 
129
                    if(!lastUndecided->isDone())
 
130
                        addDependency(e, t);
 
131
            }                 
 
132
            if (lastUndecided->assignment == UNKNOWN) {
 
133
                explore(lastUndecided);
 
134
            }
 
135
        }
 
136
    }
 
137
    if(e->refcnt > 0  && !only_assign) e->processed = true;
 
138
    if(e->refcnt == 0) graph->release(e);
 
139
}
 
140
 
 
141
void Algorithm::CertainZeroFPA::finalAssign(DependencyGraph::Configuration *c, DependencyGraph::Assignment a)
 
142
{
 
143
    assert(a == ONE || a == CZERO);
 
144
 
 
145
    c->assignment = a;
 
146
    c->nsuccs = 0;
 
147
    for (DependencyGraph::Edge *e : c->dependency_set) {
 
148
        if(e->source->isDone()) continue;
 
149
        if(!e->is_negated || a == CZERO)
 
150
        {
 
151
            strategy->pushDependency(e);
 
152
        }
 
153
        else
 
154
        {
 
155
            strategy->pushNegation(e);
 
156
        }
 
157
        assert(e->refcnt > 0);
 
158
        --e->refcnt;
 
159
        if(e->refcnt == 0) graph->release(e);
 
160
    }
 
161
    
 
162
    c->dependency_set.clear();
 
163
}
 
164
 
 
165
void Algorithm::CertainZeroFPA::explore(Configuration *c)
 
166
{
 
167
    
 
168
    c->assignment = ZERO;
 
169
 
 
170
    {
 
171
        auto succs = graph->successors(c);
 
172
        c->nsuccs = succs.size();
 
173
 
 
174
        _exploredConfigurations += 1;
 
175
        _numberOfEdges += c->nsuccs;
 
176
        // before we start exploring, lets check if any of them determine 
 
177
        // the outcome already!
 
178
 
 
179
        for(int32_t i = c->nsuccs-1; i >= 0; --i)
 
180
        {
 
181
            checkEdge(succs[i], true);
 
182
            if(c->isDone()) 
 
183
            {
 
184
                for(Edge *e : succs){
 
185
                    assert(e->refcnt <= 1);
 
186
                    if(e->refcnt >= 1) --e->refcnt;
 
187
                    if(e->refcnt == 0) graph->release(e);
 
188
                }
 
189
                return;
 
190
            }
 
191
        }
 
192
 
 
193
        if (c->nsuccs == 0) {
 
194
            for(Edge *e : succs){
 
195
                assert(e->refcnt <= 1);
 
196
                if(e->refcnt >= 1) --e->refcnt;
 
197
                if(e->refcnt == 0) graph->release(e);
 
198
            }
 
199
            finalAssign(c, CZERO);
 
200
            return;
 
201
        }
 
202
 
 
203
        for (Edge *succ : succs) {
 
204
            assert(succ->refcnt <= 1);
 
205
            if(succ->refcnt > 0)
 
206
            {
 
207
                strategy->pushEdge(succ);
 
208
                --succ->refcnt;
 
209
                if(succ->refcnt == 0) graph->release(succ);
 
210
            }
 
211
            else if(succ->refcnt == 0)
 
212
            {
 
213
                graph->release(succ);
 
214
            }
 
215
        }
 
216
    }
 
217
    strategy->flush();
 
218
}
 
219
 
 
220
void Algorithm::CertainZeroFPA::addDependency(Edge *e, Configuration *target)
 
221
{
 
222
    auto sDist = e->is_negated ? e->source->getDistance() + 1 : e->source->getDistance();
 
223
    auto tDist = target->getDistance();
 
224
 
 
225
    target->setDistance(std::max(sDist, tDist));
 
226
    auto lb = std::lower_bound(std::begin(target->dependency_set), std::end(target->dependency_set), e);
 
227
    if(lb == std::end(target->dependency_set) || *lb != e)
 
228
    {
 
229
        target->dependency_set.insert(lb, e);
 
230
        assert(e->refcnt >= 0);
 
231
        ++e->refcnt;
 
232
    }
 
233
}