上午做了演示，原计划一个小时就可以完成，实际时间一小时四十分。马导师问了不少问题，提出了很多重要的指导和建议，这些建议可以让我当前的工作更具有理论意义，很爽的一件事情。

下午看了些文档，但不是很深入，后来干脆就去和马老师聊天了，GoogleBaidu，MSJava，肆意乱谈，后来他还给我看他当年写的java程序，可惜java不争气，没有配置好环境，恁是跑不起来。后面还聊了保送的问题，他突然给我看所里2008年保送招生计划表，体会很深地说，考的学生都不怎样，保的质量要好得多。

今天是立秋，北方有长秋膘的说法。晚上，马导竟然请我去吃北京火锅，涮羊肉。这北京火锅的做法果然不一样！武汉的火锅属于川锅，底锅是做好了的，这里的底锅是—–白开水！Orz！自己下料，等水开，然后在放羊肉，等肉吃的差不多了，锅里面有了些油之后才可以放白菜之类的小东西。否则，开水煮白菜，就太faint了。

羊肉经过这么一涮，竟然没了那怪异的味道，很鲜呢！

喝酒，吃肉。嗯~ 干杯！

吃饱了，喝了一瓶。

1个小时候，脑子恢复了正常。然而事实证明，还是不够清醒：
回来的时候在公汽上发呆了，结果，坐过站了……等我意识到的时候，车门已关，离站好多米  

明天、后天，把理论工作做好，完善报告文档。

另外，明天去见见北京的一个哥哥，晚上吧。

周六，去见一个mm，还没见过~

灌水完毕！

效果很不错。某些问题~~~haha

下面是进一步工作的指导:
1. Spin背后的理论支持。概念性的必须了解。

2. 完善Spin的介绍：并发性、随机性、同步机制。

3. 证明该验证程序可以处理实际系统中的下列情况：
    a. 主机方发送方和接收方同时存在的情况
    b. 多个主机相互通信的情况

4. 认真考虑实际模型的阻塞原因，对照真实系统。

我什么时候能回家??????????????????????????????????

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