10時と3時に流れる牧歌的な職場体操は本当に気が抜けてまさにのびのびリラックス。誰も実際には体操していないけど。雨は嫌だなあ、というのはさておき、家では眠くて何もできないのが困った。特にインターンシップで疲れることをやっているわけではないのだ…

Uppaalを使い続ける。良い所は次の動作の選択肢が明示的に示されるところ。SPINにはそういう概念は特になかったはず…あんまり覚えていないけど。悪いところはGuardの中で他のプロセスの状態を参照できないところ。これは本当に意味がわからない。オートマト…