並行システムの検証と実装第1章状態遷移図によるプロセスのモデル化 PRINCIPIA Limited 初谷久史 ©2015 PRINCIPIA Limited 状態遷移図によるプロセスのモデル化 ● モデル化とシミュレーションひとめぐり ● Scheme 入門 ● チャネル通信 ● 状態変数 ● ガード ● プロセスの終了 ©2015 PRINCIPIA Limited 2 SyncStitch スクリーンショット ©2015 PRINCIPIA Limited 3 SyncStitch 起動とモデル作成 SyncStich アイコンを開く ©2015 PRINCIPIA Limited 右クリックでメニューを開き "New model" を選択 Process list ウィンドウが開く 4 イベントの定義 Definitions ウィンドウイベントや関数など，モデル全体で共有する定義を記述するウィンドウ ©2015 PRINCIPIA Limited 5 プロセスの作成（状態遷移図）クライアントエリアで右クリックメニューから "add diagram" を選択プロセス名を入力して Enter キーで確定状態遷移図で記述するプロセスが作成される ©2015 PRINCIPIA Limited 6 プロセスダイアグラムプロセスエントリ上で右クリックメニューから "edit" を選択するダイアグラムウィンドウ状態遷移図を作成・編集するウィンドウ ©2015 PRINCIPIA Limited 7 状態の作成 "state" ボタンを押してからマウスをドラッグする作成した状態図形のプロパティが Properties ウィンドウに表示される ©2015 PRINCIPIA Limited 8 状態名の指定 Propertiesウィンドウの "name" フィールドをクリックして，状態名を入力する状態図形に名前が表示される ©2015 PRINCIPIA Limited 9 遷移の作成 "Transition" ボタンを押してからマウスをドラッグする作成した遷移図形のプロパティが Properties ウィンドウに表示される ©2015 PRINCIPIA Limited 10 遷移図形の編集 Alt キーを押しながら遷移図形上をクリックすると，ハンドルを追加・削除できる遷移先に接続していない遷移図形を作ってから，端点を遷移元状態に接続すると，ループ状の遷移になる ©2015 PRINCIPIA Limited 11 イベントの指定 Properties ウィンドウの "event" フィールドをクリックして，イベント名を入力する遷移の近くにイベント名が表示される ©2015 PRINCIPIA Limited 12 練習以下のような状態遷移図を描いてください ©2015 PRINCIPIA Limited 13 状態のグローバル指定状態 P を図面の外から参照できるように "scope" を "Global" に設定する状態 Q, R の名前はこの状態遷移図にローカルなので，他の状態遷移図でも Q, R という名前を使うことができる ©2015 PRINCIPIA Limited 14 初期状態の指定 Process list ウィンドウでメニューから "property" を選ぶ初期状態として状態名を指定する ©2015 PRINCIPIA Limited 15 モデルの保存 Process list ウィンドウでメニューから "Save" を選ぶフォルダとファイル名を指定して "Save" するフォルダ部分は右ボタンドラッグでスクロールできる ©2015 PRINCIPIA Limited 16 モデルのコンパイル Process list ウィンドウで "Compile" ボタンを押す Status ウィンドウが開き進捗メッセージが表示される ©2015 PRINCIPIA Limited 17 コンパイルエラー Definitions ウィンドウなどで式にエラーがあるとBacktrace ウィンドウが開く状態遷移図にエラーがあると，ダイアグラムウィンドウとエラーウィンドウが開く ©2015 PRINCIPIA Limited 18 プロセスのシミュレーションプロセスエントリ上で右クリックメニューから "explore" を選択する Process Explorer ウィンドウと Transitions ウィンドウが開く選択されている状態から可能な遷移のリスト ©2015 PRINCIPIA Limited 初期状態 19 プロセスエクスプローラの操作既出の状態は太字で表示される遷移をチェックすると対応する遷移図形が表示される ©2015 PRINCIPIA Limited 遷移先図形を選択するとさらにそこからの遷移が表示される 20 プロセスエクスプローラの操作遷移をダブルクリックする対応する遷移が表示されさらに遷移先状態が選択状態となる ©2015 PRINCIPIA Limited 21 プロセスエクスプローラの操作状態図形にフォーカスがある状態で Ctrl+E を押すすべての遷移が表示される ©2015 PRINCIPIA Limited 22 状態遷移図と計算木ループがあるので繰り返し同じ状態が出現する Explorer は計算木を表示する ©2015 PRINCIPIA Limited 23 状態図形の色と意味非表示の遷移ありすべての遷移を表示計算木上で唯一の状態他にも現れている状態選択されている状態と同じ状態 ©2015 PRINCIPIA Limited 24 パス初期状態から選択されている状態までの遷移列を表示するダブルクリックで対応する遷移図形を選択できる ©2015 PRINCIPIA Limited 25 まとめ ● イベントを定義する ● 状態遷移図としてプロセスをモデル化する ● 計算木としてプロセスを確認する ©2015 PRINCIPIA Limited 26 Scheme 入門データ型 ● 整数 0 314 -271 ● シンボル X apple Z80 Runge-Kutta + ● リスト () (a b c) (0 1) (x . y) ● 真偽値 #f #t ● 関数 ©2015 PRINCIPIA Limited 28 リストペア: 対を作る (X . Y) X Y シンボル = (0 . (1 . (2 . ()))) (0 1 2) 空リスト 0 ©2015 PRINCIPIA Limited 1 2 29 リスト (0 (a b) 2) 0 2 a b R (0 1 2 . R) 0 ©2015 PRINCIPIA Limited 1 2 30 関数型プログラミング ● 関数を定義したり組み合わせたりしてプログラムを書く関数適用の記法例 (関数名引数0 引数1 引数2 ...) (+ 1 2 3) (+ (f x 2) 1) (map fn xlist) ©2015 PRINCIPIA Limited 31 式の評価 ● 式の値を計算することを「評価する」という (+ (* 2 3) 4) => 10 ©2015 PRINCIPIA Limited 評価する式評価結果の値 32 SyncStitch 上での式の評価 Definitions ウィンドウで式を書く式の後ろのカーソルを移動して Ctrl+E を押すと評価できるウィンドウが縦に分割されて下部に評価結果の値が表示される Escape キーを押すとウィンドウ分割が解除される ©2015 PRINCIPIA Limited 33 主な関数 (null? x) 空リスト述語 (car x) リストの先頭要素 (list? x) リスト述語 (cdr x) リストの先頭を除いたリスト (symbol? x) シンボル述語 (cons x y) リスト y の先頭に x を (integer? x) 整数述語 (equal? x y) 同値 (list x ...) (+ x y ...) 加算 (append x ...) リストの連結 (- x y) 減算 (length x) リストの長さ (* x y ...) 乗算 (member x y) x が y の要素かどうか (div x y) 除算 (remove x y) y から x を除いた残り (mod x y) 剰余 (interval a b) 整数区間 [a,b) (< x y) 大小判定 (map f x) (> x y) (<= x y) ©2015 PRINCIPIA Limited (>= x y) 加えたリスト x ... を要素とするリスト x の各要素に関数 f を適用した結果からなるリスト 34 変数の定義 ● 変数は define で定義する ● 式を評価した結果が変数の値となる define の書式例 (define 変数式) (define x 3) => ? ; 変数 x を定義，値は 3 ; define の評価結果は未定義（使用しない） x => 3 ; 変数 x を評価 (+ x 2) => 5 ; 変数の使用 ©2015 PRINCIPIA Limited 35 引用符 ● ● プログラム中に現れるシンボルは、変数または関数だと見なされる．リストは式だと見なされるシンボルやリストがデータであることを表すために引用符を使う ABC => error ; 変数とみなされる ; 未定義エラー 'ABC => ABC ; 引用符をつけてシンボルをデータとして使う ; ABC というシンボル (+ 1 2) => 3 ; リストは式とみなされる '(+ 1 2) => (+ 1 2) ; 引用符をつけるとデータとみなされる ©2015 PRINCIPIA Limited 36 map 関数 ● リストの各要素に関数を適用して，その結果をリストにまとめて返す関数書式 (map 関数リスト) (map car ’((A 0) (B 1 2) (C))) => (A B C) (map cdr ’((A 0) (B 1 2) (C))) => ((0) (1 2) ()) (map list ’(0 1 2)) => ((0) (1) (2)) ©2015 PRINCIPIA Limited 37 条件判定 ● 条件式を評価し，結果が偽 #f でなければ式0を評価して返す．結果が #f であれば式1を評価して返す書式 (if 条件式式0 式1) (if (member 1 '(0 1 2 3)) 'sync 'async) => sync ©2015 PRINCIPIA Limited 38 関数定義関数定義の書式 (define (関数名パラメータ...) 式) (define (f x) (+ x 3)) => ? ; 関数 f を定義 ; define の評価結果は未定義 (f 4) => 7 ; 関数 f を使用 (define (g x y) (* (f x) y)) => ? ; 関数 f を使って関数 g を定義 (g 2 3) => 15 ©2015 PRINCIPIA Limited 39 ローカル変数 let の書式 (let ((変数0 式0) (変数1 式1) ...) 式) (define x 3) => ? ; x はグローバル変数 x => 3 (let ((x -2)) (* x x)) => 4 ; ローカル変数 x を定義して使用 x => 3 ; グローバル変数の値は影響なし ©2015 PRINCIPIA Limited 40 多値 ● ● 関数は2個以上の値を返すことができる．これを多値という多値を返すには values を使用する values の書式 (values 0 17 'X) => 0 17 X ©2015 PRINCIPIA Limited (values 式0 式1 ...) ; 3つの値が返される 41 多値の受け取り ● 多値を受け取るには let-values を使用する let-values の書式 (let-values (((変数00 変数01 ...) 式0) (変数10 変数11 ...) 式1) ...) 式) (let-values (((x y) (values 0 1))) (list x y)) => (0 1) ©2015 PRINCIPIA Limited 42 Backtrace によるエラー分析 Ctrl+E で評価エラーが発生 ©2015 PRINCIPIA Limited この状態で Ctrl+B を押すと Backtrace が開く 43 Backtrace ウィンドウエラーメッセージ呼び出し履歴 ©2015 PRINCIPIA Limited 選択するとフレーム情報が右上に表示される 44 Inspector ウィンドウ右クリックメニューから "inspect" を選択 Inspector ウィンドウが開くオブジェクトの内部を調べることができる ©2015 PRINCIPIA Limited 45 練習: 評価してください (car ’(0 1 2)) => 0 (cdr ’(0 1 2)) => (1 2) (cons 0 ’(1 2)) => (0 1 2) (list 0 1 2) => (0 1 2) (append ’(0 1 2) ’(a b)) => (0 1 2 a b) (append ’() ’(x y)) => (x y) (length ’(a b c)) => 3 (length ’()) => 0 (length ’(a (x y z) ())) => 3 (member 4 ’(0 1 2 3)) => #f (member 2 ’(0 1 2 3)) => (2 3) (remove 2 ’(0 1 2 3)) => (0 1 3) (remove 4 ’(0 1 2 3)) => (0 1 2 3) (remove 2 ’(0 1 2 3 2 1)) => (0 1 3 1) ©2015 PRINCIPIA Limited 46 チャネル通信 ● チャネル定義 ● 送信 ● 受信 ● チャネルイベントチャネル定義 define-channel の書式 (define-channel チャネル名パラメータリスト定義域) 例 (define-channel ch (x) '((0) (1) (2))) (define-channel ch2 (x y) '((0 0) (0 1) (1 0))) 定義域は引数のリストのリストとして指定する ©2015 PRINCIPIA Limited 48 遷移の送信指定遷移の "type" で "send" を選択 ©2015 PRINCIPIA Limited 送信用のプロパティに切り替わる 49 チャネルの指定 "channel" フィールドにチャネル名 "ch" を指定する ©2015 PRINCIPIA Limited 50 チャネル引数の指定 "argument" フィールドをクリックすると Argument ウィンドウが開く遷移図形にチャネル名と送信値が表示される送信は ! で表される ©2015 PRINCIPIA Limited 51 チャネル送信プロセスの計算木 "ch.0" という名前のイベント ©2015 PRINCIPIA Limited 52 チャネル受信 "type" に "receive" を指定受信は ? で表される受信した値を受け取るパラメータ名を指定 ©2015 PRINCIPIA Limited 53 チャネル受信プロセスの計算木 3つのイベントから選択する形チャネル受信は選択の省略記法 ©2015 PRINCIPIA Limited 54 チャネルイベントチャネルはイベントの集合とみなすことができる (define-channel ch (x) '((0) (1) (2))) ≈ { ch.0, ch.1, ch.2 } これは表示のみこれをチャネルイベントというチャネルイベントを作成するには関数 $ を使用する $ の書式例 ©2015 PRINCIPIA Limited ($ チャネル引数 ...) ($ ch 0) 55 チャネルイベントによる遷移 "type" は "event" として "event" フィールドにチャネルイベント ($ ch 0) を指定する計算木は送信と同じになる ©2015 PRINCIPIA Limited 56 チャネルイベントによる受信各チャネル引数ごとに遷移と遷移先状態を用意する計算木は受信と同じになる ©2015 PRINCIPIA Limited 57 チャネル通信まとめ ● define-channel でチャネルを定義する ● チャネル送受信の遷移 – 遷移のプロパティで send または receive を指定する – チャネルを指定する – 送信の場合は引数，受信の場合はパラメータを指定する ● チャネル受信はイベント選択の省略記法 ● チャネルイベントは関数 $ で作ることができる ©2015 PRINCIPIA Limited 58 状態変数 ● 状態変数 ● 遷移関数 ● target 式 ● アトミック状態 ● 状態の展開 ● Environment ウィンドウ状態変数 ● 状態は変数をもつことができる ● 変数を使う目的 – 対象とする問題領域に含まれる数値やデータ構造を表すため – チャネルを通して受信した値を保持するため – 類似の状態をグループ化して 1 つにまとめるため ©2015 PRINCIPIA Limited 60 状態変数複数の状態を1つにまとめたもの (P 0) (P x) (P 1) 状態変数 (P 2) 状態変数の変域 x ∈ { 0, 1, 2, 3, ... } ©2015 PRINCIPIA Limited 61 遷移関数遷移元状態遷移先状態 ch?u (Q z) (P x y) z = f (x, y; u) 状態変数遷移先状態の状態変数の値を，遷移元状態の状態変数の値およびチャネルから受信した値（受信の場合）より計算する関数を遷移関数と呼ぶ（ここだけの用語） ©2015 PRINCIPIA Limited 62 状態変数の指定状態図形の "state variable" プロパティに状態変数名をスペースで区切って指定する ©2015 PRINCIPIA Limited 63 遷移関数の指定: 多値 x: 不変 y: 受信値 "transformation" をクリックすると Transformation ウィンドウが開く．ここに遷移関数を記述する ©2015 PRINCIPIA Limited 遷移先状態 Q は2つの状態変数 x, y を持つのでそれぞれの値を多値で指定する 64 遷移関数の指定: target 式同じ変数名は無指定なら不変変化する変数だけを指定する target の書式 (target 変数指定式 ...) 変数指定 = ":" + 変数名 ©2015 PRINCIPIA Limited 65 遷移関数の指定: 暗黙指定同じ変数名は無指定なら不変チャネル引数において状態変数を参照できる ©2015 PRINCIPIA Limited 66 初期状態の指定初期状態が状態変数をもつ場合は状態変数の初期値を指定する ©2015 PRINCIPIA Limited 67 状態変数をもつプロセスの計算木アトミック状態に分解することを展開する（unfold）というアトミック状態受信値を保存 ©2015 PRINCIPIA Limited 68 状態変数をもつプロセスの計算木 ©2015 PRINCIPIA Limited 69 Environment ウィンドウ状態変数の値を確認することができる Inspector を開いて，さらに詳細に調べることができる ©2015 PRINCIPIA Limited 70 状態変数まとめ ● 状態は状態変数を持つことができる ● 変数を使う目的 – 対象とする問題領域に含まれる数値やデータ構造を表すため – チャネルを通して受信した値を保持するため – 類似の状態をグループ化して 1 つにまとめるため ● 状態変数の値は遷移関数によって決定される ● 状態変数に具体的な値を入れた状態をアトミック状態という ● ● 状態変数を持つ状態をアトミック状態に分解することを展開するという Environment ウィンドウで状態変数の値を確認できる ©2015 PRINCIPIA Limited 71 ガード ● ガード ● 例: スタックのモデル ● 受信ガードガード ● 遷移元状態の状態変数からなる条件 ● 条件が成立するときだけ遷移が可能遷移元状態ガード遷移先状態 e [g(x, y)] (P x y) ©2015 PRINCIPIA Limited (Q z) 73 例: スタックのモデルチャネル定義 in (define-channel in (x) '((0) (1) (2))) (define-channel out (x) '((0) (1) (2))) out 状態変数 s: リストでスタックを表す ©2015 PRINCIPIA Limited 74 例: スタックのモデル空ではない (not (null? s)) (< (length s) 3) ©2015 PRINCIPIA Limited フルではない 75 例: スタックのモデル追加するとき x: 1 s: (2 1 0 1) (cons x s) s: (1 2 1 0 1) 遷移後 ©2015 PRINCIPIA Limited 取り出すとき s: (1 2 1 0 1) (car s) x: 1 送信値 (cdr s) s: (2 1 0 1) 遷移後 76 例: スタックのモデル初期状態は空（s = 空リスト） ©2015 PRINCIPIA Limited 77 スタックモデルの計算木空のときは出力がないフルのときは入力がない ©2015 PRINCIPIA Limited 78 受信ガード ● チャネル受信でのみ利用できるガード ● 受信しようとしている値を参照できる遷移元状態受信ガード遷移先状態 ch?u [rg(x, y; u)] (P x y) ©2015 PRINCIPIA Limited (Q z) 79 例: 受信ガードのモデルチャネル定義 (define-channel c (x) '((0) (1))) (define-channel d (x y) '((0 0) (0 1) (1 0) (1 1))) ©2015 PRINCIPIA Limited 80 例: 受信ガードのモデル状態変数 x だけでなく受信パラメータ u, v も参照している (= x u v) ©2015 PRINCIPIA Limited 81 受信ガードモデルの計算木ガードがない場合 ©2015 PRINCIPIA Limited 82 遷移タイプとプロパティのまとめガードイベント同期 (P x y) e [g(x, y)] / z = f(x, y) 遷移関数 (Q z) 送信値チャネル送信 (P x y) ch!v(x, y) [g(x, y)] / z = f(x, y) (Q z) 受信ガードチャネル受信 (P x y) ©2015 PRINCIPIA Limited ch?u [rg(x, y; u)][g(x, y)] / z = f(x, y; u) 状態変数 (Q z) 83 プロセスの終了 ● 終了イベント tick ● 終了状態 SKIP ● 終了後の状態 OMEGA プロセスの終了 ● ● ● ● プロセスは自ら終了することができる終了したプロセスはいかなるイベントも発生しないプロセスが終了することを他のプロセスは止めることはできない終了と停止（デッドロック）は異なる ©2015 PRINCIPIA Limited 85 終了状態 SKIP ©2015 PRINCIPIA Limited 86 終了イベント tick と終了後の状態 OMEGA 終了イベント tick 終了後の状態 OMEGA 点線は自発的な遷移を意味する ©2015 PRINCIPIA Limited 87