From f8a2d4a2d68a4c322f72946f6c12d455ef13aa44 Mon Sep 17 00:00:00 2001
From: Marco Realacci <marco@marcorealacci.me>
Date: Tue, 15 Apr 2025 16:15:01 +0200
Subject: [PATCH] vault backup: 2025-04-15 16:15:01

---
 .obsidian/workspace.json                         | 6 +++---
 Concurrent Systems/notes/12b - CCS cose varie.md | 4 ++--
 2 files changed, 5 insertions(+), 5 deletions(-)

diff --git a/.obsidian/workspace.json b/.obsidian/workspace.json
index 5a53c98..5ce5b0a 100644
--- a/.obsidian/workspace.json
+++ b/.obsidian/workspace.json
@@ -41,12 +41,12 @@
             "state": {
               "type": "markdown",
               "state": {
-                "file": "Concurrent Systems/notes/12 - Calculus of communicating system.md",
+                "file": "Concurrent Systems/notes/12b - CCS cose varie.md",
                 "mode": "source",
                 "source": false
               },
               "icon": "lucide-file",
-              "title": "12 - Calculus of communicating system"
+              "title": "12b - CCS cose varie"
             }
           }
         ],
@@ -221,8 +221,8 @@
   },
   "active": "a222ab88db5cfdd0",
   "lastOpenFiles": [
-    "Concurrent Systems/notes/11 - LTSs and Bisimulation.md",
     "Concurrent Systems/notes/12 - Calculus of communicating system.md",
+    "Concurrent Systems/notes/11 - LTSs and Bisimulation.md",
     "Concurrent Systems/notes/10 - Implementing Consensus.md",
     "Concurrent Systems/notes/12b - CCS cose varie.md",
     "Concurrent Systems/slides/class 12.pdf",
diff --git a/Concurrent Systems/notes/12b - CCS cose varie.md b/Concurrent Systems/notes/12b - CCS cose varie.md
index 472ff5b..03f0efa 100644
--- a/Concurrent Systems/notes/12b - CCS cose varie.md	
+++ b/Concurrent Systems/notes/12b - CCS cose varie.md	
@@ -2,10 +2,10 @@ An n-ary semaphore S(n)(p,v) is a process used to ensure that there are no more
 
 The specification of a unary semaphore is the following:
 $$S^{(1)} \triangleq p \cdot S_{1}^{(1)}$$
-$$S_{1}^{(1)} \triangleq p \cdot S_{1}^{(1)}$$
+$$S_{1}^{(1)} \triangleq p \cdot S_{}^{(1)}$$
 The specification of a binary semaphore is the following:
 $$S_{}^{(2)} \triangleq p \cdot S_{1}^{(2)}$$
-$$S_{1}^{(2)} \triangleq p \cdot S_{1}^{(2)}+v\cdot S^{(2)}$$
+$$S_{1}^{(2)} \triangleq p \cdot S_{2}^{(2)}+v\cdot S^{(2)}$$
 $$S_{2}^{(2)} \triangleq v \cdot S_{1}^{(2)}$$
 
 If we consider S(2) as the specification of the expected behavior of a binary semaphore and S(1) | S(1) as its concrete implementation, we can show that $$S^{(1)}|S^{(1)} \space \textasciitilde \space S^{2}$$