続・形式仕様記述Alloyで時系列の仕様を試してみる

昨日、時系列の仕様を試してみました。
http://d.hatena.ne.jp/nowokay/20120104#1325696475

だけど、カート自体を時間ごとの状態とみなしたので、同一時間でのカート同士の関係を記述できなかったり、いろいろ不便。
なので、「時間」というシグネチャを導入して、時間によって変わる「含む」が時系列データとなるようにしてみます。
「含む」に時間を対応付けてますね。

module exec/cart
open util/ordering[時間]

sig 商品{}
sig 時間{}
sig カート{
  含む: set 商品 -> 時間
}

あとは、「c.含む」を「c.含む.t」に、「c'.含む」だったものを「c.含む.t'」にするという感じでモデルを修正します。

pred 商品追加(c :カート, s:商品, t, t': 時間){
  t' = t.next
  not s in c.含む.t
  c.含む.t' = c.含む.t + s
}
pred 商品削除(c:カート, s:商品, t, t': 時間){
  t' = t.next
  c.含む.t' = c.含む.t - s
}

assert 追加して削除したら元に戻る{
  all c:カート, s: 商品, t, t', t'':時間 |{
    商品追加[c, s, t, t']
    商品削除[c, s, t', t'']
   } implies c.含む.t = c.含む.t''
}
check 追加して削除したら元に戻る

pred show{
  some c:カート, s:商品, t, t', t'':時間 | {
    商品追加[c, s, t, t']
    商品削除[c, s, t', t'']
  }
}

run show

そしたら、こんな感じ。わけわかんない！

「時間」を「Projection」に指定して時間ごとに見てみます。



時間０でカート２に含まれてなかった商品が、時間１で追加されて、時間２で削除されていることがわかります。でも、カート０とカート１にはずっと含まれてますね。

やっぱり複数のカートにひとつの商品が含まれるのが気になるので、これをなんとか制限したい。

  all s:商品, t:時間| lone xxx

のようなことを書けばいいはずなんだけど、xxxの部分、どう書いていいやら・・・
「s.含む」にtをつければいいかと思ったけど*1、「s.含む.t」も「t.s.含む」もだめ。「t->s.含む」とかやってみてもだめ。「s.含む->t」もだめ。
と思ったら、こうやるととりあえず警告とか構文エラーとか出なくなった。

fact{
  all s:商品, t:時間| lone s->含む->t
}

でrun showしてみると、こんな感じに。試行錯誤してる間に、Projection指定しなくても見れるようになってきました。

うまくいったのかな。
でも、ほかの例をみてみると、どうもカートに商品が入るのがひとつのタイミングだけにも絞られてるっぽい。

ということで、追加して削除したあと、また追加してみる。

pred show{
  some c:カート, s:商品, t, t', t'',t''':時間 | {
    商品追加[c, s, t, t']
    商品削除[c, s, t', t'']
    商品追加[c, s, t'', t''']
  }
}

run show for 2 カート, 1 商品, 4 時間

ここで、時間が４つに必要になっているのだけど、runになにも指定しないと時間を３つまでしかとってくれないので、それぞれのインスタンス数を指定してます。
なんだけど、実行してもインスタンスを見つけてくれない。追加したfactをはずすとちゃんとインスタンスが出る。
やっぱり、一度商品に入ったものがもういちどカートに入らないようになっているっぽい。

で、試行錯誤したら、こういうfactの指定でうまくいった。

fact{
  all s:商品, t:時間| lone s->含む.t
}

でも、なにやってるかわかんないので、あとでちゃんとおさらいしないと・・・
ちなみに「含む.t.s」と「含む.t->s」でもおっけーっぽい。(24通り試した)

実行して見てみると、ちゃんと時間０でカート０にあったものが、時間１でカート０からはずれてカート１に追加され、時間２でカート１から削除されてカート０に入り、時間３で再びカート０からはずれてカート１に追加されています。

いやいや。カート０から奪い取っちゃだめだよね。ということで、商品追加時の「カートにすでに商品が入っていないように」という制約を「商品が入ったカートがないように」という制約に書き換えます。

pred 商品追加(c :カート, s:商品, t, t': 時間){
  t' = t.next
  no c':カート | s in c'.含む.t
  c.含む.t' = c.含む.t + s
}

これで実行すると、他のカートから商品を横取りすることがなくなりました。

なんだかんだで、Alloyさんのおかげで、商品追加するときの制約としてカートにあらかじめ入っていないというだけでは不十分で、商品を含んだカートがないという制約にしないといけないことがわかって、仕様が検証されたわけですね。
ユニットテスト書いたところで、正しく「カートにあらかじめ入っていない」が実装されていることが確認できるだけで、「カートにあらかじめ入っていない」という仕様では不十分だということはなかなかわからないわけです。

これがAlloyさんの力か。結構小さいものにでも使えるかも。
Alloyの本をもう少しちゃんと読んでみよう。

抽象によるソフトウェア設計−Alloyではじめる形式手法−

最終的な仕様記述はこんな感じ。

module exec/cart
open util/ordering[時間]

sig 商品{}
sig 時間{}
sig カート{
  含む: set 商品 -> 時間
}
fact{
  all s:商品, t:時間| lone s->含む.t
}
pred 商品追加(c :カート, s:商品, t, t': 時間){
  t' = t.next
  no c':カート | s in c'.含む.t
  c.含む.t' = c.含む.t + s
}
pred 商品削除(c:カート, s:商品, t, t': 時間){
  t' = t.next
  c.含む.t' = c.含む.t - s
}

assert 追加して削除したら元に戻る{
  all c:カート, s: 商品, t, t', t'':時間 |{
    商品追加[c, s, t, t']
    商品削除[c, s, t', t'']
   } implies c.含む.t = c.含む.t''
}
check 追加して削除したら元に戻る

assert 同じ商品が別のカートに{
  all s: 商品, c:カート, t:時間 | no c':カート |{
    c != c'
    s in c.含む.t
    s in c'.含む.t
  }
}
check 同じ商品が別のカートに

pred show{
  some c:カート, s:商品, t, t', t'',t''':時間 | {
    商品追加[c, s, t, t']
    商品削除[c, s, t', t'']
    商品追加[c, s, t'', t''']
  }
}

run show for 2 カート, 1 商品, 4 時間

*1:2012/1/7追記：これが勘違いで、ほんとは「含む.s」にtをつける