Alloy による Git のコミットグラフのモデリング

alloy_git.als

// ************************************
//   Git のコミットグラフのモデル
// ************************************

open util/ordering[Time]

// ------------------------------------
//   グラフの構成要素
// ------------------------------------

// 時刻パラメータ
sig Time {
    // 現在、チェックアウトしているブランチ
    // 今回はリビジョンを直接指定するチェックアウトは考えない
    currentBranch : Branch
}

// コミットを表すグラフのノード
sig Commit {
    // 各時刻における親コミット
    // none ならばそのコミットはまだ生じていない
    parents : Commit -> Time
}

// 初期コミット
one sig InitCommit extends Commit {}

// どのコミットも自分自身の子孫にはならない
fact acyclic {
    all t : Time, c : Commit | c not in c.^(parents.t)
}

// ブランチ名のラベル
sig Branch {
    // 各時刻において参照しているコミット
    // none ならばそのブランチはまだ作成されていない
    pointsAt : Commit lone -> Time
}

// マスターブランチ
one sig MasterBranch extends Branch {}


// ------------------------------------
//   各種 Git コマンド
// ------------------------------------

// Git コマンドのテンプレート
abstract sig Command {
    pre, post : some Time  // コマンドの事前時刻と事後時刻
} {
    post = pre.next  // コマンドによる状態遷移にはちょうど 1 単位時間必要
}

// commit コマンド
sig GitCommit extends Command {
    newCommit : Commit  // コマンドによって新しく生じるコミット
} {
    // 事前状態においてチェックアウトされていたブランチを cb とする
    let cb = pre.currentBranch {
        // 新しく生じるコミットは、事前状態においてグラフ中に存在しない
        newCommit.parents.pre = none
        // ブランチが参照していた場所の子コミットが新しく生じる
        newCommit.parents.post = cb.pointsAt.pre
        // 事後状態において、cb は新しく生じたコミットを参照
        cb.pointsAt.post = newCommit
        // チェックアウトしているブランチ名は変化なし
        post.currentBranch = cb
        // 他のコミットの親子関係は変化なし
        all c : Commit - newCommit | c.parents.post = c.parents.pre
        // 他のブランチの参照は変化なし
        all b : Branch - cb | b.pointsAt.post = b.pointsAt.pre
    }
}

// branch コマンド
sig GitBranch extends Command {
   newBranch : Branch  // コマンドによって新しく生じるブランチ
} {
    // 事前状態においてチェックアウトされていたブランチを cb とする
    let cb = pre.currentBranch {
        // 新しく生じるブランチは、事前状態においてグラフ中に存在しない
        newBranch.pointsAt.pre = none
        // 新しいブランチは今まで参照していたコミットと同じ場所を参照する
        newBranch.pointsAt.post = cb.pointsAt.pre
        // チェックアウトしているブランチ名は変化なし
        post.currentBranch = cb
        // コミットの親子関係は変化なし
        all c : Commit | c.parents.post = c.parents.pre
        // 他のブランチの参照は変化なし
        all b : Branch - newBranch | b.pointsAt.post = b.pointsAt.pre
    }
}

// checkout コマンド
sig GitCheckout extends Command {
    to : Branch  // コマンドによって移動する先のブランチ
} {
    // 移動先のブランチは事前状態において既にグラフ中に存在している
    to.pointsAt.pre != none
    // 移動先ブランチは現在のブランチとは異なる
    pre.currentBranch != to
    // 事後状態において指定した移動先ブランチに移動している
    post.currentBranch = to
    // コミットの親子関係は変化なし
    all c : Commit | c.parents.post = c.parents.pre
    // ブランチの参照は変化なし
    all b : Branch | b.pointsAt.post = b.pointsAt.pre
}

// merge コマンド
sig GitMerge extends Command {
    with      : Branch,  // マージする相手ブランチ
    newCommit : Commit   // コマンドによって新しく生じるコミット
} {
    // 事前状態においてチェックアウトされていたブランチを cb とする
    let cb = pre.currentBranch {
        // マージ相手のブランチは事前状態において既にグラフ中に存在している
        with.pointsAt.pre != none
        // マージ相手のブランチは現在のブランチとは異なる
        cb != with
        // 新しく生じるコミットは、事前状態においてグラフ中に存在しない
        newCommit.parents.pre = none
        // 新しく生じるコミットの親は、マージされた 2 個のコミット
        newCommit.parents.post = (cb.pointsAt.pre + with.pointsAt.pre)
        // 事後状態にいて、cb は新しく生じるコミットを参照する
        cb.pointsAt.post = newCommit
        // チェックアウトしているブランチ名は変化なし
        post.currentBranch = cb
        // それ以外のコミットの親子関係は変化なし
        all c : Commit - newCommit | c.parents.post = c.parents.pre
        // それ以外のブランチの参照は変化なし
        all b : Branch - cb | b.pointsAt.post = b.pointsAt.pre
    }
}


// ------------------------------------
//   状態遷移に関する制約
// ------------------------------------

// 初期状態
pred initState (t : Time) {
    // コミット間の親子関係は存在しない
    Commit.parents.t = none
    // 初期ブランチはマスターブランチ
    t.currentBranch = MasterBranch
    // マスターブランチは初期コミットを参照
    MasterBranch.pointsAt.t = InitCommit
    // それ以外のブランチは存在しない
    all b : Branch - MasterBranch | b.pointsAt.t = none
}

// トレース制約
fact trace {
    // 初期状態からスタート
    initState[first]
    // 状態間はコマンドによって遷移
    all t : Time - last | let t' = t.next |
        one cmd : Command | cmd.pre = t && cmd.post = t'
}

run {} for 7 Commit, 3 Branch, 8 Time, 7 Command

alloy_git.thm

<?xml version="1.0"?>
<alloy>

<view nodetheme="Martha" edgetheme="Martha">

<projection> <type name="Time"/> </projection>

<defaultnode hideunconnected="yes" showinattr="yes"/>

<defaultedge color="Black" layout="yes"/>

<node>
   <type name="GitBranch"/>
   <type name="GitCheckout"/>
   <type name="GitCommit"/>
   <type name="GitMerge"/>
   <type name="Int"/>
   <type name="String"/>
   <type name="Time"/>
   <type name="univ"/>
   <type name="ordering/Ord"/>
   <type name="seq/Int"/>
   <set name="currentBranch" type="Branch"/>
   <set name="First" type="ordering/Ord"/>
   <set name="Next" type="ordering/Ord"/>
</node>

<node hideunconnected="no">
   <type name="InitCommit"/>
   <type name="MasterBranch"/>
</node>

<node shape="Box" color="White">
   <type name="Command"/>
</node>

<node shape="Ellipse" color="Green">
   <type name="Commit"/>
</node>

<node shape="Hexagon" color="Yellow">
   <type name="Branch"/>
</node>

<node visible="yes" hideunconnected="no">
   <set name="post" type="Command"/>
   <set name="pre" type="Command"/>
</node>

<edge style="Dotted">
   <relation name="pointsAt"> <type name="Branch"/> <type name="Commit"/> </relation>
</edge>

<edge style="Solid">
   <relation name="parents"> <type name="Commit"/> <type name="Commit"/> </relation>
</edge>

<edge visible="no" attribute="yes">
   <relation name="newBranch"> <type name="GitBranch"/> <type name="Branch"/> </relation>
   <relation name="newCommit"> <type name="GitCommit"/> <type name="Commit"/> </relation>
   <relation name="newCommit"> <type name="GitMerge"/> <type name="Commit"/> </relation>
   <relation name="to"> <type name="GitCheckout"/> <type name="Branch"/> </relation>
   <relation name="with"> <type name="GitMerge"/> <type name="Branch"/> </relation>
</edge>

</view>

</alloy>