← Back to branch summary

~tapaal-ltl/verifypn/scc-optimise

« back to all changes in this revision

Viewing changes to PetriEngine/Reachability/ResultPrinter.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:
PetriEngine/Reachability/ResultPrinter.cpp
1
 
 
2
 
#include "ReachabilityResult.h"
3
 
#include "../PetriNetBuilder.h"
4
 
#include "../options.h"
5
 
#include "PetriEngine/PQL/Expressions.h"
6
 
 
7
 
namespace PetriEngine {
8
 
    namespace Reachability {
9
 
        ResultPrinter::Result ResultPrinter::printResult(
10
 
                size_t index,
11
 
                PQL::Condition* query, 
12
 
                ResultPrinter::Result result,
13
 
                size_t expandedStates,
14
 
                size_t exploredStates,
15
 
                size_t discoveredStates,
16
 
                const std::vector<size_t> enabledTransitionsCount,
17
 
                int maxTokens,
18
 
                const std::vector<uint32_t> maxPlaceBound, Structures::StateSetInterface* stateset,
19
 
                size_t lastmarking)
20
 
        {
21
 
            if(result == Unknown) return Unknown;
22
 
 
23
 
            Result retval = result;
24
 
            
25
 
            if(options->cpnOverApprox)
26
 
            {
27
 
                if (result == Satisfied)
28
 
                    retval = query->isInvariant() ? Unknown : Unknown;
29
 
                else if (result == NotSatisfied)
30
 
                    retval = query->isInvariant() ? Satisfied : NotSatisfied;                
31
 
                if(retval == Unknown)
32
 
                {
33
 
                    std::cout << "\nUnable to decide if " << querynames[index] << " is satisfied.\n\n";
34
 
                    std::cout << "Query is MAYBE satisfied.\n" << std::endl;
35
 
                    return Ignore;
36
 
                }
37
 
            }
38
 
            std::cout << std::endl;    
39
 
            
40
 
            bool showTrace = (result == Satisfied);
41
 
            
42
 
            if(!options->statespaceexploration && retval != Unknown)
43
 
            {
44
 
                std::cout << "FORMULA " << querynames[index] << " ";
45
 
            }
46
 
            else {
47
 
                retval = Satisfied;
48
 
                uint32_t placeBound = 0;
49
 
                for (size_t p = 0; p < maxPlaceBound.size(); p++) {
50
 
                    placeBound = std::max<uint32_t>(placeBound, maxPlaceBound[p]);
51
 
                }
52
 
                // fprintf(stdout,"STATE_SPACE %lli -1 %d %d TECHNIQUES EXPLICIT\n", result.exploredStates(), result.maxTokens(), placeBound);
53
 
                std::cout   << "STATE_SPACE STATES "<< exploredStates           << " " << techniquesStateSpace
54
 
                            << std::endl
55
 
                            << "STATE_SPACE TRANSITIONS "<< -1                  << " " << techniquesStateSpace
56
 
                            << std::endl
57
 
                            << "STATE_SPACE MAX_TOKEN_PER_MARKING "<< maxTokens << " " << techniquesStateSpace
58
 
                            << std::endl
59
 
                            << "STATE_SPACE MAX_TOKEN_IN_PLACE "<< placeBound   << " " << techniquesStateSpace 
60
 
                            << std::endl;
61
 
                return retval;
62
 
            }
63
 
 
64
 
            if (result == Satisfied)
65
 
                retval = query->isInvariant() ? NotSatisfied : Satisfied;
66
 
            else if (result == NotSatisfied)
67
 
                retval = query->isInvariant() ? Satisfied : NotSatisfied;           
68
 
 
69
 
            //Print result
70
 
            auto bound = query;
71
 
            if(auto ef = dynamic_cast<PQL::EFCondition*>(query))
72
 
            {
73
 
                bound = (*ef)[0].get();
74
 
            }
75
 
            bound = dynamic_cast<PQL::UnfoldedUpperBoundsCondition*>(bound);
76
 
            
77
 
            if (retval == Unknown)
78
 
            {
79
 
                std::cout << "\nUnable to decide if " << querynames[index] << " is satisfied.";
80
 
            }
81
 
            else if(bound)
82
 
            {
83
 
                std::cout << ((PQL::UnfoldedUpperBoundsCondition*)bound)->bounds() << " " << techniques << printTechniques() << std::endl;
84
 
                std::cout << "Query index " << index << " was solved" << std::endl;
85
 
            }
86
 
            else if (retval == Satisfied) {
87
 
                if(!options->statespaceexploration)
88
 
                {
89
 
                    std::cout << "TRUE " << techniques << printTechniques() << std::endl;
90
 
                    std::cout << "Query index " << index << " was solved" << std::endl;
91
 
                }
92
 
            } else if (retval == NotSatisfied) {
93
 
                if(!options->statespaceexploration)
94
 
                {
95
 
                    std::cout << "FALSE " << techniques << printTechniques() << std::endl;
96
 
                    std::cout << "Query index " << index << " was solved" << std::endl;
97
 
                }
98
 
            }
99
 
            
100
 
            std::cout << std::endl;
101
 
 
102
 
            std::cout << "Query is ";
103
 
            if(options->statespaceexploration)
104
 
            {
105
 
                retval = Satisfied;
106
 
            }
107
 
 
108
 
            if (result == Satisfied)
109
 
                retval = query->isInvariant() ? NotSatisfied : Satisfied;
110
 
            else if (result == NotSatisfied)
111
 
                retval = query->isInvariant() ? Satisfied : NotSatisfied;
112
 
 
113
 
            //Print result
114
 
            if (retval == Unknown)
115
 
            {
116
 
                std::cout << "MAYBE ";
117
 
            }
118
 
            else if (retval == NotSatisfied) {
119
 
                std::cout << "NOT ";
120
 
            }
121
 
            std::cout << "satisfied." << std::endl;
122
 
            
123
 
            if(options->cpnOverApprox)
124
 
                std::cout << "\nSolved using CPN Approximation\n" << std::endl;
125
 
            
126
 
            if(showTrace && options->trace)
127
 
            {
128
 
                if(stateset == NULL)
129
 
                {
130
 
#ifdef ENABLE_TAR
131
 
                    if(options->tar)
132
 
                        std::cout << "No trace could be generated" << std::endl;
133
 
                    else
134
 
#endif
135
 
                    {
136
 
                        // No trace was generated, printing the empty trace
137
 
                        std::cerr << "Trace:\n<trace>\n";
138
 
                        std::cerr << "</trace>\n" << std::endl;
139
 
                    }
140
 
                }
141
 
                else
142
 
                {
143
 
                    printTrace(stateset, lastmarking);                        
144
 
                }
145
 
            }
146
 
            
147
 
            std::cout << std::endl;
148
 
            return retval;
149
 
        }
150
 
        
151
 
        std::string ResultPrinter::printTechniques() {
152
 
            std::string out;
153
 
                        
154
 
            if(options->queryReductionTimeout > 0)
155
 
            {
156
 
                out += "LP_APPROX ";
157
 
            }
158
 
 
159
 
            if(options->cpnOverApprox)
160
 
            {
161
 
                out += "CPN_APPROX ";
162
 
            }
163
 
            
164
 
            if(options->isCPN && !options->cpnOverApprox)
165
 
            {
166
 
                out += "UNFOLDING_TO_PT ";
167
 
            }
168
 
            
169
 
            if(options->queryReductionTimeout == 0 
170
 
#ifdef ENABLE_TAR
171
 
                            && !options->tar 
172
 
#endif
173
 
                            && options->siphontrapTimeout == 0)
174
 
            {
175
 
                out += "EXPLICIT STATE_COMPRESSION ";
176
 
                if(options->stubbornreduction)
177
 
                {
178
 
                    out += "STUBBORN_SETS ";
179
 
                }
180
 
            }
181
 
#ifdef ENABLE_TAR            
182
 
            if(options->tar)
183
 
            {
184
 
                out += "TRACE_ABSTRACTION_REFINEMENT ";
185
 
            }
186
 
#endif            
187
 
            if(options->siphontrapTimeout > 0)
188
 
            {
189
 
                out += "TOPOLOGICAL SIPHON_TRAP ";
190
 
            }
191
 
            
192
 
            return out;
193
 
        }
194
 
        
195
 
        void ResultPrinter::printTrace(Structures::StateSetInterface* ss, size_t lastmarking)
196
 
        {
197
 
            std::cerr << "Trace:\n<trace>\n";
198
 
            std::stack<size_t> transitions;
199
 
            size_t next = lastmarking;
200
 
            while(next != 0) // assume 0 is the index of the first marking.
201
 
            {
202
 
                // (parent, transition)
203
 
                std::pair<size_t, size_t> p = ss->getHistory(next);
204
 
                next = p.first;
205
 
                transitions.push(p.second);
206
 
            }
207
 
            
208
 
            if(reducer != NULL)
209
 
                reducer->initFire(std::cerr);
210
 
            
211
 
            while(transitions.size() > 0)
212
 
            {
213
 
                size_t trans = transitions.top();
214
 
                transitions.pop();
215
 
                std::string tname = ss->net().transitionNames()[trans];
216
 
                std::cerr << "\t<transition id=\"" << tname << "\">\n";
217
 
                
218
 
                // well, yeah, we are not really efficient in constructing the trace.
219
 
                // feel free to improve
220
 
                for(size_t p = 0; p < ss->net().numberOfPlaces(); ++p)
221
 
                {
222
 
                    size_t cnt = ss->net().inArc(p, trans);
223
 
                    for(size_t token = 0; token < cnt; ++token )
224
 
                    {
225
 
                        std::cerr << "\t\t<token place=\"" << ss->net().placeNames()[p] << "\" age=\"0\"/>\n";
226
 
                    }
227
 
                }
228
 
                
229
 
                if(reducer != NULL)
230
 
                    reducer->extraConsume(std::cerr, tname);
231
 
                
232
 
                std::cerr << "\t</transition>\n";
233
 
                
234
 
                if(reducer != NULL)
235
 
                    reducer->postFire(std::cerr, tname);
236
 
                
237
 
            }
238
 
            
239
 
            std::cerr << "</trace>\n" << std::endl;
240
 
        }
241
 
 
242
 
    }
243
 
}