本日はTopSEセミナーにて、PATツールを使ってCSPを勉強しています。 ということで、PATのCSPモデルをSyncStitchのモデルにコンバート。 ; Definitions (define-event setorange) (define-event setlemon) (define-event orange) (define-event lemon) (define-event tomato) ;DrinkDispenser (define-process DD (alt (! setorange O) (! setlemon L))) (define-process O (alt (! orange O) (! setlemon L) (! setorange O) (! tomato STOP))) (define-process L (alt (! lemon L) (
![[SyncStitch]an example of deadlock - Qiita](https://cdn-ak-scissors.b.st-hatena.com/image/square/9cd62fe1b41df19dc4a3c0333020ff3b3557d671/height=288;version=1;width=512/https%3A%2F%2Fqiita-user-contents.imgix.net%2Fhttps%253A%252F%252Fcdn.qiita.com%252Fassets%252Fpublic%252Farticle-ogp-background-9f5428127621718a910c8b63951390ad.png%3Fixlib%3Drb-4.0.0%26w%3D1200%26mark64%3DaHR0cHM6Ly9xaWl0YS11c2VyLWNvbnRlbnRzLmltZ2l4Lm5ldC9-dGV4dD9peGxpYj1yYi00LjAuMCZ3PTkxNiZoPTMzNiZ0eHQ9JTVCU3luY1N0aXRjaCU1RGFuJTIwZXhhbXBsZSUyMG9mJTIwZGVhZGxvY2smdHh0LWNvbG9yPSUyMzIxMjEyMSZ0eHQtZm9udD1IaXJhZ2lubyUyMFNhbnMlMjBXNiZ0eHQtc2l6ZT01NiZ0eHQtY2xpcD1lbGxpcHNpcyZ0eHQtYWxpZ249bGVmdCUyQ3RvcCZzPThhMjdiMTM3ZmYyZTYwM2E5YmM3NTBhNWRhZTdiMmM3%26mark-x%3D142%26mark-y%3D112%26blend64%3DaHR0cHM6Ly9xaWl0YS11c2VyLWNvbnRlbnRzLmltZ2l4Lm5ldC9-dGV4dD9peGxpYj1yYi00LjAuMCZ3PTYxNiZ0eHQ9JTQwa2VuY29iYSZ0eHQtY29sb3I9JTIzMjEyMTIxJnR4dC1mb250PUhpcmFnaW5vJTIwU2FucyUyMFc2JnR4dC1zaXplPTM2JnR4dC1hbGlnbj1sZWZ0JTJDdG9wJnM9Y2ZmOTRjZmJmNjU4OTFkZDIzZDhlY2M1ZWZkYjI0MDA%26blend-x%3D142%26blend-y%3D491%26blend-mode%3Dnormal%26s%3D12a80b1b71de8194c5e7789a80a85765)