博客@利田小子

周五时基本上把程序改到最小了，系统能砍的我都看了，变量能不用的我都删了，能做的我都做了，但不是所有的system properties都能验证出来，还是一个属性验证时会出现out of memory的错误。能验证出来的属性对验证系统的正确性没有什么帮助，比如证明某属性是否可能存在时（即Uppaal的Possibly属性，E<>p），我们要求的是“肯定的”，比如Invariantly属性（A[]p），Potentially always属性（E[]p），和Eventually属性（A<>p）”，而不是“可能的”。此外，Uppaal的这些属性验证似乎也达不到我们想要的效果，他们的验证方法和我们预想的不大一样。我想，也许，可能，我们的系统不适合在Uppaal上模拟。看过一些别人用Uppaal做验证的paper之后，发现我们的model的确过于复杂，而且数量太多。普通的paper最多只用了两三个，但模拟中，我们用了至少9个automata。
Read more…

RPE做完后，这段时间老板没有给我新的活，而且看样子好像不会继续做RPE时做的东西，这样有点可惜，毕竟整了大半年，总不能没有什么产出就放弃了。老板政务缠身，学术方面已经不再那么热衷了，这可以从他从不和我提发paper的事看出。倒是我自己，一直想着什么时候能发我的第一篇论文，目前还是鸭蛋，这学期一过，来美也算两年了，一年TA，一年RA，一篇paper都没有，说出去有点丢人。来美读了两年PhD的而没有发paper的人，应该没有多少，我不想成为其中一员。咱不是大牛，但不能因此放弃努力，该争取的还是要去争取。
Read more…

从上学期开始，RPE的三个presentation我拖到今天才做完。2009.10.1第一个，2009.11.10第二个，2010.02.23第三个。第三个原定于1.26号做的，但种种原因，拖到现在。期间，一方面自己有点不自觉，凡事能拖则拖，不到deadline绝不干活，另一方面，老板太忙，没什么时间管我，这也助长了自己的惰性。但，不管怎样，总算给RPE划上句号了。今天的presentation做的还不错，不紧张，自我感觉良好，这次对时间把握得比较好，和第一次一样，上次内容太多，超时了。老板昨天叮嘱我，要控制好时间，40分钟之内要讲完。昨晚自己熟悉了一下，什么该讲，什么不该讲，都搞得比较清楚。昨晚的准备还是挺有效的，今天基本按照昨晚想好的路线走。RPE过了，成了phd candidate，也算轻松了，剩下的日子就是平平淡淡的做research了。希望自己能够自觉，毕竟phd是为自己读的，不出点东西对不起自己，对不起在这上面耗掉的时间，还有我可怜的青春年华。还有件让人欣慰的事，老板给我涨工资了，暗自高兴。

这周和上周基本上都在忙RPE的事，下周二就presentation了，需要对报告和程序作最后的修改，免得不符合要求。按规定，RPE的final report要15页，但没有规定格式，本以为我写不了那么多，结果我写了整整22页。问老板是否有关系，他说it’s OK，松了口气，让写多一些比较好办，让写少的话就难办了。初稿上周就写好了，发给老板，但老板太忙，一直都没时间改，拖了一周才给我他修改过的。我一边调程序，一边改报告，同时把一些新发现的东西也加进报告里。程序得调好了，presentation时会做demo，如果出问题就糗大了。到昨天，周五，程序基本上OK了，报告也将老板指出的地方纠正了，算是定稿了。为了保险，昨晚再查了一遍，用Office。报告我是用OpenOffice写的，起初用它提供的拼写检查功能查了一遍，没错，然后发给老板，老板在Office下修改的，一堆小错，大部分是拼写和单复数错误。现在对OpenOffice的纠错能力极度不信任。于是昨晚把报告的内容都拷到了Office的word文档里，从头到尾查了一遍，果然还有一些小错，修改完毕之后，确定了没有问题，就转成pdf格式的，给所有committee member发了一份，他们需要在presentation之前稍微读一下。这个周末就是准备ppt，有时间可以再弄弄程序，因为demo时只打算模拟一部分程序，这一部分一定搞定了，剩下的还得test。今天去rec运动了快两个小时，打壁球，玩了会健身器材。回家之后洗了个澡，去参加Jardine组织的sushi party，好多寿司，我吃了得有二十几个吧，当晚饭了。因为准备的寿司太多，可以take home。我对寿司不是很感兴趣，就没拿。

Jardine的RSVP (Resident Space Virtual Preferencing)开始了，这名字听着有点奇怪，其实就是公寓的住宿问题，所以住在Jardine的人都必须说明下个学年是否还在Jardine住，是否要换宿舍，这样公寓管理方好安排。下个学年本打算自己出来住，一个人住一室一厅的公寓。但斟酌再三，考虑了一些可能出现的问题之后，还是住两室一厅的吧，但不会在现在所住的apartment继续住下去，要换个apartment，还有室友也换。这边房子公寓分成好几种，我只考虑traditional和renovated的，便宜，其他类型的公寓不是我消费得起的。traditional或renovated的两室一厅公寓的房租平摊下来之后，一个月两百五十左右。如果住一室一厅的，一个月要四百左右，差了一百五，数目不小啊，能省则省。已经填了transfer request form，首选traditional 双人公寓，希望能分到。目前还没有室友，到时再找吧。
Read more…

查了一遍原来写的系统模拟代码，在代码和自动机上做了写必要的修改，没什么大的问题。但到模拟时，出现了一个exception，提示range error，好像是数值的范围问题，但没有指出在哪出的错。Uppaal没提供调试工具，我也不知错在哪，通查了一遍程序，没找到可能的出错点。这样耗着也不是办法，最后我新建了一个系统，将原系统一块一块分割出来，分别调试。最开始测试了Timer自动机，模拟timeout的，同时测试了消息的插入和删除，车辆位置关系确定，不变式判断等函数，并在自动机上调用，发现了一些问题，改过之后就能模拟了。Timer自动机和原系统的差不多是一样的，另外一个自动机则是后来新建的，没什么移植性可言。第二次尝试，只添加了三个自动机，一个Timer，一个Message，一个Trigger Vehicle，和相应的定义声明，在没有syntax error的情况下，进行模拟，出现了range error的exception，看来问题可能就在这三个自动机里。于是一个一个测试，先测Timer，这个Timer和我已经测过的就在自动机参数上有所区别，原来的Timer定义了一个整型值，并通过值传递的方式传给Timer，新加的Timer定义的是const整型值，用引用传递（带const），觉得应该不会有什么问题。但测试结果并非如此，提示有syntax error，依旧没指出在哪。为了简单，就把该整型值设成普通的，而不是const，及完全按测过的Timer自动机进行修改，进行模拟，可以了。于是把原系统的三个Timer自动机都改了一下，check syntax，没问题，试着simulation，居然成功了，再没有什么exception和syntax error。虽然比较偶然，但能出结果还是很高兴的，跑去跟老板说了一下。至今还没搞清楚为什么这些参数会导致那个exception，不过无所谓了，现在要的是结果，因为赶着做presentation。剩下的事就稍微好办些了，在原系统基础上进行修改，一是完善一下系统的功能，二是确定要要验证的东西，并在系统里实现。因为做presentation时，不能光给个系统实现，之所以做这个系统实现是有目的的，就是要验证我的系统在给定or假设的环境下能够work，所以我得prove。至于怎么prove，今天在给老板看模拟过程时讨论了一下，有了个idea，就先按着做吧。打算后周做Presentation，下周老板没空，这周把程序弄完，下周写report和ppt。

RPE还剩最后一个presentation，原定于1月26日做的，但目前来看，恐怕得推迟了。最近在做系统的模拟，Uppaal这工具功能实在让人憋屈，很多东西都无法实现。模型，函数等都弄好了，但运行不起来，说是有syntax error，但用Uppaal自带的Syntax Check功能根本就无法找出错误的地方。没有办法，现在的打算是，把所有函数和自动机模型重新翻查一遍，看能不能找到问题。看过一些用Uppaal做模拟工具的paper，和他们的系统相比，我们的系统要复杂的多，如果用Java，C之类的语言实现，应该不难，但我们挑了Uppaal，没办法，来不及换了，只能尽可能地去实现，系统该简化的就简化，直到能模拟出结果。和老板开会了，预计是无法在1月26日前完成模拟，除了模拟，还有report和ppt，这些也都还没准备。明天就给committee member发邮件，看能不能推迟一到两周。希望这周之内能把模拟的问题解决，下周写报告和ppt。

RPE最后一个Presentation就在月底，1月26日，到时我提交系统的模拟结果。最近一段时间忙着编程，看Uppaal已有些时日了，也看过一些编程的例子（都是很简单模拟），但没有在上面写过程序。Uppaal使用的语言有点像C语言，但Uppaal的功能不是很强，它的编程语言也有不少限制。对于要模拟的系统，我已经把它的伪代码写完了。根据Uppaal的情况，已经搞清如何把系统移植到Uppaal上，需要建多少自动机，自动机之间如何协调等，并且在草稿纸上根据构思好的函数和变量等构建好了这些自动机。这些天的工作，就是编程，按着脑子里的系统模型和画好的自动机在Uppaal上实现。刚开始使用Uppaal编程，免不了一些问题，但都解决了，一切还算顺利。时间有点紧，希望能提前十天完成任务（还有五天时间），这样才有足够的时间写report，准备PPT。

感觉这学期过得好快，估计是负担较轻的缘故，三门课只有一门需要忙，不像第一年，每学期三门课都让我累得够呛，写不完的作业，还有程序。这学期不出意外，三门课应该都是A了。昨天的考试今天成绩就出来了，25分拿了24分，班里最高，最后的总成绩是93.8%，A。下学期的课还是选九个学分的课，但只有两门，都是老板的课，一门要上课，CIS 825，三个学分，一门是research，CIS 999，打算选6个学分。过了Breadth Exam算是没有选课的负担了，但research还不见起色，自己有点懒散，还是得加把劲，不能太闲了。这时候也该撇开兴趣问题了，既然都是该做的，那就早点完成吧。寒假到了，本来想去travel，但预算不够，只能宅在家里了，继续在屯里悠哉。圣诞节和元旦，应该和去年一样，也在平淡中度过。
Read more…

今天中午系里又有Pizza Party，免费的匹萨和饮料。不知道是因为想吃pizza，还是因为天气冷，一个早上醒了好几次，每次都觉得睡过头了，但一看时间，还很早，这样反反复复好几次，折腾。Pizza Party十一点半开始，我十点左右起的床，洗洗弄弄，上了会网，然后屁颠屁颠地去做校车。天太冷，昨天下的雪都堆得厚厚的，估计都结冰了，走路不方便，还是坐车吧，也暖和，不用在寒风中折磨自己。到系里时还不到十一点半，以前的Pizza Party我都很晚才去，基本是去吃剩下的，今天去打头阵，不错。我饭量不大，吃三块匹萨就吃不下了，其他人都吃了不少。期间和老板聊了一下，最近有人发邮件给我问CPS的事情，我也问问老板，得到的答案是，CPS只是一个松散的概念而已，大家不要老揪着CPS不放，到具体的应用领域才有意义。周一因为老板去KC开会，meeting取消，老板说明天十点或十一点补上，我说十一点吧，十点实在太早了。明天的meeting应该有点东西可说，这次我把碰到的问题，还有想法记下来了。
Read more…