← Back to branch summary

~tapaal-contributor/verifypn/unfoldTACPN

« back to all changes in this revision

Viewing changes to src/PetriEngine/PQL/Contexts.cpp

  • Committer: tpede16 at aau
  • Date: 2020-11-20 12:40:58 UTC
  • Revision ID: tpede16@student.aau.dk-20201120124058-a21zlqk70r4l753c
Merge with trunk

Show diffs side-by-side

added added

removed removed

Lines of Context:
src/PetriEngine/PQL/Contexts.cpp
 
1
/*
 
2
 *  Copyright Peter G. Jensen, all rights reserved.
 
3
 */
 
4
 
 
5
#include "PetriEngine/PQL/Contexts.h"
 
6
 
 
7
 
 
8
 
 
9
namespace PetriEngine {
 
10
    namespace PQL {
 
11
       
 
12
        bool ColoredAnalysisContext::resolvePlace(const std::string& place, std::unordered_map<uint32_t, std::string>& out)
 
13
        {
 
14
            auto it = _coloredPlaceNames.find(place);
 
15
            if (it != _coloredPlaceNames.end()) {
 
16
                out = it->second;
 
17
                return true;
 
18
            }
 
19
            return false;
 
20
        }
 
21
        
 
22
        bool ColoredAnalysisContext::resolveTransition(const std::string& transition, std::vector<std::string>& out)
 
23
        {
 
24
            auto it = _coloredTransitionNames.find(transition);
 
25
            if (it != _coloredTransitionNames.end()) {
 
26
                out = it->second;
 
27
                return true;
 
28
            }
 
29
            return false;
 
30
        }
 
31
 
 
32
       
 
33
        AnalysisContext::ResolutionResult AnalysisContext::resolve(const std::string& identifier, bool place)
 
34
        {
 
35
            ResolutionResult result;
 
36
            result.offset = -1;
 
37
            result.success = false;
 
38
            auto& map = place ? _placeNames : _transitionNames;
 
39
            auto it = map.find(identifier);
 
40
            if (it != map.end()) {
 
41
                result.offset = (int) it->second;
 
42
                result.success = true;
 
43
                return result;
 
44
            }
 
45
            return result;
 
46
        }
 
47
 
 
48
        uint32_t SimplificationContext::getLpTimeout() const
 
49
        {
 
50
            return _lpTimeout;
 
51
        }
 
52
 
 
53
        double SimplificationContext::getReductionTime()
 
54
        {
 
55
            // duration in seconds
 
56
            auto end = std::chrono::high_resolution_clock::now();
 
57
            return (std::chrono::duration_cast<std::chrono::microseconds>(end - _start).count())*0.000001;
 
58
        }
 
59
        
 
60
        glp_prob* SimplificationContext::makeBaseLP() const
 
61
        {
 
62
            if (_base_lp == nullptr)
 
63
                _base_lp = buildBase();
 
64
            if (_base_lp == nullptr)
 
65
                return nullptr;
 
66
            auto* tmp_lp = glp_create_prob();
 
67
            glp_copy_prob(tmp_lp, _base_lp, GLP_OFF);
 
68
            return tmp_lp;
 
69
        }
 
70
        
 
71
        glp_prob* SimplificationContext::buildBase() const
 
72
        {
 
73
            constexpr auto infty = std::numeric_limits<double>::infinity();
 
74
            if (timeout())
 
75
                return nullptr;
 
76
 
 
77
            auto* lp = glp_create_prob();
 
78
            if (lp == nullptr)
 
79
                return lp;
 
80
 
 
81
            const uint32_t nCol = _net->numberOfTransitions();
 
82
            const int nRow = _net->numberOfPlaces();
 
83
            std::vector<int32_t> indir(std::max<uint32_t>(nCol, nRow) + 1);
 
84
 
 
85
            glp_add_cols(lp, nCol + 1);
 
86
            glp_add_rows(lp, nRow + 1);
 
87
            {
 
88
                std::vector<double> col = std::vector<double>(nRow + 1);
 
89
                for (size_t t = 0; t < _net->numberOfTransitions(); ++t) {
 
90
                    auto pre = _net->preset(t);
 
91
                    auto post = _net->postset(t);
 
92
                    size_t l = 1;
 
93
                    while (pre.first != pre.second ||
 
94
                           post.first != post.second) {
 
95
                        if (pre.first == pre.second || (post.first != post.second && post.first->place < pre.first->place)) {
 
96
                            col[l] = post.first->tokens;
 
97
                            indir[l] = post.first->place + 1;
 
98
                            ++post.first;
 
99
                        }
 
100
                        else if (post.first == post.second || (pre.first != pre.second && pre.first->place < post.first->place)) {
 
101
                            if(!pre.first->inhibitor)
 
102
                                col[l] = -(double) pre.first->tokens;
 
103
                            else
 
104
                                col[l] = 0;
 
105
                            indir[l] = pre.first->place + 1;
 
106
                            ++pre.first;
 
107
                        }
 
108
                        else {
 
109
                            assert(pre.first->place == post.first->place);
 
110
                            if(!pre.first->inhibitor)
 
111
                                col[l] = (double) post.first->tokens - (double) pre.first->tokens;
 
112
                            else
 
113
                                col[l] = (double) post.first->tokens;
 
114
                            indir[l] = pre.first->place + 1;
 
115
                            ++pre.first;
 
116
                            ++post.first;
 
117
                        }
 
118
                        ++l;
 
119
                    }
 
120
                    glp_set_mat_col(lp, t + 1, l - 1, indir.data(), col.data());
 
121
                    if (timeout()) {
 
122
                        std::cerr << "glpk: construction timeout" << std::endl;
 
123
                        glp_delete_prob(lp);
 
124
                        return nullptr;
 
125
                    }
 
126
                }
 
127
            }
 
128
            int rowno = 1;
 
129
            for (size_t p = 0; p < _net->numberOfPlaces(); p++) {
 
130
                glp_set_row_bnds(lp, rowno, GLP_LO, (0.0 - (double) _marking[p]), infty);
 
131
                ++rowno;
 
132
                if (timeout()) {
 
133
                    std::cerr << "glpk: construction timeout" << std::endl;
 
134
                    glp_delete_prob(lp);
 
135
                    return nullptr;
 
136
                }
 
137
            }
 
138
            return lp;
 
139
        }
 
140
    }
 
141
}
 
 
b'\\ No newline at end of file'