-
Notifications
You must be signed in to change notification settings - Fork 3
/
Copy pathgenerate_table1
104 lines (104 loc) · 10.6 KB
/
generate_table1
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
# Drift on 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 0 -if-part false -io-effects false -out 2 -domain Polka_ls -thold true
# evDrift on 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 0 -if-part false -io-effects false -out 2 -domain Polka_ls -thold true
# Drift on alt-inev:
./drift.exe -file tests/effects/alt-inev.ml -prop tests/effects/alt-inev.yml.prp -ev-trans trans -trace-len 0 -if-part false -io-effects false -out 2 -domain Polka_ls -thold true
# evDrift on alt-inev:
./drift.exe -file tests/effects/alt-inev.ml -prop tests/effects/alt-inev.yml.prp -ev-trans direct -trace-len 0 -if-part false -io-effects true -out 2 -domain Polka_ls -thold true
# Drift on auction:
./drift.exe -file tests/effects/auction.ml -prop tests/effects/auction.yml.prp -ev-trans trans -trace-len 1 -if-part false -io-effects false -out 2 -domain Polka_ls -thold true
# evDrift on auction:
./drift.exe -file tests/effects/auction.ml -prop tests/effects/auction.yml.prp -ev-trans direct -trace-len 0 -if-part false -io-effects true -out 2 -domain Polka_ls -thold true
# Drift on binomial_heap:
./drift.exe -file tests/effects/binomial_heap.ml -prop tests/effects/binomial_heap.yml.prp -ev-trans trans -trace-len 0 -if-part false -io-effects false -out 2 -domain PolkaGrid -thold false
# evDrift on binomial_heap:
./drift.exe -file tests/effects/binomial_heap.ml -prop tests/effects/binomial_heap.yml.prp -ev-trans direct -trace-len 0 -if-part false -io-effects true -out 2 -domain Polka_ls -thold true
# Drift on concurrent_sum:
./drift.exe -file tests/effects/concurrent_sum.ml -prop tests/effects/concurrent_sum.yml.prp -ev-trans trans -trace-len 0 -if-part false -io-effects false -out 2 -domain PolkaGrid -thold false
# evDrift on concurrent_sum:
./drift.exe -file tests/effects/concurrent_sum.ml -prop tests/effects/concurrent_sum.yml.prp -ev-trans direct -trace-len 0 -if-part false -io-effects false -out 2 -domain Polka_ls -thold true
# Drift on depend:
./drift.exe -file tests/effects/depend.ml -prop tests/effects/depend.yml.prp -ev-trans trans -trace-len 0 -if-part false -io-effects false -out 2 -domain Polka_ls -thold true
# evDrift on depend:
./drift.exe -file tests/effects/depend.ml -prop tests/effects/depend.yml.prp -ev-trans direct -trace-len 0 -if-part false -io-effects true -out 2 -domain Polka_ls -thold true
# Drift on disj:
./drift.exe -file tests/effects/disj.ml -prop tests/effects/disj.yml.prp -ev-trans trans -trace-len 0 -if-part false -io-effects false -out 2 -domain PolkaGrid -thold false
# evDrift on disj:
./drift.exe -file tests/effects/disj.ml -prop tests/effects/disj.yml.prp -ev-trans direct -trace-len 0 -if-part false -io-effects true -out 2 -domain PolkaGrid -thold false
# Drift on disj-gte:
./drift.exe -file tests/effects/disj-gte.ml -prop tests/effects/disj-gte.yml.prp -ev-trans trans -trace-len 0 -if-part false -io-effects false -out 2 -domain PolkaGrid -thold false
# evDrift on disj-gte:
./drift.exe -file tests/effects/disj-gte.ml -prop tests/effects/disj-gte.yml.prp -ev-trans direct -trace-len 0 -if-part false -io-effects true -out 2 -domain Polka_ls -thold true
# Drift on disj-nondet:
./drift.exe -file tests/effects/disj-nondet.ml -prop tests/effects/disj-nondet.yml.prp -ev-trans trans -trace-len 0 -if-part false -io-effects false -out 2 -domain PolkaGrid -thold false
# evDrift on disj-nondet:
./drift.exe -file tests/effects/disj-nondet.ml -prop tests/effects/disj-nondet.yml.prp -ev-trans direct -trace-len 0 -if-part false -io-effects true -out 2 -domain Polka_ls -thold true
# Drift on higher-order:
./drift.exe -file tests/effects/higher-order.ml -prop tests/effects/higher-order.yml.prp -ev-trans trans -trace-len 0 -if-part false -io-effects false -out 2 -domain Polka_ls -thold true
# evDrift on higher-order:
./drift.exe -file tests/effects/higher-order.ml -prop tests/effects/higher-order.yml.prp -ev-trans direct -trace-len 0 -if-part false -io-effects false -out 2 -domain Polka_ls -thold true
# Drift on 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 0 -if-part false -io-effects false -out 2 -domain Polka_ls -thold true
# evDrift on 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 true -io-effects false -out 2 -domain PolkaGrid -thold false
# Drift on lics18-amortized:
./drift.exe -file tests/effects/lics18-amortized.ml -prop tests/effects/lics18-amortized.yml.prp -ev-trans trans -trace-len 0 -if-part false -io-effects false -out 2 -domain Polka_ls -thold true
# evDrift on lics18-amortized:
./drift.exe -file tests/effects/lics18-amortized.ml -prop tests/effects/lics18-amortized.yml.prp -ev-trans direct -trace-len 0 -if-part false -io-effects false -out 2 -domain Polka_ls -thold true
# Drift on 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 false -io-effects false -out 2 -domain PolkaGrid -thold false
# evDrift on 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 -io-effects false -out 2 -domain Polka_ls -thold true
# Drift on 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 false -io-effects false -out 2 -domain Polka_ls -thold true
# evDrift on lics18-web:
./drift.exe -file tests/effects/lics18-web.ml -prop tests/effects/lics18-web.yml.prp -ev-trans direct -trace-len 0 -if-part false -io-effects true -out 2 -domain Polka_ls -thold true
# Drift on market:
./drift.exe -file tests/effects/market.ml -prop tests/effects/market.yml.prp -ev-trans trans -trace-len 1 -if-part false -io-effects false -out 2 -domain PolkaGrid -thold false
# evDrift on market:
./drift.exe -file tests/effects/market.ml -prop tests/effects/market.yml.prp -ev-trans direct -trace-len 1 -if-part true -io-effects true -out 2 -domain Polka_ls -thold true
# Drift on max-min:
./drift.exe -file tests/effects/max-min.ml -prop tests/effects/max-min.yml.prp -ev-trans trans -trace-len 0 -if-part false -io-effects false -out 2 -domain PolkaGrid -thold false
# evDrift on 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 true -io-effects true -out 2 -domain Polka_ls -thold true
# Drift on monotonic:
./drift.exe -file tests/effects/monotonic.ml -prop tests/effects/monotonic.yml.prp -ev-trans trans -trace-len 0 -if-part false -io-effects false -out 2 -domain Polka_ls -thold true
# evDrift on monotonic:
./drift.exe -file tests/effects/monotonic.ml -prop tests/effects/monotonic.yml.prp -ev-trans direct -trace-len 1 -if-part false -io-effects false -out 2 -domain Polka_ls -thold true
# Drift on nondet_max:
./drift.exe -file tests/effects/nondet_max.ml -prop tests/effects/nondet_max.yml.prp -ev-trans trans -trace-len 0 -if-part false -io-effects false -out 2 -domain Polka_ls -thold true
# evDrift on nondet_max:
./drift.exe -file tests/effects/nondet_max.ml -prop tests/effects/nondet_max.yml.prp -ev-trans direct -trace-len 0 -if-part false -io-effects false -out 2 -domain Polka_ls -thold true
# Drift on order-irrel:
./drift.exe -file tests/effects/order-irrel.ml -prop tests/effects/order-irrel.yml.prp -ev-trans trans -trace-len 0 -if-part false -io-effects false -out 2 -domain PolkaGrid -thold false
# evDrift on 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 true -io-effects false -out 2 -domain PolkaGrid -thold false
# Drift on 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 0 -if-part false -io-effects false -out 2 -domain Polka_ls -thold true
# evDrift on 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 true -io-effects false -out 2 -domain Polka_ls -thold true
# Drift on overview1:
./drift.exe -file tests/effects/overview1.ml -prop tests/effects/overview1.yml.prp -ev-trans trans -trace-len 1 -if-part false -io-effects false -out 2 -domain Polka_ls -thold true
# evDrift on overview1:
./drift.exe -file tests/effects/overview1.ml -prop tests/effects/overview1.yml.prp -ev-trans direct -trace-len 0 -if-part false -io-effects false -out 2 -domain Polka_ls -thold true
# Drift on reentr:
./drift.exe -file tests/effects/reentr.ml -prop tests/effects/reentr.yml.prp -ev-trans trans -trace-len 0 -if-part false -io-effects false -out 2 -domain Polka_ls -thold true
# evDrift on reentr:
./drift.exe -file tests/effects/reentr.ml -prop tests/effects/reentr.yml.prp -ev-trans direct -trace-len 0 -if-part false -io-effects false -out 2 -domain Polka_ls -thold true
# Drift on resource-analysis:
./drift.exe -file tests/effects/resource-analysis.ml -prop tests/effects/resource-analysis.yml.prp -ev-trans trans -trace-len 0 -if-part false -io-effects false -out 2 -domain Polka_ls -thold true
# evDrift on resource-analysis:
./drift.exe -file tests/effects/resource-analysis.ml -prop tests/effects/resource-analysis.yml.prp -ev-trans direct -trace-len 0 -if-part false -io-effects false -out 2 -domain Polka_ls -thold true
# Drift on sum-appendix:
./drift.exe -file tests/effects/sum-appendix.ml -prop tests/effects/sum-appendix.yml.prp -ev-trans trans -trace-len 0 -if-part false -io-effects false -out 2 -domain Polka_ls -thold true
# evDrift on 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 true -io-effects true -out 2 -domain Polka_ls -thold true
# Drift on 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 0 -if-part false -io-effects false -out 2 -domain PolkaGrid -thold false
# evDrift on 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 0 -if-part false -io-effects false -out 2 -domain PolkaGrid -thold false
# Drift on temperature:
./drift.exe -file tests/effects/temperature.ml -prop tests/effects/temperature.yml.prp -ev-trans trans -trace-len 0 -if-part false -io-effects false -out 2 -domain Polka_ls -thold true
# evDrift on temperature:
./drift.exe -file tests/effects/temperature.ml -prop tests/effects/temperature.yml.prp -ev-trans direct -trace-len 0 -if-part false -io-effects false -out 2 -domain PolkaGrid -thold false