Alloy Analyzer で状態の変化を表現する方法 - ソフトウェア開発のひみつ

alloyで状態の変化を表現する方法はいろいろありますが、なるべく単純なかたちでこれを実現してみたいと思います。

状態は、事前状態と事後状態のふたつだけ
事前状態と事後状態が同時に表示される中で、どのAtomが事前状態にあり、
その事後状態を表すのがどのAtomか、分かりやすく見えるようにする

ことを目的とします。
なお状態変化を引き起こす、イベントについては、ここでは表現しません。

状態表現用のフィールドを付加する

単純に、上記の2要素をフィールドに落とし込みました。
つまり、事前/事後の状態あらわすフィールドと、識別子としてのフィールド、を用意することで、状態の変化は表現できるはずです。

module main

// Boundaryは、何らかの1次元の位置、つまり何らかの値を表す。
sig Boundary { val: one Int }  
sig Entity {
  some_field: one Boundary,
  // 状態変化を表現することを目的に付加したフィールド
  meta_id: one Int,
  meta_state: one Int
}

fact {
  /** meta_state は、-1か0しかない。つまり、事前と事後。*/
  all e:Entity | e.meta_state = 0 or e.meta_state = -1
  /** 
   ID が等しいふたつAtomがあったら、
   それはひとつのAtomの事前状態と事後状態であると考える。
  */
  all e1,e2:Entity |
    (e1 != e2 and e1.meta_id = e2.meta_id) => 
      (e1.meta_state != e2.meta_state)
}

run {} for 3 but 4 Entity, 3 Int

すると、こうなります。

Entity0はEntity1が、Entity3はEntity2が状態変化したものである、ことを示しているといえます。

しかし、ちょっとまってください。
確かにEntity2は、Entity3に状態が変化しているといえます。その証拠に、"some_field" の値が変わっています。
しかし、Entity0は、Entity1と較べて、値は何も変わっていません。これは状態変化したと言えないのではないか？

その通りです。
「何を以って状態が変化した」とするのか、その定義が無ければ筋が通りませんね。
それも記述しましょう。ついでに、状態変化の対象となるAtomと、ならないAtomがあるというケースにも対応します。

上記のalloyモジュールにさらに編集して
たとえば以下のように、くじ引きをモデリングしてみます。
＜抽選前＞

参加者は、重複の無いユニークな抽選番号をひとつづつ与えられている

＜抽選後＞

一番大きな抽選番号を持っていた参加者が、賞品を得ている

module main

// Boundaryは、何らかの1次元の位置、つまり何らかの値を表す。
sig Boundary { val: one Int }  
sig Participant {
  loto_num: one Boundary,
  prize_num: lone Boundary,
  // 状態変化を表現することを目的に付加したフィールド
  meta_id: one Int,
  meta_state: one Int
}
fact {
  /** meta_state は、-1か0しかない。つまり、事前と事後。*/
  all p:Participant | p.meta_state = -1 or p.meta_state = 0
  /** 
   ID が等しいふたつAtomがあったら、
   それはひとつのAtomの事前状態と事後状態であると考える。
  */
  all p1,p2:Participant |
    (p1 != p2 and p1.meta_id = p2.meta_id) => 
      (p1.meta_state != p2.meta_state)
}

--------------------------------------------------------------
-- くじ引きとしてloto_numがあり、
-- loto_num の値が一番大きかったParticipantに、
-- prize_num、つまり賞品が与えられている。 
--------------------------------------------------------------

-- 事前条件
pred BeforeLoto {
  all participant:Participant |
    participant.meta_state = -1 => 
      /** 誰も賞品を与えられていないこと。*/
      participant.prize_num = none
}
-- 不変条件
pred Immutable {
  all participant:Participant |
    /** 事前状態、事後状態それぞれの中で、IDとloto_numは重複していないこと。 */
    participant.meta_state = -1 => 
      all p1,p2:participant |
        p1 != p2 => eternalUnique[p1,p2]
    &&
    participant.meta_state = 0 => 
      all p1,p2:participant |
        p1 != p2 => eternalUnique[p1,p2]
  /** 
   IDが等しく、状態が異なるAto同士は、loto_numが共通であること。
   それ以外は、loto_numは必ず異なる。
  */
  all p1,p2:Participant |
    p1 != p2 implies (
      (p1.meta_id = p2.meta_id and
      p1.meta_state != p2.meta_state) implies 
        (p1.loto_num = p2.loto_num) && (p1.loto_num.val = p2.loto_num.val) else
          (p1.loto_num != p2.loto_num) && (p1.loto_num.val != p2.loto_num.val)
    )
}
pred eternalUnique[p1:Participant,p2:Participant] {
  (p1.meta_id != p2.meta_id) and (p1.loto_num != p2.loto_num)
}

/** 
 状態変化のための条件：loto_numがmaxであること。
 そのmaxであるloto_numを返す。
*/
fun win_num : Int{
  Boundary.(Participant.(Participant<:loto_num)<:val).max
}
-- 事後条件
pred AfterLoto {
  /** 事後状態Atomには必ず、対になる事前状態のAtomが存在すること。*/
  Participant.(
    (Participant<:meta_state & Participant->0).Int<:meta_id
  )  // 抽選後参加者 とそのID、から、IDだけを取り出す
  in
  Participant.(
    (Participant<:meta_state & Participant->-1).Int<:meta_id
  )  // 抽選前参加者 とそのID、から、IDだけを取り出す
  && 
  /** loto_num がmaxの者だけが prize_num を持っていること。*/
  let winner = loto_num:>(Boundary<:val & Boundary->win_num).Int |
    Participant<:prize_num in winner
}

run {Immutable && BeforeLoto && AfterLoto} 
  for 3 but 4 Participant, 3 Int

これで表現できました。

結果がこれです。
Participant1 と Participant2 が、同じidを持っていますので、
これは同じオブジェクトの事前状態と事後状態をあらわしているはずです。
果たしてその通り、Participant1 の meta_state が 0、Participant2 の meta_state が -1 である、ので、
Participant1 は Participant2 が状態変化したものだといえます。両者の loto_num には変化はありません。
そして事前状態の Participant2 は、最大の loto_num を与えられていました。
つまり抽選に当選しているので、事後状態の Participant1 は、prize_num を、ただ一人保持しているわけです。