日常業務で何をやっていたのかは逐一メモしているわけですが、 それを集計するというのはよくやるわけです。 というわけでそんなプログラム。 # 09:00 12:00 Hoge メール対応 # 12:00 13:00 社内 休憩 # 13:00 16:00 Fuga 訪問 # # という形式のファイルを元…

グループ内(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,…

深さ優先探索で、橋渡し問題を解く。 ; 各stateは'n か's(対岸)のどちらか) (defstruct state :farmer :wolf :goat :cabbage) (defn opposite [x] (if (= x 'n) 's 'n)) (defn expand [st] (let [f (:farmer st) w (:wolf st) g (:goat st) c (:cabbage st)]…

何度見ても美しいと思うSchemeの課題をClojureで。 (defn third [x] (first (next (next x)))) (defn constant? [exp] (cond (contains? #{'+ '- '* '/ '**} exp) false (coll? exp) false :else true)) (defn diff [e x] (cond (constant? e) (if (= e x) 1…

こういう数独を解きます。 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…

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

CommonLispのatomに対抗してatom?を作る。 user> (defn atom? [x] (cond (not (seq? x)) true (empty? x) true :else false)) #'user/atom? user> (atom? 'sss) true user> (atom? (cons '1 '())) false user> (atom? nil) true user> (atom? '()) true user…

うーむ、CommonLispではさくっと動くものがClojureだと動かない・・・ user> (defn count-anywhere [item tree] "count the times item appears anywhere within tree." (cond (= item tree) 1 (not (seq? tree)) 0 :else (+ (count-anywhere item (first tr…

関数型でやるとこんな感じ？ (defn insert [sorted-coll val] (concat (filter #(> val %) sorted-coll) [val] (filter #(<= val %) sorted-coll))) (defn insertion-sort [coll] (loop [vals (rest coll) sorted-coll (list (first coll))] (if (empty? val…

状態遷移を表現するように変更。 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) }*/ …

早いもので、もう第6回FormalMethods勉強会のお知らせです。 http://atnd.org/events/4750 今回はマイスペース「大久保店」です。会場間違えないようにご注意ください。CoqはcpdtのChapter4からですかね。 Alloyは7月の無料セミナー直前対策です。 第5回で、…

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 …

やったー！VBAとおさらばだー。 user=> (import '(org.apache.poi.hssf.usermodel HSSFSheet HSSFWorkbook HSSFRow HSSFCell)) org.apache.poi.hssf.usermodel.HSSFCell user=> (def wb (new HSSFWorkbook)) #'user/wb user=> (import '(java.io FileOutputS…

最初に見つけた要素だけ置き換えたいんです。 (use '[clojure.contrib.seq-utils]) ;(defn- position-sub [x coll i] ; (if (= (first coll) x) i ; (position-sub x (rest coll) (inc i)))) ; ;(defn position [x coll] ; (position-sub x coll 0)) ; ;別バ…

Clojureハッカソンで教えていただいたこと、その１。leiningen:Clojure版MAVENみたいなもの。 http://github.com/technomancy/leiningenWindows版は自動インストールできないので、 以下のファイルを用意する。 leiningen-1.1.0-standalone.jar lein.bat(Git…

CommonLispにもML系Matchがないのか。 (in-package "ACL2") (defun not-3 (x) (cond ((equal x "yes") "no") ((equal x "no") "yes") ((equal x "maybe") "maybe"))) (defun and-3 (x y) (cond ((and (equal x "yes") (equal y "yes")) "yes") ((and (equal …

某ProofCafeではCoqでやってみたという話の、 リストの反転問題。 reverse (reverse xs) = xs http://study-func-prog.blogspot.com/2010/04/coq-reverse-reverse-xs-xs.htmlACL2ではどうなんのかな、と思ってやってみた。 環境はACL2s。 (in-package "ACL2"…

clojure.contrib.typesの使い方がいまいち分からない。 もうちょっと賢いマッチングしてくれないのかな。 (use '[clojure.contrib.types]) (defn not-3 [x] (match [x] [:yes] :no [:no] :yes [:maybe] :maybe)) (defn and-3 [x y] (match [x y] [:yes :yes]…

http://norvig.com/paip/README.html勉強ネタ。