← Back to branch summary

~tapaal-ltl/verifypn/scc-optimise

« back to all changes in this revision

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