Strong Bisimulation Checker

今までにみた関係を覚えておくことで、くるくる回ってもいいようにしてみた。ソースがいよいよ汚い。

import Control.Monad.State
import Control.Monad (liftM)

trans = [("p0","a","p1"),("p0","a","p2"),("p1","b","p0"),("p1","a","p2")
        ,("p2","b","p0"),("p2","a","p2")
        ,("q0","a","q1"),("q1","a","q1"),("q1","b","q2"),("q2","a","q1")
        ]

simulates p q = evalState (simulates' p q) []
simulates' :: String -> String -> State [(String, String)] Bool
simulates' p q =
    do sims <- get
       if elem (p,q) sims
         then return True
         else 
           let t1 = [ (s,l,t) | (s,l,t) <- trans, q==s ] in
           let f (ss,ll,tt) = [ (t,tt) | (s,l,t) <- trans, s==p, ll==l ] in
           let t2 = map f t1 in
           do modify ((p,q):)
              let g l = liftM or $ mapM (uncurry simulates') l
              liftM and $ mapM g t2
bisimulate p q = simulates p q && simulates q p

めんどいので LTS の図示はしませんが、遷移がくるくる回っています。

Main> bisimulate "p0" "q0"
True
Main> bisimulate "p0" "q1"
False
Main> 

evalState を runState に変えれば、simulation な関係の中身が見られます。