ボンジュール・マドモアゼル

本サイトの情報は自己責任にてご利用下さい。

[Alloy] 抽象によるソフトウェア設計 Alloyではじめる形式手法 練習問題 A.5.1 解答例3

 
A.5.1 Unix ファイルシステム 解答例3

解答例1
http://monado.dtiblog.com/blog-entry-147.html
解答例2
http://monado.dtiblog.com/blog-entry-148.html

Path シグネチャに検索のための機構を導入。
FileSystem シグネチャは簡略化のため削除。

module exercises/inode

open util/integer

/**** File System Model ****/
sig Inumber {
inodeTable: disj lone Inode
}
abstract sig Inode {
addresses: disj (some Address),
iname: lone Name,
parent: lone Inode
} {
this in Root implies {
no iname
no parent
} else {
one iname
one parent
this in parent.children
parent in Root iff this in TopLevelInode
}
}
fact InodeInv {

-- inode は自身を祖先に持たない
no iden & ^parent

-- 同じ親の下で同じ名前を持つ異なる inode はない
no disj i, i': Inode - Root | i.parent = i'.parent and i.iname = i'.iname

-- 親ノードはファイルにはならない
no Inode.parent & File

-- ディレクトリノードはディレクトリブロックを参照する
Directory.addresses.block in DirectoryBlock

-- ファイルノードはファイルブロックを参照する
File.addresses.block in FileBlock
}

sig File extends Inode {}
sig Directory extends Inode {}
one sig Root extends Directory {}
sig TopLevelInode in Inode {}
fun children (i: Inode): Inode {inodeTable[i.addresses.block.inumbers]}

sig Name {}
sig Address {block: disj Block}
abstract sig Block {}
sig FileBlock extends Block {}
sig DirectoryBlock extends Block {
inumbers: disj (set Inumber),
inodes: set Inode -- ビュワーで見やすくする為
} {inodes=inodeTable [inumbers]}


/**** Path Model ****/
abstract sig Path {
rest: lone Path,
index: Path -> Inode
}
fun parents (p: Path): Path {p.~rest}
fun ancestors (p: Path): Path {p.^~rest}

one sig EmptyPath extends Path {} {no rest}

abstract sig NonEmptyPath extends Path {
name: Name
} {
some rest

all p: Path, i: Inode | p -> i in index iff {
p in this + ancestors[this]
this = p implies i in TopLevelInode
else i in (this.parents.@index[p].children)
i.iname = name
}
}

fact PathInv {
no iden & ^rest
all path: NonEmptyPath | EmptyPath in path.^rest
}
fact CanonicalizePath {
all disj p, p': NonEmptyPath | p.name != p'.name or p.rest != p'.rest
}
fun last(path: Path): Path {
(path.*rest <: rest).EmptyPath
}
fun lookup (p: Path): Inode {
p=EmptyPath implies Root else last[p].index[p]
}

assert LookupAtMostOne {
all p: Path | lone lookup [p]
}
check LookupAtMostOne for 4 but 5 Path

assert LookupIsInjective {
all disj p, p': Path | let result = lookup [p] |
some result implies result != lookup [p']
}
check LookupIsInjective for 4

-- lookup デモ用
-- 実行方法
-- 1. Viewer -> Theme -> general graph setttings の Use original atom names: にチェックを付ける.
-- 2. Evaluator を開き lookup[NonEmptyPath$1] のように関数呼び出しを記述しリターン.
run {
Address in Inode.addresses
Block in Address.block

all i: Inode | some p: Path | lookup[p] = i
-- all p: Path | some i: Inode | lookup[p] = i

some f: File | #(f.^parent) = 3
} for 6 but exactly 6 Inode, 1 File, 7 Path
インスタンス・グラフ
Alloy 練習問題 A.5.1 解答例3インスタンス・グラフ
Themeファイル
<?xml version="1.0"?>

<alloy>
<view nodetheme="Martha" useOriginalAtomNames="yes">
<defaultnode/>
<defaultedge/>
<node>
<type name="DirectoryBlock"/>
<type name="EmptyPath"/>
<type name="File"/>
<type name="FileBlock"/>
<type name="Int"/>
<type name="NonEmptyPath"/>
<type name="String"/>
<type name="univ"/>
<type name="seq/Int"/>
<set name="$f" type="File"/>
</node>
<node color="Yellow">
<type name="Directory"/>
</node>
<node hideunconnected="yes" shape="Box" color="Blue">
<type name="Block"/>
</node>
<node shape="Ellipse" color="White">
<type name="Address"/>
</node>
<node shape="Hexagon" color="Gray">
<type name="Path"/>
</node>
<node shape="Trapezoid" color="Green">
<type name="Inode"/>
</node>
<node style="Bold" color="Red">
<type name="Root"/>
</node>
<node visible="no" hideunconnected="yes" color="Gray">
<type name="Inumber"/>
</node>
<node visible="no" shape="Hexagon" color="White">
<type name="Name"/>
</node>
<edge color="Blue">
<relation name="parent"> <type name="Inode"/> <type name="Inode"/> </relation>
</edge>
<edge color="Magic" style="Dotted">
<relation name="addresses"> <type name="Inode"/> <type name="Address"/> </relation>
</edge>
<edge visible="no">
<relation name="$p"> <type name="Inode"/> <type name="Path"/> </relation>
<relation name="index"> <type name="Path"/> <type name="Path"/> <type name="Inode"/> </relation>
</edge>
<edge visible="no" attribute="no">
<relation name="inumbers"> <type name="DirectoryBlock"/> <type name="Inumber"/> </relation>
</edge>
<edge visible="no" attribute="yes">
<relation name="iname"> <type name="Inode"/> <type name="Name"/> </relation>
<relation name="inodes"> <type name="DirectoryBlock"/> <type name="Inode"/> </relation>
<relation name="name"> <type name="NonEmptyPath"/> <type name="Name"/> </relation>
</edge>
</view>
</alloy>

[Alloy] 抽象によるソフトウェア設計 Alloyではじめる形式手法 練習問題 A.5.1 解答例2

 
A.5.1 Unix ファイルシステム 解答例2

解答例1
http://monado.dtiblog.com/blog-entry-147.html
解答例3
http://monado.dtiblog.com/blog-entry-149.html

変更点は、Inode シグネチャの path フィールドを削除し
lookup関数の呼び出しの都度、ファイル階層を検索するようにしたこと。
これにより、ファイルシステムのモデルとパスモデルがより疎結合になったが
よりわかりにくくなった。
module exercises/inode

open util/integer

/**** File System Model ****/
sig FileSystem {
inodeTable: Inumber lone -> lone Inode,
}
fun FileSystem.inodes: Inode {this.inodeTable[Inumber]}
fun FileSystem.directories: Directory {this.inodes & Directory}
fun FileSystem.addresses: Address {this.inodes.addresses}

sig Inumber {}
abstract sig Inode {
addresses: some Address,
depth: Int,
parent: lone Inode,
iname: Name
} {
this in Root implies {
depth = 0
no parent
iname = EmptyName
} else {
depth > 0
one parent
iname != EmptyName
}
}
sig File extends Inode {}
sig Directory extends Inode {}
sig Root extends Directory {}
fun Inode.blocks: Block {this.addresses.block}

sig Name {}
one sig EmptyName extends Name {}
sig Address {block: Block}
abstract sig Block {}
sig FileBlock extends Block {}
sig DirectoryBlock extends Block {
inumbers: set Inumber,
inodes: set Inode -- ビュワーで見やすくする為
}

pred FileSystemInv (sys: FileSystem) {

-- ルートディレクトリを唯一持つ
one sys.directories & Root

-- 異なるノードはアドレスを共有しない
all disj i, i': sys.inodes | no i.addresses & i'.addresses

-- 異なるアドレスは異なるブロックを指す
all disj a, a': sys.addresses | a.block != a'.block

-- 異なるディレクトリブロックは inumber を共有しない
all disj b, b': blocks[sys.inodes] | no b.inumbers & b'.inumbers

-- システムで参照されている inumber はいずれかのディレクトリブロックに含まれる
sys.inodeTable.(sys.inodes - Root) = sys.directories.blocks.inumbers

all d: sys.directories {
-- ディレクトリブロックの inumbers と inodes の同期
all b: d.blocks | b.inodes = sys.inodeTable [b.inumbers]

let children = sys.inodeTable [d.blocks.inumbers] |
all c: children | c.parent = d and c.depth = d.depth + 1
}

}

fact InodeInv {
-- inode は自身を祖先に持たない
no iden & ^parent

-- 同じ親の下で同じ名前を持つ異なる inode はない
no disj i, i': Inode - Root | i.parent = i'.parent and i.iname = i'.iname

-- 親ノードはファイルにはならない
no Inode.parent & File

-- ディレクトリノードはディレクトリブロックを参照する
Directory.addresses.block in DirectoryBlock

-- ファイルノードはファイルブロックを参照する
File.addresses.block in FileBlock

}

/**** Path Model ****/
abstract sig Path {
name: Name
} {this in EmptyPath iff name = EmptyName}
sig NonEmptyPath extends Path {
rest: Path
}
one sig EmptyPath extends Path {}

fact PathInv {
no iden & ^rest
all path: NonEmptyPath | EmptyPath in path.^rest
}
fact CanonicalizePath {
all disj p, p': NonEmptyPath | p.name != p'.name or p.rest != p'.rest
}
fun toArray(path: Path, indexOffset: Int): Int -> Name {
let paths = path.*rest - EmptyPath |
{idx: Int, n:Name, p: paths | idx = add [distance [path, p], indexOffset] and n = p.name}.univ
}
fun distance (from, to: Path): Int {
sub [#(from <: ^rest), #(to <: ^rest)]
}
fun FileSystem.lookup (p: Path): Inode {
let array = toArray [p, 1] + (0 -> EmptyName), lastIndex = #array - 1 {
{i: this.inodes | i.depth = lastIndex and array [lastIndex] = i.iname
and array = {idx: Int, n: Name, i': allParentsAndSelf [this, i] | idx = i'.depth and n = i'.iname}.univ
}
}
}
fun FileSystem.allParentsAndSelf(self: Inode): Inode {
{i: self.*(this.inodes <: parent)}
}

assert LookupAtMostOne {
all sys: FileSystem, p: Path | FileSystemInv [sys] implies lone sys.lookup [p]
}
check LookupAtMostOne for 4 but 5 int, 5 Path

assert LookupIsInjective {
all sys:FileSystem {
FileSystemInv [sys] implies {
all disj p, p': Path | let result = sys.lookup [p] |
some result implies result != sys.lookup [p']
}
}
}
check LookupIsInjective for 5 but 5 int, 6 Path

-- lookup デモ用
-- 実行方法
-- 1. Viewer -> Theme -> general graph setttings の Use original atom names: にチェックを付ける.
-- 2. Evaluator を開き FileSystem$0.lookup[NonEmptyPath$1] のように関数呼び出しを記述しリターン.
run {
Inode in FileSystem.inodes
Block in FileSystem.inodes.blocks
Address in FileSystem.inodes.addresses
all sys: FileSystem {
FileSystemInv [sys]
all i: Inode | some p: Path | sys.lookup [p] = i
}
no disj i,i': Inode | i.iname = i'.iname
some f: File | #(f.^parent) = 3
} for 4 but 4 int, 1 FileSystem, 1 File, 7 Path
インスタンス・グラフ
Alloy 練習問題 A.5.1 別解インスタンス・グラフ
Themeファイル
<?xml version="1.0"?>

<alloy>
<view nodetheme="Martha" useOriginalAtomNames="yes">
<defaultnode/>
<defaultedge/>
<node>
<type name="DirectoryBlock"/>
<type name="EmptyName"/>
<type name="EmptyPath"/>
<type name="File"/>
<type name="FileBlock"/>
<type name="Int"/>
<type name="NonEmptyPath"/>
<type name="String"/>
<type name="univ"/>
<type name="seq/Int"/>
<set name="$f" type="File"/>
</node>
<node color="Yellow">
<type name="Directory"/>
</node>
<node hideunconnected="yes" shape="Box" color="Blue">
<type name="Block"/>
</node>
<node hideunconnected="yes" shape="Trapezoid" color="Green">
<type name="Inode"/>
</node>
<node shape="Box" color="White">
<type name="FileSystem"/>
</node>
<node shape="Ellipse" color="White">
<type name="Address"/>
</node>
<node shape="Hexagon" color="Gray">
<type name="Path"/>
</node>
<node style="Bold" color="Red">
<type name="Root"/>
</node>
<node visible="no" hideunconnected="yes" color="Gray">
<type name="Inumber"/>
</node>
<node visible="no" shape="Hexagon" color="White">
<type name="Name"/>
</node>
<edge color="Blue">
<relation name="parent"> <type name="Inode"/> <type name="Inode"/> </relation>
</edge>
<edge color="Magic" style="Dotted">
<relation name="addresses"> <type name="Inode"/> <type name="Address"/> </relation>
</edge>
<edge visible="no">
<relation name="$p"> <type name="FileSystem"/> <type name="Inode"/> <type name="Path"/> </relation>
</edge>
<edge visible="no" attribute="no">
<relation name="inumbers"> <type name="DirectoryBlock"/> <type name="Inumber"/> </relation>
</edge>
<edge visible="no" attribute="yes">
<relation name="depth"> <type name="Inode"/> <type name="Int"/> </relation>
<relation name="iname"> <type name="Inode"/> <type name="Name"/> </relation>
<relation name="inodes"> <type name="DirectoryBlock"/> <type name="Inode"/> </relation>
<relation name="name"> <type name="Path"/> <type name="Name"/> </relation>
</edge>
</view>
</alloy>

[Alloy] 抽象によるソフトウェア設計 Alloyではじめる形式手法 練習問題 A.5.1 解答例1

 
A.5.1 Unix ファイルシステム 解答例1

解答例2
http://monado.dtiblog.com/blog-entry-148.html
解答例3
http://monado.dtiblog.com/blog-entry-149.html
module exercises/inode

open util/integer

/**** File System Model ****/
sig FileSystem {
inodeTable: Inumber lone -> lone Inode,
}
fun FileSystem.inodes: Inode {this.inodeTable[Inumber]}
fun FileSystem.directories: Directory {this.inodes & Directory}
fun FileSystem.addresses: Address {this.inodes.addresses}
fun FileSystem.lookup (p: Path): Inode {p.~(this.inodes <: path)}

sig Inumber {}
abstract sig Inode {
addresses: some Address,
iname: lone Name,
parent: lone Inode,
path: one Path
} {
this in Root implies {
no iname
no parent
path = EmptyPath
} else {
one iname
one parent
path != EmptyPath
}
}
sig File extends Inode {}
sig Directory extends Inode {}
sig Root extends Directory {}
fun Inode.blocks: Block {this.addresses.block}

sig Name {}
sig Address {block: Block}
abstract sig Block {}
sig FileBlock extends Block {}
sig DirectoryBlock extends Block {
inumbers: set Inumber,
inodes: set Inode -- ビュワーで見やすくする為
}

pred FileSystemInv (sys: FileSystem) {

-- ルートディレクトリを唯一持つ
one sys.directories & Root

-- 異なるノードはアドレスを共有しない
all disj i, i': sys.inodes | no i.addresses & i'.addresses

-- 異なるアドレスは異なるブロックを指す
all disj a, a': sys.addresses | a.block != a'.block

-- 異なるディレクトリブロックは inumber を共有しない
all disj b, b': blocks[sys.inodes] | no b.inumbers & b'.inumbers

-- システムで参照されている inumber はいずれかのディレクトリブロックに含まれる
sys.inodeTable.(sys.inodes - Root) = sys.directories.blocks.inumbers

all d: sys.directories {
-- ディレクトリブロックの inumbers と inodes の同期
all b: d.blocks | b.inodes = sys.inodeTable [b.inumbers]

let children = sys.inodeTable [d.blocks.inumbers] |
all c: children | c.parent = d
}

}

fact InodeInv {
-- inode は自身を祖先に持たない
no iden & ^parent

-- 同じ親の下で同じ名前を持つ異なる inode はない
no disj i, i': Inode - Root | i.parent = i'.parent and i.iname = i'.iname

-- 親ノードはファイルにはならない
no Inode.parent & File

-- ディレクトリノードはディレクトリブロックを参照する
Directory.addresses.block in DirectoryBlock

-- ファイルノードはファイルブロックを参照する
File.addresses.block in FileBlock

}

/**** Path Model ****/
abstract sig Path {}
sig NonEmptyPath extends Path {
name: Name,
rest: Path
}
one sig EmptyPath extends Path {}

fact PathInv {
no iden & ^rest
all path: NonEmptyPath | EmptyPath in path.^rest
}
fact CanonicalizePath {
no disj p, p': NonEmptyPath | toArray[p, 0] = toArray[p', 0]
}

fun length(path: Path): Int {
#(path.*rest - EmptyPath)
}
pred append (a, b, c: Path) {
let offset = length[a] |
toArray[c, 0] = toArray[a, 0] + toArray[b, offset]
}
fun toArray(path: Path, indexOffset: Int): Int -> Name {
let paths = path.*rest - EmptyPath |
{idx: Int, n:Name, p: paths | idx = add [distance [path, p], indexOffset] and n = p.name}.univ
}
fun distance (from, to: Path): Int {
sub [#(from <: ^rest), #(to <: ^rest)]
}

fact PathGenerator {
-- パスの生成
all i: Inode - Root |
some p: Path {
p.name = i.iname
p.rest = EmptyPath
append [i.parent.path, p, i.path]
}
}

assert LookupAtMostOne {
all sys: FileSystem, p: Path | FileSystemInv [sys] implies lone sys.lookup [p]
}
check LookupAtMostOne for 4 but 5 int, 5 Path

assert LookupIsInjective {
all sys:FileSystem {
FileSystemInv [sys] implies {
all disj p, p': Path | let result = sys.lookup [p] |
some result implies result != sys.lookup [p']
}
}
}
check LookupIsInjective for 5 but 5 int, 6 Path

-- lookup デモ用
-- 実行方法
-- 1. Viewer -> Theme -> general graph setttings の Use original atom names: にチェックを付ける.
-- 2. Evaluator を開き FileSystem$0.lookup[NonEmptyPath$1] のように関数呼び出しを記述しリターン.
run {
Inode in FileSystem.inodes
Block in FileSystem.inodes.blocks
Address in FileSystem.inodes.addresses
all sys: FileSystem | FileSystemInv [sys]
no disj i,i': Inode | i.iname = i'.iname
some f: File | #(f.^parent) = 3
} for 4 but 4 int, 1 FileSystem, 1 File, 7 Path
インスタンス・グラフ
Alloy 練習問題 A.5.1 インスタンス・グラフ
Themeファイル
<?xml version="1.0"?>

<alloy>
<view nodetheme="Martha" useOriginalAtomNames="yes">
<defaultnode/>
<defaultedge/>
<node>
<type name="DirectoryBlock"/>
<type name="EmptyPath"/>
<type name="File"/>
<type name="FileBlock"/>
<type name="Int"/>
<type name="NonEmptyPath"/>
<type name="String"/>
<type name="univ"/>
<type name="seq/Int"/>
<set name="$f" type="File"/>
</node>
<node color="Yellow">
<type name="Directory"/>
</node>
<node hideunconnected="yes" shape="Box" color="Blue">
<type name="Block"/>
</node>
<node hideunconnected="yes" shape="Trapezoid" color="Green">
<type name="Inode"/>
</node>
<node shape="Box" color="White">
<type name="FileSystem"/>
</node>
<node shape="Ellipse" color="White">
<type name="Address"/>
</node>
<node shape="Hexagon" color="Gray">
<type name="Path"/>
</node>
<node style="Bold" color="Red">
<type name="Root"/>
</node>
<node visible="no" hideunconnected="yes" color="Gray">
<type name="Inumber"/>
</node>
<node visible="no" shape="Hexagon" color="White">
<type name="Name"/>
</node>
<edge color="Blue">
<relation name="parent"> <type name="Inode"/> <type name="Inode"/> </relation>
</edge>
<edge color="Green">
<relation name="path"> <type name="Inode"/> <type name="Path"/> </relation>
</edge>
<edge color="Magic" style="Dotted">
<relation name="addresses"> <type name="Inode"/> <type name="Address"/> </relation>
</edge>
<edge visible="no">
<relation name="$p"> <type name="Inode"/> <type name="Path"/> </relation>
</edge>
<edge visible="no" attribute="no">
<relation name="inumbers"> <type name="DirectoryBlock"/> <type name="Inumber"/> </relation>
</edge>
<edge visible="no" attribute="yes">
<relation name="iname"> <type name="Inode"/> <type name="Name"/> </relation>
<relation name="inodes"> <type name="DirectoryBlock"/> <type name="Inode"/> </relation>
<relation name="name"> <type name="NonEmptyPath"/> <type name="Name"/> </relation>
</edge>
</view>
</alloy>

[Alloy] Alloy 4.1.10 シーケンス seq/Int MaxSeq

 
シーケンスの使用例
open util/sequniv  -- 省略可


sig E {}
one sig A {
s: seq E -- 予約語 seq でシーケンスを定義
} {
#s > 5 -- 要素数は 5 より多い
not s.hasDups -- 各要素は重複しない
}

run {} for 10 E, 7 seq -- シーケンスの要素数の上限を 7 と指定
実行例:
Executing "Run run$1 for 7 seq, 10 E"

Solver=sat4j Bitwidth=4 MaxSeq=7 SkolemDepth=2 Symmetry=20
1233 vars. 80 primary vars. 3589 clauses. 296ms.
. found. Predicate is consistent. 156ms.
Alloy Sequence
seq/Int について
seq/Int は シーケンスのインデックスの集合であり、Int の部分集合となっている。
0 以上 MaxSeq - 1 以下の正の整数(MaxSeq個)の要素を含む。
MaxSeq はスコープ指定 MaxSeq seq で指定する。
指定できる数値は

0 ≤ MaxSeq ≤ (2^(Bitwidth-1))-1

である。
one sig A {

Min: seq/Int,
Max: seq/Int
} {
all n: seq/Int | int Min =< int n
all n: seq/Int | int n =< int Max
}
run {} for 4 int, 7 seq
実行例:
Executing "Run run$1 for 4 int, 7 seq"

Solver=sat4j Bitwidth=4 MaxSeq=7 SkolemDepth=2 Symmetry=20
159 vars. 14 primary vars. 362 clauses. 212ms.
. found. Predicate is consistent. 60ms.

Alloy seq/Int
参考:
http://alloy.mit.edu/alloy4/xmlformat.html