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

---
 .obsidian/workspace.json         | 45 ++++++++++++++++++++++++++++----
 Concurrent Systems/notes/13 -.md |  9 +++++++
 2 files changed, 49 insertions(+), 5 deletions(-)
 create mode 100644 Concurrent Systems/notes/13 -.md

diff --git a/.obsidian/workspace.json b/.obsidian/workspace.json
index 1455b79..5c30757 100644
--- a/.obsidian/workspace.json
+++ b/.obsidian/workspace.json
@@ -6,9 +6,10 @@
       {
         "id": "ceb8ca67f2b32f40",
         "type": "tabs",
+        "dimension": 42.76504297994269,
         "children": [
           {
-            "id": "84845736e00d5c98",
+            "id": "fc3ff5f9792d4a40",
             "type": "leaf",
             "state": {
               "type": "markdown",
@@ -20,6 +21,40 @@
               "icon": "lucide-file",
               "title": "12 - Calculus of communicating system"
             }
+          },
+          {
+            "id": "9d3f25b0eb9b478f",
+            "type": "leaf",
+            "state": {
+              "type": "markdown",
+              "state": {
+                "file": "Concurrent Systems/notes/13 -.md",
+                "mode": "source",
+                "source": false
+              },
+              "icon": "lucide-file",
+              "title": "13 -"
+            }
+          }
+        ],
+        "currentTab": 1
+      },
+      {
+        "id": "7fb7c9cd25b3003c",
+        "type": "tabs",
+        "dimension": 57.23495702005731,
+        "children": [
+          {
+            "id": "46d9dfa1750fc4db",
+            "type": "leaf",
+            "state": {
+              "type": "pdf",
+              "state": {
+                "file": "Concurrent Systems/slides/class 12.pdf"
+              },
+              "icon": "lucide-file-text",
+              "title": "class 12"
+            }
           }
         ]
       }
@@ -191,13 +226,14 @@
       "companion:Toggle completion": false
     }
   },
-  "active": "84845736e00d5c98",
+  "active": "46d9dfa1750fc4db",
   "lastOpenFiles": [
-    "Concurrent Systems/notes/11 - LTSs and Bisimulation.md",
+    "Concurrent Systems/notes/13 -.md",
+    "Concurrent Systems/slides/class 12.pdf",
     "Concurrent Systems/notes/12 - Calculus of communicating system.md",
+    "Concurrent Systems/notes/11 - LTSs and Bisimulation.md",
     "Concurrent Systems/notes/images/Pasted image 20250414164549.png",
     "Concurrent Systems/notes/images/Pasted image 20250414181443.png",
-    "Concurrent Systems/slides/class 12.pdf",
     "Concurrent Systems/slides/class 11.pdf",
     "Concurrent Systems/notes/images/Pasted image 20250414173011.png",
     "Concurrent Systems/notes/images/Pasted image 20250414082824.png",
@@ -232,7 +268,6 @@
     "Concurrent Systems/notes/6a - Alternatives to Atomicity.md",
     "Concurrent.md",
     "Concurrent Systems/ignore this folder/Untitled.md",
-    "Foundation of data science/notes/9 XGBoost.md",
     "HCIW/slides/1 Interface and Interaction for IoT.pdf",
     "Concurrent Systems/slides/class 4.pdf",
     "Foundation of data science/class 9.pdf",
diff --git a/Concurrent Systems/notes/13 -.md b/Concurrent Systems/notes/13 -.md
new file mode 100644
index 0000000..a60a1d1
--- /dev/null
+++ b/Concurrent Systems/notes/13 -.md	
@@ -0,0 +1,9 @@
+An n-ary semaphore S(n)(p,v) is a process used to ensure that there are no more than n istances of the same activity concurrently in execution. An activity is started by action p and is terminated by action v.
+
+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)}$$
+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_{2}^{(2)} \triangleq v \cdot S_{1}^{(2)}$$