forked from reactive-systems/bosy
-
Notifications
You must be signed in to change notification settings - Fork 0
/
run_hyper.sh
executable file
·173 lines (113 loc) · 6.49 KB
/
run_hyper.sh
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
151
152
153
154
155
156
157
158
159
160
161
162
163
164
165
166
167
168
169
170
171
172
173
#!/usr/bin/env bash
slow=$1
if [ -z "$1" ]; then
printf "Note: Only run fast experiments, start script with --slow to run all\n\n"
fi
swift build -c release
# define colors for better readability
RED='\033[0;31m'
BLUE='\033[0;34m'
NC='\033[0m' # No Color
printf "\n${RED}Symmetric Mutex${NC}\n"
# Symmetric arbiter (moore)
printf "\n* ${BLUE}Symmetric Mutex (moore,non-sym)${NC}\n"
time swift run -c release BoSy --player system Samples/HyperLTL/bakery_sym_unrealizable_moore.bosy
printf "\n* ${BLUE}Symmetric Mutex (moore,sym)${NC}\n"
time swift run -c release BoSyHyper --environment Samples/HyperLTL/bakery_sym_unrealizable_moore.bosy
printf "\n* ${BLUE}Symmetric Mutex (moore,tie)${NC}\n"
time swift run -c release BoSyHyper Samples/HyperLTL/bakery_tie_realizable_moore.bosy
# Symmetric arbiter (mealy)
printf "\n* ${BLUE}Symmetric Mutex (mealy,non-sym)${NC}\n"
time swift run -c release BoSy --player system Samples/HyperLTL/bakery_sym_unrealizable.bosy
printf "\n* ${BLUE}Symmetric Mutex (mealy,sym)${NC}\n"
time swift run -c release BoSyHyper --environment Samples/HyperLTL/bakery_sym_unrealizable.bosy
printf "\n* ${BLUE}Symmetric Mutex (mealy,tie)${NC}\n"
time swift run -c release BoSyHyper Samples/HyperLTL/bakery_tie_realizable.bosy
# Full arbiter (moore)
printf "\n* ${BLUE}Symmetric Mutex (moore,full-non-sym)${NC}\n"
time swift run -c release BoSy --player system Samples/HyperLTL/bakery_full_sym_unrealizable_moore.bosy
printf "\n* ${BLUE}Symmetric Mutex (moore,full-sym)${NC}\n"
time swift run -c release BoSyHyper --environment Samples/HyperLTL/bakery_full_sym_unrealizable_moore.bosy
printf "\n* ${BLUE}Symmetric Mutex (moore,tie)${NC}\n"
if [[ -n "$slow" ]]; then
time swift run -c release BoSyHyper Samples/HyperLTL/bakery_full_tie_realizable_moore.bosy # slow ~1h
else
echo "omitted, re-run with --slow"
fi
# Full arbiter (mealy)
printf "\n* ${BLUE}Symmetric Mutex (mealy,full-non-sym)${NC}\n"
time swift run -c release BoSy --player system Samples/HyperLTL/bakery_full_sym_unrealizable.bosy
printf "\n* ${BLUE}Symmetric Mutex (mealy,full-sym)${NC}\n"
time swift run -c release BoSyHyper --environment Samples/HyperLTL/bakery_full_sym_unrealizable.bosy
printf "\n* ${BLUE}Symmetric Mutex (mealy,tie)${NC}\n"
time swift run -c release BoSyHyper Samples/HyperLTL/bakery_full_tie_realizable.bosy
printf "\n\n${RED}Encoder/Decoder${NC}\n"
# Encoder/Decoder (moore)
printf "\n* ${BLUE}Encoder/Decoder (moore,1-2-hamming-2)${NC}\n"
time swift run -c release BoSyHyper Samples/HyperLTL/encoder_1_2_hamming_2_moore.bosy
printf "\n* ${BLUE}Encoder/Decoder (moore,1-2-fault-tolerant)${NC}\n"
time swift run -c release BoSyHyper --environment Samples/HyperLTL/encoder_1_2_unrealizable_moore.bosy
printf "\n* ${BLUE}Encoder/Decoder (moore,1-3-fault-tolerant)${NC}\n"
time swift run -c release BoSyHyper Samples/HyperLTL/encoder_1_3_realizable_moore.bosy
#time swift run -c release BoSyHyper --environment Samples/HyperLTL/encoder_2_2_hamming_2_moore.bosy
printf "\n* ${BLUE}Encoder/Decoder (moore,2-3-hamming-2)${NC}\n"
if [[ -n "$slow" ]]; then
time swift run -c release BoSyHyper Samples/HyperLTL/encoder_2_3_hamming_2_moore.bosy --min-bound 16 # slow ~4h
else
echo "omitted, re-run with --slow"
fi
# Encoder/Decoder (mealy)
printf "\n* ${BLUE}Encoder/Decoder (mealy,1-2-hamming-2)${NC}\n"
time swift run -c release BoSy --player system Samples/HyperLTL/encoder_1_2_hamming_2.bosy
#time swift run -c release BoSyHyper --environment --paths 3 Samples/HyperLTL/encoder_1_2_unrealizable.bosy # does not work due to encoding
printf "\n* ${BLUE}Encoder/Decoder (mealy,1-3-fault-tolerant)${NC}\n"
time swift run -c release BoSyHyper Samples/HyperLTL/encoder_1_3_realizable.bosy
printf "\n* ${BLUE}Encoder/Decoder (mealy,2-2-hamming-2)${NC}\n"
time swift run -c release BoSyHyper --environment --paths 3 Samples/HyperLTL/encoder_2_2_hamming_2.bosy
printf "\n* ${BLUE}Encoder/Decoder (mealy,2-3-hamming-2)${NC}\n"
time swift run -c release BoSyHyper Samples/HyperLTL/encoder_2_3_hamming_2.bosy
printf "\n* ${BLUE}Encoder/Decoder (mealy,2-3-hamming-3)${NC}\n"
time swift run -c release BoSyHyper --environment --paths 3 Samples/HyperLTL/encoder_2_3_hamming_3.bosy
# CAP Theorem
printf "\n\n${RED}CAP Theorem${NC}\n"
printf "\n* ${BLUE}CAP Theorem (moore,cap-2-linear)${NC}\n"
time swift run -c release BoSy --player system Samples/HyperLTL/cap_2_moore.bosy
printf "\n* ${BLUE}CAP Theorem (mealy,cap-2-linear)${NC}\n"
time swift run -c release BoSy --player system Samples/HyperLTL/cap_2.bosy
printf "\n* ${BLUE}CAP Theorem (moore,cap-2)${NC}\n"
if [[ -n "$slow" ]]; then
time swift run -c release BoSyHyper --environment Samples/HyperLTL/cap_2_moore.bosy # slow ~30min
else
echo "omitted, re-run with --slow"
fi
#time swift run -c release BoSyHyper --environment Samples/HyperLTL/cap_2.bosy # does not work due to encoding
printf "\n* ${BLUE}CAP Theorem (mealy,ca-2)${NC}\n"
time swift run -c release BoSyHyper Samples/HyperLTL/ca_2.bosy
printf "\n* ${BLUE}CAP Theorem (mealy,ca-3)${NC}\n"
time swift run -c release BoSyHyper Samples/HyperLTL/ca_3.bosy
printf "\n* ${BLUE}CAP Theorem (mealy,cp-2)${NC}\n"
time swift run -c release BoSyHyper Samples/HyperLTL/cp_2.bosy
printf "\n* ${BLUE}CAP Theorem (moore,cp-2)${NC}\n"
time swift run -c release BoSyHyper Samples/HyperLTL/cp_2_moore.bosy
printf "\n* ${BLUE}CAP Theorem (mealy,cp-3)${NC}\n"
time swift run -c release BoSyHyper Samples/HyperLTL/cp_3.bosy
printf "\n* ${BLUE}CAP Theorem (moore,cp-3)${NC}\n"
time swift run -c release BoSyHyper Samples/HyperLTL/cp_3_moore.bosy
printf "\n* ${BLUE}CAP Theorem (mealy,ap-2)${NC}\n"
time swift run -c release BoSyHyper Samples/HyperLTL/ap_2.bosy
printf "\n* ${BLUE}CAP Theorem (mealy,ap-3)${NC}\n"
time swift run -c release BoSyHyper Samples/HyperLTL/ap_3.bosy
printf "\n\n${RED}Bus protocol${NC}\n"
# bus protocol (moore)
printf "\n* ${BLUE}Bus protocol (moore,ni1)${NC}\n"
time swift run -c release BoSyHyper --environment Samples/HyperLTL/bus_master_unrealizable.bosy
printf "\n* ${BLUE}Bus protocol (moore,ni2)${NC}\n"
time swift run -c release BoSyHyper Samples/HyperLTL/bus_master_forget.bosy
# bus protocol (mealy)
printf "\n* ${BLUE}Bus protocol (mealy,ni1)${NC}\n"
time swift run -c release BoSyHyper --environment Samples/HyperLTL/bus_master_unrealizable_mealy.bosy
printf "\n* ${BLUE}Bus protocol (mealy,ni2)${NC}\n"
time swift run -c release BoSyHyper Samples/HyperLTL/bus_master_forget_mealy.bosy
printf "\n\n${RED}Dining Cryptographers${NC}\n"
# dining cryptographers
time swift run -c release BoSyHyper Samples/HyperLTL/dining-cryptographers.bosy