1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
45
46
47
48
49
50
51
52
53
54
55
56
57
58
59
60
61
62
63
64
65
66
67
68
69
70
71
72
73
74
75
76
77
78
79
80
81
82
83
84
85
86
87
88
89
90
91
92
93
94
95
96
97
98
99
100
101
102
103
104
105
106
107
108
109
110
111
112
113
114
115
116
117
118
119
120
121
122
|
package dk.aau.cs.verification.batchProcessing;
import java.util.List;
import pipe.dataLayer.TAPNQuery.SearchOption;
import dk.aau.cs.translations.ReductionOption;
import dk.aau.cs.util.Require;
public class BatchProcessingVerificationOptions {
public enum QueryPropertyOption {
KeepQueryOption, SearchWholeStateSpace, ExistDeadlock, Soundness, StrongSoundness
};
public enum SymmetryOption {
KeepQueryOption, Yes, No
};
public enum StubbornReductionOption{
KeepQueryOption, Yes, No
};
public enum ApproximationMethodOption {
KeepQueryOption, None, OverApproximation, UnderApproximation
}
private List<ReductionOption> reductionOptions;
private ReductionOption reductionOption;
private SearchOption searchOption;
private QueryPropertyOption queryPropertyOption;
private SymmetryOption symmetryOption;
private StubbornReductionOption stubbornReductionOption;
private ApproximationMethodOption approximationMethodOption;
private int approximationDenominator = 0;
private boolean keepQueryCapacity;
private int capacity;
private boolean discreteInclusion = false; // only for VerifyTAPN
private boolean useTimeDartPTrie = false;
private boolean useTimeDart = false;
private boolean usePTrie = false;
public BatchProcessingVerificationOptions(QueryPropertyOption queryPropertyOption, boolean keepQueryCapacity, int capacity, SearchOption searchOption, SymmetryOption symmetryOption, StubbornReductionOption stubbornReductionOption, ReductionOption reductionOption, boolean discreteInclusion,
boolean useTimeDartPTrie, boolean useTimeDart, boolean usePTrie, ApproximationMethodOption approximationMethodOption, int approximationDenominator, List<ReductionOption> reductionOptions) {
Require.that(!(reductionOptions == null && reductionOption == ReductionOption.BatchProcessingUserDefinedReductions), "ReductionOption was given as userdefined but a list of reductionoptions was not given");
this.searchOption = searchOption;
this.reductionOption = reductionOption;
this.queryPropertyOption = queryPropertyOption;
this.symmetryOption = symmetryOption;
this.stubbornReductionOption = stubbornReductionOption;
this.keepQueryCapacity = keepQueryCapacity;
this.capacity = capacity;
this.discreteInclusion = discreteInclusion;
this.useTimeDartPTrie = useTimeDartPTrie;
this.useTimeDart = useTimeDart;
this.usePTrie = usePTrie;
this.reductionOptions = reductionOptions;
this.approximationMethodOption = approximationMethodOption;
this.approximationDenominator = approximationDenominator;
}
public BatchProcessingVerificationOptions(QueryPropertyOption queryPropertyOption, boolean keepQueryCapacity, int capacity, SearchOption searchOption, SymmetryOption symmetryOption, StubbornReductionOption stubbornReductionOption, ReductionOption reductionOption, boolean discreteInclusion,
boolean useTimeDartPTrie, boolean useTimeDart, boolean usePTrie, ApproximationMethodOption approximationMethodOption, int approximationRValue) {
this(queryPropertyOption, keepQueryCapacity, capacity, searchOption, symmetryOption, stubbornReductionOption, reductionOption, discreteInclusion, useTimeDartPTrie, useTimeDart, usePTrie, approximationMethodOption, approximationRValue, null);
}
public boolean isReductionOptionUserdefined(){
return reductionOption == ReductionOption.BatchProcessingUserDefinedReductions;
}
public List<ReductionOption> reductionOptions() {
Require.that(reductionOption == ReductionOption.BatchProcessingUserDefinedReductions, "Tried to get the userdefined reductionoptions, but the reductionoption is not userdefined");
return reductionOptions;
}
public SearchOption searchOption() {
return searchOption;
}
public boolean discreteInclusion() {
return discreteInclusion;
}
public boolean useTimeDartPTrie(){
return useTimeDartPTrie;
}
public boolean useTimeDart(){
return useTimeDart;
}
public boolean usePTrie(){
return usePTrie;
}
public QueryPropertyOption queryPropertyOption() {
return queryPropertyOption;
}
public SymmetryOption symmetry() {
return symmetryOption;
}
public StubbornReductionOption stubbornReductionOption(){
return stubbornReductionOption;
}
public boolean KeepCapacityFromQuery() {
return keepQueryCapacity;
}
public int capacity() {
return capacity;
}
public ApproximationMethodOption approximationMethodOption() {
return approximationMethodOption;
}
public int approximationDenominator() {
return approximationDenominator;
}
}
|