Zenn
Open40

Alloy

alloy
hayaohayao

fact

常に成り立つと仮定した制約を記述

assert

モデルのfactから導かれると考えられる制約

check

asesertの反例を探す

fun

再利用可能な式

pred

再利用可能な制約

run

制約の解を探す

hayaohayao

論理系

atom

JavaScriptでいうSymbolのようなもの？

tuple

atomの並び

relation

tupleの集合

size

relationのtupleの数

arity

relationのtupleの長さ

hayaohayao

domain

最初の列のatomの集合

range

最後の列のatomの集合

hayaohayao

定数

none

空集合

univ

普遍集合
全てのatomの単項関係

iden

恒等関係
全てのatomから自分自身への二項関係

hayaohayao

関係演算子

p -> q

直積

p.q

{ (N0, A0)}.{(A0, D0)} = {(N0,D0)}

p [q]

p [q] = q.p

~r

各tupleのatomの順序を反転させた関係

対象閉包

r + ~r

推移閉包

^r = r + r.r + r.r.r + ...

反射推移閉包

*r = ^r + iden

<:, :>

s <: r
集合sの要素で始まるtupleのみをrから集めた関係

r :> s
集合sの要素で終わるtupleのみをrから集めた関係

p ++ q

和集合に違いがqのtupleがpのtupleを置き換える

hayaohayao

限量

Q x: e | F
のQで使われる

all, some, no, lone, one

all

任意の

some

ある～

no

not all

lone

0 or 1

one

1

式に適用した場合

some e

eはtupleをいくつかもつ

no e

eはtupleをもたない

lone e

eはtupleを高々一つもつ

one e

eはtupleをちょうど一つもつ

hayaohayao

宣言

関係名: 式

多重度制約

x: m eのm

set, one, lone, some

関係多重度

r: A m -> n B

hayaohayao

言語

sig

atomの集合

sig A {}

sig A1 extends A {}
A1はAの部分集合

extends

互いに素

in

互いに素とは限らない

hayaohayao

field

sig A {f: e}
定義域がAで値域がeである関係fが導入される。

Aからeへの矢印fが引かれるような感じ？
f{(A0, e0),(A1,e1),...}みたいな？

hayaohayao

シグネチャでモデリングする。クラス図に近い気がする

predやfactで制約を表現

assertで制約を満たすか確認

run assertで反例を探せる

run pred で制約を満たす関係を探検できる
predがtrueになるようなものを探す？

hayaohayao

モデル図

* 任意の個数
! ただひとつ
? 高々一つ
+ 1つ以上

hayaohayao

software abstractionの「事例」では関係にTimeを持たせて、Traceファクトを定義するみたいな定石が紹介されているが、alloy 6で時相論理に対応して、定石が廃れたっぽい

hayaohayao

時相式

after

after Fがstate iでtrue <=> Fがstate i+1でtrue

always

always Fがstate iでtrue <=> あらゆるstate >= iでFがtrue

eventually

eventually Fがstate iでtrue <=> あるstate >= iでFがtrue

until

F until Gがstate iでtrue <=> あるstate j >= iでGがtrueかつi<=k<=jとなる全てのkでFがtrue
(口語）GがtrueになるまでFはtrue　（Gはある状態でtrueになる）

release

F release Gがstate iでtrue <=> Fが真であるstate kまでのすべてのstate >= iにおいて真
、またはそのようなkが存在せず、その場合Gは任意のstate>=iで成立する（よくわからない）
(口語) GがtrueになるまでFがtrue (Gがtrueにならなくても良い)

a ; b

a and after bと等価

hayaohayao

New Config

モデルのimmutableな部分を変える

New Init

新しい初期状態と新しいふるまいのトレース

New Trace

新しいふるまいのトレース

New Fork

トレースの中間地点でのみ使える。新しい次の状態を見つける

hayaohayao

時相論理の導入はalloyにとって結構革命的では。。

hayaohayao

alloyが役立ちそうな場面

  • 並行処理
  • 分散システム
  • 仕様が複雑なシステム ex.) 自動販売機
hayaohayao

テクニック

はやめにrun example {}をして仕様をバリデートする

hayaohayao

alloyの型システムの主な目的はいわゆる無関係な式を見つけること

hayaohayao

列挙型

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

enum Color { Red, Green, Blue}

enumの場合は宣言した順に全順序がつく

hayaohayao

Tips

StringやIntはできるだけさけるべき。

  • セマンティクスが通常のシグネチャよりトリッキー
  • 要求しているより豊かな意味論を持っている場合が多い

Stringの使い道はほとんどない。Intは算術演算を行う場合に有効な場合がある。

hayaohayao

themeでvisualizerの見え方を色々カスタマイズできる。

hayaohayao

object in Entry lone -> Dir
はobejctが(Entry,Dir)という関係しか持たないことも意味する

hayaohayao
  1. factを追加する
  2. run example {}を走らせる
  3. 1に戻る

というループを続けて設計を洗練させていく

hayaohayao

factやassertにコメントつけるの大事。なれていないとコードをみてもぱっと意味を理解できない

hayaohayao

形式的な仕様を作成する際には，できるだけ抽象的であることが望ましく，特に不必要な制限を加えないことが重要

hayaohayao
fact {
  Id in first.*next
}

って

fact {
  all id : Id | id in first.*next
}

の省略形という解釈でよい？

hayaohayao

alloyの定数

  • none
  • univ
  • iden

トップレベルのシグネチャが可変の場合(varで定義されている場合)
univとidenは可変であり、univはその状態におけるすべてのシグネチャに含まれる原子を含む

hayaohayao

モジュール機能がある

moduleでモジュール化してopenでモジュールを使う

hayaohayao

時相機能を使うと、制限なしではどのような遷移も可能になる。

有効な遷移を制限する最も簡単な方法はシステムで発生しうるすべてのイベントを考慮し、いつ発生しうるか（そのガード）と、変更可能な関係に対するその影響を指定すること

hayaohayao

ステップ間で変化してほしくない関係にはフレーム条件を指定する

例
inbox' = inbox
hayaohayao

predの記述はすべて成立しなければならない。なのでif A then Bだったら

pred {
   A
   B
}

と書けば所望の動作を実現できる

hayaohayao

特性の種類

安全特性

(望ましくない)振る舞いを禁じる

活性特性

(望ましい)振る舞いを強制する

hayaohayao

弱い公平性

(eventually always xxx) implies (always eventually yyy)

強い公平性

(always eventually xxx) implies (always eventually yyy)