Concurrent

好蠢，Summary写到正面了，晕晕。抓紧时间还没忘掉总结一下。

Week1

这门课一开始的理念就把 Concurrent 和系统间通信连到了一起，并提出了 External 和 Internal 的概念，并认为内部状态外部不可见，以 $\tau$ 来表示，其他的就是正常 Transition。

主要就是把模型以 FSM 的形式表示出来。比较重要的感觉有一下几点

FSM 相关

这一块主要还是定义。

结构

$TS = (S,\to,s_0), \to\subseteq S\times Act\times S$

分别代表状态集，转移规则和起始状态。

操作的定义

$Act$： 动作集合
$Com$： 交流动作
$Int$： 内部转移

还有 $Act = Com\cup Int$

Post 操作

分为对元素和集合的操作， 2*2 共四种

$$Post(s,\alpha) = \{s'|s\mathop{\to}\limits^{\alpha} s'\}$$

$$Post(S,\alpha) = \bigcup_{s\in S}Post(s,\alpha)$$

$$Post(s,A) = \bigcup_{\alpha\in A}Post(s,\alpha)$$

$$Post(S,A) = \bigcup_{\alpha\in A}Post(S,\alpha)$$

Non-determinism

在这节课上，我们认为有两种 Non-determinism.

一种是内部的，另一种是外部的。例子如下：

stateDiagram-v2
    [*]--> Start
    Start--> End1 : a
    Start--> End2 : b

和生活结合就是一个手机，两个按钮

另一种是内部的：

stateDiagram-v2
[*]--> Start
    Start--> End1 : [a]
    Start--> End2 : [b]

和生活结合就是一个按钮，按下后是什么和内部状态相关。

还有一种是两不沾的，如：

stateDiagram-v2
    [*]--> Start
    Start--> End1 : [a]
    Start--> End2 : b

Reachability

就是定义。

$$Post^0(\{s\}) = s$$

$$Post^{n+1}(C) = Post(Post^n(C))$$

$$Reach(S) = \bigcup_{n\in\mathbb{N}}Post^n(S) \quad$$

根据定义， $s\in Reach(\{s\})$

$CSS$ 相关

$CSS_0$

这是自创的描述语言，语法如下

$S := 0| S + S | a.S \quad a\in Act$

+left associative
.right associative
prefix have higher priority

还有两个个语法扩展

$CSS_0^\omega$

这个是加上了递归语法。Reference Rule 如下：

$$\textbf{rec}\frac{P\mathop{\to}^\alpha P' \quad \Gamma(X)=P}{X\mathop{\to}\limits^{\alpha}P'}$$

$CSS$

加了一个“锁”来提供 sync。

语法是夹在了 $Act$ 上。 对于 $a\in Act$ , 我们规定 $a! , a?$ 分别为发射端和接收端。接收端接收到发射端信号才会进一步执行。图示如下：

stateDiagram-v2
    [*]--> Start
    Start--> Mid1 : a?
    Start--> Mid2 : a!
    Mid1--> End :a!
    Start-->End : τ
    Mid2--> End :a?

感觉这个实现方法有点阻塞的意思。

第一周内容大概就这么多，没写上的就是一些 Inference Rules， 准备复习的时候一起记。