---
# System prepended metadata

title: Model Cheking 3

---

# Model Cheking 3

去年の資料
https://ryutaro-kodama.github.io/slides/semi/journal_club/ModelChecking_ch3/

## 目的
* システム(プログラム)の正しさを検証するために
    * 正しさ=システムが持つべき特徴(specification)の定式化
    * システム(プログラム)のmodel化

3章はmodel化について

----

## モデルを作る際のポイント

* 適切に抽象化する
    * **特徴(specification)に影響を与える部分の**モデルは正確である(現実のシステムをよく表している)べき
    * 与えない部分は抽象化する
        * 例 デジタル回路のmodel化: 電圧ではなく、その解釈のbool値を考える
        * 例 communication protocolのmodel化: 暗号化やネットワーク上でのバイナリ列は考えず、protocol階層でのメッセージを考える。
    * 「無かったことにする」のではなく、summary（入力と出力の関係）を考える
* 内部状態を考える
    * プログラムを想定すると、入力には多くのパターンがある
        * そのため、単にinput-outputに応じたモデルを構築するのは困難
            * $\{f(00)=1,f(10)=2,f(30)=3,\dots\}$
    * 状態(state)と、状態遷移(transition)を考えることで解決

----

## Transition System

### Transition System

transition system $T = (S,S_0, R)$
* $S$: 状態の集合(断りが無い限りは有限集合)
* $S_0$: 初期状態の集合 ($S_0 \subseteq S$)
* $R$: 状態遷移 ($R \subseteq S\times S$, left total)
    * $s$から$s'$に遷移するとき、$(s,s') \in R$であり、$R(s,s')$とかく。
    * left total: 全ての$s$についてその遷移先がある $\forall s \in S, \exists s' \in S, R(s,s')$

----

### 例1

* $S = \{s_0,s_1,s_2\}$:
* $S_0 = \{s_0\}$:
* $R = \{(s_0,s_1), (s_1,s_0), (s_2,s_1)\}$
```graphviz
digraph def_graph {
// the first layer
start [shape = none, label = ""];
S0 [label = "S0"];

S1 [label = "S1"];
S2 [label = "S2"];

start -> S0
S0 -> {S1}
S1 -> {S0}
S2 -> {S1}
}
```

----

### 例2

* $S = \{s_0,s_1,s_2\}$:
* $S_0 = \{s_0\}$:
* $R = \{(s_0,s_1), (s_1,s_2), (s_2,s_1)\}$

Q. 遷移はどうなる？
```graphviz
digraph def_graph {
// the first layer
S0 [label = "S0"];

S1 [label = "S1"];
S2 [label = "S2"];
}
```


<details>
<summary>答え</summary>


```graphviz
digraph def_graph {
// the first layer
start [shape = none, label = ""];
S0 [label = "S0"];

S1 [label = "S1"];
S2 [label = "S2"];

start -> S0
S0 -> {S1}
S1 -> {S2}
S2 -> {S1}
}
```

</details>

----

### path

finite path(有限パス)
* $p=s_0,s_1,\dots,s_n$ ($R(s_i,s_{i+1})$)

infinite path(無限パス)
* $p=s_0,s_1,\dots$ ($R(s_i,s_{i+1})$)

----

## Kripke structure

各状態にlabelをつけたTransition System

### Kripke structure

Kripke structure $M = (S,S_0, R, AP, L)$
* $S,S_0,R$はTransition Systemと同じ
    * $S$: 状態の集合(断りが無い限りは有限集合)
    * $S_0$: 初期状態の集合 ($S_0 \subseteq S$)
    * $R$: 状態遷移 ($R \subseteq S\times S$, left total)
* $AP$: atomic propositionの全体集合
* $L$: ある状態でtrueなatomic propositionの集合を得る関数 ($S \to 2^{AP}$)

### atomic proposition と state label

stateの持つ性質の一つ一つを、atomic proposition(原子命題)、又は、labelという。
> We refer to these labels as atomic propositions

例:
* p: 変数aが0に等しい
* q: 変数bが1に等しい

$L$の例:
$L = \{s_0 \mapsto \{p\}, s_1 \mapsto \{p,q\}\}$

----

### 例1

* $S = \{s_0,s_1,s_2\}$:
* $S_0 = \{s_0\}$:
* $R = \{(s_0,s_1), (s_1,s_0), (s_2,s_1)\}$
* $AP = \{p,q\}$
* $L = \{s_0 \mapsto \{p\}, s_1 \mapsto \{p,q\}, s_2 \mapsto \emptyset\}$
```graphviz
digraph def_graph {
// the first layer
start [shape = none, label = ""];
S0 [label = "S0\np"];

S1 [label = "S1\np,q"];
S2 [label = "S2\n∅"];

start -> S0
S0 -> {S1}
S1 -> {S0}
S2 -> {S1}
}
```

----

### 例2

* $S = \{s_0,s_1,s_2\}$:
* $S_0 = \{s_0\}$:
* $R = \{(s_0,s_1), (s_1,s_2), (s_2,s_1)\}$
* $AP = \{p,q\}$
* $L = \{s_0 \mapsto \{p\}, s_1 \mapsto \emptyset, s_2 \mapsto \{p,q\}\}$

Q. labelはどうな
```graphviz
digraph def_graph {
// the first layer
start [shape = none, label = ""];
S0 [label = "S0"];

S1 [label = "S1"];
S2 [label = "S2"];

start -> S0
S0 -> {S1}
S1 -> {S0}
S2 -> {S1}
}
```

<details>
<summary>答え</summary>


```graphviz
digraph def_graph {
// the first layer
start [shape = none, label = ""];
S0 [label = "S0\np"];

S1 [label = "S1\n∅"];
S2 [label = "S2\np,q"];

start -> S0
S0 -> {S1}
S1 -> {S0}
S2 -> {S1}
}
```

</details>

----

### ※補足

文脈によってkripke structureが表すmodelが異なる
* model checkingの文脈: 解析対象のシステムのmodel
* 論理学の文脈: 仕様のmodel


---

## Nondeterminism (非決定性)

ある状態に対し、2つ以上の遷移可能な次状態が存在すること。
初期状態が2つ以上ある場合を含む。
外界からの入力を扱ったり、乱数をあつかったりする場合におこる。

----

### 例: 電気のスイッチ

* 0: 電気が消えている
* 1: 電気がついている
* p: ボタンが押されている
* r: ボタンが押されていない
* 非決定性
    * 初期状態: ボタンを押しているか・押していないかは分からない
    * 状態遷移: ボタンをそのままにするか・しないかはわからない

![](https://hackmd.io/_uploads/By2ph8fYn.png)

<!--
```graphviz
digraph def_graph {
// the first layer
start0 [shape = none, label = ""];
start1 [shape = none, label = ""];
S0 [label = "0,p"];
S1 [label = "0,r"];

S2 [label = "1,r"];
S3 [label = "1,p"];

start0 -> S0
start1 -> S1
S0 -> {S0,S1}
S1 -> {S1,S2}
S2 -> {S2,S3}
S3 -> {S0,S3}
}
```
-->

---

## state の表現
### informal 一階述語論理(first-order logic)

個体の量化のみを許す(述語論理上の関数の量化はない)述語論理。
プログラムを考えると、変数が量化できるので殆どの state を表現することができる。
今回使うのは$\wedge,\vee,\neg,\implies,\forall,\exists$

今後の状態遷移を考える上で、 state が一階述語論理で表現されているとすると嬉しい。
(本質的な問題ではない)

### first-order logic で state 集合を表現

元々の state (valuation): $V \to D$
$V$: 変数集合
$D$: 変数の定義域
変数とその値のマッピング。

ある一階述語論理の式には、その式が true となる全ての state 集合が対応する。
state 集合 $A$ について、$A$に対応する式が$\varphi$であるとき、
$(s \in A) \iff (s \models \varphi)$

#### 例1

$V = \{v_1, v_2, v_3\}$
元々の state (valuation) 集合の書き方
$$
\begin{aligned}
\{<v_1 \mapsto 1, v_2 \mapsto 2, v_3 \mapsto 5>\}
\end{aligned}
$$
first-order logic を使った state の書き方
$$
\begin{aligned}
(v_1 = 1) \wedge (v_2 = 2) \wedge (v_3 = 5)
\end{aligned}
$$


#### 例2

$V = \{v_1, v_2, v_3\}$

元々の state の書き方
$$
\begin{aligned}
\{&<v_1 \mapsto 1, v_2 \mapsto 2, v_3 \mapsto 5>,\\
&<v_1 \mapsto 1, v_2 \mapsto 2, v_3 \mapsto 6>,\\
&<v_1 \mapsto 1, v_2 \mapsto 2, v_3 \mapsto 7>\}
\end{aligned}
$$
first-order logicを使ったstateの書き方
$$
\begin{aligned}
(&((v_1 = 1) \wedge (v_2 = 2) \wedge (v_3 = 5)) \vee\\
&((v_1 = 1) \wedge (v_2 = 2) \wedge (v_3 = 6)) \vee\\
&((v_1 = 1) \wedge (v_2 = 2) \wedge (v_3 = 7)) )
\end{aligned}
$$

### first-order formula を使うメリット1: 式の単純化

一階述語論理のまま、式を単純にできることがある。
$$
\begin{aligned}
&((v_1 = 1) \wedge (v_2 = 2) \wedge (v_3 \geq 5) \wedge (v_3 \leq 7))
\end{aligned}
$$

### first-order formula を使うメリット2: 集合演算が一階述語論理に閉じている

* $A,B$: 状態集合
* $\varphi_A,\varphi_B$: 対応する一階述語論理
    * $(s \in A) \iff (s \models \varphi_A)$
    * $(s \in B) \iff (s \models \varphi_B)$

|集合演算|論理式演算|補足|
|-|-|-|
|$A \cup B$|$\varphi_A \vee\varphi_B$|$(s \in A\cup B) \iff (s \models \varphi_A\vee\varphi_B)$|
|$A \cap B$|$\varphi_A \wedge\varphi_B$|$(s \in A\cap B) \iff (s \models \varphi_A\wedge\varphi_B)$|
|$S \setminus A$|$\neg\varphi_A$|$(s \in S \setminus A) \iff (s \models \neg\varphi_A)$|
|$A \subseteq B$|$\varphi_A \implies \varphi_B$|$(A \subseteq B) \\\iff (\forall s\in S, s \in A \implies s \in B) \\\iff (\forall s\in S, s \models \varphi_A \implies s \models \varphi_B)$|


---

## transition の表現

### first-order logic で transition を表現

遷移前の変数と、遷移後の変数を区別する必要がある。
遷移後の変数集合を$V'$と書く。各変数についても同様。
* $V = \{v_1,v_2\}$であれば、$V' = \{v'_1,v'_2\}$

以下のように transition の 論理式表現$\mathcal{R}$を定義
$$
R(s,s') \iff (s,s' \models \mathcal{R}) \iff ((\varphi_{\{s\}} \wedge \varphi'_{\{s'\}}) \implies \mathcal{R})
$$

### イメージ例

$\mathcal{R} := (v'_1 = v_1) \wedge (v'_2 = v_2 + 1)$

のとき、例えば
$s \in (v_1 = 1 \wedge v_2 = 1 \wedge v_3 = 0), s' \in (v'_1 = 1 \wedge v'_2 = 2)$は$R(s,s')$

※この$\mathcal{R}$だと、状態数有限かつleft totalにならない。実際はもっと複雑な式が必要。

---

## Kripke 構造の一階述語論理表現

Kripke 構造 $M = (S,\mathcal{S}_0, \mathcal{R}, AP, L)$
* $S$: stateの集合
    * すなわち、Vの各変数とその値のマッピング、の集合
* $\mathcal{S}_0$: 初期状態の集合を表す論理式
    * $S_0$: 初期状態の集合 $S_0 \subseteq S$について、$\forall s, (s_0 \in S_0) \iff (s_0 \models \mathcal{S}_0)$
* $\mathcal{R}$: 状態遷移を表す論理式
    * $R$: 状態遷移 ($R \subseteq S\times S$, left total)について、$R(s,s') \iff (s,s' \models \mathcal{R})$
* $AP$: atomic propositionの全体集合
* $L$: ある状態でtrueなatomic propositionの集合を得る関数 ($S \to 2^{AP}$)

### 例

* $D$(変数の定義域)$= \{0,1\}$
* $V=\{x,y\}$
* $S = \{(0,0),(0,1),(1,0),(1,1)\}$※(x,y)の形式でstateを表現
* $\mathcal{S}_0 = (x=1 \wedge y=1)$
* $\mathcal{R}((x,y),(x',y')) = (x' = (x+y)\text{mod} 2 \wedge y'=y)$



```graphviz
digraph def_graph {
// the first layer
start0 [shape = none, label = ""];
S0 [label = "0,0"];
S1 [label = "0,1"];

S2 [label = "1,0"];
S3 [label = "1,1"];

start0 -> S1
S0 -> {S0}
S1 -> {S3}
S2 -> {S2}
S3 -> {S1}
}
```

### Boolean Encoding

$D$(変数の定義域)$= \{0,1\}$のとき、$v$を論理式上のbool変数とすることで
* $v=0$を$\neg v$
* $v=1$を$v$

と略記したような結果が得られる。


* $D$(変数の定義域)$= \{0,1\}$
* $V=\{x,y\}$
* $S = \{(0,0),(0,1),(1,0),(1,1)\}$※(x,y)の形式でstateを表現
* $\mathcal{S}_0 = (x=0 \wedge y=0)$
$$
\begin{aligned}
\mathcal{R}((x,y),(x',y')) &= (\neg x \wedge \neg y \wedge x' \wedge \neg y')\\
&\vee (x \wedge \neg y \wedge y')&\text{※辺を二本纏めて表現}\\
&\vee (\neg x \wedge y \wedge \neg x' \wedge \neg y')\\
&\vee (x \wedge y \wedge x' \wedge y')\\
\end{aligned}
$$


```graphviz
digraph def_graph {
// the first layer
start0 [shape = none, label = ""];
S0 [label = "0,0"];
S1 [label = "1,0"];
S2 [label = "0,1"];
S3 [label = "1,1"];

start0 -> S0
S0 -> {S1}
S1 -> {S2,S3}
S2 -> {S0}
S3 -> {S3}
}
```

## 例: Modeling Digital Circuits

論理回路のモデリング

### Synchronous circuits

同期回路
register が0/1の値を持っている。
クロックに従い、各レジスタが同時に更新される。

#### 例 mod8 カウンタ
$V = \{v_0,v_1,v_2\}$
![](https://hackmd.io/_uploads/HykazGtt2.png)

$\mathcal{R}$を算出してみる。
それぞれの変数の変化に注目すると、
$$
\begin{aligned}
\mathcal{R}_0 &:= (v'_0 \iff \neg v_0)\\
\mathcal{R}_1 &:= (v'_1 \iff v_0 \text{ xor } v_1)\\
\mathcal{R}_2 &:= (v'_2 \iff (v_0 \wedge v_1) \text{ xor } v_2)\\
\end{aligned}
$$
これらを纏めた結果が$\mathcal{R}$になる。
$\mathcal{R} = \mathcal{R}_0 \wedge \mathcal{R}_1 \wedge\mathcal{R}_2 \\\quad= (v'_0 \iff \neg v_0) \wedge(v'_1 \iff v_0 \text{ xor } v_1)\wedge(v'_2 \iff (v_0 \wedge v_1) \text{ xor } v_2)$


#### $\mathcal{R}$ の一般的な構築

n レジスタのデジタル回路のモデル化
各変数について、その変化を表す関数が回路から作れる。
$$
\mathcal{R}_i := \begin{cases}
true \quad\text{ 値が入力によって決まる場合}\\
(v'_i \iff f_i(V))  \quad\text{otherwize}
\end{cases}
$$
これらの$\wedge$をとれば遷移が得られる
$$
\mathcal{R} := \bigwedge_i \mathcal{R}_i
$$

### Asynchronous Circuits

非同期回路
wire が0/1の値を持っている。
各導線上を流れる電流が、非同期に更新される。

同期回路では同時に更新が行われたが、非同期回路では同時ではない更新=一つだけが更新されることが繰り返される、と捉えることが出来る。
$$
\mathcal{R} := \bigwedge_i \mathcal{R}_i\\
\mathcal{R}_i := \begin{cases}
true \quad\text{ 値が入力によって決まる場合}\\
(v'_i \iff f_i(V))\wedge\bigwedge_{j\neq i} (v'_j\iff v_j)  \quad\text{otherwize}
\end{cases}
$$

$\bigwedge_{j\neq i} (v'_j\iff v_j)$で、他の変数が同時に更新されない(interleaving semantics)を表現している。
非同期回路に限って言えばinterleaving semanticsでなくても良いはずだが、今後の議論を簡単にするため？


### 例題

$V = \{v_0,v_1\}$
$v_0' = v_0\text{ xor }v_1, v_1' = v_0\text{ xor }v_1$
$S_0 = (v_0 \wedge v_1)$

同期の場合の遷移
```graphviz
digraph def_graph {
// the first layer
start0 [shape = none, label = ""];
S0 [label = "0,0"];
S1 [label = "1,0"];
S2 [label = "0,1"];
S3 [label = "1,1"];

start0 -> S3
S0 -> {S0}
S1 -> {S3}
S2 -> {S3}
S3 -> {S0}
}
```


非同期の場合
```graphviz
digraph def_graph {
// the first layer
start0 [shape = none, label = ""];
S0 [label = "0,0"];
S1 [label = "1,0"];
S2 [label = "0,1"];
S3 [label = "1,1"];

start0 -> S3
S0 -> {S0}
S1 -> {S1,S3}
S2 -> {S2,S3}
S3 -> {S1,S2}
}
```

* Q. 非同期の場合で、$v_0,v_1$の順番で更新された後の状態は？
  ::: spoiler 答え
  (0,1)
  :::
* Q. 非同期の場合で、$v_1,v_0$の順番で更新された後の状態は？？
  ::: spoiler 答え
  (1,0)
  :::
* Q. 非同期の場合で、$v_0,v_0$の順番で更新された後の状態は？？
  ::: spoiler 答え
  (1,1)
  :::

理論上、特定の変数が長期間変更されないことがある。
そのような場合を除くため、公平性 (Fairness) 制約を考えることがある。(4章)

## sequantial program の model化

sequantial program $P$を入力として、論理式$\mathcal{R}$を得るアルゴリズム。

### $P$の書式

```
var ::= "x" | "y" | ...
exp ::= "0" | "1" | ... | exp + exp | ...
statement ::=  var ":=" exp | "skip" | "wait" | "lock" | "unlock" | ...
program ::= statement |
            program ";" program |
            "if" exp "then" program "else" program "end if" |
            "while" exp "do" program "end while"
```

**program:**

![program](data:image/png;base64,iVBORw0KGgoAAAANSUhEUgAAAk8AAACpCAYAAAAyRdnYAAAAIGNIUk0AAHomAACAhAAA%2BgAAAIDoAAB1MAAA6mAAADqYAAAXcJy6UTwAAAAEZ0FNQQAAsY58%2B1GTAAAAAXNSR0IArs4c6QAAAAZiS0dEAP8A%2FwD%2FoL2nkwAAAAlwSFlzAAAOxAAADsQBlSsOGwAAIABJREFUeNrtnQlcFVX%2Fxp97ueyb7AgoGCgCprKoaIJLbqm5pLwuuZSZ2atmpmVZ77%2B0ejWXFtNKX8NsMdTMNDPN3JJUFFREQRABUZFFFgFZL%2Ff%2BzzkIgimLXrgLv6%2Bf8d7LzJyZOeeZ33nmnDMzAEEQBEEQBNFgJLpwEP5eUFJRNg1RcbqhEYIgCIJQFTJdOZDIo6FUmiomIGgaZQJBEARB3IOUsoCoC96qRy17BEEQBEHmiSAIgiAIgswTQRAEQRAEmSeCIAiCIAgyTwRBEARBEGSeCIIgCIIgyDwRBEEQBEEQZJ4IgiAIgiDIPBEEQRAEQTSLeerRCQ51LVTffF0gIioBFxOuN3j58OOxSEpJ17jjuJycjmMRF0nZBEEQBKFiP1O1vjBP5RVI8%2FfC1gclWt98XeCHLUdw6GhMg5f%2F36b9OH4qXuOO4%2B8Tcfj6uz%2FpDCEIgiAIFfmZ7l4Y7e%2BNq%2FIKJPPf4t12kkoTFVJRwWZ6YYdMD3MiziOjaqX65msT0edT8ONPfyEntxAuTjaYGBKMktJyxMZfQ1Z2PoqLS9G2jR3GjuyF78IO43T0ZdzKL4Jzaxu8MGUA3NraI%2BrMZSSlZGD%2FwWhkZOShg4cThg%2FphttFpdiw6Q9EnkmErY0Fpk8dCJ%2BObcV2N35%2FAN3822PXnpOIi7%2BKIQP9MGpYIDM6%2BxFxKgHeHdtgwSujYGigL5bPyMxjBu0PxMSmwpOlP3PaEDi1toZcrsDqr37F0091xzebD%2BBKahZLpwfGjuoljunPw9G4cjULH6%2FZCZm%2BHl55aTidLQRBEATxEH6Gm6YKCVZXKOFS80VltcY8KSvNFE%2F02v2cWX3zNZ3radmY8MIq%2BHdxx%2FgxQbC0MMFfxy7A1MRQTPx3G2db2NlYiuUzb95Cj4AOeGHyAOjpSTBm8keQM9tqZmYEYyMDWLUyFcvbWJtDoVDi2ekfIzunAHOYYeHrjXt%2BpTBBnFBmnqbPXoNWlqYY0LcLlizbgsGj30NBQTFGMvOz988zWL%2FxD7FsXt5tjJzwXzjYtcL82SPFOv96boUwThWKCqxixmjW%2FHXMVDmjb1AnLHz3W5yNSYY%2BU4GVlZnYN75f3PARBEEQBFGb%2BvxMVUtTBfAzuHG6B1k9iQpnVt98bWmJSkxKh6GBDIOf9IUFM0r9gx%2Bvnufaxg5enm0QMvqJ6r9x41JQWIzLbD1ueDZuPojr6dnwbO%2BM1o5WCPDzqF7%2BSPgFlJSUYcnbEysz3r89Dh45h%2F2HozHpX33E31Z9%2BDyeCPQS348ej0WXTu2Y0RomfnPTFXU2UXwP%2B%2Fkoenb3xIvPDapO6%2BdfTyCaGaROPpUtWWEbF8CaGSXOob9icCY6CV0fbyeMYWFhSa3jIAiCIAiifr8jk%2BB3ObDk3pamBpmnKhTAWSkwRFnPfLkcyWyjxpqeST17eKKzjxu69p4HH%2B%2B2CO7lLbrDzM3%2BuesVFQosfHcTDjJj0qWTm2j94fDWn%2FuRcDlNDNYOfPKNWn%2BvMkscqVRS%2Fd2MbVMiufvb3MyoOu2ExDTsO3j2H2mVlJbdTavmuubGkFcomjTvWPkq6TQjCIIgdBHuZ1itOkyuxFj2qaivwruveWIrHmMrXmefA1iCG9jnvLrm68vwUVXLUwigl9IBrhVSeLMF%2B7NlJrBlz8uUmHXyIhLUWbEbsB3d9NVc0ZUWdfYyvgzdK76v%2FOD5SgeqvJvMgSPnxODr8H1LYWJsKP72%2B%2F7TtR1rja2amRqha%2Bd22LbpjYc7iBpmiKcVMrIXFi%2Ba8I%2FFSsvK77Oq5J79Ur3PiYqDhE4vgiAIQlPp3hEd5BKsZZVVJ1YL%2FsicwUE9BWLdEnBlG1BxP79Q08%2Bwz3VG%2BggtKcc0KTBdKcGt%2B3XZ%2FcM8VSWirEwkQl8PXtwUsY3Nq2t%2BzTTEDiYgiX3l024PD7xlqY%2FXKyQ44euNkDOxOKCujI2JvQJ9mQwdOzhj6CB%2FMeibDwjnWFqYIjHpRvWyZcyk6OnpQSbTE795t1xxjZYfPj6KtzRV0S%2BoE%2F7vw804%2BNc59A%2FuLP526fINyOVy0R3YGIYM8MOLc9diwthgsa%2BcE5EJeMzVAZaWJnWuy7sjU1IzRcuZnh49xosgCILQfZi%2FeLJCiW3Mp3x8qxzDExNRWjXv1P3aK%2Br2M6%2F16ISPyiuw8EEmqqZ52laXKWrA%2FPty5wA%2B8Osouvi2MWcY2FQtUPVRVFyKl175RBgMPqha3B33%2BSwxb%2FzY3mJQdo8nX4c3MzvrPvs3Qr87AN%2BgeeIOOD4AXCbVq05r0ri%2BmDLzU%2Fz%2BR5QYk7R6%2BYtsnZfxxv9tqm4J4i1AX33ycqP3s1ePjlgwexSembwMrcxNxH5aW5vhx6%2Fn17vuk8y4rf5qNwL6zIeeTIrIw6vorCIIgiB0Ft7ixI0Tq3KnnL6I3Q1YpV4%2Fc%2BdvDzRRopb390IRS%2BQrlshH90ukvvkNhaXzDvsIjorDIFVmHG%2BGizwa2uDlr13PFuOP%2BK3%2FNSkvkyM9Kw9OjtbVrTZ8WRMTw%2BrB2TXhXWiZWbfEIw9qdp2l3ciBgaEMttYWj3RcvPUoLT0HlsxAccPXGPh%2Bc8NV1eX4MAQETav%2BTt12BEEQhCbCPAC%2FVf0vVk990IBlH8rP8LvxuIliFeFMth0T0fIk00O7uhKpb35DMS%2FGygJjzPL1QZczFxCtrox2cb7%2FLfz6BjJxi39DluXwFql7l%2Bfca8oeFm7g7pf%2BoxwjQRAEQegK3E9AgceZvxjRkOUf1s%2FUbIniv6U1%2FljfSo%2FM4RSUQILNUgXGUJETBEEQBPEoCD%2FBfIXwFw03QQ9N1frNP6JYiYNKoCcVOUEQBEEQj2YpmJ9gvqLZTVtzb7BCiQsSoAMVOUEQBEEQjwL3E9xX6Lx5Mi4UTV52VOQEQRAEQTwidnd8hW6bp%2BPXRL%2BkEZU3QRAEQRCPiNEdX6Hb5gmii5JueycIgiAI4pGR3PEVOm%2BeCIIgCIIgtBYyTwRBEARBEGSeCIIgCIIgyDwRBEEQBEGoHZmuHEjN97ARBEEQBEE0FTrR8sRfWksvriUIgiAIgswTQRAEQRCEhiHTpYOh1ieCIAiCIJoaankiCIIgCIIg80QQBEEQBEHmiSAIgiAIgswTQRAEQRAEmSeCIAiCIAgyTwRBEARBEASZJ4IgCIIgCDJPBEEQBEEQTYNOPCTT3wtKKsqG0dQPElVGztD%2F6fiJubEJuVPiL99qn3OrzDArp%2BQf27SxMpSbGuvn2VobHklMLV56KKIoinTScnRCEARB5kkDiDwaSqVZD0398uT93%2Fi%2F%2FOpnv6xISM43Hd6%2FDUbNbAtHexPY2xj9Y9nM7BJZemaRbXhk5pgr11NHjuhrEnn9ZtGkqPO4TDrRbZ0QBEGQeSK0iqrWF1W2LCiV70m3rt6%2BZflX58dOesYdy9%2FqBgP9unuEuaHiU2cva0wf30EWtjs5cENYwvmAx5XPRMZU%2FE4lpXs6IQiC0BVozBPxyHDjFLrl0thV73TDlNHu9Rqne%2BHL8%2FXWLgk0MjGQ%2FBrgDWr6IAiCIMg8EboJ76rbEJYwdsWiADzuafVIafH11ywO1JPJpBt8yUARBEEQZJ4IXYMPDt994OqKSaPdH9k41TRQE0c%2BJpFBsi7AG09RLhMEQRBknu5CYym0HH5XXeKVAtPxw9upNN2XJnjCwEAqUyixxb8T3CmnCYIgCE3yEWozTz1dYETlrt3EXsqdOqSPc6PHONUHT697Fzt%2BVshQgZWU0wRBEIQm%2BQi1madiMzhQ0Ws38Un57r0DmqYYBwU78Q9jNvX29UEXym2CIAhCU3yE2syTngQ%2BVPTaTXZOqZGzo0mTpO3t0aryiwSZUgXGUG4TBEEQmuIj1DfmSYL%2BVPTaTU5%2BqcTG0rBJ0nZxqDZlZmwaSLlNEARBaIqPUJ95UmJiXzca96TNKCqUkOo1zXi9qnSVSlizj7aU2wRBEEQVwj8wH9HyzBMQU2CMBSQBou4LC9HyROPjCIIgiGru%2BIcYdW1fba9n0VNidoUEJ%2Fw64uzpi9jdXNv9KnQvevXoiJ93HUdiUjqGDPDFpHF9xbzTZy%2FjRkYuOng448CRaLR1scPQQf6IPp%2BCTZsPIutmPp4I7IjpkwdCpq8n1snLu4113%2BxDzIUr8PFqg1aWZmwdP7i2scfh8POQSiSwtDTF0WOx8O3cDq0drbDx%2B4PIyMqDoYEMgd09MXFsMCRsubQbOdizPwpdOrmJZaRSCWbPGCq28%2FV3fyI9Iw%2FjxwZhGNsnbWPD1mREx93CkGBHDOvn2Gi5NPf%2Bkk4IgiA0E%2BYbhrOP15iPCGQ%2BIr5FmaeTF5Hg640QKbDN3wsf3yrHisRElDb1dr%2FcsBdh24%2Fi2ZA%2BcGvrgOWf7oCxsSHGjOiJ0%2BeS8MWG32FnY4FegV4wMzNGbPxVTJy%2BCm%2FPD4GLkw3WbdyHuIRr%2BGzZdMjLKzB26nJ4dXDGtMlPIvXqTSxfvQM%2BHdtUV4p7%2FoiCo0Mr%2BHf1QF5%2BEQwN9WFna4HgJ7xRUlKOZZ9sR4VcgSkT%2BuH6jWy8v3wLgnr6YMhAP5yLScG451bCwb4Vqwx7izRnLVgH333L4NTaWqvE%2FndkNnYfugFnB%2BOHMU%2FNDumEIAhCs%2FDwgKGlPl7nxkkhQUhUHBKYf2hZLU%2BcM7E40L0jAuUSrGUZMsvPCz9CiYN6CsS6JeDKNqCiKba7dtVLrOKqHEZTUlomWhd4pchxb%2BeIsNAF0NOr7NGc%2F%2FZGTBgThIkhweL3496u6Bo8T1SSUWcvQy6XY%2FXyF0WLAOe7LYdqbSswoIOYX5MAXw%2BkpGbiRnoOerD5PB1eKXIcHazw%2Ff%2Fmie%2F5Q7rhh21HsH%2FXYtjbWoq%2Fbd91DBcupmpdpej5mDly88vQ1slYa%2FaZdEIQBKE%2BQgC9lA5wrZDCmw8OZ9FzghI4L1MikBsnde6bTN2Zw1ug2MdA%2FiwfqRLPsO%2BvKPTQPskLrv7N8PTQx9wcse2Xv6t%2F21ibV1eInOSUDASODar%2BbWVlJlocklMzkJSSLrpuqirE%2B2FvZ1nrd0RUAl5duAHWVubwcG%2BNxMs30M717pAeaY20eIvGvfC%2FyeWKRz5u5taVzVnOb8701Kr9JZ1oRr4TBNFySYKIP1dYtLvE3MBxhQRDzlxAtCbsm0xTMulOhjxUpjxKgM%2FJLYBVK%2FMHzjczM0J%2BYXH1b6VSicLCEpiZGsHC3ATZ2fmN2t5%2F3t%2BMl194qroFYf3GfTh34Uqz5zdz7Y9sTBuT72mZJUi%2BehvmpjJ07mip8ftLOlFdvhMEQegaLfLFwPn5ReKzoKAYmzYfqnNgbf%2Fgzti%2B85jotuHs2B0BCwsTeHq4ILi3D86cS8auPSeRkJgmBuvy8Sx1US6Xi%2FEsVftx%2FFR8i8jzVV8nYNTMY%2FjzWCbphHRCEASh1cha4kG%2FtiiUPz8IuXmFGDWsB6ZOfPBztiaP74szMUno%2BeRCMX4kPTMP6z%2F9N2QyKVxd7LBm5QysWrMTpaXl4o4sO1vLWt0597JgzijMXbgBn6zdJbpe2rk5wNRE9%2FP86KmbMDORYdpYN9IJ6YQgCILMk7axYc1sODlYi1u8%2Be3hVUyfMlBMNeEVHL9jKie3ELeLSuDkaF2r0uO3qA%2B90yJRVFyK77ccEXc7cd57c%2Fw%2Ftj1scACCe%2FkgL%2F%2F2P9Lq5tcex%2F9cXv2b79%2F1i6G11v817G2ty%2B9r6cWiy27WZHe0stAnnZBOCIIgyDxpI3xAb2OwZstb32edWfPXie4VfvfTgcPRGDzAFy7ONnWmZW5uLKaWQnjkTRgYSPHys4%2BRTkgnBEEQZJ60jfffmQhnRxuVpffcs%2F1xPjYVBbeLsWh%2BiHguT0uBv0KlIa9oeaqPI%2FoG2sHBpuFv4ym8XU46IQiCIMg8aQIjhnZXaXq8C4VPLZFW5gby7FulMjvruk2Rpbm%2BmBrDpZR80glBEAShmY0HlAXEw2Juqp93Pb2oSdI%2BGV15N5pEiQI00cNSCYIgCILME9Gs2FgZHgmPzGiStPeHp4lPpQT82QYZlNsEQRAEmSdC60lMLV7628Fr8rJyhUrTTb5WgJRrhVUKTWL%2Fp1JuEwRBEGSeCK3nUERRlIG%2BNDJsd7JK033zo6i7P5S4zf7fT7lNEARBkHkidILrN4smbQhLKImJz1VJesvXn8flKwVVximJTf4KKbZTThMEQRBkngidIIp5nbJy5ZjZ756oeFQDxY3T1pqtWBKES4BTmvIiSIIgCIIg80SohIiYij2FxfIXX3rrmPLzb%2BPQ2DFQfIzTuDmHaxsnJX5g%2Fw9W6uENymGCIAhCk5BRFhCq4HQsNgZ4KaTfbb%2F8VdiuZFlgV1sM6eOCDu4WcHWq%2FcTtohI54pPycfJsFv4MT2PmqbB2Ytw4SdBfIsHzkedxmXKXIAiCIPPUBAQETaPSVDORcfjaz0d5vaKsYtuRkxl6bGrcu0X4GCcJwtm3IUoppkZdwF7SCUEQBKFp6ES3XVQcJHyi4lQ%2Fp5nhkeihK%2Fu6j5mhbFYo59l0lZXO7fssXsjmJUuVbFlghxIwZL%2FNmKXvdboJjBPphCAIglAF1G1HqN7MVna1jfb1QRepAmPY90FQMNMigek9i5oplchTStCKfT%2Bp1MPiSBocThAEQRD%2FxN8LSsoFgiAIgiC00U%2FQ3XYEQRAEQRBkngiCIAiCIMg8EQRBEARBkHkiCIIgCIIg80QQBEEQBEHmiSAIgiAIgiDzRBAEQRAEQeaJIAiCIAiiadDZJ4wrI2fo%2F3T8xNzYhNwp8Zdvtc%2B5VWaYlVNS76s5bKwM5abG%2Bnm21oZHElOLlx6KKIpq6n3VpoeGNvXrTR623JoK0gPpUZ16JP2R%2FjQpHmqiXsk8qZD93%2Fi%2F%2FOpnv6xISM43Hd6%2FDUbNbAtHexPY2xjVu25mdoksPbPINjwyc8yV66kjR%2FQ1ibx%2Bs2jSnVeONBmRR0M1Pl%2Bb%2BqW6j1JuTQXpgfSoTj2S%2Fkh%2FmhQPNVWv6kBPHRt1ssN7N25iscpduvI9qbd19tbPv4l7fXBfF4MP5vsh0NcODnbGMDVpmE%2Fky%2FHlu3Wxxbjh7aQKJVxi4nJn2NtKTqdlKhObKj9mTBup8WJZv3Gn2FdVl58qyq2pID2QHtWpR9If6U%2BT4qGm6rUp%2FER96NSYp62rt28J3XJp7Kp3umHKaHcY6D%2Fa4fH1eTprlwQamRhIfg3wxjQKGZpfbk0F6YH0SPojKB6SXnXKPPEmzg1hCWNXLArA455WKk2bp7dmcaCeTCbd4EsBS2vKrakgPZAeSX8ExcOWrVedME98UN3uA1dXTGIut6kEx9OdOPIxiQySdcxBP0WnuXaUW1MGBNID6ZH0R1A8bJl6Vad5UtkdA%2FxuhMQrBabjh7dr0h1%2BaYInDAykMoUSW%2Fw7wZ1Od%2B0oN9IDoYt6JP2R%2FiheQm13HqrNPPV0gcpuGYi9lDt1SB%2FnJu8b5ul372LHS0uGCqyk0107yo30QOiiHkl%2FpL%2BWHi9V6SO0xjwVm8FBVWnFJ%2BW79w5waJb9HhTsxD%2BM2dTb1wdd6JTXjnIjPRC6qEfSH%2BmvJetVlT5Ca8yTngQ%2BqkorO6fUyNnRpFn229ujVeUXCTKlCoyhU147yo30QOiiHkl%2FpL%2BWrFdV%2BgitMU8s8%2FqrKqmc%2FFKJjaVhvcspFEpcvVEkpnK5ovrv8oq7fy8uqagzDReHanGbsWkgnfJNX24PIi%2B%2FXJRZLvtUF6QH0uO9KJWojic85pD%2BiObU38NQVq4Qer2eUVyvpmvWnRU16s6ieurOJtGrCn1EY1HfE7eUmNjXDW8fTkHJoyalYAUo1at%2F3FjBbTn8RhwQ38O39oVnO3OcT8jH%2BFcikJFduRtfLPFFyFMuD3abd7bDxGQt0eHX2zQHDS03zrofk5BfKMfEEW3g7GAs%2FrZ6UyI%2B%2FzYRL45rh%2F8u6KSeqw%2FSQ4vUY12UllVUx5n4PwfD2tKA9Ec0m%2F4ehrjEAgyY8hfsbAwRu3fQP%2BYXFt2tO%2F8K6wsvd3PEXsrHOFZ3pt%2BsrDvXvOeLccNcmk2vzD8YFTAf0fLMExBTYIwF7POD5tqgkaEe3pjhKb7btqp0%2BGtY5cuN0%2BhBzhgzxBkdHzNvoOEVztmYTvnmgZunqzeK0ae7bbV50iRIDwTpj9BVDPWl1XWnnVXlxcDa7y8L4zRyoJNocPBsZ9aser3jH2LY5NiizJOeErMrJDjh1xFnT1%2FE7mYRgIEUqWlFldtnDvjbn68gPDJb%2FL6ZW4rDJ7IwOKhR48%2Ba%2FfU2ZeVyhH73J45FXISFuQmmTuyHbn7tce16NrbuCMcLkwfA0tJULPvHwbMoZ8sPGxyA3%2FZFwtrKDJFnLuPEqXh07uSGV2YOh7GRgcafuLyFKSevsmvuk42XYGtlyE7kDnev2BRKbNyegj2H0tHKUh%2Bvv%2BiJDm6VJzJvYg7dloJDrGxLSivg6myKOVPc4eFqJpqcX%2F0gWizHW6%2F%2BtyUZ19KL8WQve8ya5A5J4y8Cm10PX4XuRa8eHfHzruNITErHkAG%2BmDSur5h3%2Buxl3MjIRQcPZxw4Eo22LnYYOsgf0edTsGnzQWTdzMcTgR0xffJAyPQrdz0v7zbWfbMPMReuwMerDctPM7aOH1zb2ONw%2BHlIWaZwfR09Fgvfzu3Q2tEKG78%2FiIysPHZ%2ByRDY3RMTxwazvJMg7UYO9uyPQhemNb6MVCrB7BlDxXa%2BZhpOz8jD%2BLFBGMb2Sdvg3Rxfb03BkZOVunJzMcUrUzzwWFvT%2By7PuzW%2BZjqMib8FfZkU7djyz45si04dLMT87fuuY%2Bf%2BNOQXlour%2FxdC2iGwqzXpj%2FTXaP3xmPfah%2BfEcjPGtxMXnmmZJRjA4trLz96Na3%2BdvInNu1KRk18GNyfTOrdnULPuZPr9bkeqWJ%2BTnVuGg8cyG1t3PpJemW8Yzj5eYz4ikPmI%2BBZlnk5eRIKvN0KkwDZ%2FL3x8qxwrEhNR2pTb5P22Ybuviu%2BL%2Ft0R8cmFyCsoE78vXMoXY2g0nZfmfiGCx%2BwZw3D9RjamzfocP3%2F%2FFtq7t0Z8YhrmLQpF6No5OHchBQvf3YRfflwk1vt17ymEn4jDZBbYRgztjm9%2B4MHrFlZ%2B8LzGH%2FOFhHzRFcKJuZgvTuTC2%2FLq%2BZuYCebj1qqIZcv%2Fva2fKO9nXzuJQ8ezMKyfIxxsjbD1t6v4%2FfANHP%2BpPzOfsmo9%2FPT7teo0wiNvwtHOCGOHOGt83ny5YS%2FCth%2FFsyF94NbWAcs%2F3QFjY0OMGdETp88l4YsNv7PK2AK9Ar1gZmaM2PirmDh9Fd6eHwIXJxus27gPcQnX8Nmy6ZCXV2Ds1OXw6uCMaZOfROrVm1i%2Begd8Oraprrz2%2FBEFR4dW8O%2Fqwc6XIhga6sPO1gLBT3ijpKQcyz7ZjgoWvKdM6Cf0%2Bf7yLQjq6YMhA%2F1wLiYF455bCQf7VqzS6i3SnLVgHXz3LYNTa2toC1xXE16NEJXH8P6tYc%2FMDtfR70fSma76wcSodp2QmV2KAZOP4hYzRv0D7aFgCWxjeuMmiZun%2F%2Fv0Ar78IQk9mFl6vIMltjCN7j5wA3s3BqGLlyXpj%2FTXaP3dL64dPXUTTvbGGDXICQePZ7I0TooLT3dXUySm3K53u1yXfNtvzvREQkoBqzsr68vYxHzk3iprlmP38IAhvz7mxkkhQUhUHBKYf1ALau0jPxOLA907IlAuwVqWIbP8vPAjlDiop0CsWwKubAMqmnL7H873QdzlfCGq9%2Bf54F9DXTTbRFxMFcHn%2BP7l4ioKaI%2BIyAQWUCIx9%2BWnserD5zEs5H18vGYnduyOwKdLp8OVXe1VMXfm03hxauUYvY4dXDBm0jJ8tHgq9PQ0%2B7ki6z70w6mYHNFtF%2FqRP7p3qQp018X%2FT%2FV1xLoP%2FBAZk4sRM46xE7tQjG87fSFXGCdeAfHy5aRlFONwRBb2HE7H%2BKfvlveer3ujq3crjJt7Qqxz%2BnyuVpgn0Xy%2B6iVWwbQV30tKy0QrAK%2B8OO7tHBEWuqC6jOe%2FvRETxgRhYkiw%2BP24tyu6Bs8TlVnU2cuQy%2BVYvfxFceXO%2BW7LoVrbCgzoIObXJMDXAympmbiRnoMebD5Ph1deHEcHK3z%2Fv3nie%2F6Qbvhh2xHs37UY9raVpmD7rmNC19pUeR06kSkqLj%2BfVljyqrf4G2%2Bx5HFk318ZGD3IqdbyXIc5rHKxbmWAF8e3E%2BvxIQSpN4pEt8f6sGRYmuvj8%2F%2FrCpmsMt83bE0WlZWmmyfSn2br749NQcygWyJk9gnRSnU6NleYp09CLwnjVDVeNDrulhjz1FB4POXjpHiai%2Bd6Y%2FzwNk1yrCGAXkoHuFZI4c0HhzNVTGD%2B7bxMiUBunNRZDmofYMhboNjHQP7MB6kSz7Dvryj00D7JC67%2Banx6aENhrlfZXNuKv5SGrKx89Bq4sNbfx7NgxDEzNcKXn8zEoFHvYcZzg9Cnd%2B27OGt2Qz3m5oDikjLcYldvvDtPk4%2B7PhxtjURXiLeHRfXf%2BNUWP7k5PDBUDXasIiu3diOni6OxyB%2BeBjdPcrlS4%2FVwPx5zc8S2X%2F6u%2Fm1jbV7LHCenZCBwbFD1bytW9rxlIDk1A0kp6aKLRVJHf6W9Xe3KPCIqAa8u3MA0ZA4P99ZIvHwD7VzvNt9La6TFWx7uhf9NXuPuHW04D2Pv6Or0hbx%2F6Coz55%2BN5907WwuNcqP0rzknxN%2B4UV%2FNzFJ8UoHoPr7FruK7P3OwTo2S%2Fkh%2FjdWf85241tHdXBid8jtxjeuOM7SvozrlUm%2B%2BJUHMv8IO4RJzA8cVEgw5cwHRmlDvaMzdGXcyJFrThXsvzP1KmuvEMzczgpurPQ7%2B%2Bv4Dl9m%2B8zg6ebUV3XS8a%2B9BxignrxD6BjKYmxpp%2FHHXRFnHGnr33KnCr%2BY53u0t8P2qbrXmGRncv7tdJpVojR7uW665BbBq9eCbHsyYhvILi2vkpxKFhSXCePMxdNnZ%2BY3a3n%2Fe34yXX3iq%2Bkp%2F%2FcZ9OHfhik70fyIUAAAbCElEQVSfh5Zmlbp63NMSm1YE1JpnbPhPXZmZyPDXlr7Y%2BWcaomIqW0PPxubhgzVxWDC9Q%2FUyB74Lhr6%2BpIaepaQ%2F0t8j60%2FENVnt3TM20hOPeFH3UBVV5Ju60M3nwOsogQGeSM%2FMw087j1X%2FLfXaTZyJThLff%2FsjCvsPncX2799E%2F%2BDOoj%2B%2F5nNm8vMrB%2FxVVCjwxfo9GNSvqzBQ2oDFnYDx7Y4r%2BGFnavXtsXUxqLeDWI%2FfUrt8fQKOn8nBQVZxvfFRDA6eyNIZXVSVa0FBMTZtPlTnAFiui%2B1MP7x7hcO7dy0sTODp4YLg3j44cy4Zu%2FacREJimhhUy8ed1EW5XC7GnVTtx%2FFT8Tp%2FHg4OdmAXHTIx%2BHvF%2Fyp1dYDpasHSGBw59c%2F82rE%2FDXOXnEUrpkXevdE30LayAjPWQ%2BeOluLmBn4rONfl31HZYlr6ZTxCtyaT%2Fkh%2Fj6y%2F%2B%2FGEf6UGlzADz7vwVm5IAKGlLU9EA1qezI2x8Ys5eO2tUHy4chuMWNAoLi7Dqv9OQ2LSDbz17rcI%2B2YBTE0MseTtCRg69n2sWvMLXn9ltFg%2F7Odw%2FLDtLxG4PN2dsf7zf2vNsc%2BZ6oF5H0Rj655rYtq%2FKajedWysDPDTmkAsWHZODKCsGkTZ2s5I3E2nK7y2KFS0yOXmFWLUsB6YOvHBz42bPL4vzsQkoeeTC8U4D27G13%2F6b3ZlKhXj49asnME0sxOlpeXizik7W8s6W0AWzBmFuQs34JO1u0QXSTs3B6Y%2F3T4P%2BQDdrUxXry89hx9%2FvSomjpO9kZjuxdHOkFVw2WJAbxW9A2zFuBHeWhq2mmmUpcUH8fKuFdG6YK5fPZ6F9Ef6exT93Y93ZnvhTGweEq8UCgM2KMieKthGopYmM948qcrmOp5e5K6nm23%2FA0b8Wv1dVc21kUdDG7VOBgs6fGzAvWMAHsTMeV%2BKgZV8oCZvJm%2FoerWOO2ia6o%2B7EeVWVqYQz%2BQyM9WHlYV%2Bo7bFB%2BzeZlf3fKC9qp8TpU49dOn1KjaHvgYnB2txbFWPqag3P3ILWX6UwMnR%2BoGVU1FxKfyCXsOfO5fAxdnmgWnxFoe8%2FNt1ptUk56Ga9VhTV%2Fy466u4%2BKBe3k1laiK774MzeetT1V1L%2FK4ovQY%2BMJH0R%2FpriP7uhfdK8CeKc6Ne1bKvrfWnOrr%2FqOVJS%2BG32z4MJsaGYtJG%2BCMK2rR%2BuMtKXlk15ZOe1Y1VIwf987Fw9xsPN2v%2BOtENwu9SOnA4GoPZ1X9dFReHt4jyqSXSGF3xmxLqgo974hPpj%2FTXHHGNm92HjaeEjpgn%2Fsj35nq0feHtcq3MI96UbmNl3mLLTVf18P47E%2BHsaKOy9J57tj%2FOx6ai4HYxFs0PEc%2FPaSloox5Jf6Q%2Fipdknh6aVuYG8uxbpTI7a6Mm39allHytzKOe3TxbdLnpqh74A09VCX9aPZ9aItqoR9If6Y%2FipZrMri4chLmpft719KJm2dbJ6Mq7GSRK8AdlVIDQinIjPRC6qEfSH%2BmP9Erm6aGxsTI8Eh6Z0Szb2h%2BeJj6VEmSyjww65bWj3EgPhC7qkfRH%2BiO9knl6aBJTi5f%2BdvCanL8ssSlJvlaAlGuFVTnHH66USqe85pcb6YHQRT2S%2Fkh%2FFC%2FJPD0ShyKKogz0pZFhu5v2oXJvfhR194cS%2FE2K%2B%2BmU1%2FxyIz0QuqhH0h%2Fpj%2BIlmadH5vrNokkbwhJKYuJzmyT95evP4%2FKVgqqCT2KTv0KK7XTKa3a5NRWkB9Ij6Y%2BgeNhy9aoz5imKlU1ZuXLM7HdPVKhaeLzgt9a8GpAgXAKc0pQXFFK5NX8gID2QHkl%2FBMXDlqtXnXq3XURMxZ7CYvmLL711TPn5t3F41L5j3kc7bs7h2gWvxA%2Fs%2F8FKPbxBp7pmlltTQXogPZL%2BCIqHpFeOzj1h%2FHQsNgZ4KaTfbb%2F8VdiuZFlgV1sM6eOCDu4WcHWq%2Bym4RSVyxCfl4%2BTZLPwZnsYKv7D2ArzgJegvkeD5SHaFQKe5ZpRbU0F6ID2qU4%2BkP9KfJsVD0quOmydOZBy%2B9vNRXq8oq9h25GSGHpse7dn9vI9WgnD2bYhSiqlRF7BX1ftc8z1JLRWVl1tTQXogPZL%2BCIqHGqNXdaCnjo062eG9GzexuCm3cSMLiU6O2MoKzp1NdsztJkmAUlaI3DDW9zKgQrbsdakSJ5USxCgBV6kEWWzN8acv4JTK95XlBZ94vmiLcJqq%2FB6x3JoK0gPpUZ16JP2R%2FjQpHmqUXpvDT9wPnX4xcFRl0%2BBoXx90kSowhn0fBAWTnQT1vfrbTKlEHit4%2Fvbdk0o9LI6kwZjaUG5NBemB9KhOPZL%2BSH%2BaFA9Jr%2BrC34t5aIIgCIIgCC30E1LKeoIgCIIgCDJPBEEQBEEQZJ4IgiAIgiDIPBEEQRAEQZB5IgiCIAiCIPNEEARBEARB5omygCAIgiAIgswTQRAEQRBEk6CzTxhXRs7Q%2F%2Bn4ibmxCblT4i%2Ffap9zq8wwK6dEomn7aWNlKDc11s%2BztTY8kphavPRQRFFUU29Tmx5SGhUHiTbqhMqVdKUN8aclxT2CIPNUD%2Fu%2F8X%2F51c9%2BWZGQnG86vH8bjJrZFo72JrC3MdK4fc3MLpGlZxbZhkdmjrlyPXXkiL4mkddvFk2KauK3TkceDdX4cmzql5M2pU6oXElX2hB%2FWlrcIwhVoVMvBlYq35N6W2dv%2FfybuNcH93Ux%2BGC%2BHwJ97eBgZwxTE830iXy%2F%2BP5162KLccPbSRVKuMTE5c6wt5WcTstUJjZV%2Fs%2BYNlLjxbl%2B406xr6rWS3PohMqVdKUN8aclxT1CN1HXi4F1aszT1tXbt4RuuTR21TvdMGW0Owz0tevw%2BP7y%2FV67JNDIxEDya4A3ptGpof06oXIlXRF0fhC6hc6c3bypfENYwtgViwLwuKeVVh8L3%2F81iwP1ZDLpBl8KJDqjEypX0hVB5wdB5klj4IMzdx%2B4umISu3rRlcDFj2PiyMckMkjWsSuxp0iquqETKlfSFUHnB0Hm6aHjDZtUducJv6sl8UqB6fjh7XSqcF6a4AkDA6lMocQW%2F05wJ7nqhk6oXElXBJ0fhEqQ3PETLcY8lfR0gcpuPYm9lDt1SB9nnRtjwI%2Bnexc7rg4ZKrCSzhPd0AmVK%2BmKoPODeHTu%2BIiSlmSesorN4KCqxOKT8t17BzjopDgGBTvxD2M29fb1QRc6XXRDJ1SupCuCzg%2Fi0bjjI7JajHlSAgl6EvioKr3snFIjZ0cTnRSHt0eryi8SZEoVGEOni27ohMqVdEXQ%2BUE8GtxHcD%2FRYsyTBDjO%2FuuvqvRy8kslNpaGKt%2FP0jIFrt4owo2sB7cKZmaXimXyC8sr9%2BVWmfh9q6BcJfvg4lAdlM3YNJBOF%2FXoJOtOOd8ullO5Es0SfxpCWXlljLqeUaya9DQg5tH5QTTCTPQXfqKlmCeFFNuhxMS%2BbqoZ96SoUEKqp%2Fo3H0TG5MJvxAGMfOnYA5d54c1Iscymn6%2BI3x9%2BcVH8%2FmpzkmoK6M5xKZWwZh9t6WxRj07mLDkrynXHvjQqV6JZ4k9DiEssELocOPWoStKLulAZ855%2B8e8HLjPj7SixTOhPKeL3si%2Fjxe%2B136vu4eB0fhD1IfwD8xHCT6gBtTz29swFRPt7IabAGAvYzw%2B0uQAnjmiL4O526NHFuokNtrgCM6ZTRtcunKhcCe1i%2FPA2eMLfFoFdbej8INTGHf8Qw%2F1EizFPHD0lZldIcMKvI86evojdzbHNb36%2BgqiYXDzZ0x6jBjmhqKQCCz%2BKgZGBFMvf7AwJO1M%2F%2FzYRCcmFGDfMhf2%2BezX5d1Q21ocloaRUgcmj22J4v9bi77zpOjWtCOXyB98teT4hX6zLlzMy1MOgIAc894wrpNJGX602%2B%2Bt0ysrlCP3uTxyLuAgLcxNMndgP3fza49r1bGzdEY4XJg%2BApaWpWPaPg2dRzpYfNjgAv%2B2LhLWVGSLPXMaJU%2FHo3MkNr8wcDmMjA604MXm5rv3uMs7E5sHRzui%2B3Rh%2F%2Fp2JH3alIvdWGVpZ6ItKZUiw40OdDs19fF%2BF7kWvHh3x867jSExKx5ABvpg0rq%2BYd%2FrsZdzIyEUHD2ccOBKNti52GDrIH9HnU7Bp80Fk3czHE4EdMX3yQMj0K3c9L%2B821n2zDzEXrsDHqw1aWZqxdfzg2sYeh8PPQ8rOJa6To8di4du5HVo7WmHj9weRkZUHQwMZArt7YuLYYHHOpd3IwZ79UejCNMOX4efJ7BlDxXa%2BZlpMz8jD%2BLFBGMb2Sdvg3Wxfb03BkZNZLJZUwM3FFK9M8cBjbU1ZDFHgtQ%2FPVbbujG%2BHdT8mIS2zBAN62ePlZ91RFY7%2BOnkTm5nucvLL4OZkWuf2vmUx7xSLef162uGZQc4oZjHvDRbzDFjMW3kn5nGdX0wqwL%2BGukAmuxuTjp3OFvvAY96kkW3x9JOVMa%2Fgtrwy5rFjeRAXLvGYl4wr12%2BLmDewtwOeH%2FNQMU8t5weh2TDfMJx9vMZ8RKC69kFt5unkRST4eiNECmzz98LHt8qxIjERpU25Td5HGbb7quif5%2Bbp4PFM8ZszebQrOnWwwOpNicjLL8crz3kg82bl7lxlgWLUzLtddzzwnfipnwh8PJD9EZ6BgMet2NXYP6%2FEjp66iXGvRMDB1hBP9XEUv7lhu5lTijdmeGq8SF%2Ba%2B4Wo9GbPGIbrN7Ixbdbn%2BPn7t9DevTXiE9Mwb1EoQtfOwbkLKVj47ib88uMisd6ve08h%2FEQcJrMKecTQ7vjmB17p3sLKD57X%2BGNWKJT415wIRJ3PhZmJTFRsl68U1lqGd9MuWHoOpsYy%2BHVqhSMRN%2FHboXQsXdAJ08dp%2FvN%2BvtywF2Hbj%2BLZkD5wa%2BuA5Z%2FugLGxIcaM6InT55LwxYbfYWdjgV6BXjAzM0Zs%2FFVMnL4Kb88PgYuTDdZt3Ie4hGv4bNl0yMsrMHbqcnh1cMa0yU8i9epNLF%2B9Az4d21Sbpz1%2FRMHRoRX8u3qw86sIhob6sLO1QPAT3igpKceyT7ajgpmHKRP6CZ29v3wLgnr6YMhAP5yLScG451bCwb4VM029RZqzFqyD775lcGptrTUBX8murya8GiFixvD%2BrWFvYyjiz%2B9H0nGcxRMTI73qePTT79cgr1BWxxAne%2BPqmDXh1ZNCo%2B6upkhMuV13zGNmhad55XqRME%2BHTmRVb2PSiLbo6t1KxDw%2Bbmn2FHfk5JWJedfTi2sNV%2BAx72%2BPfmKbfH%2F4Pvv6tEJQN9t%2FbJNfaP5rzgnYWRtiaF9HhEfexJvLY8S4wTdneoIgHhYPDxha6uN1bpwUEoRExalnsLhazRPnTCwOdO%2BIQLkEa1mGzPLzwo9Q4qCeArFuCbiyDahQ5fYG93HAgmVglWKeGBi5lwUAc1OZuJLa%2F3cG9PQkwjh5uJqhPZuqzJOtlSGOhPVhV8hSdB99UAyYPBt7S5in%2Blj65UVxRfnObC9072yFvoF2eHbeSXbleFXjzdOFi6mi0jy%2Bf%2FmdK8b2iIhMYBVhJOa%2B%2FDRWffg8hoW8j4%2FX7MSO3RH4dOl0uLrYVa8%2Fd%2BbTeHFq5VjPjh1cMGbSMny0eCrLZ81%2BHg43Qtw4cW38va0fWtsZYfzcCBw4llldCS5fHy%2B%2Br13si2H9HEVlMmXBKazYkIBpIW4Pe4XdrKxd9RIzOJXDSUpKy0QrFDdPHPd2jggLXVBdVvPf3ogJY4IwMSRY%2FH7c2xVdg%2BcJMxV19jLkcjlWL3%2BxurX2uy2Ham0rMKCDmF%2BTAF8PpKRm4kZ6Dnqw%2BTwdbp44jg5W%2BP5%2F8ypbAYd0ww%2FbjmD%2FrsWwt7UUf9u%2B65jQpzaZp0MnMoVx8mOmY8mr3uJv15hJ4WZk318ZGD3IqXrZPzYFsYs5S4TMPiGMy%2BnYXGGePgm9JIzTi8yg%2F5cZ9ei4Wxgw5a8HbpO3cnMt8rFMvKWL69TCTF%2B0rPKYZ8QMGzdO%2FALBs505jp%2FJFutZtzLA0bC%2BzORKEfjMIaTfLEF0fJ4wT%2FXGvK8uiha2Rf%2FuiJ6%2B1ujf016YRt5aRuaJaAwhgF5KB7hWSOF9Z3D4BBZ%2Bz8uUCFSncVK7eapqgWIfA%2FmzPKRKPMO%2Bv6LQQ%2FskL7j6q%2FAp5BwHGyP4siut0xfyEBGdgz%2BOZmDMYGdxpbQ%2FPBOWLKhweAtRTYyN9WBtWdnd5OpkIsyTXNGwh5rGJhaIz5nvnK7196ych2tk8%2Fdqvqepxl9KQ1ZWPnoNXFjr7%2BNZJcoxMzXCl5%2FMxKBR72HGc4PQp3ftp0%2FU6PXEY24OKC4pw638ItGdp8nHzbswOPyqnBune8krKBcaqFymsjLv9njlazn4lXt2bhnsbAw19vjux2Nujtj2y91BwjbW5rVMbnJKBgLHBlX%2FtmJlyFumklMzkJSSLrr4anZz34u9nWWt3xFRCXh14QamBXN4uLdG4uUbaOd691lJ0hpp8Zave%2BF%2Fk8sVj3zczZnvVbGAxx8%2BwLommffEA2dHY3H%2BdHQ3F%2BapalhA%2FB1t8hadhsBbt%2FyZWeNddyLmhWdg5MDWOHk2l5mnTNhYGd4%2F5jFTxQ2UiHkuJsI8yeUNy6q4O8c5690zdR6jNp0fhHpIqnx6%2BBV2KlxibuC4QoIh6hrjpHHmqboVqjJDopv6xOJjUnjw%2BphdweXml2NQsAMzATJ88UMS9O%2F09z%2FV58EPvNNr5F01luYycXv75%2B92rdWtV1b2cLGAue1HNpQNzS9zMyO4udrj4K%2FvP3CZ7TuPo5NXW9FNx7v2HmSMcvIKoW8gg7mpkcYfNzfLwiTl3%2F%2FWa1NWsejLpKJFkZslZwdj5N65TZvrg%2BtJk4%2FvvuWTWwCrVuYPnG%2FGtJBfePd2eKVSicLCEmGg%2BVi47Oz8Rm3vP%2B9vxssvPFXd0rR%2B4z6cu3Cl2eNOc%2BZ71cXZ456W2LQioLbmDO8%2FrKfmGKQqU8Pj1oO0eT8GM2PEzRNvteJ6HdTbAdYWBlj9baIY7yliXh1j9fSkjY95vGXrs%2F90qdWtxx%2F9os5yIghV0uLeJzDkzhUW74fngSgowBaDWeDgTeEnzuaIFgP%2FTqp7ueeYIS7ik3fz7P0rA8fP5OC7X1IxZ%2FEZjc%2BrwABPpGfm4aedd8c%2BpF67iTPRlY9h%2BO2PKOw%2FdBbbv38T%2FYM7i3Eoihotcvn5ReKzokKBL9bvwaB%2BXYWB0nR6%2BdmIro6Y%2BFuYv%2FQcln0Vz8x9XvV8Pth2cFClwV7yeZzoCvnPxxfEbz64l%2BtKG6gqn4KCYmzafKjOAdi8fLczHfDuPQ7vprWwMIGnhwuCe%2FvgzLlk7NpzEgmJaWJQNx%2F3VBflcrkY91S1H8dPxet87BnMLtR4VzDX1Yr%2FJYhYcOB4FhYsjcGRUzcblAa%2Fy03obk2cMEMrN9TfczEkuFKrvIWdDz3o091O7AvvfuYxz8bKAN06qzDmDa6MefwYq2Le9yzm3dsSRRDajKylHbCXuzlcnU3EAEpunPidILzLhTdR86uywXfGCKgK3u9fwQzFNz%2BlYNHK85WZrifB0086aXxemZsbY%2BMXc%2FDaW6H4cOU2llf6KC4uw6r%2FTkNi0g289e63CPtmAUxNDLHk7QkYOvZ9rFrzC15%2FZbRYP%2BzncPyw7S9R4Xq6O2P95%2F%2FWCo10cDPDmy95Ytm6eHG3kpeHhRj8yseGVLFqUWfcLpHjEKv8DkdUvh2AV0qfvqM9b5J4bVGoqEBz8woxalgPTJ344OfWTh7fF2diktDzyYVinBE31es%2F%2FTdkMqkY57Zm5QxW9jtRWlou7tyzs7Wsc2zbgjmjMHfhBnyydpfoomvn5sB0pNuxh3ehbV0TiNeZIf%2Fx16ti4jjZG4mpIfCxk%2FwO0MQrhcKcDAqyr3cdPpapXRtTJF%2B9jd4s5nFzzy8QbZmm%2BY0rg4McVRrzFs70hJxdMIVuqx3zhvVvTTUuoTPoRFMobzaP3PW0Ru9jRYUSaZmV3R5WlgbiLq6GEjDi1%2BrvqupmiDwa2qh1Mlhlyce03Dt25UHMnPelGBDMBxjz7p2GrlfruIOmqf64G6ET3j1SeFuONq0f%2FJgZbrj505353VD8Cr5Rx6fGcu3S61VsDn0NTg7WouKsetxEfeTkFuJ2UQmcHK0faI6KikvhF%2FQa%2Fty5BC7OD34WEG%2Fxysu%2FXWdaTYG6dSXykRnx20VycdwNNU5V8NZdrjlLc30x%2BFsXY15TnB8EQS1PWggfC9OmtfZeWvPbxB8GE2NDMWkjVhb6YqoL3mJZNbBWK4%2BxkYP3%2BZi2%2B41rmzV%2FneiG43fJHTgcjcEDfOs0Thzessmnlgi%2FAaXqJpTGws2uNsQSbY95BKHz5ok%2Fyl%2Bdr0hoSgpvl2vlfvMuIBsrc9KJhpbr%2B%2B9MhLOj6p4Q%2Fdyz%2FXE%2BNhUFt4uxaH6IeH5TS0GX4w%2FFPYLQYfPUytxAnn2rVGZnbaRzBXQpJV8r97tnN0%2FSiQaXK39wqSrhT53nU0tEl%2BMPxT2CeMBFky4chLmpft719CKdLKCT0ZV34UiU4A9PqSDJ6oZOqFxJVwSdHwSZJ7ViY2V4JDwyQycLaH94mvhUSsAfb51BktUNnVC5kq4IOj8IMk9qJTG1eOlvB6%2FJy8oVOlU4ydcKkHKtsKqk%2BMOVUkmy2q8TKlfSFUHnB0HmSe0ciiiKMtCXRobtTtapwnnzo6i7P5TgbwDdT5LVfp1QuZKuCDo%2FCDJPGsH1m0WTNoQllMTE5%2BrE8Sxffx6XrxRUBZAkNvkrpNhOktVunVC5kq4IOj8IMk8aQxQ758rKlWNmv3uiQtsDGA8gW2texUoQLgFOacoLEUknVK6E7sYfinsE0YLMEycipmJPYbH8xZfeOqb8%2FNs4aNsYBN7XP27O4doBRIkf2P%2BDlXp4g%2BSqnTqhciVdEXR%2BELqFzj1h%2FHQsNgZ4KaTfbb%2F8VdiuZFlgV1sM6eOCDu4WcHUy06h9LSqRIz4pHyfPZuHP8DQWRAprL8ADiAT9JRI8H8mubEmu2qETKlfSlTbEH4p7BPHw6Owjcf18MAQKbGMHyF9xr13vgOB9%2FRKEs88h7Mpr6ukL2KvK5Pm7uLStPJvq3VbNqhMqV9IVobbzgyBUiZ6uHtiNLCQ6OWIrOxHd2WTHrmKSWCArZScnb23TtJeRFbJ9uy5V4qRSghhWA7pKJchiezqeBZBTKs%2Bbm1jMJyc7vKc15cn2Vwt1QuVKutKG%2BNMi4h5BqBKdfjFwVGWT72hfH3SRKjCGfR%2FErgYl7J%2Bphu2qmVKJPBZA%2BNt3T7KrrsWRNEhSF3RC5Uq60ob4Q3GPIAiCIAiCIIim4%2F8BLzXdlplnri0AAAAASUVORK5CYII%3D)


### 前処理: statement に label を付ける

labelが無いプログラム↓は扱いにくいので、
```cpp=
a = 0;
b = 1;
if (flag) {
  c = a + b;
}
else {
  c = a - b;
}
while(flag){
  d = a;
}
```
このようなイメージでラベルを付ける。
```cpp=
labelstart:; a = 0;
label2:
b = 1;
label4:
if (flag) {
  label6:
  c = a + b;
}
else {
  label10:
  c = a - b;
}
label13:
while(flag){
  label15:
  d = a;
}
labelend:;
```

#### 数式表現

$P$のラベル付き表現を$P^L$と書く。
* Pが単純な命令(`v := e`,`wait`,...)のとき
  $P^L := P$
* $P = P_1;P_2$のとき
  $P^L = P_1^L;l_1;P_2^L$のようにラベル$l_1$を追加
* $P = \text{if } b \text{ then } P_1 \text{ else } P_2 \text{ end if}$のとき
  $P = \text{ if } b \text{ then } l_1;P_1^L \text{ else } l_2;P_2^L \text{ end if}$のようにラベル$l_1,l_2$を追加
* $P = \text{while } b \text{ then } P_1 \text{ end while}$のとき
  $P = \text{while } b \text{ then } l_1;P_1^L \text{ end while}$のようにラベル$l_1$を追加

これに加えてプログラムの先頭と末尾にラベルをつける。
これで、各文の先頭と末尾にラベルがあることを保証できる。

### 前準備: プログラムカウンタの導入

プログラム上の変数に加えて、program counter $pc$を定義する。
$pc$は、現在実行中のプログラム行を表す。
$pc$の定義域は上で定義したlabelの全体と、未実行状態を表すsuspである。

後半の章では、pcが同じ state は、クリプキ構造の図上で1頂点にまとめてしまうこともあるかもしれない。
この章で扱っているクリプキ構造は、変数すべて(pc以外を含む)で表される state の完全一致で1頂点。

### 前準備: sameの導入

プログラムの1文の実行においては、ほとんどの変数の値は変化しない。
それを表す補助関数$same$を定義。
$same(Y) := \bigwedge_{v \in Y} (v \iff v')$


### translation procedure の定義

translation procedure$\mathcal{C}$は、プログラム及びその前後のラベルを入力とし、$\mathcal{R}$を出力する関数。

$\mathcal{C}(l,P,l')$
* $l$: entry label
* $P$: program
* $l'$: exit label

#### P が $v := e$

$$
\mathcal{C}(l,P,l') = (pc = l) \wedge (pc' = l') \wedge (v' = e) \wedge same(V\setminus \{v\})
$$

#### P が skip

$$
\mathcal{C}(l,P,l') = (pc = l) \wedge (pc' = l') \wedge same(V)
$$

#### P が $P_1;l_{mid};P_2$

$$
\mathcal{C}(l,P,l') = \mathcal{C}(l,P_1,l_{mid}) \vee \mathcal{C}(l_{mid},P_2,l')
$$

* $l$から$l_{mid}$への遷移も、$l_{mid}$から$l'$への遷移も、両方とも許可するので$\vee$

#### P が $\text{ if } b \text{ then } l_1;P_1^L \text{ else } l_2;P_2^L \text{ end if}$

$$
\begin{aligned}
\mathcal{C}(l,P,l') &= ((pc = l) \wedge b \wedge (pc' = l_1) \wedge same(V)) \vee \mathcal{C}(l_1,P_1,l')\\
&\vee ((pc = l) \wedge \neg b \wedge (pc' = l_2) \wedge same(V)) \vee \mathcal{C}(l_2,P_2,l')\\
\end{aligned}
$$

* trueなら$\mathcal{C}(l_1,P_1,l')$に行くために$pc' = l_1$
* falseなら$\mathcal{C}(l_2,P_2,l')$に行くために$pc' = l_2$

#### P が $\text{while } b \text{ then } l_1;P_1^L \text{ end while}$

$$
\begin{aligned}
\mathcal{C}(l,P,l') &= ((pc = l) \wedge b \wedge (pc' = l_1) \wedge same(V)) \vee \mathcal{C}(l_1,P_1,l)\\
&\vee ((pc = l) \wedge \neg b \wedge (pc' = l') \wedge same(V)) \\
\end{aligned}
$$

* trueなら$\mathcal{C}(l_1,P_1,l)$に行くために$pc' = l_1$
    * $P_1$の実行後は$l$に戻る
* falseならこの命令は終わりで$pc' = l'$


## Concurrent Processes の model化

concurrent systemは同時に実行されるコンポーネントの集合から構成される
コンポーネント同士はお互いにやり取りを行う


種類
* 実行方法
    * asynchronous: 1ステップで全てとは限らない複数コンポーネントが実行
        * interleaved executions: 1ステップで1コンポーネントだけが実行
    * synchronous: 1ステップで全てのコンポーネントが同時に実行
* コンポーネント間の通信方法
    * shared variables: 共有変数を介した値のやり取り
    * exchanging messages: queueやある種のprotocolに基づいたやり取り

今回扱うのはinterleaved executionsでshared variablesを使う方法。
マルチスレッドのプログラムが近い


### $P$の書式 (cobegin)

$P = \text{cobegin }P_1 \parallel P_2 \parallel \dots \parallel P_n\text{ coend}$
$P^L = \text{cobegin }l_1;P_1;l'_1 \parallel l_2;P_2;l'_2 \parallel \dots \parallel l_n;P_n;l'_n\text{ coend}$


### 初期状態

$\mathcal{S_0} = (pc = m) \wedge \bigwedge_i (pc_i = susp) \wedge pre(V)$
$m$: $P$の先頭ラベル
$susp$: 実行されていないことを表す特別なラベル
$pre(V)$: Vの各変数の初期値

$P_1$がメインスレッドではなく、$P_1,\dots,P_n$全部子スレッド

### translation procedure の Concurrent Processes 拡張


#### P が $\text{cobegin }l_1;P_1;l'_1 \parallel l_2;P_2;l'_2 \parallel \dots \parallel l_n;P_n;l'_n\text{ coend}$

$$
\begin{aligned}
PC = &\{pc, pc_1, pc_2, \dots, pc_n\}\\
\mathcal{C}(l,P,l') =
&(pc = l \wedge pc' = susp \wedge  \bigwedge_i pc_i' = l_i \wedge same(V))\\
\vee &\bigvee_i (\mathcal{C}(l_i,P_i,l'_i) \wedge same(PC \setminus \{pc_i\}) \wedge same(V \setminus V_i))\\
\vee &(pc = susp \wedge \bigwedge_i pc_i = l_i' \wedge pc' = l' \wedge \bigwedge_i pc_i' = susp \wedge same(V))\\
\end{aligned}
$$

* 1行目: $(pc = l \wedge pc' = susp \wedge  \bigwedge_i pc_i' = l_i \wedge same(V ))$
    * Concurrent Processes の起動
* 2行目: $i$番目のコンポーネント(スレッド)のみを動かす
    * $same(PC \setminus \{pc_i\}) \wedge same(V \setminus V_i)$: 他のコンポーネントは動かさない(interleaving semantics)
    * $\mathcal{C}(l_i,P_i,l'_i)$はコンポーネントi内の動作
        * 複数ステップあるが各ステップが$\vee$で接続されているため、そのすべてのステップに他のコンポーネントは動かさないの制約が$\wedge$でつく
    * コンポーネント0を動かす場合、コンポーネント1を動かす場合...なので$\vee$
* 3行目: $(pc = susp \wedge \bigwedge_i pc_i = l_i' \wedge pc' = l' \wedge \bigwedge_i pc_i' = susp \wedge same(V ))$
    * Concurrent Processes のjoin

#### 例

$$
\begin{aligned}
&l_1&\\
&\text{cobegin}&\\
&\quad	(l_{1a};skip;l_{1b}) &\parallel\\
&\quad	(l_{2a};skip;l_{2b};skip;l_{2c}) \\
&\text{coend}&\\
&l_2&\\
\end{aligned}
$$
の translation procedure は

* ::: spoiler Concurrent Processes の起動
  $pc = l_1 \wedge pc' = susp \wedge pc_1' = l_{1a} \wedge pc_2' = l_{2a} \wedge same(V)$
  :::
* ::: spoiler thread 1 の処理
  $\mathcal{C}(l_{1a},P_1,l_{1b}) \wedge same(\{pc, pc_2\}) \wedge same(V\setminus V_1)$
  $= (pc_1 = l_{1a}) \wedge (pc_1' = l_{1b}) \wedge same(\{pc, pc_2\}) \wedge same(V)$
  :::
* ::: spoiler thread 2 の処理
  $\mathcal{C}(l_{2a},P_1,l_{2c}) \wedge same(\{pc, pc_1\}) \wedge same(V\setminus V_2)$
  $= ((pc_2 = l_{2a} \wedge pc_2' = l_{2b}) \vee (pc_2 = l_{2b} \wedge pc_2' = l_{2c})) \wedge same(\{pc, pc_1\}) \wedge same(V)$
  $= (pc_2 = l_{2a} \wedge pc_2' = l_{2b} \wedge same(\{pc, pc_1\}) \wedge same(V)) \vee\\\quad (pc_2 = l_{2b} \wedge pc_2' = l_{2c} \wedge same(\{pc, pc_1\}) \wedge same(V))$
  :::
* ::: spoiler Concurrent Processes のjoin
  $pc = susp \wedge pc_1 = l_{1b} \wedge pc_2 = l_{2c} \wedge pc' = l_2 \wedge pc_1' = susp \wedge pc_2' = susp \wedge same(V)$
  :::

の$\vee$



### 排他制御に関係する命令の書式と translation procedure

スレッド間同期に使う atomic な命令。 (atomic: この命令の実行中に他の命令が実行されない)

#### $P$が $wait(b)$

b が true になるまで待つ (busy wait)

$$
\begin{aligned}
P &= wait(b)\\
\mathcal{C}(l,P,l') &= (pc = l \wedge \neg b \wedge pc' = l \wedge same(V))\\
&\vee (pc = l \wedge b \wedge pc' = l' \wedge same(V))\\
\end{aligned}
$$

#### $P$が $lock(v)$

b が true になるまで busy wait で待ち、lockを取得する。
$wait(locked = 0);locked = 1;$を atomic にやるイメージ。

$$
\begin{aligned}
P &= lock(v)\\
\mathcal{C}(l,P,l') &= (pc = l \wedge v = 1 \wedge pc' = l \wedge same(V))\\
&\vee (pc = l \wedge v = 0 \wedge pc' = l' \wedge v' = 1 \wedge same(V \setminus \{v\}))\\
\end{aligned}
$$

#### $P$が $unlock(v)$

lockを解放する。
このスレッドが lock を取得済みであることを保証するのはプログラム側の責任。

$$
\begin{aligned}
P &= unlock(v)\\
\mathcal{C}(l,P,l') &= (pc = l \wedge pc' = l' \wedge v' = 0 \wedge same(V \setminus \{v\}))\\
\end{aligned}
$$

#### wait の例: 交互実行

以下のプログラムを考える
$$
\begin{aligned}
P_0 =&                               &P_1 = & \\
&l_{0};\text{while } true\text{ do}  & &l_{1};\text{while } true\text{ do}\\
&\quad NC_{0}; wait(turn = 0);       & &\quad NC_{1}; wait(turn = 1);\\
&\quad CR_{0}; turn := 1;            & &\quad CR_{1}; turn := 0;\\
&\text{end while}; l_{0}'            & &\text{end while}; l_{1}'\\
\end{aligned}
\begin{aligned}
P =\\
&m&\\
&\text{cobegin }P_0 \parallel P_1\text{ coend}&\\
&m'&\\
\end{aligned}\\
$$

クリプキ構造の図
![](https://ryutaro-kodama.github.io/slides/semi/journal_club/ModelChecking_ch3/reachable_state.png)

translation procedure は

* Concurrent Processes の起動
  $pc = m \wedge pc' = susp \wedge pc_0' = l_{0} \wedge pc_1' = l_{1}$
* thread 0 の処理
  $\mathcal{C}(l_{0},P_0,l'_{0}) \wedge same(\{pc, pc_1\})$
* thread 1 の処理
  $\mathcal{C}(l_{1},P_1,l'_{1}) \wedge same(\{pc, pc_0\})$
* Concurrent Processes のjoin
  $pc = susp \wedge pc_0 = l_{0}' \wedge pc_1 = l_{1}' \wedge pc' = m' \wedge pc_0' = susp \wedge pc_1' = susp$

の$\vee$

ただし、
$$
\begin{aligned}
\mathcal{C}(l_{i},P_i,l'_{i}) =&
(pc_i = l_i \wedge pc_i' = NC_i \wedge turn'=turn)\\
\vee& (pc_i = NC_i \wedge turn \neq i \wedge pc_i' = NC_i \wedge turn'=turn)\\
\vee& (pc_i = NC_i \wedge turn = i \wedge pc_i' = CR_i \wedge turn'=turn)\\
\vee& (pc_i = CR_i \wedge pc_i' = l_i \wedge turn'=(turn+1)%2)\\
\end{aligned}
$$


二つのプロセスが同時にCRに入ることが無いことがわかる。
::: spoiler Q. starvation (どちらかのプロセスのCRが実行されない) が起こるパスは存在するか
存在する。
turn=1の状態で、プロセス0を実行し続ける場合に starvation が起こる。
プロセス0を実行し続ける場合は無いという主張をするのが後述の Fairness 。
:::


### Transition の粒度

model 上の処理の最小単位と、実装での処理の最小単位が一致していない場合、問題が起こることがある。

2つの命令
$$
\begin{aligned}
\alpha: &x = x + y\\
\beta: &y = y + x
\end{aligned}
$$
と、$\alpha,\beta$をより細かく分解した命令群
$$
\begin{aligned}
\alpha_0: &\text{load }R_1,x &\beta_0: &\text{load }R_2,y\\
\alpha_1: &\text{add }R_1,y &\beta_1: &\text{add }R_2,x\\
\alpha_2: &\text{store }R_1, x &\beta_2: &\text{store }R_2, y\\
\end{aligned}
$$
を考える。

初期状態が$x = 1 \wedge y = 2$とする。
αとβを並列に実行する。
このときの実行結果として考えられる値は
* αとβの粒度のとき
    * ::: spoiler αβ
      $x = 3 \wedge y = 5$
      :::
    * ::: spoiler βα
      $x = 4 \wedge y = 3$
      :::
* 細かい粒度のとき
    * α0α1α2β0β1β2
      $x = 3 \wedge y = 5$
    * β0β1β2α0α1α2
      $x = 4 \wedge y = 3$
    * ::: spoiler α0β0α1β1α2β2
      $x = 3 \wedge y = 3$
      :::


#### 粒度が違うと困る例

* 実際のシステムがαとβの粒度だが、modelが細かい粒度のとき
    * model上の方がより多くの状態に到達できてしまう
        * liveness の証明に使えない
        * 例えば、モデル上で$x = 3 \wedge y = 3$に到達するという結果が出ても、信頼できない
    * 状態数が増えるので検査の時間計算量が増える
* 実際のシステムが細かい粒度だが、modelがαとβの粒度のとき
    * 実際のシステムの方がより多くの状態に到達できてしまう
        * エラー検出に使えない
        * 例えば、モデル上で$x = 3 \wedge y = 3$にならないという結果が出ても、信頼できない


## Fairness

Concurrent Processes があるときにどのパスを実行するかは、実システム上では scheduler が決める。
scheduler は複雑なので、直接モデル化するのではなく、代わりに Fairness 制約を導入する。

Kripke structure $M = (S,S_0, R, AP, L, F)$
* $F \subseteq 2^{S}$: Fairness 制約

### Fairness 制約の定義

無限長パス$\pi$が Fairness 制約$F = \{F_1,F_2,\dots,F_n\}$を満たしているとは
$\forall F_i \in F,\quad \exists s \in F_i,\quad M, \pi \models GF s$

$F_1$に含まれている要素のどれかが無限にしばしば現れる、かつ
$F_2$に含まれている要素のどれかが無限にしばしば現れる、かつ
$\vdots$
$F_n$に含まれている要素のどれかが無限にしばしば現れる


#### スケジューリングによる starvation を回避する Fairness 制約

直前に実行されたプロセスIDを保存する変数を用意する。
$\sigma_i$を直前に実行されたプロセスが i のときに true になる変数、とする。
$$
\begin{aligned}
F_i &= (\sigma_i \vee pc_i = susp)\\
F &= \{F_1, \dots, F_n\}
\end{aligned}
$$

各プロセスが、
* 実行されていない
* 無限にしばしば実行される

のどちらかであれば良い。







