Mercurial > hg > Members > atton > seminar_slides
annotate slides/20151215/slide.md @ 119:9f874edd19a4
Add slide for seminar
author | Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp> |
---|---|
date | Tue, 15 Dec 2015 18:35:10 +0900 |
parents | |
children |
rev | line source |
---|---|
119
9f874edd19a4
Add slide for seminar
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
diff
changeset
|
1 title: Verification of programs using Code Segments and Data Segments |
9f874edd19a4
Add slide for seminar
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
diff
changeset
|
2 author: Yasutaka Higa |
9f874edd19a4
Add slide for seminar
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
diff
changeset
|
3 profile: |
9f874edd19a4
Add slide for seminar
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
diff
changeset
|
4 lang: Japanese |
9f874edd19a4
Add slide for seminar
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
diff
changeset
|
5 |
9f874edd19a4
Add slide for seminar
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
diff
changeset
|
6 |
9f874edd19a4
Add slide for seminar
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
diff
changeset
|
7 # 研究目的 |
9f874edd19a4
Add slide for seminar
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
diff
changeset
|
8 * コードセグメントとデータセグメントという単位を用いてプログラムを記述する手法を提案する |
9f874edd19a4
Add slide for seminar
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
diff
changeset
|
9 * プログラムはコードセグメントという処理の集合として表され、相互に接続される |
9f874edd19a4
Add slide for seminar
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
diff
changeset
|
10 * 個々のコードセグメントを検証し、検証されたコードセグメントどうしの組み合わせによりプログラム全体を検証する |
9f874edd19a4
Add slide for seminar
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
diff
changeset
|
11 |
9f874edd19a4
Add slide for seminar
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
diff
changeset
|
12 # 研究内容 |
9f874edd19a4
Add slide for seminar
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
diff
changeset
|
13 * コードセグメントとデータセグメントを用いたプログラムに対し、自動で検証する機構を提案する |
9f874edd19a4
Add slide for seminar
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
diff
changeset
|
14 * 検証機構には可能な状態を列挙できるモデルチェッカーや、型システムを用いた証明を用いる |
9f874edd19a4
Add slide for seminar
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
diff
changeset
|
15 * 検証をメタ計算として定義し、通常のプログラムから検証を含んだプログラムを導出する |
9f874edd19a4
Add slide for seminar
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
diff
changeset
|
16 * メタ計算の形式化には Monad を用い、通常の計算とメタ計算間の一対一対応を保証する |
9f874edd19a4
Add slide for seminar
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
diff
changeset
|
17 |
9f874edd19a4
Add slide for seminar
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
diff
changeset
|
18 # 近況報告 |
9f874edd19a4
Add slide for seminar
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
diff
changeset
|
19 * Overview: Principles of Model Checker(1-8) |
9f874edd19a4
Add slide for seminar
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
diff
changeset
|
20 * Liner Temporal Logic |
9f874edd19a4
Add slide for seminar
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
diff
changeset
|
21 * Computation Tree Logic |
9f874edd19a4
Add slide for seminar
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
diff
changeset
|
22 |
9f874edd19a4
Add slide for seminar
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
diff
changeset
|
23 # Overview: Principles of Model Checker |
9f874edd19a4
Add slide for seminar
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
diff
changeset
|
24 * 1: System Verification |
9f874edd19a4
Add slide for seminar
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
diff
changeset
|
25 * 2: Modeling Concurrent Systems |
9f874edd19a4
Add slide for seminar
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
diff
changeset
|
26 * 3: Liner-Time Properties |
9f874edd19a4
Add slide for seminar
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
diff
changeset
|
27 * 4: Regular Properties |
9f874edd19a4
Add slide for seminar
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
diff
changeset
|
28 * 5: Liner Temporal Logic |
9f874edd19a4
Add slide for seminar
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
diff
changeset
|
29 * 6: Computation Tree Logic |
9f874edd19a4
Add slide for seminar
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
diff
changeset
|
30 * 7: Equivalences and Abstraction |
9f874edd19a4
Add slide for seminar
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
diff
changeset
|
31 * 8: Partial Order Reduction |
9f874edd19a4
Add slide for seminar
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
diff
changeset
|
32 |
9f874edd19a4
Add slide for seminar
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
diff
changeset
|
33 # 1: System Verification |
9f874edd19a4
Add slide for seminar
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
diff
changeset
|
34 * そもそもシステムを検証するとは何なのか的なお話 |
9f874edd19a4
Add slide for seminar
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
diff
changeset
|
35 * Hardware/Software Verification Verification |
9f874edd19a4
Add slide for seminar
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
diff
changeset
|
36 * 仕様を命題として記述してシステムのモデルが命題を満たすかチェック |
9f874edd19a4
Add slide for seminar
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
diff
changeset
|
37 * 満たす/満たさない |
9f874edd19a4
Add slide for seminar
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
diff
changeset
|
38 * 満たさないなら反例を提出 |
9f874edd19a4
Add slide for seminar
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
diff
changeset
|
39 |
9f874edd19a4
Add slide for seminar
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
diff
changeset
|
40 # 2: Modeling Concurrent Systems |
9f874edd19a4
Add slide for seminar
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
diff
changeset
|
41 * System は Transition System として表わされる |
9f874edd19a4
Add slide for seminar
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
diff
changeset
|
42 * TS = (S, Act, ->, I, AP, L) |
9f874edd19a4
Add slide for seminar
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
diff
changeset
|
43 * S is Set of States |
9f874edd19a4
Add slide for seminar
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
diff
changeset
|
44 * Act is Set of Actions |
9f874edd19a4
Add slide for seminar
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
diff
changeset
|
45 * -> is transition relation ( S x Act x S ) |
9f874edd19a4
Add slide for seminar
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
diff
changeset
|
46 * AP is set of atomic proposition |
9f874edd19a4
Add slide for seminar
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
diff
changeset
|
47 * L is labeling function (S -> 2^{AP}) |
9f874edd19a4
Add slide for seminar
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
diff
changeset
|
48 |
9f874edd19a4
Add slide for seminar
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
diff
changeset
|
49 # Figure: Transition System |
9f874edd19a4
Add slide for seminar
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
diff
changeset
|
50 * Vending Machine |
9f874edd19a4
Add slide for seminar
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
diff
changeset
|
51 ![TS](http://i.stack.imgur.com/bgJM8.png) |
9f874edd19a4
Add slide for seminar
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
diff
changeset
|
52 |
9f874edd19a4
Add slide for seminar
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
diff
changeset
|
53 # 2: Modeling Concurrent Systems |
9f874edd19a4
Add slide for seminar
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
diff
changeset
|
54 * Concurrent System は transition system の相互接続として表現 |
9f874edd19a4
Add slide for seminar
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
diff
changeset
|
55 * Shared Variable や Channel によって接続される |
9f874edd19a4
Add slide for seminar
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
diff
changeset
|
56 * Channel は容量の上限が決まった Message Queue |
9f874edd19a4
Add slide for seminar
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
diff
changeset
|
57 * Spin とかは Channel Connected Process として System を表現 |
9f874edd19a4
Add slide for seminar
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
diff
changeset
|
58 * Promela (Process Meta Language) を使って書く |
9f874edd19a4
Add slide for seminar
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
diff
changeset
|
59 |
9f874edd19a4
Add slide for seminar
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
diff
changeset
|
60 # 3: Liner-Time Properties |
9f874edd19a4
Add slide for seminar
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
diff
changeset
|
61 * 満たすべき命題をどうやって判断するか |
9f874edd19a4
Add slide for seminar
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
diff
changeset
|
62 * TS の遷移の path ら命題が満たされるか判断できる |
9f874edd19a4
Add slide for seminar
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
diff
changeset
|
63 * 例えば無限に動くシステムでも、命題を満たさない path-prefix があればダメ |
9f874edd19a4
Add slide for seminar
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
diff
changeset
|
64 |
9f874edd19a4
Add slide for seminar
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
diff
changeset
|
65 # 4: Regular Properties |
9f874edd19a4
Add slide for seminar
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
diff
changeset
|
66 * 具体的にどのように検証するか |
9f874edd19a4
Add slide for seminar
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
diff
changeset
|
67 * Automaton に変換してしまえば良い |
9f874edd19a4
Add slide for seminar
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
diff
changeset
|
68 * Nondeterministic Finite Automaton とか |
9f874edd19a4
Add slide for seminar
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
diff
changeset
|
69 * ω-Regular Language |
9f874edd19a4
Add slide for seminar
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
diff
changeset
|
70 |
9f874edd19a4
Add slide for seminar
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
diff
changeset
|
71 # 5: Liner Temporal Logic |
9f874edd19a4
Add slide for seminar
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
diff
changeset
|
72 * 命題をどのように記述するか |
9f874edd19a4
Add slide for seminar
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
diff
changeset
|
73 * Liner Temporal Logic |
9f874edd19a4
Add slide for seminar
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
diff
changeset
|
74 * ``φ ::= true | a | φ1 ∩ φ2 | ¬ φ | ○φ | φ1 U φ2`` |
9f874edd19a4
Add slide for seminar
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
diff
changeset
|
75 * ○は next |
9f874edd19a4
Add slide for seminar
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
diff
changeset
|
76 * U は until。 right-operand を満たすまで left-operand は true である |
9f874edd19a4
Add slide for seminar
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
diff
changeset
|
77 |
9f874edd19a4
Add slide for seminar
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
diff
changeset
|
78 # 5: Liner Temporal Logic |
9f874edd19a4
Add slide for seminar
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
diff
changeset
|
79 * 信号は赤になる時がある |
9f874edd19a4
Add slide for seminar
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
diff
changeset
|
80 * eventually ◇ == true U φ |
9f874edd19a4
Add slide for seminar
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
diff
changeset
|
81 * eventually red |
9f874edd19a4
Add slide for seminar
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
diff
changeset
|
82 * true U red |
9f874edd19a4
Add slide for seminar
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
diff
changeset
|
83 * 信号は赤か青か黄色である |
9f874edd19a4
Add slide for seminar
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
diff
changeset
|
84 * always □ == not eventually not φ |
9f874edd19a4
Add slide for seminar
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
diff
changeset
|
85 * always (red or green or yellow) |
9f874edd19a4
Add slide for seminar
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
diff
changeset
|
86 * not (eventually (not (red or green or yellow))) |
9f874edd19a4
Add slide for seminar
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
diff
changeset
|
87 |
9f874edd19a4
Add slide for seminar
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
diff
changeset
|
88 # 5: Liner Temporal Logic |
9f874edd19a4
Add slide for seminar
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
diff
changeset
|
89 * 検証は automaton とセットで。 |
9f874edd19a4
Add slide for seminar
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
diff
changeset
|
90 * 無限に生成される言語の受理状態をチェックできるω-Automaton もある |
9f874edd19a4
Add slide for seminar
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
diff
changeset
|
91 * NBA (Nondeterministic Buchi Automata) を使って infinite transition system の検証も |
9f874edd19a4
Add slide for seminar
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
diff
changeset
|
92 |
9f874edd19a4
Add slide for seminar
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
diff
changeset
|
93 # 6: Computation Tree Logic |
9f874edd19a4
Add slide for seminar
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
diff
changeset
|
94 * 命題の別の記述方法 |
9f874edd19a4
Add slide for seminar
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
diff
changeset
|
95 * transition を tree にしてチェック |
9f874edd19a4
Add slide for seminar
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
diff
changeset
|
96 * `` state formula : Φ ::= true | Φ1 ∧ Φ2 | ¬Φ | ∃φ | ∀φ `` |
9f874edd19a4
Add slide for seminar
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
diff
changeset
|
97 * `` path formula : φ ::= ○Φ | Φ1 U Φ2 `` |
9f874edd19a4
Add slide for seminar
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
diff
changeset
|
98 * eventually/always もあります |
9f874edd19a4
Add slide for seminar
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
diff
changeset
|
99 |
9f874edd19a4
Add slide for seminar
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
diff
changeset
|
100 # 7: Equivalences and Abstraction |
9f874edd19a4
Add slide for seminar
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
diff
changeset
|
101 * Equivalences な TS を検証することでサイズを小さくしよう |
9f874edd19a4
Add slide for seminar
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
diff
changeset
|
102 * Bisimulation とか |
9f874edd19a4
Add slide for seminar
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
diff
changeset
|
103 * 一部置き換えたシステムとかもあるみたいです |
9f874edd19a4
Add slide for seminar
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
diff
changeset
|
104 |
9f874edd19a4
Add slide for seminar
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
diff
changeset
|
105 # 8: Partial Order Reduction |
9f874edd19a4
Add slide for seminar
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
diff
changeset
|
106 * 並列に実行した再に順番が変わっても大丈夫なやつをまとめてサイズを小さくしよう |
9f874edd19a4
Add slide for seminar
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
diff
changeset
|
107 * Ample Set とか |
9f874edd19a4
Add slide for seminar
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
diff
changeset
|
108 * この辺から最適化っぽかったのでとりあえず一旦読むのを中断 |
9f874edd19a4
Add slide for seminar
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
diff
changeset
|
109 |
9f874edd19a4
Add slide for seminar
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
diff
changeset
|
110 # 現状検証するべき condition |
9f874edd19a4
Add slide for seminar
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
diff
changeset
|
111 * おそらく一番安直には |
9f874edd19a4
Add slide for seminar
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
diff
changeset
|
112 * always balanced |
9f874edd19a4
Add slide for seminar
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
diff
changeset
|
113 * insertion/deletion 途中は回転とかするはずなので |
9f874edd19a4
Add slide for seminar
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
diff
changeset
|
114 * always (balancing or balanced) |
9f874edd19a4
Add slide for seminar
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
diff
changeset
|
115 * これで必要十分? |
9f874edd19a4
Add slide for seminar
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
diff
changeset
|
116 |
9f874edd19a4
Add slide for seminar
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
diff
changeset
|
117 # 命題の記述に何を採用するか |
9f874edd19a4
Add slide for seminar
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
diff
changeset
|
118 * CTL のが簡単そうなのでまずはこれでやろうかと |
9f874edd19a4
Add slide for seminar
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
diff
changeset
|
119 * bounded になるはず |
9f874edd19a4
Add slide for seminar
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
diff
changeset
|
120 * insertion/deletion の operation 列が有限 |
9f874edd19a4
Add slide for seminar
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
diff
changeset
|
121 |
9f874edd19a4
Add slide for seminar
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
diff
changeset
|
122 # CbC をどうやって Transition System に変更にするか |
9f874edd19a4
Add slide for seminar
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
diff
changeset
|
123 * goto を transition にすれば簡単 |
9f874edd19a4
Add slide for seminar
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
diff
changeset
|
124 * next は次の state |
9f874edd19a4
Add slide for seminar
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
diff
changeset
|
125 * conditional な Transition System をどうするか |
9f874edd19a4
Add slide for seminar
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
diff
changeset
|
126 * condition を覚えておいて SAT する |
9f874edd19a4
Add slide for seminar
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
diff
changeset
|
127 * でいけそうな気はしてます |
9f874edd19a4
Add slide for seminar
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
diff
changeset
|
128 |
9f874edd19a4
Add slide for seminar
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
diff
changeset
|
129 # 課題 |
9f874edd19a4
Add slide for seminar
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
diff
changeset
|
130 * このやり方だとメタ計算でやるよりも CbC を直接パースした方が簡単そう |
9f874edd19a4
Add slide for seminar
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
diff
changeset
|
131 * SAT が必要なので condition 覚えるのと SAT の実装が |
9f874edd19a4
Add slide for seminar
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
diff
changeset
|
132 |
9f874edd19a4
Add slide for seminar
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
diff
changeset
|
133 |
9f874edd19a4
Add slide for seminar
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
diff
changeset
|
134 <!-- vim: set filetype=markdown.slide: --> |