vault backup: 2025-04-28 17:56:27

.obsidian/app.json

@@ -0,0 +1,12 @@
+{
+  "alwaysUpdateLinks": true,
+  "pdfExportSettings": {
+    "includeName": true,
+    "pageSize": "A4",
+    "landscape": false,
+    "margin": "0",
+    "downscalePercent": 84
+  },
+  "useMarkdownLinks": true,
+  "newLinkFormat": "relative"
+}

.obsidian/workspace.json

@@ -6,7 +6,7 @@
       {
         "id": "ceb8ca67f2b32f40",
         "type": "tabs",
-        "dimension": 40.83094555873926,
+        "dimension": 59.43977591036415,
         "children": [
           {
             "id": "56150e6df7869900",
@@ -27,7 +27,7 @@
       {
         "id": "e6a32eeb8d1da29c",
         "type": "tabs",
-        "dimension": 59.16905444126075,
+        "dimension": 40.56022408963585,
         "children": [
           {
             "id": "6c4a39240e6da514",
@@ -213,6 +213,7 @@
   },
   "active": "56150e6df7869900",
   "lastOpenFiles": [
+    "Pasted image 20250428175449.png",
     "Concurrent Systems/slides/class 13.pdf",
     "Concurrent Systems/notes/13 - Weak Bisimilarity.md",
     "Pasted image 20250428085837.png",

Concurrent Systems/notes/13 - Weak Bisimilarity.md

@@ -96,3 +96,10 @@ Furthermore, we should also consider commutativity of parallel in pairs of the s
 Thus, R is actually made up of 1+6+2+2+9+6+6+2 = 34 pairs.
  *exercise: write down the LTSs*
 
+### EXAMPLE: Lottery
+We want to model a lottery L where we can select any ball from a bag that contains n balls; after every extraction, the extracted ball is put back in the bag and the procedure is repeated.
+
+The specification is: $$L \triangleq \tau.\bar{p_{1}}L+\tau.\bar{p_{2}}.L+\dots+\tau.\bar{p_{n}}.L$$
+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)
+