diff --git a/.obsidian/app.json b/.obsidian/app.json
index e69de29..88a03a4 100644
--- a/.obsidian/app.json
+++ b/.obsidian/app.json
@@ -0,0 +1,12 @@
+{
+  "alwaysUpdateLinks": true,
+  "pdfExportSettings": {
+    "includeName": true,
+    "pageSize": "A4",
+    "landscape": false,
+    "margin": "0",
+    "downscalePercent": 84
+  },
+  "useMarkdownLinks": true,
+  "newLinkFormat": "relative"
+}
\ No newline at end of file
diff --git a/.obsidian/workspace.json b/.obsidian/workspace.json
index f83ad92..9107af6 100644
--- a/.obsidian/workspace.json
+++ b/.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",
diff --git a/Concurrent Systems/notes/13 - Weak Bisimilarity.md b/Concurrent Systems/notes/13 - Weak Bisimilarity.md
index d90616e..c3f701f 100644
--- a/Concurrent Systems/notes/13 - Weak Bisimilarity.md	
+++ b/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)
+
diff --git a/Pasted image 20250428175449.png b/Pasted image 20250428175449.png
new file mode 100644
index 0000000..0882ff4
Binary files /dev/null and b/Pasted image 20250428175449.png differ