← Back to branch summary

~verifypn-maintainers/verifypn/emptyTracePrint

« back to all changes in this revision

Viewing changes to CTL/SearchStrategy/DFSSearch.cpp

  • Committer: Jiri Srba
  • Date: 2018-04-18 10:58:36 UTC
  • mfrom: (197.3.78 cpn_ctlss)
  • Revision ID: srba.jiri@gmail.com-20180418105836-a5rha272u0om4u77
merged in branch lp:~verifypn-cpn/verifypn/cpn_ctlss/

CPN unfolding
CPN linear overapproximation
Export of reduced queries and model
parallel query simplification
TAR for P/T nets
Improved structural reduction rules

Show diffs side-by-side

added added

removed removed

Lines of Context:
CTL/SearchStrategy/DFSSearch.cpp
1
 
 
2
 
#include <iostream>
3
 
#include "assert.h"
4
 
#include "DFSSearch.h"
5
 
#include "CTL/DependencyGraph/Configuration.h"
6
 
 
7
 
bool SearchStrategy::DFSSearch::empty() const
8
 
{
9
 
    return W.empty() && N.empty() && D.empty();
10
 
}
11
 
 
12
 
void SearchStrategy::DFSSearch::pushNegation(DependencyGraph::Edge* edge)
13
 
{
14
 
    edge->status = 3;
15
 
    ++edge->refcnt;
16
 
    bool allOne = true;
17
 
    bool hasCZero = false;
18
 
 
19
 
    for (DependencyGraph::Configuration *c : edge->targets) {
20
 
        if (c->assignment == DependencyGraph::Assignment::CZERO) {
21
 
            hasCZero = true;
22
 
            break;
23
 
        }
24
 
        if (c->assignment != DependencyGraph::Assignment::ONE) {
25
 
            allOne = false;
26
 
        }
27
 
    }
28
 
 
29
 
    if(allOne || hasCZero)
30
 
    {
31
 
        D.push_back(edge);
32
 
    }
33
 
    else
34
 
    {
35
 
        N.push_back(edge);
36
 
        possibleTrivial = true;
37
 
    }
38
 
}
39
 
 
40
 
void SearchStrategy::DFSSearch::pushEdge(DependencyGraph::Edge *edge)
41
 
{
42
 
    if(edge->status > 0 || edge->source->isDone()) return;
43
 
    if(edge->processed && edge->is_negated)
44
 
    {
45
 
        pushNegation(edge);
46
 
        return;
47
 
    }
48
 
    edge->status = 1;
49
 
    ++edge->refcnt;
50
 
    W.push_back(edge);
51
 
}
52
 
 
53
 
void SearchStrategy::DFSSearch::pushDependency(DependencyGraph::Edge* edge)
54
 
{
55
 
    if(edge->source->isDone()) return;
56
 
    edge->status = 2;
57
 
    ++edge->refcnt;
58
 
    D.push_back(edge);
59
 
}
60
 
 
61
 
DependencyGraph::Edge* SearchStrategy::DFSSearch::popEdge(bool saturate)
62
 
{
63
 
    if(saturate && D.empty()) return nullptr;
64
 
    
65
 
    if (W.empty() && D.empty()) {
66
 
        return nullptr;
67
 
    }
68
 
 
69
 
    auto edge = D.empty() ? W.back() : D.back();
70
 
 
71
 
    if(D.empty()) 
72
 
        W.pop_back();
73
 
    else
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::DFSSearch::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::DFSSearch::available() const
94
 
{
95
 
    return !W.empty() || !D.empty();
96
 
}
97
 
 
98
 
void SearchStrategy::DFSSearch::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
 
            W.push_back(*it);
106
 
            assert(W.front()->weight >= W.back()->weight);
107
 
            it = N.erase(it);
108
 
            if(N.empty() || it == N.end()) break;
109
 
        }
110
 
    }
111
 
}
112
 
 
113
 
bool SearchStrategy::DFSSearch::trivialNegation()
114
 
{
115
 
    for(auto it = N.begin(); it != N.end(); ++it)
116
 
    {
117
 
        bool allOne = true;
118
 
        bool hasCZero = false;
119
 
        auto e = *it;
120
 
        for (DependencyGraph::Configuration *c : e->targets) {
121
 
            if (c->assignment == DependencyGraph::Assignment::CZERO) {
122
 
                hasCZero = true;
123
 
                break;
124
 
            }
125
 
            if (c->assignment != DependencyGraph::Assignment::ONE) {
126
 
                allOne = false;
127
 
            }
128
 
        }
129
 
        
130
 
        if(allOne || hasCZero)
131
 
        {
132
 
            D.push_back(*it);
133
 
            it = N.erase(it);
134
 
            if(N.empty() || it == N.end()) break;
135
 
        }
136
 
    }
137
 
    possibleTrivial = false;
138
 
    return !D.empty();
139
 
}