← Back to branch summary

~tapaal-ltl/verifypn/scc-optimise

« back to all changes in this revision

Viewing changes to src/PetriEngine/TAR/PlaceUseVisitor.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/PetriEngine/TAR/PlaceUseVisitor.cpp
 
1
/*
 
2
 *  Copyright Peter G. Jensen, all rights reserved.
 
3
 */
 
4
 
 
5
/* 
 
6
 * File:   PlaceUseVisitor.cpp
 
7
 * Author: Peter G. Jensen <root@petergjoel.dk>
 
8
 * 
 
9
 * Created on April 23, 2020, 8:44 PM
 
10
 */
 
11
 
 
12
#include "PetriEngine/TAR/PlaceUseVisitor.h"
 
13
 
 
14
namespace PetriEngine {
 
15
namespace PQL {
 
16
 
 
17
    PlaceUseVisitor::PlaceUseVisitor(size_t places)
 
18
    : _in_use(places)
 
19
    {
 
20
 
 
21
    }
 
22
 
 
23
    void PlaceUseVisitor::_accept(const NotCondition* element)
 
24
    {
 
25
        (*element)[0]->visit(*this);
 
26
    }
 
27
    
 
28
    void PlaceUseVisitor::_accept(const AndCondition* element)
 
29
    {
 
30
        for(auto& e : *element)
 
31
            e->visit(*this);
 
32
    }
 
33
 
 
34
    void PlaceUseVisitor::_accept(const OrCondition* element)
 
35
    {
 
36
        for(auto& e : *element)
 
37
            e->visit(*this);
 
38
    }
 
39
    
 
40
    void PlaceUseVisitor::_accept(const LessThanCondition* element)
 
41
    {
 
42
        for(auto i : {0,1})
 
43
            (*element)[i]->visit(*this);
 
44
    }
 
45
 
 
46
    void PlaceUseVisitor::_accept(const LessThanOrEqualCondition* element)
 
47
    {
 
48
        for(auto i : {0,1})
 
49
            (*element)[i]->visit(*this);
 
50
    }
 
51
 
 
52
    void PlaceUseVisitor::_accept(const GreaterThanOrEqualCondition* element)
 
53
    {
 
54
        for(auto i : {0,1})
 
55
            (*element)[i]->visit(*this);
 
56
    }
 
57
 
 
58
    void PlaceUseVisitor::_accept(const GreaterThanCondition* element)
 
59
    {
 
60
        for(auto i : {0,1})
 
61
            (*element)[i]->visit(*this);
 
62
    }
 
63
 
 
64
    void PlaceUseVisitor::_accept(const EqualCondition* element)
 
65
    {
 
66
        for(auto i : {0,1})
 
67
            (*element)[i]->visit(*this);
 
68
    }
 
69
 
 
70
    void PlaceUseVisitor::_accept(const NotEqualCondition* element)
 
71
    {
 
72
        for(auto i : {0,1})
 
73
            (*element)[i]->visit(*this);
 
74
    }
 
75
    
 
76
    void PlaceUseVisitor::_accept(const CompareConjunction* element)
 
77
    {
 
78
        for(auto& e : *element)
 
79
            _in_use[e._place] = true;
 
80
    }
 
81
    
 
82
    void PlaceUseVisitor::visitCommutativeExpr(const CommutativeExpr* element)
 
83
    {
 
84
        for(auto& p : element->places())
 
85
            _in_use[p.first] = true;
 
86
        for(auto& e : element->expressions())
 
87
            e->visit(*this);     
 
88
    }
 
89
    
 
90
    void PlaceUseVisitor::_accept(const PlusExpr* element)
 
91
    {
 
92
        visitCommutativeExpr(element);
 
93
    }
 
94
    
 
95
    void PlaceUseVisitor::_accept(const SubtractExpr* element)
 
96
    {
 
97
        for(auto& e : element->expressions())
 
98
            e->visit(*this);
 
99
    }
 
100
 
 
101
    void PlaceUseVisitor::_accept(const MultiplyExpr* element)
 
102
    {
 
103
        visitCommutativeExpr(element);
 
104
    }
 
105
    
 
106
    void PlaceUseVisitor::_accept(const MinusExpr* element)
 
107
    {
 
108
        (*element)[0]->visit(*this);
 
109
    }
 
110
    
 
111
    void PlaceUseVisitor::_accept(const UnfoldedIdentifierExpr* element) 
 
112
    {
 
113
        _in_use[element->offset()] = true;
 
114
    }
 
115
    
 
116
    void PlaceUseVisitor::_accept(const UnfoldedUpperBoundsCondition* element)
 
117
    {
 
118
        for(auto& p : element->places())
 
119
            _in_use[p._place] = true;
 
120
    }
 
121
    
 
122
    void PlaceUseVisitor::_accept(const EUCondition* el)
 
123
    {   
 
124
        (*el)[0]->visit(*this);
 
125
        (*el)[1]->visit(*this);
 
126
    }
 
127
 
 
128
    void PlaceUseVisitor::_accept(const AUCondition* el)
 
129
    {   
 
130
        (*el)[0]->visit(*this);
 
131
        (*el)[1]->visit(*this);
 
132
    }
 
133
 
 
134
    void PlaceUseVisitor::_accept(const EFCondition* el) { (*el)[0]->visit(*this); }
 
135
    void PlaceUseVisitor::_accept(const EGCondition* el) { (*el)[0]->visit(*this); }
 
136
    void PlaceUseVisitor::_accept(const AGCondition* el) { (*el)[0]->visit(*this); }
 
137
    void PlaceUseVisitor::_accept(const AFCondition* el) { (*el)[0]->visit(*this); }
 
138
    void PlaceUseVisitor::_accept(const EXCondition* el) { (*el)[0]->visit(*this); }
 
139
    void PlaceUseVisitor::_accept(const AXCondition* el) { (*el)[0]->visit(*this); }
 
140
 
 
141
    // shallow elements, neither of these should exist in a compiled expression    
 
142
    void PlaceUseVisitor::_accept(const LiteralExpr* element) {}
 
143
    void PlaceUseVisitor::_accept(const DeadlockCondition*) {}
 
144
 
 
145
}
 
146
}
 
147