昨天，今天，我确认我处在一个灰色地带。
QQ签名修改为：Milestone: Mechanism A Verified.Proofed Correct!
现在看来，简直就是扯淡！Milestone实为Scratch.
昨天的工作仅仅是叫开个头，表示：现在开始着手做验证了。
现在发现，用Spin建模并没有想象中简单，看过的一些例子那都是很简单的模型，所以感觉不难。用Spin表达一个实用的模型，还是特别耗脑子的。
心中存了几个疑问，等了一上午也没看到研究生gg来，只能靠自己猜想，这是很难受的！天知道我那些所谓猜想错成了什么样子。
下午午睡醒来，发现马老师又来了，于是直接请教他算啦~这个协议是他一手拍脑袋设计的，第一作者，对问题的理解自然是最到位的了。
在他的讲解下，对协议中的流水线发送方式有了比较清晰的理解，可是，理解过后带来的是莫大的痛苦--建模难度大多了！！！
下午在纸上拍脑袋拍了好几个方案，但都过于复杂（或曰杂乱），一一否决。还有一些方案，Spin直接报错：解空间过大，内存溢出，无法完成搜索……
心中很乱，以致晚上和TaoTeng吃饭的时候心里还是十分不舒服，总感觉有什么堵着在，尽管TT那么有意思的表演 =.= 这个东西怎么就那么烦人呢？中邪了……
明天继续，现在脑袋中装这一个似乎可行的方案，回来的路上冒出来的。但愿可行！
周五前如果不能把这个搞定，这个周末我就哪里也不去了，不信你个邪！
喝了点点啤酒，晕了*&#$￥*%￥@#@*&*
---------------------------------------------
Just one glance, that's everything I could wish for.