Update SPIN-Promela-Concurrent-Queue-1.md

content/Blog/SPIN-Promela-Concurrent-Queue-1.md

@@ -23,10 +23,11 @@ Slug: SPIN-Promela-Concurrent-Queue-1
 在使用 SPIN/Promela 建模时，我们面临了几个挑战：
 
 * 静态内存管理：SPIN/Promela 缺乏动态内存操作，因此我们实现了一个极简的手动管理的静态内存堆栈。
+* 减少状态空间：队列的长度可以是无限的，这也就意味着无限的状态空间。因此，我们将队列的最大长度设为3，以减少状态的穷举空间。
 * 模拟CAS操作：由于缺少CAS指令，我们使用 do 循环和 atomic 块来模拟，同时开启 weak fairness 避免无限循环。（见[《在SPIN/Promela中模拟CAS》][2]一文）
 * LTL表达式的使用：使用 LTL 表达式来穷举检查所有可能的程序状态，包括边缘情况。
 	* LTL表达式偶尔会有一些”反直觉“的情况出现
-	* 例如在程序验证路径中，队列大小可以在2和3之间反复变化，如果我们声明“**永远** **最终** 一定存在 queue size==1” 的表达式会失败，因为队列大小在这种“人造场景”下永远不会为1
+	* 例如在程序验证路径中，虽然理论上队列大小可以为0~3当中的任意数。但是也存在一种可能，即队列大小可以在2和3之间反复变化。如果我们声明“**永远** **最终** 一定存在 queue size==1” 的表达式会失败，因为队列大小在这种“人造场景”下永远不会为1。
 	* 这种情况要求我们非常精确地设计 LTL 表达式
 * 代码与断言的结合：因为 LTL 表达式的表达能力有限，需要结合代码中的 assert 语句来进行更全面的验证