From 9db7dc58419a6ca9e85e0cd3bb737f716c8e4eb2 Mon Sep 17 00:00:00 2001 From: Marco Realacci Date: Wed, 30 Apr 2025 17:13:22 +0200 Subject: [PATCH] vault backup: 2025-04-30 17:13:22 --- .obsidian/workspace.json | 21 +++++-------------- .../notes/13 - Weak Bisimilarity.md | 7 ++++++- 2 files changed, 11 insertions(+), 17 deletions(-) diff --git a/.obsidian/workspace.json b/.obsidian/workspace.json index 47ce0ab..8d8779b 100644 --- a/.obsidian/workspace.json +++ b/.obsidian/workspace.json @@ -20,18 +20,6 @@ "icon": "lucide-file", "title": "13 - Weak Bisimilarity" } - }, - { - "id": "4151b8cc103dc898", - "type": "leaf", - "state": { - "type": "pdf", - "state": { - "file": "Concurrent Systems/slides/class 13.pdf" - }, - "icon": "lucide-file-text", - "title": "class 13" - } } ] } @@ -90,7 +78,8 @@ } ], "direction": "horizontal", - "width": 309.5 + "width": 309.5, + "collapsed": true }, "right": { "id": "bc4b945ded1926e3", @@ -204,10 +193,10 @@ }, "active": "ec8d1a91f1f0cc7e", "lastOpenFiles": [ - "Concurrent Systems/notes/14.md", - "Concurrent Systems/notes/13 - Weak Bisimilarity.md", - "Concurrent Systems/notes/12b - CCS cose varie.md", "Concurrent Systems/slides/class 13.pdf", + "Concurrent Systems/notes/13 - Weak Bisimilarity.md", + "Concurrent Systems/notes/14.md", + "Concurrent Systems/notes/12b - CCS cose varie.md", "Concurrent Systems/notes/12 - Calculus of communicating system.md", "Concurrent Systems/notes/images/Pasted image 20250415082906.png", "Concurrent Systems/slides/class 14.pdf", diff --git a/Concurrent Systems/notes/13 - Weak Bisimilarity.md b/Concurrent Systems/notes/13 - Weak Bisimilarity.md index ae60fc9..7927510 100644 --- a/Concurrent Systems/notes/13 - Weak Bisimilarity.md +++ b/Concurrent Systems/notes/13 - Weak Bisimilarity.md @@ -109,4 +109,9 @@ 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}$$ -In pratica ogni volta o estrae di nuovo "se stesso" oppure "abilita" il componente successivo. \ No newline at end of file +In pratica ogni volta o estrae di nuovo "se stesso" oppure "abilita" il componente successivo. + +Implementation: $$Impl \triangleq (B_{1}|A_{2}|\dots|An)$$ +basically we need to have an initially habilitated process, which can be any (the first one in our case). + +This will generate the LTS: \ No newline at end of file