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

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

@@ -79,4 +79,114 @@ $$\frac{P_1 \xrightarrow{a} P_1' \quad P_2 \xrightarrow{\bar{a}} P_2'}{P_1 \mid
 
 ![](images/Pasted%20image%2020250414104010.png)
 
-fino alla 7 compresa...
+fino alla 7 compresa...
+
+Sure Marco! Let's go step-by-step through the **CCS process transition example** in the figure, using:
+
+- **Markdown for explanations**
+    
+- **LaTeX in Obsidian format** (with `$$...$$`) for math
+    
+
+---
+
+## 📘 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
+    
+
+Our **initial process** is:  
+A∣BA \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'
+
+Using the **parallel rule** for the left-hand side:
+
+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
+
+We now have:
+
+- Left process: A′≜bˉ.AA' \triangleq \bar{b}.A
+    
+- Right process: B≜b.B′B \triangleq b.B'
+    
+
+From this, we can do:
+
+- A′→bˉAA' \xrightarrow{\bar{b}} A
+    
+- B→bB′B \xrightarrow{b} B'
+    
+
+These actions **complement each other**, so we can apply the **synchronization rule**:
+
+A′→bˉAB→bB′A′∣B→τA∣B′\frac{A' \xrightarrow{\bar{b}} A \quad B \xrightarrow{b} B'}{A' \mid B \xrightarrow{\tau} A \mid B'}
+
+✅ **Second transition:**
+
+A′∣B→τA∣B′A' \mid B \xrightarrow{\tau} A \mid B'
+
+---
+
+## ▶️ Step 3: Transition from B'
+
+From the definition:
+
+- B′≜cˉ.BB' \triangleq \bar{c}.B  
+    So:
+    
+
+B′→cˉBB' \xrightarrow{\bar{c}} B
+
+Now use the **right parallel rule**:
+
+B′→cˉBA∣B′→cˉA∣B\frac{B' \xrightarrow{\bar{c}} B}{A \mid B' \xrightarrow{\bar{c}} A \mid B}
+
+✅ **Third transition:**
+
+A∣B′→cˉA∣BA \mid B' \xrightarrow{\bar{c}} A \mid B
+
+---
+
+## 🔄 Full Transition Path
+
+Putting it all together, the full trace is:
+
+1. A∣B→aA′∣BA \mid B \xrightarrow{a} A' \mid B
+    
+2. A′∣B→τA∣B′A' \mid B \xrightarrow{\tau} A \mid B'
+    
+3. A∣B′→cˉA∣BA \mid B' \xrightarrow{\bar{c}} A \mid B
+    
+
+So the system loops back to the starting state!
+
+---
+
+Let me know if you want a **state diagram in LaTeX (TikZ)** for this or a different trace involving `B'` and `A'` again!