vault backup: 2025-04-14 16:50:00

.obsidian/workspace.json

@@ -240,6 +240,7 @@
   },
   "active": "84845736e00d5c98",
   "lastOpenFiles": [
+    "Pasted image 20250414164549.png",
     "Concurrent Systems/slides/class 12.pdf",
     "Concurrent Systems/notes/12 - CCS (che non so cosa voglia dire).md",
     "Concurrent Systems/notes/images/Pasted image 20250414082824.png",

Concurrent Systems/notes/12 - CCS (che non so cosa voglia dire).md

@@ -91,48 +91,35 @@ Sure Marco! Let's go step-by-step through the **CCS process transition example**
 ---
 
 #### Example
+![](../../Pasted%20image%2020250414164549.png)
+
+#### Example, but explained
 ##### 📘 Definitions
-
 We start with the following **process definitions**:
-
 - $A \triangleq a.A'$
 - $A' \triangleq \bar{b}.A$
 - $B \triangleq b.B'$
 - $B' \triangleq \bar{c}.B$
 
 Our **initial process** is: $A \mid B$
-
 ##### ▶️ Step 1: Transition from A
 From the definition:
 
 - $A \triangleq a.A'$
-	- So we can do: $A \xrightarrow{a} A'$ (A consumes )
+	- So we can do: $A \xrightarrow{a} A'$ (A consumes a and becomes A')
 
 Using the **parallel rule** for the left-hand side:
+$$\frac{A \xrightarrow{a} A'}{A \mid B \xrightarrow{a} A' \mid B}$$
+✅ **First transition:** $A \mid B \xrightarrow{a} A' \mid B$
 
-A→aA′A∣B→aA′∣B\frac{A \xrightarrow{a} A'}{A \mid B \xrightarrow{a} A' \mid B}
-
-✅ **First transition:**
-
-A∣B→aA′∣BA \mid B \xrightarrow{a} A' \mid B
-
----
-
-## ▶️ Step 2: Synchronization: bˉ\bar{b} and bb
-
+##### ▶️ Step 2: Synchronization: $\bar{b}$ and $b$
 We now have:
-
-- Left process: A′≜bˉ.AA' \triangleq \bar{b}.A
-    
-- Right process: B≜b.B′B \triangleq b.B'
-    
+- Left process: $A' \triangleq \bar{b}.A$
+- Right process: $B \triangleq b.B'$
 
 From this, we can do:
-
-- A′→bˉAA' \xrightarrow{\bar{b}} A
-    
-- B→bB′B \xrightarrow{b} B'
-    
+- $A' \xrightarrow{\bar{b}} A$
+- $B \xrightarrow{b} B'$
 
 These actions **complement each other**, so we can apply the **synchronization rule**: