在昨天日志的2、3、5条的指导下，将A、B、C三类机制都编写为阻塞单消息的版本，经过一些细微的改动，三个程序都能跑起来了，并且都有比较好的结果。这些结果个人认为足够说明协议的正确性。

比较令人振奋的是，今天在调试B类程序的时候发现，总有一段代码不可达(unreachable code)，首先我以为是我编写的程序的问题，后来仔细分析协议发现，是协议说明书错误！这是一个比较大的协议BUG，竟然被Spin找出来了！这让我对Spin信心大增！

发现错误后，马上跟师兄沟通，他告诉我，那的确是一个错误…… ORZ，原来已经被发现了，但是文档没有被更新。嘿嘿，他是人力看出来的，我这是机器跑出来的，不错不错~~

我选择了明天10:00~11:00给大家（也许就是老师一个人，也许还有两外两个师兄）讲解，需要把他们当作什么也不懂的对象，小心仔细地“忽悠”~

到现在为止，做了7-8个小时的调试和幻灯片制作，终于好了！

现在回顾下前面十几天干些啥：上上周基本明白了Promela，用大约5-7天的时间完成了所有代码。上周，写技术文档，用了4天。写文档过程中发现，所做的验证完全不达标，重新审视Spin和代码，到现在为止，调试、思考、写出基本符合要求的版本，用了4-5天。时间竟然是这样被打发的！

—————————-

Lonely Planet, Lonely City. Where am I?