From 32594c57e8877708f921d07c5e4b451f05863439 Mon Sep 17 00:00:00 2001 From: Marco Realacci Date: Mon, 28 Apr 2025 18:01:27 +0200 Subject: [PATCH] vault backup: 2025-04-28 18:01:27 --- .obsidian/workspace.json | 3 +-- Concurrent Systems/notes/13 - Weak Bisimilarity.md | 6 ++++++ 2 files changed, 7 insertions(+), 2 deletions(-) diff --git a/.obsidian/workspace.json b/.obsidian/workspace.json index 9107af6..65fd7df 100644 --- a/.obsidian/workspace.json +++ b/.obsidian/workspace.json @@ -213,9 +213,9 @@ }, "active": "56150e6df7869900", "lastOpenFiles": [ - "Pasted image 20250428175449.png", "Concurrent Systems/slides/class 13.pdf", "Concurrent Systems/notes/13 - Weak Bisimilarity.md", + "Pasted image 20250428175449.png", "Pasted image 20250428085837.png", "Pasted image 20250428085410.png", "Pasted image 20250428084340.png", @@ -232,7 +232,6 @@ "Concurrent Systems/notes/images/Pasted image 20250414181443.png", "Concurrent Systems/slides/class 11.pdf", "Concurrent Systems/notes/images/Pasted image 20250414173011.png", - "Concurrent Systems/notes/images/Pasted image 20250414082824.png", "HCIW/notes/3 - Beacons.md", "HCIW/slides/Zooming interfaces.pdf", "HCIW/slides/Gestural interaction.pdf", diff --git a/Concurrent Systems/notes/13 - Weak Bisimilarity.md b/Concurrent Systems/notes/13 - Weak Bisimilarity.md index c3f701f..0936221 100644 --- a/Concurrent Systems/notes/13 - Weak Bisimilarity.md +++ b/Concurrent Systems/notes/13 - Weak Bisimilarity.md @@ -103,3 +103,9 @@ The specification is: $$L \triangleq \tau.\bar{p_{1}}L+\tau.\bar{p_{2}}.L+\dots+ where $\tau$'s represent ball extractions and $\tilde{p_{i}}$ is the action that communicates with the value of the extracted ball. The LTS resulting from this specification is: ![](../../Pasted%20image%2020250428175449.png) +We now build a system with n components, one for every ball. + +Every component can be in three states: +- A (waiting for being habilitated to extraction) +- B (habilitated, with the possibility of being extracted or of habilitating the next component) +- C (extracted, waiting to externally communicate its value and start the process again): $$A_{i}=a_{i}.B_{i} \quad B_{i}=\tau.C_{i}+\bar{a}_{(i \space mod \space n)+1}.A_{i} \quad C_{i}=\bar{p}_{i}.B_{i}$$