interleaving n.[计]交叉,交错
abstraction n. 提取
reasoning n. 推理, 评理, 论证 adj. 推理的
to this end prep.为此目的,为此
mitigate v. 减轻
refinement n. 精致, (言谈, 举止等的)文雅, 精巧
syntactically adv. [语]依照句法地, 在语句构成上
tuple n. 元组
twofold adj. 两部分的, 双重的 adv. 两部分地, 双重地
depict vt. 描述, 描写
refine vt. 精炼, 精制, 使文雅高尚
compilation n. 编辑
akin adj. 同族的, 类似的  akin to vt.与…类似  [反义词] alien
on-the-fly 【信】在传输过程中；【设】高速旋转，飞击 [EXP]My wife is always on the fly. 我妻子总是忙忙碌碌。
i.e. adv. 也就是
dual adj. 双的, 二重的, 双重
temporal adj. 时间的, 当时的, 暂时的, 现世的, 世俗的  n. 世间万物, 教会财产
unary adj. [数]一元的  [EXP] unary operator 单目运算符
rendezvous n. 集合点 v. 在指定地点集合
elaborate adj. 精心制作的, 详细阐述的, 精细 vt. 精心制作, 详细阐述 v. 详细描述
arbitrary adj. 任意的, 武断的, 独裁的, 专断的
proposition n. 主张, 建议, 陈述, 命题
deviated n.偏科的
aberration n. 失常
robust 精力充沛的
algebra n. 代数学
fairness n. 公平, 正直, 美好, 明亮, 清晰, 适当, 顺利性

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

下午看了些文档，但不是很深入，后来干脆就去和马老师聊天了，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: 关于最近的天气，实在变态。白天看上去很正常，一到下午六点就有些下雨的苗头，到了七八点，那个雨啊~~~简直吓死人。前天直接淋回去的，昨天提前步行回学校，不小心躲过一劫，今天没长记性，虽然有伞，却还是湿的差不多了……现在，外面电闪雷鸣，有感觉！