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 な関係の中身が見られます。