← Back to branch summary

~tapaal-ltl/verifypn/scc-optimise

« back to all changes in this revision

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