在昨天日志的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?

14:36 2007-8-5 Sunday.

Delete the code on "out-of-order" simulation.

Then the hash factor increased from 2.34 to 221.245, which is a greate improvement!
221.245 indicates an average coverage of all the possible paths above 99.9%.

This experiment show a way to improve the hash factor. Out-Of-Order(OOO）simulation takes so many states that we must think up an idea to simplify the simulation. However, we also should try to keep the functions provided by the current simulation code.

The next step’s target in brief is to reduce states, keep functions.

报告写完了，却发现，验证工作并没有做好。B，C类虽然写对了，但是其状态空间无比硕大，Spin无法完全覆盖之。

上午没去，睡觉。下午一直在工作，晚上做到9：35才下楼，匆忙找了点吃的，赶上了末班车。

我必须重头再来了。

明天，没安排，我还是去实验室罢。

继续写文档。

明天，我买点零食带去~

今天很感动~竟然有个女生说要给我送伞，不怎么认识，还素未谋面。Orz的世界~回武汉前见见人家小mm去  

却有了伞，那么大雨，还是不能麻烦人家了。哈哈。

今天晚上加了会儿班，随意跟老师交代了下进度，老师指导了下。点点指导就可以让我明确很多了。Nice~

这两天没有仔细写日志，因为一直在写总结性文档，写的腰酸背痛手抽筋，光画板画图就画了十几张。

这个文档得好好写，有可能会作为给大家的参考资料—也就是说，我现在做的工作是对人类有贡献滴~当然咯，得做好，这是前提。

睡了，这两天看电影看的厉害了，睡的晚，早上就起不来了。这不，今天早上我一咬牙睡到了8:40，那是一个后悔啊，公交那叫一个堵啊~7点多虽然人挤，车却不堵，到了9点不仅人多，车还半天走不了几个路口。唉，武汉的车怎么不堵呢  

P.S: 关于最近的天气，实在变态。白天看上去很正常，一到下午六点就有些下雨的苗头，到了七八点，那个雨啊~~~简直吓死人。前天直接淋回去的，昨天提前步行回学校，不小心躲过一劫，今天没长记性，虽然有伞，却还是湿的差不多了……现在，外面电闪雷鸣，有感觉！

08:30 – 08:50 看博客，校内，白云
08:50 – 09:00 Tea Time
09:00 – 10:00 通过Sequence Chart跟踪分析模拟程序中的错误，反复修改测试，修正了大约6个BUG
10:00 – 10:30 开着机器让他进行局部行为测试，慢！经历大约5次序号回转。俺一边喝着茶，一边实时Trace&Observe。观察结果：模拟行为和预期完全一致。Nice！
10:30 – 10:40 生产全局测试程序，用gcc编译，执行。0错误报告！！

C1.0 OK！

2007-07-28 | ICT第十二天
2007-07-26 | ICT第十二天
2007-07-29 | ICT实习第十三天

我在和C类协议作斗争。不说细节了，我要打败它！等我捷报！

今天淋雨了，透湿。回到寝室，全身淌着水……

明天，应该可以搞定C类的！！！！！

后天，写报告~

我现在开始做好员工了，每天加班到九点，还恋恋不舍……ORZ…

昨夜看《变形金刚》睡的晚了，10点多才爬起来。磨蹭了一小会儿直接去了所里。

check mail，收到了动物园的全部直立行走智能动物的照片，另包括田鼠数只。

下午先整理了下版本注释和文档，已经完成的协议包括A类全部，B类v1~v3。

然后实现了B4–接受端到发送端的阻塞模型，发现几个BUG，调试发现是B3中遗留下的逻辑错误 =.=|| Spin真聪明~~~ 

B类协议到此基本告一段落了，剩下些优化问题后面再说，这属于非主干问题。 

接着阅读C类协议文档，写得不是十分清晰，很多疑问，跟上次一样，还是没人问。等周一吧，师兄肯定会过来。

自己琢磨着协议，乱，乱得不禁困了，倒在椅子上睡着了。 

醒来，泡了杯茶，继续。

吃过晚饭，和叶子去打了一个小时的乒乓球，然后继续分析C类协议，在纸上列举了些零碎地理解，尝试列出一个方案，直到刚才，在寝室，彻底觉得C类无法继承B类的思路来做了：（

明天再读一次文档，看看是否真的要否定原有思路。如果是，那必当又要大大折腾一次咯~来吧~我现在不怕折腾！哼哼~

—————————-

如果十分顺利，下周末可以完成一切任务。嗯~wish！

为了测试美国, 香港, 中国大陆三地警察的实力, 联合国将三只兔子放在三个森林中, 看
三地警察谁先找出兔子. 
第一个森林前是美国警察, 他们先花整整半天时间开会制定作战计划, 严格分工, 然后派
特种部队快速进入森林进行地毯式搜索, 结果开会耽搁了时间, 兔子跑了, 任务失败! 

然后轮到香港警察, 他们派了一百多号人和几十辆警车在森林外一字排开, 由带头人用喇
叭喊话:"兔子,兔子,你已经被包围了, 快出来投降......" 半天过去了, 没动静. 飞虎队
进入森林, 搜索一遍, 没结果, 任务失败! 
最后是中国警察, 只有四个, 先打了一天麻将, 黄昏时一人拿一警棍进入森林,没五分钟,
 听到森林里传来一阵动物的惨叫, 中国警察一人抽着一根烟有说有笑的出来, 后面拖着一
 只鼻青脸肿的熊, 熊奄奄一息的说到:"不要再打了, 我就是兔子......." 

无事，吃喝玩乐而已。

请北京的同学吃了顿，还是湘菜，聊表心意吧，感谢大家一直以来的帮助啦~

我又喝了两小杯啤酒，青岛，不上头。

WCG（World Cyber Games）中国赛区决赛在人大举行，上午看了魔兽，下午看了几场反恐~nice！

明天不玩了，实验室见~