← Back to branch summary

~tapaal-ltl/verifypn/scc-optimise

« back to all changes in this revision

Viewing changes to src/CTL/Algorithm/LocalFPA.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/LocalFPA.cpp
 
1
#include "CTL/Algorithm/LocalFPA.h"
 
2
#include "CTL/DependencyGraph/Configuration.h"
 
3
#include "CTL/DependencyGraph/Edge.h"
 
4
 
 
5
#include <cassert>
 
6
#include <iostream>
 
7
 
 
8
bool Algorithm::LocalFPA::search(DependencyGraph::BasicDependencyGraph &t_graph)
 
9
{
 
10
    using namespace DependencyGraph;
 
11
    graph = &t_graph;
 
12
 
 
13
    Configuration *v = graph->initialConfiguration();
 
14
    explore(v);
 
15
 
 
16
    while (!strategy->empty())
 
17
    {
 
18
        while (auto e = strategy->popEdge()) {
 
19
 
 
20
            if (v->assignment == DependencyGraph::ONE) {
 
21
                break;
 
22
            }
 
23
 
 
24
            bool allOne = true;
 
25
            Configuration *lastUndecided = nullptr;
 
26
 
 
27
            for (DependencyGraph::Configuration *c : e->targets) {
 
28
                if (c->assignment != DependencyGraph::ONE) {
 
29
                    allOne = false;
 
30
                    lastUndecided = c;
 
31
                }
 
32
            }
 
33
 
 
34
            if (e->is_negated) {
 
35
                _processedNegationEdges += 1;
 
36
                //Process negation edge
 
37
                if(allOne) {}
 
38
                else if(!e->processed){
 
39
                    addDependency(e, lastUndecided);
 
40
                    if(lastUndecided->assignment == UNKNOWN){
 
41
                        explore(lastUndecided);
 
42
                    }
 
43
                    strategy->pushNegation(e);
 
44
                }
 
45
                else{
 
46
                    finalAssign(e->source, ONE);
 
47
                }
 
48
 
 
49
            } else {
 
50
                _processedEdges += 1;
 
51
                //Process hyper edge
 
52
                if (allOne) {
 
53
                    finalAssign(e->source, ONE);
 
54
                } else {
 
55
                    addDependency(e, lastUndecided);
 
56
                    if (lastUndecided->assignment == UNKNOWN) {
 
57
                        explore(lastUndecided);
 
58
                    }
 
59
                }
 
60
            }
 
61
            e->processed = true;
 
62
            if(e->refcnt == 0) graph->release(e);
 
63
        }
 
64
        if(!strategy->trivialNegation())
 
65
        {
 
66
            strategy->releaseNegationEdges(strategy->maxDistance());
 
67
        }
 
68
    }
 
69
 
 
70
    return v->assignment == ONE;
 
71
}
 
72
 
 
73
void Algorithm::LocalFPA::finalAssign(DependencyGraph::Configuration *c, DependencyGraph::Assignment a)
 
74
{
 
75
    assert(a == DependencyGraph::ONE);
 
76
    c->assignment = a;
 
77
 
 
78
    for(DependencyGraph::Edge *e : c->dependency_set){
 
79
        if(e->is_negated)
 
80
        {
 
81
            strategy->pushNegation(e);
 
82
        }
 
83
        else
 
84
        {
 
85
            strategy->pushDependency(e);
 
86
        }
 
87
        --e->refcnt;
 
88
        if(e->refcnt == 0) graph->release(e);
 
89
    }
 
90
 
 
91
    c->dependency_set.clear();
 
92
}
 
93
 
 
94
void Algorithm::LocalFPA::explore(DependencyGraph::Configuration *c)
 
95
{
 
96
    assert(c->assignment == DependencyGraph::UNKNOWN);
 
97
    c->assignment = DependencyGraph::ZERO;
 
98
    auto succs = graph->successors(c);
 
99
 
 
100
    for (DependencyGraph::Edge *succ : succs) {
 
101
        strategy->pushEdge(succ);
 
102
        --succ->refcnt;
 
103
        if(succ->refcnt == 0) graph->release(succ);
 
104
    }
 
105
 
 
106
    _exploredConfigurations += 1;
 
107
    _numberOfEdges += succs.size();
 
108
}
 
109
 
 
110
void Algorithm::LocalFPA::addDependency(DependencyGraph::Edge *e, DependencyGraph::Configuration *target)
 
111
{
 
112
    unsigned int sDist = e->is_negated ? e->source->getDistance() + 1 : e->source->getDistance();
 
113
    unsigned int tDist = target->getDistance();
 
114
 
 
115
    target->setDistance(std::max(sDist, tDist));
 
116
 
 
117
    auto lb = std::lower_bound(std::begin(target->dependency_set), std::end(target->dependency_set), e);
 
118
    if(lb == std::end(target->dependency_set) || *lb != e)
 
119
    {
 
120
        target->dependency_set.insert(lb, e);
 
121
        ++e->refcnt;
 
122
    }
 
123
}