利田小子

今天，不想做什么，虽然有活，天气难得的好，出着大太阳，气温十几度的样子。吃完午饭后，呆在屋里，想着要干嘛，突然间想到外面走走，但不知道去哪。但，想来没有目标并无重要，享受的是过程。于是，带上mp3，相机，手机，骑着自行车，沿着公路一直骑行。骑了好几个mile，也不知道自己到哪，但心情很舒畅，使劲地踩着自行车，任凭风吹着自己，期待着能碰到农场啥的，但沿着自行车道走，两边的除了房子，没有其他东西，也许，农场，还在很远的地方。骑到某处了，看着前面又是一个大的上坡，而且边上没有期待的样子，原路折返。很难得出来瞎转，在这么好的天气里，还是自己一个人。也许，以后会多出来转转，感受一下大农村的气息。

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