From ef831cf444b580e14776776b21a7da8380d65b15 Mon Sep 17 00:00:00 2001 From: Marco Realacci Date: Mon, 14 Apr 2025 18:15:00 +0200 Subject: [PATCH] vault backup: 2025-04-14 18:15:00 --- .obsidian/workspace.json | 6 +++--- .../12 - CCS (che non so cosa voglia dire).md | 9 ++++++++- Pasted image 20250414181443.png | Bin 0 -> 10863 bytes 3 files changed, 11 insertions(+), 4 deletions(-) create mode 100644 Pasted image 20250414181443.png 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 0000000000000000000000000000000000000000..7ee09cc7b0316cfac625ac86a3a96dacf5bc04aa GIT binary patch literal 10863 zcmX9^bzGC*_eVq+NR0RZ(hb6-q!}@!yJbql=6PIGnXF#kn*4l=jKy@aJhGbnntYC|+L|UlBO7!Q%}n!}Qs%H09w9$Yd_5Ms;J(#I zAP?r$&r}^?TR>)OMI`TG7pmMB{r5Z1nrLmf6rx*jmkXE%9^o;aAK{o#-yV$-Z_VNE z6)?$1gSZLByd+ZygDx)pa?H_tqPu3Mr?8`M>BY>qZqY03UXt3l(H*RxSwF+Tr7WN! zL6Fe305NUsnj{Xo2^XCJy`jghd8W>jYvYlZq>>O1pS;<>998ODXI&&vHYl=5s*$mS zXWPJ2Y#zYgDCwmu!oiBLrOtQ^cS8KQ&V9{mJk9EzfKe|qO*xySdyBTJIKIj}uCdwn1h4+18{K6;rl*X)Ayg<_9F`=x1i%)Y7Q&t2to zojIqh4BSsc7^PX~SAL;Dc>#7rjjjayt@#u{YFDG6X&a z$HKrY2S$d^^dwSV_iR-uD{hoU&OVm|%~oPWw6LCUQawP-OvsxN+Nhq@>6WCs<-Xlf(8tOnL;J-vN1+6xtsAAouv4268E@`@YmuRO3Px^rGG$U~^R3G$wFGUPioo;g)O z!hdXhH|6oI45gZ7+qwT*Pq zcC3}4OTi<&i1i@G02-D{uXqn1U>thQ@__++(!&B$_UL#sEW?1@mEhMZQIU{hQ;@@_ zwLw0s)Z&UPE2U993|aJJ!1x}rM^BNHDk^T=hpo|$o;^XHq%o%qLorZEu9UcKR;1Fw zi+F}qcJ@Rs23(4H`M#APR=wznH$!?ybN4O3xVSHpU5PQx)6YGfNLlY>nxMK!Q+YH$ zC3GZh4>*qb{%@Z$b*l$uEWaAe=lm(ZZEB`7a9!@*A|Y z3!QhS7_n*<6PY@ZESV?-vbpG`$p_b~U$e8bTk0jcZ)N1LE@E}v-82HS{VgpkU3&IJhY-E ziu_!eX1O|u+#cHCuer|=j3r`y*ejTDqro#CZC+O>6#kHSgYDLCs%)N zCY=LZ0aPMOe5i5;IAG~2EYN1<6l)QFFi0To{!0X=_FDwxV|KUe9v-~*^}nKN_v<%T zvZMR%gq`dP%%B$@xItZ4ii1F`?C!#|vrx&qdwV}?r~JBmn|=J9g7Ux0hDJlti1;Rs zgj~T@k1EU$-@^5dli=;fkp1AgQj>*+NA&a<5ysBF*{?(jvgn6-nsz~Up9P68c`b!V zpD|eWw6p}@T%PF2UaZzN_SH@~HEdt@2_#yV=q?4`4w1=yvlW(#s07TZuH{vuKm;x- zm6&7l?EMrshF-y?%7QJ$@SV^sRGf~!fq~v-P;;K09k<1oW_bnSDfqRHIJm;XVY+ow zl!qNGiMfN3JYuJ(#6zRW$*yiLF7B@A?}Y^2{D~PEnEcAHo2i^#zpE4RFb6nS1$)J> zZ{Iq@Z`Z^7{B~zgwz2)Um)in;=hikhLn33^RR;VybyK`2vr2lCzA{*sX|WG z3jO>_we-n#&qZ>%3|TeB4Q|}R>lk9x#}{J@g}Ww@A_1z8?d`lTvnE!{OKYQ)_0orH zHaA_wUYc7p8rMP5akQf%*=Vfu$yoB=Ns$1?+FDM7F9B@iA%_<~jbpl2qEwQRlq;Ps zHHJZlBQ$(jUw{ApJysyT7=Cx-*IkHS4?l=v?r3nH`-p(o8`qgPHoku^krE{o8^@hf zkei!ZTr7~Ko}j2;WW*z}KVp?)lJAiSCchMf{^c^@+S%QWu?kq*TC8}wsmayd+uPRC zRyg+O6&rEFu%|p-3&sxq{mja4{i@Gu_>-WaQN1oC>|~9G4}~gaam&QI3;ZJTG^sQ0 zzw*a2U^kIE_^|`LiKV>iVg)kcx7U1)J%3w@Z+5mD`~4W~gMxy*ye7Dtl;%Fp;bkL4 z>5|vh)+#D0Qe`hkk9th`{g*$*?1!Co9~~Xl7^-7^gQ(Qk!f4l9pGvbGM{Fp?GkZu0 z+2KVD(egEWE&m=#NFaozE5asy%+f2sD{d!Lc2w{uTG|cu4O|(A8Uj5_QLCecZ)H_% z0!Q>6ZOVFl&Q9Ci-U^IAu5fU|Rp*To3Ue@5g=2U?GVX_HP&b}~}s zoJ8{*?+)TfYb1OaUM|I$K%1I-4Ey}|x7wU*E3J|OiyE=p^~&sWvfl-X4XLf)JLdBw z-jvzAYs}Rg7Cy{nOUV48(r=O5LFp4b_mMtXx!(Atg++hp)#>c)i)5xCITz|(j7oOo;ZRfO zqRh+XC;BvW98}5yt*oapZC`K`r%OILImyb(Qm@c˦uGBXz!7x#NCf0~>$gfdk{ z1ttb8_HCWXD%+j>OF#KWjy~@fE{nD$ZqSakF@Nruri(n%xW1e{h#gEMz=2VPF7~%~ zZC%}V&cM|o-->-<$8Xs7WZ+htSW?u=&eG&f6Bd!m2)^_ly!x`+c2P^gKU5yx~L!NAeuT8qdY-d5Jh+Nu z4m%IOI}3lavCpWTy;k?UvG4jX>IO^xR75da7JU3QH|3>kD+Kiy>aI)Sb6_Ub~{rmSlceht}M{;-UY7@?ly{DJkjXGLdn_Xd4TFhFDJ9~R>Zf-B|`u4pU z>}fxDdaoyr{08AZzW#SZmv?V`?zei4TL}?2y$0LvlAge?ETqd}{JFotsKlg@e*KwD zgc9~-t%6ev!ympbo$uyi#LIy%JZK3)C6?3*k&K2$a#%7e-aUhXiHCrQurM*{2spH+ zjkO3l97(1Z_w)DXR7)JORzRo9*$P5XT@4yhycS^>Yd}%W&d#Pwj)kDU*rv-?lb7^A z^6B=49gqgc`%pb7ng1e>Y3=RptshgDEf#3ZF~g3nA@h?zfBl#!0N$&;90$w{n5 z5&QCLOm@^IWyR2l5eUeF0=_KuqV?#c^7iDk5AlF4u%^3y;MeC20 zHL=NV%x2WNR?h<=vd-?=IfJK03UTZ3*PQy*%yEsA4hf@7e;w zM1oY&yS%M|xZby4^22>0^^_Isrs*uc=gl)a()&F}zk>IT>ZUAiww?oNUYIya_ARZA z9@XP|Mx-89MKSm6b2UjrMcHG$AC2XuB$qm$^7gi5yT0>rJPeG-A5Mxcd0jdnb3c;E z4+n}yt{i%=f3Lu7cKh##0ks*5UiXru>weeuO1x%BCcMPbq}0@P zuTCI;qUG-1TIE_d@eEzz(K5dt`MUNO04UOh+O)BS+Ut7@-GF7^tBS(_Z+=E1<76Hu zQSj+>Od8SVr(i`&79`nFx^D-H1}m18)F!AnA7Mq+!tiJ22|}fT6Yc0YuadiQL?G67 z+ZS)E!Y{d zhhMKS8yFdY@#f~{{P%w?Oi!~In3tJAzJLD?1R=SiB!H0D==k`zPT76U&?+DX=iku- zB+@Jw3y6?Zl+UJuTDmPEHOa(i7wmd;#YZPX)*h_T?zV8b!hF}!*LPb7oNyb~T!Vu` zB+vA}HC+ zc-(iTQSLfq`gej}RnU{*k_rKaJjt|3V_24zmN+5xA|8M7=Pho{SKt?>rq|f;o9ByX z;YS6FJ?Fn)M~QY)k(cNYRPWE5kN5cv?V`5@1E&`p(RXRD`6gNQ6U=ZqH0MX6vo~kg1+RmMhN-&a3eIhKg z@b*3YJu)*h(+Ko*-wUN%(@lbmagH{ENr-YNL7Y3*IcZ zUp+G}V(bbk5+jys?onU9d;zvuUtgb`oczxoq3Jz+%ZYE_h=&B7ot@c7>HaONs5`T> zx@yat_2T8rvdiugFDbx_C1_IQ=g&am`}y-H=>K>1FsZ3wJ5Teo$e3M=GBwYm`?xi+I7iLW^=;4L0-YzYKqV`Bs4R=^DbN1y&pz1JnY4(!}@?&ZsuX)!4t)bksr z{3OBIYYLo^5(I~mBeZ+Zl^a2eZPB>QnPDw9J0e_VUqsZFX-+ZG5X zw{Uh4t`??w1_0i{!NLC`%+0d&Sf@fiWkrN8nU#?fn3BeprwOd+%{L_YKNn0Ms&Y`2 z@{kI^|LwAx@QIqf$m1jrWf0@*k;~{5(-cru(fDD2sgV(?Ig*9;vmTp*3hm<(Uo&yy zp^vUe&sfjQe})hwHB~xxHAttdbh+IPQ9=Pq2E=YwrI3vZm?ot`?t491YC~_o}COt`;H-s`n8f;daNgC+14NHf3!Ky zu4oD3<6#acvZwt6lqo)F}xekyK-tg80$&|lWE zq?ynF+i?b@$2e8)ib*VSPT5LQ?#+{XT$3On(#Y|n&{cvkT5xyLGcJyPJ9unG^dCuW zssKGI#iI2D%1`Ox%2p-a^8`O*Vexw4bJ(j8Ign*f^q6HCJe$?#f%-!zH&GcXE1J)ag zJsA**gUJ(|f1vw-bfhj4E26=JQ7b8>QK{*VdR$fc;Cq}Spiip;!5d>|03Rn)p#NxN z`F+5!y1RW zmJWiZ%g4xbL45HYkBCNj(|Sx;C0SHo9wUvY7OK@1?VH;9-3TX}qS7Hup39z9%+SM- zS>ya!e6}L%|QVSiIpn0 zqw;gC8_=o@4-W&VlV#w6Trc;PphA)>S(|2^Yd*3BIV3|Ce-AIUz>4-6Lh0VlF@`cf zh%OAA`w=7j1m*W;J%+Y;wEi8Lr+d*Wn|!u|>zZzKs5Fq`ftEt{a)TWP{v>z|ZPc&% z0FegJr?+NTgGIMry$M8Lp_s(d>y{K(%pbC?I1P;#Bo2*sp%_^)F@7Gw(X06_LgM_= znjw1HulFOuKrCuZ?#FTvXwcH?^XOKsIwR*FDh0jF&Q3`fc!M2aXiz{c_I%!Gp2d-{ zBB7Sf#m$YTD0mEAEs!UhlXes{Fkp;jRT#B{r^I>WaiK)^f=An#LK7S(KPgqaO8;ZB zV@pOpTg5|dpLwKG2Ewx9N{t^eUAj{l8Ce7@$GoNynCJ(1F36K738m*{%r~kS5h+$K z&vSzvxJ(iYu`5>873bO?gb37kssdbkKDsa%lmJk=dhEovHv>w%BHIuR)fs!u2 zl4pjY{5XUiDPk}|sK*ur-2B23Jc*$?m)~$GVmo#TU@lMm1=T)Bpp^% zOr43pD?0=it#uTw$G`*)6CXrlDtB{Jo=!gKkBxJ4dPhLln!bFaI&rt!Zm;|yhEPct z{DQQnH#D5beLoZwIdIaG;wrraVW2(Sgbz& zP^+rPkT;O77(Fyd5!=Be%!p;*1lgVAuxm7nRj!;5TD_guaY)Kz!8zKIXwdoX{EUfL zhKH2pUV_VL7876M#aLU*A7lJDeh_@X}N2N)HDY50G|B-25`h_f0le&7>1T)R_92|@2iEmDpoyH z!%dKRBXy#v9R~y;Hw!c}kZ-h1dFA-TW>e5~HI8+dK&P?41`JMkh1KCc@vN0`%#NNg z#j6$h;J@0!J^SoV>i90~O?~M3xCAkbHg4dDBt^-iSdfVfbDHBAtV}Xwpm!ZtZp`-Q z+42$r+1VqN{u4zglRrb%l+zC#d~r+dCxVicRCtDpSbNZvD6wp7RF!5H6WQHX-_~8p zBGX4cwn7l;Y4lk)gKYP~vCEkK}((^Kd@a>5>SR4>QX^ zZ~gnP76vW^Q?`8}1?EB1G$FrDvX$0E4{BlYc0CZ37o&=?E&9lGt}=ra>6xD#>-v&` zz$vU{K};)S{lQ#wzK59FSt!3k_8|w)=q+(Of)ga$$u~Z zD8sS7dg-48Gdcbd&-TuI#mwyxZ(jtWt{GluG$iPu_Q}oFx6Qcz^Y6piy@u_s+Dbs# z$@{bSJtZ|nEnU@9LnoaudN`8Bsg^Cn92CcC{4R*xrg%F2_J}4L*89R$jDAF44IG{P zH>mzau$vVOBSIUoPIqY1JvCd0HOTYf&1x{J^LG=#?~^l!6iJJ>w6tJcMC{h>+S@-; z))I$Bsxx{Fi8ERXS3HJUdF!IO5@Z7=n&d}1)+|5?k*eeg7$mQ zIMjr-T6B3xy5%Qx(Mg{}2eXd@+TSmtF zd-J!T-UfPQwlohj|6penS;&y!?*v6Rhz>==fd5*QEGX56Of z3c_QUay1@n?8SyhK0zvRB#UX6&*MVve`*L20f(V- z0I7pUuOD6X2_T_11GMh0uA$e5NEq0(CqO9U3!p)ugta0kLby+a)TY$V_>Rqzq3HOL zyCQ!-wTmb3jI`*@Az8B2Ncy=tD&#pgy^U_7~l7MsqgwF-b^t?_kY?1cF&GR$8E^VX0hF=+V=c^R<=N&WNqd}0w(V+}S70w@)3&A4xCL(BFaA_o zrM*JWlf8mRVrZx$Wd{5L;HM!m@RZNT{2gFVLLWOJ|^xlWPuKEEz7t5G`Tu z7Y*yA72yZ*F#Dn7g#~o-Q?wH_Wko^@lRx$cV1tH^LTU{23k%2AkG#FTa|A5HZZFnf zkLb5Mw4OcLVpVT8Y@BkLOXqx?rrtzsP-FP{;Ya}6k2$IUU5?D>I5mTTSOy!FNTTFA^MF6 z81JN)PQk&;OIgero$QKlq-Q7TzT*(Qd1wZWt8&w=#0mM7d zHX8D_b$9b6{+^zmHj$M(??cjRqz`+&-M6#Jooq7*0*aiUo<2W6KRu<^P#-+Al=bVj@$+HNR^>`SKkGc@ z`1>Pnq%t?ALlcbmKp0J_1@IT3IMWmM-sal`Mil4gGwD};6@}kk0DZA_lf=`f-T)ICBHK8szT{Kp=u^ZFk~fUjg=Fil`=n*^(AI>KVys}JYhIwhqIE5;{%I#Mt(J`Mw#dJMdOL}xaD1PkF98ry z$$Mr_Y)N3+m9a4`RC8rz1=7;g^7W=O z8*mehrQf}}{q_xld>5w9A#|K?QlQoC^kwk-M zhM7nR&@^I`O=aq+5-X8|Dh!P^H@w~g%j|W0zfsaBZIVsRXvFC^!`5S+py;ZnkG_`n zHEm<*GDMjFJkS$w)r8trZ?P{flXWmaBnEqUK%{{t8|DscBT@Fgi&J)A6b}ZSI`_^4 zi?F_oHuFwm&TUQrQ&9CZik{?raiQ$lwqOKJQKgM`bjCeV5i)Mi?*16CG`9v@+eDOC zO4J^9`7Djj+62-$(+V-rqhhBnn-`ScU0A3Egb$w=tgNmFtg7~s5$m~o4_7=h6w)$X z;ZSB`;xoQpvTDs)R(E<>LG@MOR|>jZL_aAAY7zrWu{QL{5BAnTjAb+Mxo5%9x+5Vu=N zElhP=g^E4d##H~ELD7Bn!P0x&dW0%R;kA_&m^{C_Ha&B)p%3PD3q77T2*;WQ7l6B} zZ-5v)A~IBYhLp{PEBb_Gv%Ze392KGP!0l%58gFW9GJ*CP)#MhYAo87^>na@!i^Bnt zWjAtjj#TJR07!52O}5+tYmlY94;NQLB-bqI1Cs&>5$u{#y{_ zw+IxXer?2?W!$3X62+2`K417)C4hR6A{zv4{F2U*Fs`*0efq_7eswi-|LW|gu^AQs zONH96OLH|V0*c(l^2=4ETJdq>)(H~v(o!N9T5_1H(mzlb?&$1*d zjSAPZ5F5db5ecc+$p%*C56qu)U~}#-%B7vW=c%f)x06ra35c;K42ymbstHsU|{L=+BD(x(H(uKSirzGlTmd9b1!RSw$h6Y@y0Z??u+njEU)ACNv# z0p;2E8R(4CL!Pi`dF$A9jQ<`Jto&X$WJUWL>6k=W`2|v@>Lrymj-c3%_fQ}3e#@`X zSBY=6q0l|P()Y!2Nit9KwA*arKavuVY8qu17jsF@Y+1YIBadq%C473uSf(#UZ{yR% zh|2`%-x=IvYTk~--}?G=B5~~{ZZ?8bPsFhL8K?f!vs_Q}{G=Vug;zunBvJWYXNgm7 z=^LeBrl|WoIuzW^EVR7utx?ge$2T&5CP9L!MEU_|i%zLbEBVyjt;;&LdD6foip5j#l&g|2$^TQp?gSMBX7Rbt7w>@qNH@TXR=} zRncOIZIYY{E#E;S2`-cDIML{?k8lH3TXyTCO+1aAR(=g=N9J3{dsV3z?>fFpu#!>9 zaX_;uQ#5kFaNXA$_MoVp;g@f5SjRD8L~bm^+2;Ytqgigbkp?!Xv?ZY-yj0;K%F}G( z59MT;${stW7!iRXzGn)5PNfyAwoLh`n|+E2GoiY%w81tPA)4}z@3Etp=WxzLqri+2 zOT|Z@d7X(i&WaA5Zb3SDv+X~X#??uGlKvf4aO_RD@6ujgI?b%}k$r&bBJ6>vH$!Tg z%hRE&25(kIQC+^lmvIg2bE7TG=REBjwzBIdI2wCT1BJYW*%ea%2rfzVRn$dnms