← Back to branch summary

~tapaal-ltl/verifypn/scc-optimise

« back to all changes in this revision

Viewing changes to include/PetriEngine/options.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:
include/PetriEngine/options.h
 
1
#ifndef OPTIONS_H
 
2
#define OPTIONS_H
 
3
 
 
4
#include <ctype.h>
 
5
#include <stddef.h>
 
6
#include <limits>
 
7
#include <set>
 
8
#include <string.h>
 
9
 
 
10
#include "Reachability/ReachabilitySearch.h"
 
11
#include "../CTL/Algorithm/AlgorithmTypes.h"
 
12
 
 
13
struct options_t {
 
14
//    bool outputtrace = false;
 
15
    int kbound = 0;
 
16
    char* modelfile = NULL;
 
17
    char* queryfile = NULL;
 
18
    int enablereduction = 1; // 0 ... disabled,  1 ... aggresive (default), 2 ... k-boundedness preserving, 3 ... selection
 
19
    std::vector<uint32_t> reductions{8,2,3,4,5,7,9,6,0,1};
 
20
    int reductionTimeout = 60;
 
21
    bool stubbornreduction = true; 
 
22
    bool statespaceexploration = false;
 
23
    bool printstatistics = true;
 
24
    std::set<size_t> querynumbers;
 
25
    PetriEngine::Reachability::Strategy strategy = PetriEngine::Reachability::DEFAULT;
 
26
    bool trace = false;
 
27
    int queryReductionTimeout = 30, lpsolveTimeout = 10;
 
28
    uint32_t siphontrapTimeout = 0;
 
29
    uint32_t siphonDepth = 0;
 
30
    uint32_t cores = 1;
 
31
 
 
32
    //CTL Specific options
 
33
    bool gamemode = false;
 
34
    bool isctl = false;
 
35
    CTL::CTLAlgorithmType ctlalgorithm = CTL::CZero;
 
36
    bool tar = false;
 
37
    uint32_t binary_query_io = 0;
 
38
    
 
39
    std::string query_out_file;
 
40
    std::string model_out_file;
 
41
 
 
42
    
 
43
    //CPN Specific options
 
44
    bool cpnOverApprox = false;
 
45
    bool isCPN = false;
 
46
    uint32_t seed_offset = 0;
 
47
 
 
48
    void print() {
 
49
        if (!printstatistics) {
 
50
            return;
 
51
        }
 
52
        
 
53
        string optionsOut;
 
54
        
 
55
        if (strategy == PetriEngine::Reachability::Strategy::BFS) {
 
56
            optionsOut = "\nSearch=BFS";
 
57
        } else if (strategy == PetriEngine::Reachability::Strategy::DFS) {
 
58
            optionsOut = "\nSearch=DFS";
 
59
        } else if (strategy == PetriEngine::Reachability::Strategy::HEUR) {
 
60
            optionsOut = "\nSearch=HEUR";
 
61
        } else if (strategy == PetriEngine::Reachability::Strategy::RDFS){
 
62
            optionsOut = "\nSearch=RDFS";
 
63
        } else {
 
64
            optionsOut = "\nSearch=OverApprox";
 
65
        }
 
66
        
 
67
        if (trace) {
 
68
            optionsOut += ",Trace=ENABLED";
 
69
        } else {
 
70
            optionsOut += ",Trace=DISABLED";
 
71
        }
 
72
        
 
73
        if (kbound > 0) {
 
74
            optionsOut += ",Token_Bound=" + std::to_string(kbound);
 
75
        }
 
76
        
 
77
        if (statespaceexploration) {
 
78
            optionsOut += ",State_Space_Exploration=ENABLED";
 
79
        } else {
 
80
            optionsOut += ",State_Space_Exploration=DISABLED";
 
81
        }
 
82
        
 
83
        if (enablereduction == 0) {
 
84
            optionsOut += ",Structural_Reduction=DISABLED";
 
85
        } else if (enablereduction == 1) {
 
86
            optionsOut += ",Structural_Reduction=AGGRESSIVE";
 
87
        } else {
 
88
            optionsOut += ",Structural_Reduction=KBOUND_PRESERVING";
 
89
        }
 
90
        
 
91
        optionsOut += ",Struct_Red_Timout=" + std::to_string(reductionTimeout);
 
92
        
 
93
        if (stubbornreduction) {
 
94
            optionsOut += ",Stubborn_Reduction=ENABLED";
 
95
        } else {
 
96
            optionsOut += ",Stubborn_Reduction=DISABLED";
 
97
        }
 
98
        
 
99
        if (queryReductionTimeout > 0) {
 
100
            optionsOut += ",Query_Simplication=ENABLED,QSTimeout=" + std::to_string(queryReductionTimeout);
 
101
        } else {
 
102
            optionsOut += ",Query_Simplication=DISABLED";
 
103
        }
 
104
        
 
105
        if (siphontrapTimeout > 0) {
 
106
            optionsOut += ",Siphon_Trap=ENABLED,SPTimeout=" + std::to_string(siphontrapTimeout);
 
107
        } else {
 
108
            optionsOut += ",Siphon_Trap=DISABLED";
 
109
        }
 
110
        
 
111
        optionsOut += ",LPSolve_Timeout=" + std::to_string(lpsolveTimeout);
 
112
        
 
113
 
 
114
        if (ctlalgorithm == CTL::CZero) {
 
115
            optionsOut += ",CTLAlgorithm=CZERO";
 
116
        } else {
 
117
            optionsOut += ",CTLAlgorithm=LOCAL";
 
118
        }
 
119
        
 
120
        optionsOut += "\n";
 
121
        
 
122
        std::cout << optionsOut;
 
123
    }
 
124
};
 
125
 
 
126
#endif