利田小子

周五时基本上把程序改到最小了，系统能砍的我都看了，变量能不用的我都删了，能做的我都做了，但不是所有的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。

在和老板一番讨论之后，虽然我已经在这方面花了这么多时间，但为了能产篇paper，我们不得不弃用Uppaal，先抱抱佛脚，改用Spin，先做个简单的模拟，希望它能验证出一些系统属性，给点正面的feedback，而不是out of memory。看我有点郁闷，老板拿了个爱迪生发明灯泡的例子安慰我，说虽然没有一次成功，但至少知道了某些东西是不可行的。我也还好，只是发paper心切，想着这学期一定要弄篇paper出来。我在想，虽然不能得出一些正面的结果，能不能根据现有的result发一篇paper，但这样的paper有点水。老板说，他宁愿多等几个月，发一篇好的paper，也不愿发两三篇的水文。好吧，我也不想发水文，这个想法就放弃了。此外，也看到过一些paper根本没做simulation，而只是提出一个model，但这样的paper也很水，除非是大牛级的人物写的。

纠结之后，还是老老实实用Spin试一下吧。那个会议3.15截止，还有不到几天的时间，希望下周能把程序完成了，剩下点时间就写paper。老板说如果程序能完成，12号之后，他有free time，可以帮忙写。老板还说，会议一般都可以给个deadline extension，一周左右，但不能count on that，还是稳扎稳打好。如果Spin不行，那之后再换工具了，下次可能换成NS-2，据说要花不少时间才能学会。

唉，发paper不容易，不知道什么时候能产一篇。