From 7227bcbc96a10f4fc649def328da6b7d579059a2 Mon Sep 17 00:00:00 2001 From: Marco Realacci Date: Mon, 14 Apr 2025 17:05:00 +0200 Subject: [PATCH] vault backup: 2025-04-14 17:05:00 --- .obsidian/workspace.json | 4 ++-- .../12 - CCS (che non so cosa voglia dire).md | 18 +++++------------- 2 files changed, 7 insertions(+), 15 deletions(-) diff --git a/.obsidian/workspace.json b/.obsidian/workspace.json index f97a7e7..dc03cc2 100644 --- a/.obsidian/workspace.json +++ b/.obsidian/workspace.json @@ -238,10 +238,10 @@ "companion:Toggle completion": false } }, - "active": "2882ba3b76891dd0", + "active": "84845736e00d5c98", "lastOpenFiles": [ - "Concurrent Systems/notes/12 - CCS (che non so cosa voglia dire).md", "Concurrent Systems/slides/class 12.pdf", + "Concurrent Systems/notes/12 - CCS (che non so cosa voglia dire).md", "Pasted image 20250414164549.png", "Concurrent Systems/notes/images/Pasted image 20250414082824.png", "Concurrent Systems/notes/11 - LTSs and Bisimulation.md", 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 6079b4b..cb282b0 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 @@ -123,23 +123,15 @@ From this, we can do: 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'} +$$\frac{A' \xrightarrow{\bar{b}} A \quad B \xrightarrow{b} B'}{A' \mid B \xrightarrow{\tau} A \mid B'}$$ ✅ **Second transition:** +$$A' \mid B \xrightarrow{\tau} A \mid B'$$ -A′∣B→τA∣B′A' \mid B \xrightarrow{\tau} A \mid B' - ---- - -## ▶️ Step 3: Transition from B' - +##### ▶️ Step 3: Transition from B' From the definition: - -- B′≜cˉ.BB' \triangleq \bar{c}.B - So: - - -B′→cˉBB' \xrightarrow{\bar{c}} B +- $BB' \triangleq \bar{c}.B$ + - So: B′→cˉBB' \xrightarrow{\bar{c}} B Now use the **right parallel rule**: