From 4ff6e7d431aa1df2d6c13d27ff8e18788b4547d0 Mon Sep 17 00:00:00 2001 From: Marco Realacci Date: Wed, 30 Apr 2025 18:03:22 +0200 Subject: [PATCH] vault backup: 2025-04-30 18:03:22 --- Concurrent Systems/notes/13 - Weak Bisimilarity.md | 7 +++++++ 1 file changed, 7 insertions(+) diff --git a/Concurrent Systems/notes/13 - Weak Bisimilarity.md b/Concurrent Systems/notes/13 - Weak Bisimilarity.md index 3a8e6d8..4b83116 100644 --- a/Concurrent Systems/notes/13 - Weak Bisimilarity.md +++ b/Concurrent Systems/notes/13 - Weak Bisimilarity.md @@ -145,3 +145,10 @@ LTS for $n=2$: We can try to implement the scheduler in the following way: $$A_{i}=a_{i}.B_{i} \quad B_{i}=\bar{c}_{(i \space mod \space n)+1}.C_{i} \quad C_{i}=b_{i}.D_{i} \quad D_{i}=c_{i}.A_{i}$$ +- actions of kind $\bar{c}$ are needed to signal to the next process (i.e., with the next index) that it can start working +- actions of kind $c$ are needed to receive from the previous process such a signal + - such actions implement a token ring; the token is initially given to the first process: $$S=(A_{1}|D_{2}|\dots|D_{n})\setminus _{\{ c_{1}\dots cn \}}$$ + +Is the implementation correct? Or, in other words, $S ≈ S_{1,∅}$? +No (ci sono rimasto male anche io). +