P25の「代数的な性質の検査」の4条件のうち、2と4はandじゃなくてimpliesになるのでは。 module Queue abstract sig Node { next : lone Node } abstract sig Queue { root : lone Node } fact noCycle { no n : Node | n in n.^next } fact noReflexive { n…

http://topse.or.jp/2012/12/1678サンプルファイル群はこちら。 https://github.com/kencoba/alloy-introduction

AwodeyのP33にProjective Objectのお話が載っているのですが。Alloyで書くとこういうことなのかな。 https://gist.github.com/967745たけをさんから以下のような例をいただいた。 open util/relation sig P { f : one X } sig E { e : one X } sig X {} fun …

http://alloy.mit.edu/alloy4/ いくつか修正が入ったようだ。

http://kokucheese.com/event/index/6887/ご参加いただいた方、ありがとうございました。質問の多さからも、システム開発を真面目に考えている人が 集まった印象を強く受けました。今後も継続努力していきます。

a-sanさんの日記より、 http://d.hatena.ne.jp/a-san/20090626/p2Alloyだとこれだけなのか？ /* http://d.hatena.ne.jp/a-san/20090626/p2 */ abstract sig State { transient:set State } one sig O,A,B,C,D,E,F,G,H,I extends State {} fact { transient =…

BirthdayBookという仕様がある。 http://spivey.oriel.ox.ac.uk/~mike/zrm/これをAlloyで書いてみた。 open util/relation sig NAME {} sig DATE {} sig BirthdayBook { known: NAME, birthday : NAME -> lone DATE } { known = dom[birthday] } pred AddBir…

連載：モデリング技術の新しい動向 第3回 形式手法とモデリング - Alloy Analyzerを中心にという記事が掲載された。 http://thinkit.co.jp/story/2010/09/22/1766今回はFormal Methods Forumのみなさんの力を借りられなかったのが心残り。最低限の査読は入っ…

Alloy Analyzerはアジャイルモデリングをサポートできるツールだと 思っているわけですが、現時点では識別子に日本語が使えません。 このままだと分析モデリングに使えない(と、会社の人が文句を言ってきた)。コードを調べてみたら何のことはなかったので、…

http://alloy.mit.edu/community/node/506 に、LaTeXでAlloyのリストを表示するサンプルがあったので試す。 \documentclass{jarticle} \usepackage{amsmath} \usepackage{listings,jlisting} \lstdefinelanguage{Alloy} {morekeywords={abstract, all, and, …

7/12 名古屋市工業研究所にて、無事実施できました。ここまでいろいろとネタ提供、成果物レビューしてくれたみなさん、ありがとうございました。 当日会場でサポートしてくれたyoshihiro503さん、ありがとうございました。使用した資料はこちらにあります。 …

頑張って計算はしているようだが、 数分では結果がかえってこない・・・。 /* sudoku solver */ sig Cell { x:Int, y:Int, v:Int } { x >= 0 and x <= 8 y >= 0 and y <= 8 v >= 1 and v <= 9 } fact AllCellsPosition { no disj c1,c2:Cell | c1.x == c2.x …

グループ内(2*2,3*3などの正方マス)には同一数字は入らない、 というルールを付け加えて、前回のものと速度を比較した。 sig Cell { x:Int, y:Int, v:Int } { x >= 0 and x <= 3 y >= 0 and y <= 3 v >= 1 and v <= 4 } fact AllCellsPosition { no disj c1,…

こういう数独を解きます。 http://d.hatena.ne.jp/ku-ma-me/20080108 0, 0, 0, 4 0, 0, 1, 2 0, 1, 4, 3 4, 3, 2, 1sig Cell { x:Int, y:Int, v:Int } { x >= 0 and x <= 3 y >= 0 and y <= 3 v >= 1 and v <= 4 } fact AllCellsPosition { no disj c1,c2:Ce…

状態遷移のチェックだってできるぜ。 といいたいところだが、まぁ簡単に図を書くくらいならLTSAと同じだなぁ、 というところをやってみる。 /* LTSAのマネ.Thread Life Cycle THREAD = CREATED, CREATED = (start -> RUNNABLE |stop -> TERMINATED), RUNNING…

第6回Formal Methods 勉強会で出た、RBACのモデルのお話。 こんな感じかな。 /* Role Based Access Control ロールに階層関係を追加 */ /* ユーザアカウント */ sig User { roles: set Role } /* ロール。Admin,Guestなど */ sig Role { perms: set Permissi…

"Interface" Jan.2010 「外部センサのデータにより、モータの回転を自律制御するアルゴリズムを考えよう！（間瀬順一、吉村悠）」より。 さっと作ると、かなり落とし穴のある制御のモデルになってしまった。 上手いこと制御のアルゴリズムを考えて私に教えて…

sig Name { address: set Addr } sig Addr {} pred All [] { all n:Name | one n.address } pred Some [] { some n:Name | one n.address } pred No [] { no n:Name | one n.address } pred Lone [] { lone n:Name | one n.address } pred One [] { one n:Na…

sig Book { name:set Name } sig Name { addr:set Addr, mainaddress: one Addr } sig Addr {} fun Arrow []: set Name -> Addr { Name -> Addr } fun Dot [] : set Name { Book.(Book->Name) } fun Box [] : set Addr { (Name->Addr)[Name] } fun Transpose…

/* Name = {(G0),(A0),(A1)} Alias = {(A0),(A1)} Group = {(G0)} RecentlyUsed = {(G0),(A1)} */ abstract sig Name {} sig Alias extends Name {} sig Group extends Name {} sig RecentlyUsed in Name {} fun Union []:set Name { Alias + Group } fun In…

某社のコース申込システムをモデリング。 /* 豆蔵トレーニングコース申込システム 豆蔵のトレーニングコースの概要は以下の通り。 このシステムにおいて、コースへの申込が会場の定員数を超えないように管理したい。 [コース] コースにはセットコース、単体…

状態遷移を表現するように変更。 open util/ordering[State] as so /* 4日で学ぶモデル検査 システムα 仕様： 変数a 0->1 1->2 2->0と繰り返して変化する。 ただしb=1のときは次の時点でもその値を保ち変化しない。 初期状態は0とする。 変数b 0->1 1->2 2->…

「4日で学ぶモデル検査」より。 愚直にモデリングしてるだけで、これではスイッチがOn,Offされることを 確認できない・・・ open util/ordering[State] as so /* 4日で学ぶモデル検査 システムα */ abstract sig Switch {} one sig On,Off extends Switch {}…

Alloyの~演算の結果確認。 arityが3だとエラーになる。 sig Mail { to:one Name } sig Name { address: one Addr } sig Addr {} fun transpose1 []:set univ -> univ { ~to } /* fun transpose2 []:set univ -> univ -> univ { ~(Mail -> Name -> Addr) }*/ …

Alloyの:>, sig Group {} sig Alias {} sig Addr {} fun address [] : set univ -> univ { Group -> Alias + Group -> Group + Alias -> Addr } fun domain_restriction []: set univ -> univ { address :> Alias } fun range_restriction []: set univ -> u…

Alloyの.(ドット)演算。 sig Mail { to:one Name } sig Name { address: one Addr } sig Addr {} fun dot_join []:set univ -> univ { to.address } pred show [] { } run show for 4

Alloyのarrow(product)演算のサンプル。funで定義すると何がおこっているかよく分かる。 sig Name {} sig Addr {} fun arrow []:set univ->univ { Name -> Addr } pred show [] { #Name = 2 #Addr = 2 } run show for 5

Alloyのデフォルトで用意されている集合、none(空集合)、univ(全体集合)、iden(Identity集合)を確認。 pred empty_set [] { #none > 0 } //run empty_set for 4 sig Unit {} sig Value {} pred univ_set [] { some u:Unit | u not in univ some v:Value | v …

私も最初、訳がわからなかった。 UMLにはこれの直接表現がないし。 /* * Example : extends vs in * *author: Kenichi Kobayashi */ abstract sig Human {} sig Man,Woman extends Human {} abstract sig Employee {} sig Sales,Engineer in Employee{} /* …

「ソフトウェア科学基礎」http://books.livedoor.com/item/2024302 の練習問題1.9より。 宝石の入ったつづらを当てる問題。Alloyで。/* 「ソフトウェア科学基礎」練習問題1.9 pred showの中で、honesty,liarを変更し、 どちらであっても宝石(Jewel)と繋がる…