← Back to branch summary

~verifypn-maintainers/verifypn/emptyTracePrint

« back to all changes in this revision

Viewing changes to PetriEngine/Reachability/ResultPrinter.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:
PetriEngine/Reachability/ResultPrinter.cpp
2
2
#include "ReachabilityResult.h"
3
3
#include "../PetriNetBuilder.h"
4
4
#include "../options.h"
 
5
#include "PetriEngine/PQL/Expressions.h"
5
6
 
6
7
namespace PetriEngine {
7
8
    namespace Reachability {
18
19
                size_t lastmarking)
19
20
        {
20
21
            if(result == Unknown) return Unknown;
 
22
 
21
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
            }
22
38
            std::cout << std::endl;    
23
39
            
24
40
            bool showTrace = (result == Satisfied);
48
64
            if (result == Satisfied)
49
65
                retval = query->isInvariant() ? NotSatisfied : Satisfied;
50
66
            else if (result == NotSatisfied)
51
 
                retval = query->isInvariant() ? Satisfied : NotSatisfied;
 
67
                retval = query->isInvariant() ? Satisfied : NotSatisfied;           
52
68
 
53
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
            
54
77
            if (retval == Unknown)
55
78
            {
56
79
                std::cout << "\nUnable to decide if " << querynames[index] << " is satisfied.";
57
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
            }
58
86
            else if (retval == Satisfied) {
59
87
                if(!options->statespaceexploration)
60
88
                {
61
 
                    std::cout << "TRUE " << techniques << std::endl;
 
89
                    std::cout << "TRUE " << techniques << printTechniques() << std::endl;
 
90
                    std::cout << "Query index " << index << " was solved" << std::endl;
62
91
                }
63
92
            } else if (retval == NotSatisfied) {
64
 
                if (!query->placeNameForBound().empty()) {
65
 
                    // find index of the place for reporting place bound
66
 
 
67
 
                    std::cout << query->getBound() << " " << techniquesStateSpace << std::endl;
68
 
 
69
 
                } else {
70
 
                    if(!options->statespaceexploration)
71
 
                    {
72
 
                        std::cout << "FALSE " << techniques << std::endl;
73
 
                    }
 
93
                if(!options->statespaceexploration)
 
94
                {
 
95
                    std::cout << "FALSE " << techniques << printTechniques() << std::endl;
 
96
                    std::cout << "Query index " << index << " was solved" << std::endl;
74
97
                }
75
98
            }
76
99
            
97
120
            }
98
121
            std::cout << "satisfied." << std::endl;
99
122
            
 
123
            if(options->cpnOverApprox)
 
124
                std::cout << "\nSolved using CPN Approximation\n" << std::endl;
 
125
            
100
126
            if(showTrace && options->trace)
101
127
            {
102
128
                if(stateset == NULL)
115
141
        
116
142
        std::string ResultPrinter::printTechniques() {
117
143
            std::string out;
118
 
            
119
 
            if (options->enablereduction > 0) {
120
 
                out += " STRUCTURAL_REDUCTION STATE_COMPRESSION";
121
 
            }
122
 
            if (options->stubbornreduction) {
123
 
                out += " STUBBORN_REDUCTION";
124
 
            }
125
 
            if (options->queryReductionTimeout > 0) {
126
 
                out += " QUERY_REDUCTION";
127
 
            }
128
 
            if (options->siphontrapTimeout > 0) {
129
 
                out += " SIPHON_TRAP_ANALYSIS";
130
 
            }
131
 
            if (options->isctl) {
132
 
                if (options->ctlalgorithm == CTL::CZero) {
133
 
                    out += " CTL CZERO";
134
 
                }
135
 
                else {
136
 
                    out += " CTL LOCAL";
137
 
                }
138
 
            }
139
 
            out += "\n";
 
144
                        
 
145
            if(options->queryReductionTimeout > 0)
 
146
            {
 
147
                out += "LP_APPROX ";
 
148
            }
 
149
 
 
150
            if(options->cpnOverApprox)
 
151
            {
 
152
                out += "CPN_APPROX ";
 
153
            }
 
154
            
 
155
            if(options->isCPN && !options->cpnOverApprox)
 
156
            {
 
157
                out += "UNFOLDING_TO_PT ";
 
158
            }
 
159
            
 
160
            if(options->queryReductionTimeout == 0 
 
161
#ifdef ENABLE_TAR
 
162
                            && !options->tar 
 
163
#endif
 
164
                            && options->siphontrapTimeout == 0)
 
165
            {
 
166
                out += "EXPLICIT STATE_COMPRESSION ";
 
167
                if(options->stubbornreduction)
 
168
                {
 
169
                    out += "STUBBORN_SETS ";
 
170
                }
 
171
            }
 
172
#ifdef ENABLE_TAR            
 
173
            if(options->tar)
 
174
            {
 
175
                out += "TRACE_ABSTRACTION_REFINEMENT ";
 
176
            }
 
177
#endif            
 
178
            if(options->siphontrapTimeout > 0)
 
179
            {
 
180
                out += "TOPOLOGICAL SIPHON_TRAP ";
 
181
            }
 
182
            
140
183
            return out;
141
184
        }
142
185