← Back to branch summary

~tapaal-ltl/verifypn/scc-optimise

« back to all changes in this revision

Viewing changes to 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:
CTL/Algorithm/LocalFPA.cpp
1
 
#include "LocalFPA.h"
2
 
#include "../DependencyGraph/Configuration.h"
3
 
#include "../DependencyGraph/Edge.h"
4
 
 
5
 
#include <assert.h>
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) ? true : false;
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
 
}