diff --git a/.obsidian/workspace.json b/.obsidian/workspace.json index 2ebf1a9..03206f0 100644 --- a/.obsidian/workspace.json +++ b/.obsidian/workspace.json @@ -68,8 +68,7 @@ "title": "class 11" } } - ], - "currentTab": 1 + ] } ], "direction": "vertical" @@ -239,8 +238,9 @@ "companion:Toggle completion": false } }, - "active": "364a7591f14f033a", + "active": "84845736e00d5c98", "lastOpenFiles": [ + "Pasted image 20250414181443.png", "Concurrent Systems/slides/class 12.pdf", "Concurrent Systems/notes/12 - CCS (che non so cosa voglia dire).md", "Concurrent Systems/slides/class 11.pdf", diff --git a/Concurrent Systems/notes/12 - CCS (che non so cosa voglia dire).md b/Concurrent Systems/notes/12 - CCS (che non so cosa voglia dire).md index 526cf69..09390d1 100644 --- a/Concurrent Systems/notes/12 - CCS (che non so cosa voglia dire).md +++ b/Concurrent Systems/notes/12 - CCS (che non so cosa voglia dire).md @@ -177,4 +177,11 @@ $$\frac{a.A' \xrightarrow{a} A' \quad A \triangleq a.A'}{A \xrightarrow{a} A'} since $b$ is in $\{b, \bar{b}\}$, we will NOT see the transitions: $$\frac{\frac{\frac{b.B' \xrightarrow{b} B' \quad B \triangleq b.B'}{B \xrightarrow{b} B'}} {{A \mid B \xrightarrow{b} A \mid B'}}b \in \{b, \bar{b}\}}{{(A \mid B) \setminus b}}$$ -This time I won't split it in separate pieces since I don't feel like doing it, just buy glasses. \ No newline at end of file +This time I won't split it in separate pieces since I don't feel like doing it, just buy glasses. + +###### So... What if we restrict on b? +- The effect of the restriction on b is that we have deleted the transitions involving b (hide all transitions labelled with $b$ and $\bar{b}$). +- Notice that the τ, even if it has been generated by synchronizing on b, it is still present after applying the restriction on b! + - the purpose of the τ is exactly to signal that a synchronization has happened but to hide the event on which the involved processed synchronized. + +- In general, it is possible that whole states disappear upon restriction of some names: this would be the case, e.g., if we consider the LTS arising from $(A’ | B)\setminus a,b$:![](../../Pasted%20image%2020250414181443.png) \ No newline at end of file diff --git a/Pasted image 20250414181443.png b/Pasted image 20250414181443.png new file mode 100644 index 0000000..7ee09cc Binary files /dev/null and b/Pasted image 20250414181443.png differ