最簡試例

讓兩個 threads 交替輸出 'a' 和 'b'（應該沒有更簡單的例子了吧 XD）。以下的 P 是 specification，Q 是 implementation。目的是證明 P ≈ Q（P is weakly bisimilar to Q）。

Q 上一次可能的 atomic experiment：

未來希望從這段 Haskell 程式產出和 Q "structurally congruent" 的式子：

import Control.Concurrent
import Control.Concurrent.MVar

emit :: Char -> MVar Char -> IO ()
emit c m = 
  do d <- takeMVar m
     if c == d
        then do putMVar m c 
                emit c m 
        else do putChar c
                putMVar m c 
                emit c m 

main :: IO ()
main =
  do m <- newMVar 'b' 
     forkIO (emit 'a' m)
     emit 'a' m

--
看起來好難 XD。