diff --git a/Concurrent Systems/notes/12 - CCS (che non so cosa voglia dire).md b/Concurrent Systems/notes/12 - CCS (che non so cosa voglia dire).md index fdff64a..679a81a 100644 --- a/Concurrent Systems/notes/12 - CCS (che non so cosa voglia dire).md +++ b/Concurrent Systems/notes/12 - CCS (che non so cosa voglia dire).md @@ -49,7 +49,6 @@ $$\frac{P\{a_1/x_1, \dots, a_n/x_n\} \xrightarrow{\alpha} P'}{A(a_1, \dots, a_n) ##### 3. **Restriction (Hiding)** $$\frac{P \xrightarrow{\alpha} P'}{P \setminus a \xrightarrow{\alpha} P' \setminus a} \quad \text{if } \alpha \notin \{a, \bar{a}\}$$ - > If process `P` can do action `α` and it’s **not** the hidden action (`a` or `ā`), then `P \ a` can also do it, and the resulting process remains restricted. ##### 4. **Parallel Composition – Independent Actions** @@ -60,21 +59,12 @@ $$\frac{P_1 \xrightarrow{\alpha} P_1'}{P_1 \mid P_2 \xrightarrow{\alpha} P_1' \m ###### b. **Right process makes a move:** $$\frac{P_2 \xrightarrow{\alpha} P_2'}{P_1 \mid P_2 \xrightarrow{\alpha} P_1 \mid P_2'}$$ - > Symmetrical to the previous: `P₂` makes the move. ---- - -#### c. **Synchronization rule (communication):** - -**`P₁ ⟶ᵃ P₁'` and `P₂ ⟶ā P₂'` -—————————————— -`P₁ | P₂ ⟶^τ P₁' | P₂'`** - +###### c. **Synchronization rule (communication):** +$$\frac{P_1 \xrightarrow{a} P_1' \quad P_2 \xrightarrow{\bar{a}} P_2'}{P_1 \mid P_2 \xrightarrow{\tau} P_1' \mid P_2'}$$ > If one process can **send** (`a`) and the other can **receive** (`ā`), they **synchronize**, and the result is an **internal (τ)** action. This models communication. ---- - ## 🧠 Summary Table: |Rule Type|Description|