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 37b2ee6..b185ba3 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 @@ -90,33 +90,23 @@ Sure Marco! Let's go step-by-step through the **CCS process transition example** --- -## 📘 Definitions +#### Example +##### 📘 Definitions We start with the following **process definitions**: -- A≜a.A′A \triangleq a.A' - -- A′≜bˉ.AA' \triangleq \bar{b}.A - -- B≜b.B′B \triangleq b.B' - -- B′≜cˉ.BB' \triangleq \bar{c}.B - +- $A \triangleq a.A'$ +- $A' \triangleq \bar{b}.A$ +- $B \triangleq b.B'$ +- $B' \triangleq \bar{c}.B$ -Our **initial process** is: -A∣BA \mid B - ---- - -## ▶️ Step 1: Transition from A +Our **initial process** is: $A \mid B$ +##### ▶️ Step 1: Transition from A From the definition: -- A≜a.A′A \triangleq a.A' - So we can do: - - -A→aA′A \xrightarrow{a} A' +- $A \triangleq a.A'$ + - So we can do: $A \xrightarrow{a} A'$ (A consumes ) Using the **parallel rule** for the left-hand side: