-
Notifications
You must be signed in to change notification settings - Fork 3
/
Copy pathgenerate_table2
150 lines (150 loc) · 15.5 KB
/
generate_table2
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
123
124
125
126
127
128
129
130
131
132
133
134
135
136
137
138
139
140
141
142
143
144
145
146
147
148
149
150
# Drift + Trace partitioning all-ev-pos:
./drift.exe -file tests/effects/all-ev-pos.ml -prop tests/effects/all-ev-pos.yml.prp -ev-trans trans -trace-len 1 -if-part true -out 2 -domain Polka_ls -thold true
# evDrift without Trace partitioning all-ev-pos:
./drift.exe -file tests/effects/all-ev-pos.ml -prop tests/effects/all-ev-pos.yml.prp -ev-trans direct -trace-len 1 -if-part false -out 2 -domain Polka_ls -thold true
# evDrift + Trace partitioning all-ev-pos:
./drift.exe -file tests/effects/all-ev-pos.ml -prop tests/effects/all-ev-pos.yml.prp -ev-trans direct -trace-len 1 -if-part false -out 2 -domain Polka_ls -thold true
# Drift + Trace partitioning auction:
./drift.exe -file tests/effects/auction.ml -prop tests/effects/auction.yml.prp -ev-trans trans -trace-len 1 -if-part true -out 2 -domain Polka_st -thold true
# evDrift without Trace partitioning auction:
./drift.exe -file tests/effects/auction.ml -prop tests/effects/auction.yml.prp -ev-trans direct -trace-len 1 -if-part false -out 2 -domain Polka_ls -thold true
# evDrift + Trace partitioning auction:
./drift.exe -file tests/effects/auction.ml -prop tests/effects/auction.yml.prp -ev-trans direct -trace-len 1 -if-part false -out 2 -domain Polka_ls -thold true
# Drift + Trace partitioning binomial_heap:
./drift.exe -file tests/effects/binomial_heap.ml -prop tests/effects/binomial_heap.yml.prp -ev-trans trans -trace-len 1 -if-part true -out 2 -domain PolkaGrid -thold false
# evDrift without Trace partitioning binomial_heap:
./drift.exe -file tests/effects/binomial_heap.ml -prop tests/effects/binomial_heap.yml.prp -ev-trans direct -trace-len 1 -if-part false -out 2 -domain Polka_ls -thold true
# evDrift + Trace partitioning binomial_heap:
./drift.exe -file tests/effects/binomial_heap.ml -prop tests/effects/binomial_heap.yml.prp -ev-trans direct -trace-len 1 -if-part false -out 2 -domain Polka_ls -thold true
# Drift + Trace partitioning concurrent_sum:
./drift.exe -file tests/effects/concurrent_sum.ml -prop tests/effects/concurrent_sum.yml.prp -ev-trans trans -trace-len 1 -if-part true -out 2 -domain Polka_ls -thold true
# evDrift without Trace partitioning concurrent_sum:
./drift.exe -file tests/effects/concurrent_sum.ml -prop tests/effects/concurrent_sum.yml.prp -ev-trans direct -trace-len 1 -if-part false -out 2 -domain Polka_ls -thold true
# evDrift + Trace partitioning concurrent_sum:
./drift.exe -file tests/effects/concurrent_sum.ml -prop tests/effects/concurrent_sum.yml.prp -ev-trans direct -trace-len 1 -if-part false -out 2 -domain Polka_ls -thold true
# Drift + Trace partitioning depend:
./drift.exe -file tests/effects/depend.ml -prop tests/effects/depend.yml.prp -ev-trans trans -trace-len 1 -if-part true -out 2 -domain Polka_ls -thold true
# evDrift without Trace partitioning depend:
./drift.exe -file tests/effects/depend.ml -prop tests/effects/depend.yml.prp -ev-trans direct -trace-len 1 -if-part false -out 2 -domain Polka_st -thold true
# evDrift + Trace partitioning depend:
./drift.exe -file tests/effects/depend.ml -prop tests/effects/depend.yml.prp -ev-trans direct -trace-len 1 -if-part false -out 2 -domain Polka_st -thold true
# Drift + Trace partitioning disj:
./drift.exe -file tests/effects/disj.ml -prop tests/effects/disj.yml.prp -ev-trans trans -trace-len 1 -if-part true -out 2 -domain PolkaGrid -thold false
# evDrift without Trace partitioning disj:
./drift.exe -file tests/effects/disj.ml -prop tests/effects/disj.yml.prp -ev-trans direct -trace-len 1 -if-part false -out 2 -domain PolkaGrid -thold false
# evDrift + Trace partitioning disj:
./drift.exe -file tests/effects/disj.ml -prop tests/effects/disj.yml.prp -ev-trans direct -trace-len 1 -if-part false -out 2 -domain PolkaGrid -thold false
# Drift + Trace partitioning disj-gte:
./drift.exe -file tests/effects/disj-gte.ml -prop tests/effects/disj-gte.yml.prp -ev-trans trans -trace-len 1 -if-part true -out 2 -domain Polka_ls -thold true
# evDrift without Trace partitioning disj-gte:
./drift.exe -file tests/effects/disj-gte.ml -prop tests/effects/disj-gte.yml.prp -ev-trans direct -trace-len 1 -if-part false -out 2 -domain Polka_ls -thold true
# evDrift + Trace partitioning disj-gte:
./drift.exe -file tests/effects/disj-gte.ml -prop tests/effects/disj-gte.yml.prp -ev-trans direct -trace-len 1 -if-part false -out 2 -domain Polka_ls -thold true
# Drift + Trace partitioning disj-nondet:
./drift.exe -file tests/effects/disj-nondet.ml -prop tests/effects/disj-nondet.yml.prp -ev-trans trans -trace-len 1 -if-part true -out 2 -domain Polka_ls -thold true
# evDrift without Trace partitioning disj-nondet:
./drift.exe -file tests/effects/disj-nondet.ml -prop tests/effects/disj-nondet.yml.prp -ev-trans direct -trace-len 1 -if-part false -out 2 -domain Polka_ls -thold true
# evDrift + Trace partitioning disj-nondet:
./drift.exe -file tests/effects/disj-nondet.ml -prop tests/effects/disj-nondet.yml.prp -ev-trans direct -trace-len 1 -if-part false -out 2 -domain Polka_ls -thold true
# Drift + Trace partitioning higher-order:
./drift.exe -file tests/effects/higher-order.ml -prop tests/effects/higher-order.yml.prp -ev-trans trans -trace-len 1 -if-part true -out 2 -domain Polka_ls -thold true
# evDrift without Trace partitioning higher-order:
./drift.exe -file tests/effects/higher-order.ml -prop tests/effects/higher-order.yml.prp -ev-trans direct -trace-len 1 -if-part false -out 2 -domain Polka_ls -thold true
# evDrift + Trace partitioning higher-order:
./drift.exe -file tests/effects/higher-order.ml -prop tests/effects/higher-order.yml.prp -ev-trans direct -trace-len 1 -if-part false -out 2 -domain Polka_ls -thold true
# Drift + Trace partitioning last-ev-even:
./drift.exe -file tests/effects/last-ev-even.ml -prop tests/effects/last-ev-even.yml.prp -ev-trans trans -trace-len 1 -if-part true -out 2 -domain PolkaGrid -thold false
# evDrift without Trace partitioning last-ev-even:
./drift.exe -file tests/effects/last-ev-even.ml -prop tests/effects/last-ev-even.yml.prp -ev-trans direct -trace-len 1 -if-part false -out 2 -domain PolkaGrid -thold false
# evDrift + Trace partitioning last-ev-even:
./drift.exe -file tests/effects/last-ev-even.ml -prop tests/effects/last-ev-even.yml.prp -ev-trans direct -trace-len 1 -if-part false -out 2 -domain PolkaGrid -thold false
# Drift + Trace partitioning lics18-amortized:
./drift.exe -file tests/effects/lics18-amortized.ml -prop tests/effects/lics18-amortized.yml.prp -ev-trans trans -trace-len 1 -if-part true -out 2 -domain PolkaGrid -thold false
# evDrift without Trace partitioning lics18-amortized:
./drift.exe -file tests/effects/lics18-amortized.ml -prop tests/effects/lics18-amortized.yml.prp -ev-trans direct -trace-len 1 -if-part false -out 2 -domain Polka_ls -thold true
# evDrift + Trace partitioning lics18-amortized:
./drift.exe -file tests/effects/lics18-amortized.ml -prop tests/effects/lics18-amortized.yml.prp -ev-trans direct -trace-len 1 -if-part false -out 2 -domain Polka_ls -thold true
# Drift + Trace partitioning lics18-hoshrink:
./drift.exe -file tests/effects/lics18-hoshrink.ml -prop tests/effects/lics18-hoshrink.yml.prp -ev-trans trans -trace-len 1 -if-part true -out 2 -domain Polka_ls -thold true
# evDrift without Trace partitioning lics18-hoshrink:
./drift.exe -file tests/effects/lics18-hoshrink.ml -prop tests/effects/lics18-hoshrink.yml.prp -ev-trans direct -trace-len 1 -if-part false -out 2 -domain PolkaGrid -thold false
# evDrift + Trace partitioning lics18-hoshrink:
./drift.exe -file tests/effects/lics18-hoshrink.ml -prop tests/effects/lics18-hoshrink.yml.prp -ev-trans direct -trace-len 1 -if-part false -out 2 -domain PolkaGrid -thold false
# Drift + Trace partitioning lics18-web:
./drift.exe -file tests/effects/lics18-web.ml -prop tests/effects/lics18-web.yml.prp -ev-trans trans -trace-len 1 -if-part true -out 2 -domain Polka_ls -thold true
# evDrift without Trace partitioning lics18-web:
./drift.exe -file tests/effects/lics18-web.ml -prop tests/effects/lics18-web.yml.prp -ev-trans direct -trace-len 1 -if-part false -out 2 -domain Polka_ls -thold true
# evDrift + Trace partitioning lics18-web:
./drift.exe -file tests/effects/lics18-web.ml -prop tests/effects/lics18-web.yml.prp -ev-trans direct -trace-len 1 -if-part false -out 2 -domain Polka_ls -thold true
# Drift + Trace partitioning market:
./drift.exe -file tests/effects/market.ml -prop tests/effects/market.yml.prp -ev-trans trans -trace-len 1 -if-part true -out 2 -domain PolkaGrid -thold false
# evDrift without Trace partitioning market:
./drift.exe -file tests/effects/market.ml -prop tests/effects/market.yml.prp -ev-trans direct -trace-len 1 -if-part false -out 2 -domain Polka_ls -thold true
# evDrift + Trace partitioning market:
./drift.exe -file tests/effects/market.ml -prop tests/effects/market.yml.prp -ev-trans direct -trace-len 1 -if-part false -out 2 -domain Polka_ls -thold true
# Drift + Trace partitioning max-min:
./drift.exe -file tests/effects/max-min.ml -prop tests/effects/max-min.yml.prp -ev-trans trans -trace-len 1 -if-part true -out 2 -domain Polka_st -thold true
# evDrift without Trace partitioning max-min:
./drift.exe -file tests/effects/max-min.ml -prop tests/effects/max-min.yml.prp -ev-trans direct -trace-len 1 -if-part false -out 2 -domain Polka_st -thold true
# evDrift + Trace partitioning max-min:
./drift.exe -file tests/effects/max-min.ml -prop tests/effects/max-min.yml.prp -ev-trans direct -trace-len 1 -if-part false -out 2 -domain Polka_st -thold true
# Drift + Trace partitioning monotonic:
./drift.exe -file tests/effects/monotonic.ml -prop tests/effects/monotonic.yml.prp -ev-trans trans -trace-len 1 -if-part true -out 2 -domain Polka_ls -thold true
# evDrift without Trace partitioning monotonic:
./drift.exe -file tests/effects/monotonic.ml -prop tests/effects/monotonic.yml.prp -ev-trans direct -trace-len 1 -if-part false -out 2 -domain Polka_ls -thold true
# evDrift + Trace partitioning monotonic:
./drift.exe -file tests/effects/monotonic.ml -prop tests/effects/monotonic.yml.prp -ev-trans direct -trace-len 1 -if-part false -out 2 -domain Polka_ls -thold true
# Drift + Trace partitioning nondet_max:
./drift.exe -file tests/effects/nondet_max.ml -prop tests/effects/nondet_max.yml.prp -ev-trans trans -trace-len 1 -if-part true -out 2 -domain Polka_ls -thold true
# evDrift without Trace partitioning nondet_max:
./drift.exe -file tests/effects/nondet_max.ml -prop tests/effects/nondet_max.yml.prp -ev-trans direct -trace-len 1 -if-part false -out 2 -domain Polka_ls -thold true
# evDrift + Trace partitioning nondet_max:
./drift.exe -file tests/effects/nondet_max.ml -prop tests/effects/nondet_max.yml.prp -ev-trans direct -trace-len 1 -if-part false -out 2 -domain Polka_ls -thold true
# Drift + Trace partitioning order-irrel:
./drift.exe -file tests/effects/order-irrel.ml -prop tests/effects/order-irrel.yml.prp -ev-trans trans -trace-len 1 -if-part true -out 2 -domain Polka_st -thold true
# evDrift without Trace partitioning order-irrel:
./drift.exe -file tests/effects/order-irrel.ml -prop tests/effects/order-irrel.yml.prp -ev-trans direct -trace-len 1 -if-part false -out 2 -domain Polka_st -thold true
# evDrift + Trace partitioning order-irrel:
./drift.exe -file tests/effects/order-irrel.ml -prop tests/effects/order-irrel.yml.prp -ev-trans direct -trace-len 1 -if-part false -out 2 -domain Polka_st -thold true
# Drift + Trace partitioning order-irrel-nondet:
./drift.exe -file tests/effects/order-irrel-nondet.ml -prop tests/effects/order-irrel-nondet.yml.prp -ev-trans trans -trace-len 1 -if-part true -out 2 -domain Polka_ls -thold true
# evDrift without Trace partitioning order-irrel-nondet:
./drift.exe -file tests/effects/order-irrel-nondet.ml -prop tests/effects/order-irrel-nondet.yml.prp -ev-trans direct -trace-len 1 -if-part false -out 2 -domain Polka_ls -thold true
# evDrift + Trace partitioning order-irrel-nondet:
./drift.exe -file tests/effects/order-irrel-nondet.ml -prop tests/effects/order-irrel-nondet.yml.prp -ev-trans direct -trace-len 1 -if-part false -out 2 -domain Polka_ls -thold true
# Drift + Trace partitioning overview1:
./drift.exe -file tests/effects/overview1.ml -prop tests/effects/overview1.yml.prp -ev-trans trans -trace-len 1 -if-part true -out 2 -domain Polka_ls -thold true
# evDrift without Trace partitioning overview1:
./drift.exe -file tests/effects/overview1.ml -prop tests/effects/overview1.yml.prp -ev-trans direct -trace-len 1 -if-part false -out 2 -domain Polka_ls -thold true
# evDrift + Trace partitioning overview1:
./drift.exe -file tests/effects/overview1.ml -prop tests/effects/overview1.yml.prp -ev-trans direct -trace-len 1 -if-part false -out 2 -domain Polka_ls -thold true
# Drift + Trace partitioning reentr:
./drift.exe -file tests/effects/reentr.ml -prop tests/effects/reentr.yml.prp -ev-trans trans -trace-len 1 -if-part true -out 2 -domain Polka_st -thold true
# evDrift without Trace partitioning reentr:
./drift.exe -file tests/effects/reentr.ml -prop tests/effects/reentr.yml.prp -ev-trans direct -trace-len 1 -if-part false -out 2 -domain Polka_ls -thold true
# evDrift + Trace partitioning reentr:
./drift.exe -file tests/effects/reentr.ml -prop tests/effects/reentr.yml.prp -ev-trans direct -trace-len 1 -if-part false -out 2 -domain Polka_ls -thold true
# Drift + Trace partitioning resource-analysis:
./drift.exe -file tests/effects/resource-analysis.ml -prop tests/effects/resource-analysis.yml.prp -ev-trans trans -trace-len 1 -if-part true -out 2 -domain Polka_ls -thold true
# evDrift without Trace partitioning resource-analysis:
./drift.exe -file tests/effects/resource-analysis.ml -prop tests/effects/resource-analysis.yml.prp -ev-trans direct -trace-len 1 -if-part false -out 2 -domain Polka_ls -thold true
# evDrift + Trace partitioning resource-analysis:
./drift.exe -file tests/effects/resource-analysis.ml -prop tests/effects/resource-analysis.yml.prp -ev-trans direct -trace-len 1 -if-part false -out 2 -domain Polka_ls -thold true
# Drift + Trace partitioning sum-appendix:
./drift.exe -file tests/effects/sum-appendix.ml -prop tests/effects/sum-appendix.yml.prp -ev-trans trans -trace-len 1 -if-part true -out 2 -domain Polka_ls -thold true
# evDrift without Trace partitioning sum-appendix:
./drift.exe -file tests/effects/sum-appendix.ml -prop tests/effects/sum-appendix.yml.prp -ev-trans direct -trace-len 1 -if-part false -out 2 -domain Polka_ls -thold true
# evDrift + Trace partitioning sum-appendix:
./drift.exe -file tests/effects/sum-appendix.ml -prop tests/effects/sum-appendix.yml.prp -ev-trans direct -trace-len 1 -if-part false -out 2 -domain Polka_ls -thold true
# Drift + Trace partitioning sum-of-ev-even:
./drift.exe -file tests/effects/sum-of-ev-even.ml -prop tests/effects/sum-of-ev-even.yml.prp -ev-trans trans -trace-len 1 -if-part true -out 2 -domain PolkaGrid -thold false
# evDrift without Trace partitioning sum-of-ev-even:
./drift.exe -file tests/effects/sum-of-ev-even.ml -prop tests/effects/sum-of-ev-even.yml.prp -ev-trans direct -trace-len 1 -if-part false -out 2 -domain PolkaGrid -thold false
# evDrift + Trace partitioning sum-of-ev-even:
./drift.exe -file tests/effects/sum-of-ev-even.ml -prop tests/effects/sum-of-ev-even.yml.prp -ev-trans direct -trace-len 1 -if-part false -out 2 -domain PolkaGrid -thold false
# Drift + Trace partitioning temperature:
./drift.exe -file tests/effects/temperature.ml -prop tests/effects/temperature.yml.prp -ev-trans trans -trace-len 1 -if-part true -out 2 -domain PolkaGrid -thold false
# evDrift without Trace partitioning temperature:
./drift.exe -file tests/effects/temperature.ml -prop tests/effects/temperature.yml.prp -ev-trans direct -trace-len 1 -if-part false -out 2 -domain PolkaGrid -thold false
# evDrift + Trace partitioning temperature:
./drift.exe -file tests/effects/temperature.ml -prop tests/effects/temperature.yml.prp -ev-trans direct -trace-len 1 -if-part false -out 2 -domain PolkaGrid -thold false