Intermezzo Alloy part 2

_main.md

Alloy part 2

前回の続き。Part 3

アトムと関係

アトムとは不可分、不変、非解釈（性質が組み込まれていない）を満たす。これだけではモデル化する能力が足りない。 そこで時空間を表せる関係を導入する。これはアトムからなるタプルの集合だ。

論理系

前提知識を要さない順に以下がある。

述語論理predicate calculus

二種類の式

• 関係名
• 限量変数からなるタプル

がある。

ナビゲーションnavigation形式expression

式は限量変数から関係をたどって集合を作る

関係演算relational calculus

限量子を持たない式が関係を表す

述語論理は冗長なのでナビゲーション形式がよく使われる。

例

// predicate calculus
all n: Name, d, d': Address |
    n -> d in address and n -> d' in address implies d = d'

// navigation expression
all n: Name | lone n.address

// relational calculus
no ~address.address - iden

sig とは何だったか

シグネチャ sig A {f: e} は次の意味と内部的に等価だ。

f in A -> e

in := ⊂, -> := ×

all this: A | this.f in e

: := ∈, A.B := {(a_1, b_1, b_2) | b_1 = a_2}

ファクト・関数・述語

ファクトは常に成り立つ制約を表す。制約を再利用するため述語を用いる。式を再利用するため関数を用いる。 例

いつ使う

常に成り立つかどうかで決めればよいが規模による。ファクトは簡潔だが制御が難しい。大域参照のような性質があるためだ。 アサーション毎に制約を切り替えたくなった場合、ファクトを最小限にして述語を用いてパッケージするほうが良い。

レシーバのような省略記法

先頭の引数がスカラなら this キーワードにより参照できる。 e.g. g [f [x, a], b] を x.f[a].g[b] と。

let

式が一つなら | expr と書いても { expr* } と書いても等価だ。

let letDecl,+ blockOrBar

lights.als

module language/lights

// 関数
//**********************************************************************

abstract sig Color {}
one sig Red, Yellow, Green extends Color {}

// 信号灯の色の変わり方
fun colorSequence : Color -> Color {
  Color <: iden + Red -> Green + Green -> Yellow + Yellow -> Red
  }

// 述語
//**********************************************************************

sig Light {}
sig LightState {
  color: Light -> one Color
  }
sig Junction {
  lights: set Light
  }

fun redLights (s:LightState): set Light {
  s.color.Red
  }

// 交差点では高々一つの信号灯を除いて赤
pred mostlyRed (s:LightState, j: Junction) {
  lone j.lights - redLights[s]
  }

// 操作を表現する述語
//**********************************************************************

// 交差点にある信号灯の色が、どう変化しうるかを表現
pred trans (
  s, s': LightState, // s は事前状態、s' は事後状態
  j: Junction) {
    // 高々一本の信号灯しか変化しない
    lone l: j.lights | s.color[l] != s'.color[l]
    all l: j.lights |
    let step = s.color[l] -> s'.color[l] {
      // 信号灯の色が順番に変わる
      step in colorSequence
      // 赤から別の色に変わるとき、残りはすべて赤
      step in Red -> (Color - Red) => j.lights in redLights[s]
      }
    }

assert Safe {
  all s, s': LightState, j: Junction |
    // 交差点で遷移前に一つの信号灯以外が全部赤
    mostlyRed[s, j] and trans[s, s', j]
      // ならば、遷移後でも一つの信号灯以外は全部赤
      => mostlyRed[s', j]
    }

check Safe

timeIdiom.als

// (Process, Time, Process)
// 中央に現れる場合、時刻tにおける関係を単純な結合関係式で表せない
sig Process_ {
  // p.toSend[t]
  toSend: Time -> Process,
}

// (Process, Process, Time)
sig Process {
  // p.toSend.t
  toSend: Process -> Time,
}

// ex. 1 プロセス上の恒等関係
pred init(t:Time) {
  // Process -> Process
  toSend.t
  = Process <: iden
}

fact ring {
  all p: Process | Process in p.^succ
}

// 動的
sig Process' {
  succ: Process -> Time
}

fact ring' {
  all t: Time, p: Process | Process in p.^(succ.t)
}

sig Process_' {
  succ: Time -> Process
}

fun succ_t'{
  p, q: Process | p -> t -> q in succ
}

// オブジェクトを起点に静的な観点と動的な観点とをまとめ、シグネチャを分類できる。
// Timeを先頭においた場合、Z・VDMのように静的な観点と動的な観点を分離する。これは状態を徐々に増やすモデリングに向く。