alloy 入門ハンズオン

2019-02-20.als

abstract sig Object {}

sig File extends Object {}
sig Directory extends Object {
	children: set Object
}

// singleParent が欠けると => 複数の directory に属する file があらわれる
fact singleParent {
	all o : Object | lone children.o 
}

// acyclic が欠けると => 自分自身に属する directory が現れる
fact acyclic {
	all d, child : Directory |
		child in d.^children => child != d
}

// connected が欠けると => ツリーが2つ以上出現する
fact connected {
	all f : File | one children.f
	one d : Directory | no children.d 
}

// 空ディレクトリ
pred emptyDirectory {
	some d: Directory | no d.children
}
run emptyDirectory for 4

// 空でないディレクトリ
pred presentDirectory {
	some d: Directory | some d.children
}
run presentDirectory for 4

// 3 段以上の深いディレクトリ
pred manyNestedDirectory {
	some d: Directory | some d.children.children.^children
}
run manyNestedDirectory for 4

// 複数のファイルを含むディレクトリ
pred directoryWithMultipleFiles {
	some d: Directory | #d.children > 1
}
run directoryWithMultipleFiles for 4

// 親を持たないオブジェクトが常にちょうど 1 個だけ存在する
assert rootIsSingleton {
	one o : Object | no children.o 
}
check rootIsSingleton for 4