0276デフォルトの名無しさん2015/04/29(水) 11:04:46.37ID:mWtY0FPp 形式仕様なんてどれもクソだが クソ未満の非形式仕様が溢れかえっている喜劇 >>271 ミューテックスとセマフォの違いって排他制御の「実装」レベルの話なんじゃ 例えばデッドロックを回避する機構を入れたいなら そういうコードを書かなきゃいけない ミューテックスの一般的と言えるような実装がない以上 promelaでの一般的な記述もないような 余計なお世話かも知れんが モデル検査は排他制御のあるシステムの検証には適しているといえるけど それは排他制御を抽象化しての話 排他制御自体の検証には向いていないと思う