From a22dffe38832582769714bd684dc8785f28c681c Mon Sep 17 00:00:00 2001 From: Guo Hua Date: Wed, 10 Jul 2024 15:12:24 +0800 Subject: [PATCH] sedeve-kit, README.md --- README.md | 6 +- doc/figure/architecture.svg | 3503 ++++++ doc/figure/design_to_impl.svg | 18202 ++++++++++++++++++++++++++++++++ doc/figure/verifying.svg | 1639 +++ 4 files changed, 23347 insertions(+), 3 deletions(-) create mode 100644 doc/figure/architecture.svg create mode 100644 doc/figure/design_to_impl.svg create mode 100644 doc/figure/verifying.svg diff --git a/README.md b/README.md index 95315bf..59290b1 100644 --- a/README.md +++ b/README.md @@ -13,7 +13,7 @@ Code development: We write the code according to the established specifications, System testing: Upon completing the coding process, we rigorously test the system using the test cases generated in the initial stage. By maintaining a connection between abstract design and concrete implementation, we can confidently guarantee the quality of our system. This approach ensures our design's accuracy and fosters consistency throughout the development process, ultimately resulting in a reliable and high-quality distributed system. -[](https://youtu.be/IKqJ6UX1q2o "Click to view the demo video") +[](https://youtu.be/IKqJ6UX1q2o "Click to view the demo video") ## Bridge the gap between design and implementation @@ -22,7 +22,7 @@ To bridge the gap between design and implementation, the tool makes the implementation a precise refinement of the design. Think of the design as a low-resolution animation, containing only the keyframes. The implementation, on the other hand, is a high-definition animation that not only preserves the keyframes but also adds more details. This ensures a seamless transition from concept to reality and aligns the original design while adding the necessary details for the implementation. -![architecture](doc/figure/design_to_impl.png) +![architecture](doc/figure/design_to_impl.svg) ## Architecture @@ -38,7 +38,7 @@ The architecture of **sedeve-kit** is as the following figure, which includes th **S-Net**: Library to build network channel -![architecture](doc/figure/architecture.png) +![architecture](doc/figure/architecture.svg) ## Workflow diff --git a/doc/figure/architecture.svg b/doc/figure/architecture.svg new file mode 100644 index 0000000..0bbdf48 --- /dev/null +++ b/doc/figure/architecture.svg @@ -0,0 +1,3503 @@ + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + 页-1 + + + + 工作表.1 + + + + + + 动态连接线 + + + + 动态连接线.114 + + + + 工作表.1116 + + 工作表.1117 + …… + + + + …… + + 圆形.3 + + + + + + + 圆形.4 + + + + + + + 圆形.5 + + + + + + + 动态连接线.13 + + + + 圆形.14 + + + + + + + 圆形.15 + + + + + + + 圆形.16 + + + + + + + 动态连接线.20 + + + + 动态连接线.21 + + + + 动态连接线.22 + + + + 动态连接线.23 + + + + 动态连接线.45 + + + + 同心圆中心层 + + + + + + + 同心圆中心层.8 + + + + + + + 圆形.49 + + + + + + + 圆形.50 + + + + + + + 动态连接线.53 + + + + 动态连接线.54 + + + + 圆形.1000 + + + + + + + 动态连接线.1001 + + + + 动态连接线.1002 + + + + 圆形.1003 + + + + + + + 动态连接线.1004 + + + + 圆形.1005 + + + + + + + 圆形.1006 + + + + + + + 动态连接线.1007 + + + + + 工作表.3 + + + + + + 工作表.1145 + Trace + + + + Trace + + 传统服务器.1067 + Deterministic Player + + + + Deterministic Player + + 工作表.1149 + Coding + + + + Coding + + 工作表.1151 + TLA+ Toolbox + + + + TLA+ Toolbox + + 工作表.1153 + .sqlite + + + + .sqlite + + 动态连接线.1077 + Input + + + + + Input + + 动态连接线.1089 + Build + + + + + Build + + 工作表.5 + + + + + + 动态连接线.1094 + Output + + + + + Output + + 动态连接线.1095 + Input + + + + + Input + + 工作表.1190 + + + 动态连接线.1097 + Output + + + + + Output + + 动态连接线.1100 + Control message + + + + + Control message + + 工作表.1217 + + 工作表.1208 + + + + + + + 矩形.54 + SERVER + + + + + + + + SERVER + + 工作表.1216 + + 工作表.1209 + + + + + + + 工作表.1210 + + + + + + + 工作表.1211 + + + + + + + 工作表.1212 + + + + + + + + + 工作表.1279 + TraceGen + + + + TraceGen + + 工作表.1292 + (1) + + + + (1) + + 工作表.1293 + (2) + + + + (2) + + 工作表.1294 + (3) + + + + (3) + + 工作表.1295 + (4) + + + + (4) + + 工作表.1296 + (5) + + + + (5) + + 工作表.1300 + + 文件 + + 工作表.1192 + + + + + + + 工作表.1193 + + + + + + + 工作表.1194 + + + + + + + 工作表.1195 + + + + + + + 工作表.1196 + + + + + + + 工作表.1197 + + + + + + + + 矩形.54 + CMD + + + + + + + + CMD + + + 工作表.1301 + + 工作表.7 + + + + + + 工作表.8 + + + + + + 工作表.9 + + + + + + + 工作表.4017 + Validating + + + + Validating + + 工作表.4018 + Generating Trace + + + + Generating Trace + + 工作表.4019 + Specifying + + + + Specifying + + 工作表.4020 + Dumping + + + + Dumping + + 工作表.4021 + + 工作表.1187 + Tested System + + + + Tested System + + 框 + + + + + + + 工作表.1241 + + 工作表.1242 + + + + + + + 工作表.1243 + + + + + + + 工作表.1244 + + + + + + + 工作表.1245 + + + + + + + 工作表.1246 + + + + + + + 工作表.1247 + + + + + + + 矩形.54 + + + + + + + + + 工作表.1249 + + 工作表.1250 + + + + + + + 工作表.1251 + + + + + + + 工作表.1252 + + + + + + + 工作表.1253 + + + + + + + 工作表.1254 + + + + + + + 工作表.1255 + + + + + + + 矩形.54 + + + + + + + + + 动态连接线.1257 + Messages from/to other tested node + + + + + Messages from/to other tested node + + 传统服务器.1258 + …… + + + + …… + + 工作表.1259 + + 工作表.1260 + + + + + + + 工作表.1261 + + + + + + + 工作表.1262 + + + + + + + 工作表.1263 + + + + + + + 工作表.1264 + + + + + + + 工作表.1265 + + + + + + + 矩形.54 + + + + + + + + + 工作表.1267 + + 工作表.1268 + + + + + + + 工作表.1269 + + + + + + + 工作表.1270 + + + + + + + 工作表.1271 + + + + + + + 工作表.1272 + + + + + + + 工作表.1273 + + + + + + + 矩形.54 + + + + + + + + + 工作表.1278 + Tested Node + + + + Tested Node + + + 工作表.4023 + + 文件 + + 工作表.1166 + + + + + + + 工作表.1167 + + + + + + + 工作表.1168 + + + + + + + 工作表.1169 + + + + + + + 工作表.1170 + + + + + + + 工作表.1171 + + + + + + + + 矩形.54 + LIB + + + + + + + + LIB + + 工作表.1173 + S-Serde + + + + S-Serde + + + 工作表.4025 + + 工作表.4016 + + 工作表.4013 + + 工作表.1176 + + + + + + + 工作表.1181 + + + + + + + 工作表.1178 + + + + + + + 工作表.1179 + + + + + + + 工作表.1180 + + + + + + + 矩形.54 + LIB + + + + + + + + LIB + + 工作表.4012 + + 工作表.1177 + + + + + + + + + + 工作表.4024 + + 工作表.1183 + S-Net + + + + S-Net + + + + 工作表.4036 + + 工作表.4010 + A-Sender + + + + A-Sender + + 工作表.4035 + + 文件 + + 工作表.4028 + + + + + + + 工作表.4029 + + + + + + + 工作表.4030 + + + + + + + 工作表.4031 + + + + + + + 工作表.4032 + + + + + + + 工作表.4033 + + + + + + + + 矩形.54 + LIB + + + + + + + + LIB + + + + diff --git a/doc/figure/design_to_impl.svg b/doc/figure/design_to_impl.svg new file mode 100644 index 0000000..43dcac0 --- /dev/null +++ b/doc/figure/design_to_impl.svg @@ -0,0 +1,18202 @@ + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + 页-1 + + + + + 现代箭头.1002 + + + + + + + + + 工作表.4001 + System Implementation + + + + System Implementation + + 工作表.4002 + Verifying the “Keyframes” + + + + Verifying the “Keyframes” + + 工作表.4003 + + + 工作表.4004 + Specification Of Design + + + + Specification Of Design + + 现代箭头.1042 + + + + + + + + + 现代箭头.1043 + + + + + + + + + 工作表.4013 + + + + + + + + + + + + + + + + + + + + + 程序.1026 + + + + + 工作表.1 + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + 工作表.4015 + + + + 工作表.4016 + + 工作表.4017 + + + + 工作表.4018 + + + + 工作表.4019 + + + + + 工作表.4020 + + 工作表.4021 + + + + 工作表.4022 + + + + 工作表.4023 + + + + 工作表.4024 + + + + + 工作表.4025 + + + + 配置.1025 + + + + + + + + 工作表.4027 + + 工作表.4028 + + + + 工作表.4029 + + + + 工作表.4030 + + + + + + 工作表.4044 + + 工作表.4045 + + 工作表.4046 + + + + 工作表.4047 + + + + 工作表.4048 + + + + 工作表.4049 + + + + 工作表.4050 + + + + 工作表.4051 + + + + 工作表.4052 + + + + 工作表.4053 + + + + 工作表.4054 + + + + 工作表.4055 + + + + 工作表.4056 + + + + 工作表.4057 + + + + 工作表.4058 + + + + 工作表.4059 + + + + + 工作表.4060 + + + + + 工作表.4061 + + + + + 工作表.4062 + + + + 工作表.4063 + + + + 工作表.4064 + + + + 工作表.4065 + + + + 工作表.4066 + + + + 工作表.4067 + + + + 工作表.4068 + + + + 工作表.4069 + + + + 工作表.4070 + + + + 工作表.4071 + + + + 工作表.4072 + + + + 工作表.4073 + + + + 工作表.4074 + + + + 工作表.4075 + + + + 工作表.4076 + + + + 工作表.4077 + + + + 工作表.4078 + + + + 工作表.4079 + + + + 工作表.4080 + + + + 工作表.4081 + + + + 工作表.4082 + + + + + 工作表.4083 + + + + + 工作表.4084 + + + + + 工作表.4085 + + + + 工作表.4086 + + + + 工作表.4087 + + + + + 工作表.4088 + + + + 工作表.4089 + + + + 工作表.4090 + + + + 工作表.4091 + + + + 工作表.4092 + + + + 工作表.4093 + + + + 工作表.4094 + + + + 工作表.4095 + + + + 工作表.4096 + + + + 工作表.4097 + + + + 工作表.4098 + + + + 工作表.4099 + + + + 工作表.4100 + + + + 工作表.4101 + + + + 工作表.4102 + + + + 工作表.4103 + + + + 工作表.4104 + + + + 工作表.4105 + + + + 工作表.4106 + + + + 工作表.4107 + + + + 工作表.4108 + + + + 工作表.4109 + + + + 工作表.4110 + + + + 工作表.4111 + + + + 工作表.4112 + + + + 工作表.4113 + + + + 工作表.4114 + + + + 工作表.4115 + + + + 工作表.4116 + + + + 工作表.4117 + + + + 工作表.4118 + + + + 工作表.4119 + + + + 工作表.4120 + + + + 工作表.4121 + + + + 工作表.4122 + + + + 工作表.4123 + + + + 工作表.4124 + + + + 工作表.4125 + + + + 工作表.4126 + + + + 工作表.4127 + + + + 工作表.4128 + + + + + 框.1220 + + + + + + + 框.1221 + + + + + + + 工作表.4131 + + 动态连接线.1000 + + + + 工作表.2 + + + + + + 工作表.3 + + + + + + 工作表.4 + + + + + + 工作表.5 + + + + + + 工作表.6 + + + + + + 工作表.7 + + + + + + 工作表.8 + + + + + + 工作表.9 + + + + + + 工作表.10 + + + + + + 工作表.4133 + + + + 工作表.4134 + + + + 工作表.4135 + + + + 工作表.4136 + + + + 工作表.4137 + + + + 工作表.4138 + high-definition animation + + + + high-definition animation + + + 工作表.4139 + + 动态连接线.1004 + + + + 工作表.11 + + + + + + 工作表.12 + + + + + + 工作表.13 + + + + + + 工作表.14 + + + + + + 工作表.15 + + + + + + 工作表.4141 + animation with only the keyframes + + + + animation with only the keyframes + + + 工作表.4142 + sedeve-kit + + + + sedeve-kit + + 工作表.4143 + + + 工作表.4144 + + 工作表.16 + + + + + + 工作表.4145 + + 工作表.4146 + + 工作表.4147 + + + + 工作表.4148 + + + + 工作表.4149 + + + + 工作表.4150 + + + + 工作表.4151 + + + + 工作表.4152 + + + + + + + 工作表.17 + + + + + + 工作表.18 + + + + + + 工作表.19 + + + + + + + + + HDFS 群集.1044 + + + + + 工作表.4163 + + 工作表.4164 + + + + + + + 工作表.4165 + + + + + + + 工作表.4166 + + + + + + + 工作表.4167 + + + + + + + 工作表.4168 + + + + + + + 工作表.4169 + + + + + + + 工作表.4170 + + + + + + + 工作表.4171 + + + + + + + 工作表.4172 + + + + + + + 工作表.4173 + + + + + + + 工作表.4174 + + + + + + + 工作表.4175 + + + + + + + 工作表.4176 + + + + + + + + + diff --git a/doc/figure/verifying.svg b/doc/figure/verifying.svg new file mode 100644 index 0000000..cad1c22 --- /dev/null +++ b/doc/figure/verifying.svg @@ -0,0 +1,1639 @@ + + + + + + + + + + 页-1 + + + + 工作表.4049 + + 工作表.4050 + + + + 工作表.4051 + + + + 工作表.4052 + + + + 工作表.4053 + + + + 工作表.4054 + + + + + outline.1099 + + 工作表.4056 + + + + 工作表.4057 + + + + 工作表.4058 + + + + 工作表.4059 + + + + 工作表.4060 + + + + 工作表.4061 + + + + + + 工作表.4153 + + + + + + + + + 工作表.4154 + + 工作表.4063 + + 工作表.4064 + + + + 工作表.4065 + + + + 工作表.4066 + + + + 工作表.4067 + + + + 工作表.4068 + + + + 工作表.4069 + + + + 工作表.4070 + + + + 工作表.4071 + + + + 工作表.4072 + + + + 工作表.4073 + + + + 工作表.4074 + + + + 工作表.4075 + + + + 工作表.4076 + + + + 工作表.4077 + + + + + 工作表.4078 + + + + + 工作表.4079 + + + + + 工作表.4080 + + + + 工作表.4081 + + + + 工作表.4082 + + + + 工作表.4083 + + + + 工作表.4084 + + + + 工作表.4085 + + + + 工作表.4086 + + + + 工作表.4087 + + + + 工作表.4088 + + + + 工作表.4089 + + + + 工作表.4090 + + + + 工作表.4091 + + + + 工作表.4092 + + + + 工作表.4093 + + + + 工作表.4094 + + + + 工作表.4095 + + + + 工作表.4096 + + + + 工作表.4097 + + + + 工作表.4098 + + + + 工作表.4099 + + + + 工作表.4100 + + + + + 工作表.4101 + + + + + 工作表.4102 + + + + + 工作表.4103 + + + + 工作表.4104 + + + + 工作表.4105 + + + + + 工作表.4106 + + + + 工作表.4107 + + + + 工作表.4108 + + + + 工作表.4109 + + + + 工作表.4110 + + + + 工作表.4111 + + + + 工作表.4112 + + + + 工作表.4113 + + + + 工作表.4114 + + + + 工作表.4115 + + + + 工作表.4116 + + + + 工作表.4117 + + + + 工作表.4118 + + + + 工作表.4119 + + + + 工作表.4120 + + + + 工作表.4121 + + + + 工作表.4122 + + + + 工作表.4123 + + + + 工作表.4124 + + + + 工作表.4125 + + + + 工作表.4126 + + + + 工作表.4127 + + + + 工作表.4128 + + + + 工作表.4129 + + + + 工作表.4130 + + + + 工作表.4131 + + + + 工作表.4132 + + + + 工作表.4133 + + + + 工作表.4134 + + + + 工作表.4135 + + + + 工作表.4136 + + + + 工作表.4137 + + + + 工作表.4138 + + + + 工作表.4139 + + + + 工作表.4140 + + + + 工作表.4141 + + + + 工作表.4142 + + + + 工作表.4143 + + + + 工作表.4144 + + + + 工作表.4145 + + + + 工作表.4146 + + + + + 工作表.1 + + + + + + 思想气泡.1098 + Cannot reproduce the bug. Multiple nodes are executing concur... + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + Cannot reproduce the bug. Multiple nodes are executing concurrently. What exactly is happening inside the system? + + + + + + + + + + + + + + + + 缩放.1112 + Testing is an attempt to exhaustively cover all possible comb... + + 工作表.4149 + + + + + + + + + + + + + + + + + 工作表.4150 + + + + + + + + + + + + + + + + + Testing is an attempt to exhaustively cover all possible combinations of program states. The combinatorial explosion of program states in a distributed system is daunting, and it is nearly impossible for the human mind to envision all possibilities and test them perfectly. + + + 工作表.4152 + + + + + + + + + + + + + 工作表.4155 + + 缩放.1130 + Instead of 'testing' the system, 'validate' the system by lev... + + + + + + + + + + + + + + + + + Instead of 'testing' the system, 'validate' the system by leveraging tools and computers. Use computational power to conquer the combinatorial explosion." + + +