いろいろ考えたら無限の内部遷移()のループに陥る可能性があることを プロパティでかけばよいではないか。 prop can_livelock = min X = livelock_now \/ <->X prop livelock_now = max X = <t>X最大不動点と最小不動点の組み合わせたプロパティになる。 proc X</t>…
引用をストックしました
引用するにはまずログインしてください
引用をストックできませんでした。再度お試しください
限定公開記事のため引用できません。