← Back to branch summary

~yrke/tapaal/slimImageIcons-2

« back to all changes in this revision

Viewing changes to src/dk/aau/cs/verification/VerifyTAPN/VerifyDTAPNOptions.java

  • Committer: Jiri Srba
  • Date: 2020-04-28 19:15:28 UTC
  • mfrom: (998.2.376 testbranch)
  • Revision ID: srba@cs.aau.dk-20200428191528-3xxjqa1r4jcob5ur
merged in lp:~yrke/tapaal/testbranch doing majour refactoring of the GUI

Show diffs side-by-side

added added

removed removed

Lines of Context:
src/dk/aau/cs/verification/VerifyTAPN/VerifyDTAPNOptions.java
11
11
        private boolean timeDarts;
12
12
        private boolean pTrie;
13
13
        private WorkflowMode workflow;
14
 
        private long workflowbound;
 
14
        private long workflowbound;
15
15
        //only used for boundedness analysis
16
16
        private boolean dontUseDeadPlaces = false;
17
17
        private boolean useStubbornReduction = true;
18
18
        
19
19
        //Only used for boundedness analysis
20
 
        public VerifyDTAPNOptions(boolean dontUseDeadPlaces, int extraTokens, TraceOption traceOption,
21
 
                        SearchOption search, boolean symmetry, boolean timeDarts,
 
20
        public VerifyDTAPNOptions(
 
21
                        boolean dontUseDeadPlaces,
 
22
                        int extraTokens,
 
23
                        TraceOption traceOption,
 
24
                        SearchOption search,
 
25
                        boolean symmetry,
 
26
                        boolean timeDarts,
22
27
                        boolean pTrie,
23
 
                        boolean enableOverApproximation, boolean enableUnderApproximation, int approximationDenominator,
24
 
                        boolean stubbornReduction) {
 
28
                        boolean enableOverApproximation,
 
29
                        boolean enableUnderApproximation,
 
30
                        int approximationDenominator,
 
31
                        boolean stubbornReduction
 
32
        ) {
25
33
                this(extraTokens, traceOption, search, symmetry, true, timeDarts, pTrie, false, false, new InclusionPlaces(), WorkflowMode.NOT_WORKFLOW, 0, enableOverApproximation, enableUnderApproximation, approximationDenominator, stubbornReduction);
26
34
                this.dontUseDeadPlaces = dontUseDeadPlaces;
27
35
        }
28
36
 
29
 
        public VerifyDTAPNOptions(int extraTokens, TraceOption traceOption,
30
 
                        SearchOption search, boolean symmetry, boolean gcd, boolean timeDarts,
31
 
                        boolean pTrie, boolean useOverApproximation, boolean discreteInclusion,
32
 
                        InclusionPlaces inclusionPlaces, WorkflowMode workflow, long workflowbound,
33
 
                        boolean enableOverApproximation, boolean enableUnderApproximation, int approximationDenominator,
34
 
                        boolean stubbornReduction) {
35
 
                super(extraTokens, traceOption, search, symmetry, useOverApproximation, discreteInclusion, inclusionPlaces, enableOverApproximation, enableUnderApproximation, approximationDenominator);
 
37
        public VerifyDTAPNOptions(
 
38
                        int extraTokens,
 
39
                        TraceOption traceOption,
 
40
                        SearchOption search,
 
41
                        boolean symmetry,
 
42
                        boolean gcd,
 
43
                        boolean timeDarts,
 
44
                        boolean pTrie,
 
45
                        boolean useStateequationCheck,
 
46
                        boolean discreteInclusion,
 
47
                        InclusionPlaces inclusionPlaces,
 
48
                        WorkflowMode workflow,
 
49
                        long workflowbound,
 
50
                        boolean enableOverApproximation,
 
51
                        boolean enableUnderApproximation,
 
52
                        int approximationDenominator,
 
53
                        boolean stubbornReduction
 
54
        ) {
 
55
                super(extraTokens, traceOption, search, symmetry, useStateequationCheck, discreteInclusion, inclusionPlaces, enableOverApproximation, enableUnderApproximation, approximationDenominator);
36
56
                this.timeDarts = timeDarts;
37
57
                this.pTrie = pTrie;
38
58
                this.workflow = workflow;
43
63
        
44
64
        @Override
45
65
        public String toString() {
46
 
                StringBuffer result = new StringBuffer(super.toString());
 
66
                StringBuilder result = new StringBuilder(super.toString());
47
67
                
48
68
                result.append(' ');
49
69
                result.append("-m ");
58
78
                        result.append(" -w 1");
59
79
                }else if(workflow == WorkflowMode.WORKFLOW_STRONG_SOUNDNESS){
60
80
                        result.append(" -w 2");
61
 
                        result.append(" -b ");
62
 
                        result.append(workflowbound);
63
 
                }
 
81
                        result.append(" -b ");
 
82
                        result.append(workflowbound);
 
83
                }
64
84
                result.append(' ');
65
85
                result.append(dontUseDeadPlaces ? "-d" : "");
66
86
                result.append(' ');
67
 
                if (workflow != WorkflowMode.WORKFLOW_SOUNDNESS && workflow != WorkflowMode.WORKFLOW_STRONG_SOUNDNESS) {
68
 
                    result.append(gcd ? "-c" : ""); // GCD optimization is not sound for workflow analysis
69
 
                }
 
87
 
 
88
                if (workflow != WorkflowMode.WORKFLOW_SOUNDNESS && workflow != WorkflowMode.WORKFLOW_STRONG_SOUNDNESS) {
 
89
                        result.append(gcd ? "-c" : ""); // GCD optimization is not sound for workflow analysis
 
90
                }
 
91
 
70
92
                return result.toString();
71
93
        }
72
94
 
78
100
                return pTrie;
79
101
        }
80
102
        
81
 
        public WorkflowMode getWorkflowMode(){
82
 
            return workflow;
83
 
        }
 
103
        public WorkflowMode getWorkflowMode(){
 
104
                return workflow;
 
105
        }
84
106
        
85
107
}