← Back to branch summary

~tapaal-ltl/verifypn/scc-optimise

« back to all changes in this revision

Viewing changes to PetriEngine/Reachability/ReachabilityResult.h

  • 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/ReachabilityResult.h
1
 
/* PeTe - Petri Engine exTremE
2
 
 * Copyright (C) 2011  Jonas Finnemann Jensen <jopsen@gmail.com>,
3
 
 *                     Thomas Søndersø Nielsen <primogens@gmail.com>,
4
 
 *                     Lars Kærlund Østergaard <larsko@gmail.com>,
5
 
 *                     Peter Gjøl Jensen <root@petergjoel.dk>
6
 
 * 
7
 
 * This program is free software: you can redistribute it and/or modify
8
 
 * it under the terms of the GNU General Public License as published by
9
 
 * the Free Software Foundation, either version 3 of the License, or
10
 
 * (at your option) any later version.
11
 
 * 
12
 
 * This program is distributed in the hope that it will be useful,
13
 
 * but WITHOUT ANY WARRANTY; without even the implied warranty of
14
 
 * MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE.  See the
15
 
 * GNU General Public License for more details.
16
 
 * 
17
 
 * You should have received a copy of the GNU General Public License
18
 
 * along with this program.  If not, see <http://www.gnu.org/licenses/>.
19
 
 */
20
 
#ifndef REACHABILITYRESULT_H
21
 
#define REACHABILITYRESULT_H
22
 
 
23
 
#include <vector>
24
 
#include "../PQL/PQL.h"
25
 
#include "../Structures/StateSet.h"
26
 
#include "../Reducer.h"
27
 
 
28
 
struct options_t;
29
 
 
30
 
namespace PetriEngine {
31
 
    class PetriNetBuilder;
32
 
    namespace Reachability {
33
 
 
34
 
        /** Result of a reachability search */
35
 
 
36
 
        class ResultPrinter {
37
 
        protected:
38
 
            PetriNetBuilder* builder;
39
 
            options_t* options;
40
 
            std::vector<std::string>& querynames;
41
 
            Reducer* reducer;
42
 
        public:
43
 
                        /** Types of results */
44
 
            enum Result {
45
 
                /** The query was satisfied */
46
 
                Satisfied,
47
 
                /** The query cannot be satisfied */
48
 
                NotSatisfied,
49
 
                /** We're unable to say if the query can be satisfied */
50
 
                Unknown,
51
 
                /** The query should be verified using the CTL engine */
52
 
                CTL,
53
 
                /** Just ignore */
54
 
                Ignore
55
 
            };
56
 
            
57
 
            const string techniques = "TECHNIQUES COLLATERAL_PROCESSING STRUCTURAL_REDUCTION QUERY_REDUCTION SAT_SMT ";
58
 
            const string techniquesStateSpace = "TECHNIQUES EXPLICIT STATE_COMPRESSION";
59
 
            
60
 
            ResultPrinter(PetriNetBuilder* b, options_t* o, std::vector<std::string>& querynames) 
61
 
            : builder(b), options(o), querynames(querynames), reducer(NULL)
62
 
            {};
63
 
            
64
 
            void setReducer(Reducer* r) { this->reducer = r; }
65
 
            
66
 
            Result printResult(
67
 
                size_t index,
68
 
                PQL::Condition* query, 
69
 
                ResultPrinter::Result result = Unknown,
70
 
                size_t expandedStates = 0,
71
 
                size_t exploredStates = 0,
72
 
                size_t discoveredStates = 0,
73
 
                const std::vector<size_t> enabledTransitionsCount = std::vector<size_t>(),
74
 
                int maxTokens = 0,
75
 
                const std::vector<uint32_t> maxPlaceBound = std::vector<uint32_t>(),
76
 
                Structures::StateSetInterface* stateset = NULL, size_t lastmarking = 0 );
77
 
            
78
 
            std::string printTechniques();
79
 
            
80
 
            void printTrace(Structures::StateSetInterface*, size_t lastmarking);
81
 
            
82
 
        };
83
 
    } // Reachability
84
 
} // PetriEngine
85
 
 
86
 
#endif // REACHABILITYRESULT_H