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 5c3d542..fdff64a 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 @@ -53,27 +53,13 @@ $$\frac{P \xrightarrow{\alpha} P'}{P \setminus a \xrightarrow{\alpha} P' \setmin > 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** -$$\frac{P_1 \xrightarrow{\alpha} P_1'}{P_1 \mid P_2 \xrightarrow{\alpha} P_1' \mid P_2}$$ -$$\frac{P_2 \xrightarrow{\alpha} P_2'}{P_1 \mid P_2 \xrightarrow{\alpha} P_1 \mid P_2'}$$ There are three rules here for different situations in `P₁ | P₂`. - ---- - -#### a. **Left process makes a move:** - -**`P₁ ⟶ᵅ P₁'` -——————————— -`P₁ | P₂ ⟶ᵅ P₁' | P₂`** - +###### a. **Left process makes a move:** +$$\frac{P_1 \xrightarrow{\alpha} P_1'}{P_1 \mid P_2 \xrightarrow{\alpha} P_1' \mid P_2}$$ > If `P₁` makes a move alone, the parallel composition can reflect it. ---- - -#### b. **Right process makes a move:** - -**`P₂ ⟶ᵅ P₂'` -——————————— -`P₁ | P₂ ⟶ᵅ P₁ | P₂'`** +###### 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.