diff --git a/CHANGELOG.md b/CHANGELOG.md
--- a/CHANGELOG.md
+++ b/CHANGELOG.md
@@ -1,5 +1,9 @@
 # Revision history for typed-session-state-algorithm
 
+## 0.2.0.0
+
+* Fix Pipeline, add check and verify.
+
 ## 0.1.0.2
 
 *New protocol check function.
diff --git a/src/TypedSession/State/GenDoc.hs b/src/TypedSession/State/GenDoc.hs
deleted file mode 100644
--- a/src/TypedSession/State/GenDoc.hs
+++ /dev/null
@@ -1,199 +0,0 @@
-{-# LANGUAGE AllowAmbiguousTypes #-}
-{-# LANGUAGE ConstraintKinds #-}
-{-# LANGUAGE DeriveFunctor #-}
-{-# LANGUAGE EmptyCase #-}
-{-# LANGUAGE FlexibleContexts #-}
-{-# LANGUAGE LambdaCase #-}
-{-# LANGUAGE MultiWayIf #-}
-{-# LANGUAGE NamedFieldPuns #-}
-{-# LANGUAGE OverloadedStrings #-}
-{-# LANGUAGE PatternSynonyms #-}
-{-# LANGUAGE RankNTypes #-}
-{-# LANGUAGE ScopedTypeVariables #-}
-{-# LANGUAGE TypeAbstractions #-}
-{-# LANGUAGE TypeApplications #-}
-{-# LANGUAGE TypeFamilies #-}
-{-# LANGUAGE TypeOperators #-}
-{-# LANGUAGE UndecidableInstances #-}
-
-module TypedSession.State.GenDoc where
-
-import qualified Data.List as L
-import qualified Data.Set as Set
-import Prettyprinter
-import Prettyprinter.Render.String (renderString)
-import TypedSession.State.Piple
-import TypedSession.State.Render
-import TypedSession.State.Type (Creat, Protocol, ProtocolError)
-
-genRole :: forall r ann. (Enum r, Bounded r, Show r) => String -> Doc ann
-genRole rname =
-  let rg = rRange @r
-      sRole = pretty ("S" <> rname)
-      header = "data" <+> sRole <+> "::" <+> pretty rname <+> "-> Type where"
-   in vsep
-        [ nest 2 $ vsep $ header : [(pretty ("S" <> show r) <+> "::" <+> sRole <+> pretty (show r)) | r <- rg]
-        , "type" <+> "instance" <+> "Sing" <+> "=" <+> sRole
-        ]
-        <> line
-        <> vsep
-          [ nest
-              2
-              ( vsep
-                  [ "instance" <+> "SingI" <+> pretty (show r) <+> " where"
-                  , "sing" <+> "=" <+> pretty ("S" <> show r)
-                  ]
-              )
-          | r <- rg
-          ]
-        <> line
-        <> ( nest 2 $
-              vsep
-                [ "instance SingToInt" <+> pretty rname <+> "where"
-                , "singToInt x = I# (dataToTag# x)"
-                ]
-           )
-
-genSt :: forall r bst ann. String -> String -> PipleResult r bst -> Doc ann
-genSt protName bstName (PipleResult{dnySet, stBound = (start, end)}) =
-  let
-    protNameSt = protName <> "St"
-    sProtNameSt = "S" <> protName <> "St"
-    protSt =
-      nest 2 $
-        vsep $
-          ["data" <+> pretty protNameSt]
-            ++ [ if
-                  | i == -1 -> "= End"
-                  | i `Set.member` dnySet -> pretty ("| S" ++ show i) <+> pretty bstName
-                  | otherwise -> pretty ("| S" ++ show i)
-               | i <- [start .. end]
-               ]
-    protSSt =
-      nest 2 $
-        vsep $
-          ["data" <+> pretty sProtNameSt <+> "::" <+> pretty protNameSt <+> "-> Type where"]
-            ++ [ if
-                  | i == -1 -> "SEnd ::" <+> pretty sProtNameSt <+> "End"
-                  | i `Set.member` dnySet -> pretty ("SS" ++ show i ++ " ::") <+> pretty sProtNameSt <+> pretty ("(S" <> show i <> " s)")
-                  | otherwise -> pretty ("SS" ++ show i ++ " ::") <+> pretty sProtNameSt <+> pretty ("S" <> show i)
-               | i <- [start .. end]
-               ]
-    instVal i =
-      nest 2 $
-        vsep $
-          [ "instance SingI"
-              <+> ( if i == -1
-                      then "End"
-                      else
-                        if i
-                          `Set.member` dnySet
-                          then parens (pretty ("S" <> show i) <> " s")
-                          else pretty ("S" <> show i)
-                  )
-              <+> "where"
-          , "sing =" <+> if i == -1 then "SEnd" else pretty ("SS" <> show i)
-          ]
-    instVals = vsep [instVal i | i <- [start .. end]]
-    stoInt =
-      ( nest 2 $
-          vsep
-            [ "instance SingToInt" <+> pretty protNameSt <+> "where"
-            , "singToInt x = I# (dataToTag# x)"
-            ]
-      )
-   in
-    vsep
-      [ protSt
-      , protSSt
-      , "type instance Sing =" <+> pretty sProtNameSt
-      , instVals
-      , stoInt
-      ]
-
-genProtIns :: forall r bst ann. (Enum r, Bounded r, Show bst, Show r) => String -> String -> PipleResult r bst -> Doc ann
-genProtIns roleName protName PipleResult{msgT1} =
-  let
-    protNameSt = protName <> "St"
-    typeDone = ["type Done" <+> pretty (show r) <+> "= End" | r <- rRange @r]
-   in
-    nest 2 $
-      vsep
-        [ "instance Protocol" <+> pretty roleName <+> pretty protNameSt <+> "where"
-        , vsep typeDone
-        , nest 2 $
-            vsep
-              [ "data Msg" <+> pretty roleName <+> pretty protNameSt <+> "from send recv where"
-              , vsep (genDoc roleName protName msgT1)
-              ]
-        ]
-
-genGraph :: (Enum r, Bounded r, Show bst, Ord r, Show r) => StrFillEnv -> PipleResult r bst -> String
-genGraph sfe PipleResult{msgT} = runRender sfe (stMsgT sfe) msgT
-
-genAllDoc'
-  :: forall r bst ann
-   . (Enum r, Bounded r, Ord r, Show r, Show bst)
-  => StrFillEnv
-  -> Protocol Creat r bst
-  -> String -- role name
-  -> String -- protocol name
-  -> String -- bst name
-  -> [String] -- module Name
-  -> Either (ProtocolError r bst) (Doc ann)
-genAllDoc' sfe prot rName pName bstName moduleNames = case piple prot of
-  Left e -> Left e
-  Right pipResult1 ->
-    Right $
-      vsep
-        [ "{-# LANGUAGE DataKinds #-}"
-        , "{-# LANGUAGE FlexibleInstances #-}"
-        , "{-# LANGUAGE GADTs #-}"
-        , "{-# LANGUAGE MagicHash #-}"
-        , "{-# LANGUAGE MultiParamTypeClasses #-}"
-        , "{-# LANGUAGE TypeFamilies #-}"
-        , "module" <+> pretty (L.intercalate "." moduleNames) <+> "where"
-        , "import Data.IFunctor (Sing, SingI (sing))"
-        , "import Data.Kind"
-        , "import GHC.Exts (dataToTag#)"
-        , "import GHC.Int (Int (I#))"
-        , "import TypedProtocol.Core"
-        , "{-"
-        , pretty $ genGraph sfe pipResult1
-        , "-}"
-        , genRole @r rName
-        , genSt pName bstName pipResult1
-        , genProtIns rName pName pipResult1
-        ]
-
-genAllDoc
-  :: forall r bst
-   . (Enum r, Bounded r, Ord r, Show r, Show bst)
-  => StrFillEnv
-  -> Protocol Creat r bst
-  -> String -- role name
-  -> String -- protocol name
-  -> String -- bst name
-  -> [String] -- module names
-  -> Either (ProtocolError r bst) String
-genAllDoc sfe a b c d e =
-  renderString . layoutPretty defaultLayoutOptions
-    <$> genAllDoc' sfe a b c d e
-
-genAllFile
-  :: forall r bst
-   . (Enum r, Bounded r, Ord r, Show r, Show bst)
-  => StrFillEnv
-  -> Protocol Creat r bst
-  -> String -- role name
-  -> String -- protocol name
-  -> String -- bst name
-  -> [String] -- module names
-  -> IO ()
-genAllFile sfe a b c d e = case genAllDoc sfe a b c d e of
-  Left er -> print er
-  Right st -> do
-    let name = case e of
-          [] -> "Type"
-          xs -> last xs
-    writeFile name st
diff --git a/src/TypedSession/State/Parser.hs b/src/TypedSession/State/Parser.hs
--- a/src/TypedSession/State/Parser.hs
+++ b/src/TypedSession/State/Parser.hs
@@ -12,8 +12,7 @@
 import Text.Megaparsec hiding (Label, label)
 import Text.Megaparsec.Char (char, space1, string)
 import qualified Text.Megaparsec.Char.Lexer as L
-import TypedSession.State.Pattern
-import TypedSession.State.Type (BranchSt, Creat, MsgOrLabel, Protocol)
+import TypedSession.State.Type
 
 {-
 
@@ -105,24 +104,24 @@
   args <- brackets (constrOrType `sepBy` comma)
   from <- mkParserA @r
   to <- mkParserA @r
-  pure $ Msg constr args from to
+  pure $ Msg () constr args from to
 
 parseLabel :: (Show r) => Parser (MsgOrLabel Creat r)
 parseLabel = dbg "Label" $ do
   label
   i <- fromIntegral <$> integer
-  pure $ Label i
+  pure $ Label () i
 
 parseGoto :: (Show bst, Show r) => Parser (Protocol Creat r bst)
 parseGoto = dbg "Goto" $ do
   goto
   i <- fromIntegral <$> integer
-  pure $ Goto i
+  pure $ Goto () i
 
 parseTerminal :: (Show bst, Show r) => Parser (Protocol Creat r bst)
 parseTerminal = dbg "Terminal" $ do
   terminal
-  pure $ Terminal
+  pure $ Terminal ()
 
 parseBranchSt
   :: forall bst r
@@ -132,7 +131,7 @@
   branchSt
   bst <- mkParserA @bst
   prot <- parseProtocol @r @bst
-  pure (BranchSt bst prot)
+  pure (BranchSt () bst prot)
 
 parseBranch
   :: forall r bst
@@ -142,7 +141,7 @@
   r1 <- mkParserA @r
   braces $ do
     branchSts <- some (parseBranchSt @bst @r)
-    pure (Branch r1 branchSts)
+    pure (Branch () r1 branchSts)
 
 parseMsgOrLabel
   :: forall r bst
diff --git a/src/TypedSession/State/Pattern.hs b/src/TypedSession/State/Pattern.hs
deleted file mode 100644
--- a/src/TypedSession/State/Pattern.hs
+++ /dev/null
@@ -1,29 +0,0 @@
-{-# LANGUAGE PatternSynonyms #-}
-
-module TypedSession.State.Pattern where
-
-import TypedSession.State.Type (Creat, Protocol)
-import qualified TypedSession.State.Type as N
-
-pattern Msg :: String -> [String] -> r -> r -> N.MsgOrLabel Creat r
-pattern Msg a b c d = N.Msg () a b c d
-
-pattern Label :: Int -> N.MsgOrLabel Creat r
-pattern Label i = N.Label () i
-
-pattern BranchSt :: bst -> Protocol Creat r bst -> N.BranchSt Creat r bst
-pattern BranchSt a b = N.BranchSt () a b
-
-infixr 5 :>
-
-pattern (:>) :: N.MsgOrLabel Creat r -> Protocol Creat r bst -> Protocol Creat r bst
-pattern (:>) a b = a N.:> b
-
-pattern Branch :: r -> [N.BranchSt Creat r bst] -> Protocol Creat r bst
-pattern Branch a b = N.Branch () a b
-
-pattern Goto :: Int -> Protocol Creat r bst
-pattern Goto i = N.Goto () i
-
-pattern Terminal :: Protocol Creat r bst
-pattern Terminal = N.Terminal ()
diff --git a/src/TypedSession/State/Pipeline.hs b/src/TypedSession/State/Pipeline.hs
new file mode 100644
--- /dev/null
+++ b/src/TypedSession/State/Pipeline.hs
@@ -0,0 +1,436 @@
+{-# LANGUAGE AllowAmbiguousTypes #-}
+{-# LANGUAGE ConstraintKinds #-}
+{-# LANGUAGE DeriveFunctor #-}
+{-# LANGUAGE EmptyCase #-}
+{-# LANGUAGE FlexibleContexts #-}
+{-# LANGUAGE GeneralizedNewtypeDeriving #-}
+{-# LANGUAGE LambdaCase #-}
+{-# LANGUAGE MultiWayIf #-}
+{-# LANGUAGE NamedFieldPuns #-}
+{-# LANGUAGE OverloadedStrings #-}
+{-# LANGUAGE PatternSynonyms #-}
+{-# LANGUAGE RankNTypes #-}
+{-# LANGUAGE ScopedTypeVariables #-}
+{-# LANGUAGE TypeAbstractions #-}
+{-# LANGUAGE TypeApplications #-}
+{-# LANGUAGE TypeFamilies #-}
+{-# LANGUAGE TypeOperators #-}
+{-# LANGUAGE UndecidableInstances #-}
+{-# LANGUAGE NoFieldSelectors #-}
+{-# OPTIONS_GHC -Wno-unused-do-bind #-}
+
+module TypedSession.State.Pipeline where
+
+import Control.Algebra ((:+:))
+import Control.Carrier.Error.Either (runError)
+import Control.Carrier.Fresh.Strict
+import Control.Carrier.Reader (runReader)
+import Control.Carrier.State.Strict
+import Control.Carrier.Writer.Strict (runWriter)
+import Control.Effect.Error
+import Control.Effect.Reader
+import Control.Effect.Writer
+import Control.Monad
+import Data.Foldable (Foldable (toList), for_)
+import Data.IntMap (IntMap)
+import qualified Data.IntMap as IntMap
+import qualified Data.List as L
+import Data.Map (Map)
+import qualified Data.Map as Map
+import Data.Sequence (Seq)
+import qualified Data.Sequence as Seq
+import Data.Set (Set)
+import qualified Data.Set as Set
+import Prettyprinter
+import qualified TypedSession.State.Constraint as C
+import TypedSession.State.Render
+import TypedSession.State.Type
+import TypedSession.State.Utils
+
+------------------------
+
+newtype Index = Index Int deriving (Show, Eq, Ord, Num)
+
+addIdxXTraverse
+  :: forall r bst sig m
+   . ( Has (State Int :+: State Index :+: State (Set Int) :+: Error (ProtocolError r bst)) sig m
+     , Enum r
+     , Bounded r
+     , Ord r
+     )
+  => XTraverse m Creat Idx r bst
+addIdxXTraverse =
+  ( \_ -> do
+      inputIdx <- get @Int
+      modify @Int (+ 1)
+      Index idx <- get @Index
+      modify @Index (+ 1)
+      outputInx <- get @Int
+      pure (inputIdx, outputInx, idx)
+  , const get
+  , \(_, _) -> do
+      inputIdx <- get @Int
+      modify (Set.insert inputIdx)
+      pure (inputIdx, id)
+  , \_ -> do
+      put (Index 0)
+      modify @Int (+ 1)
+  , const get
+  , const get
+  )
+
+reRankXTraverse :: (Monad m) => IntMap Int -> XTraverse m Idx Idx r bst
+reRankXTraverse sbm =
+  ( \((a, b, idx), _) -> pure (replaceVal sbm a, replaceVal sbm b, idx)
+  , \(xs, _) -> pure (replaceVal sbm xs)
+  , \(a, _) -> pure (replaceVal sbm a, id)
+  , \_ -> pure ()
+  , \(xs, _) -> pure (replaceVal sbm xs)
+  , \xs -> pure (replaceVal sbm xs)
+  )
+
+addNumsXTraverse
+  :: forall r bst sig m
+   . ( Has (Error (ProtocolError r bst)) sig m
+     , Enum r
+     , Bounded r
+     , Ord r
+     )
+  => XTraverse m Idx AddNums r bst
+addNumsXTraverse =
+  let mkNums i =
+        let sized = fromEnum (maxBound @r) + 1
+         in fmap (\x -> i * sized + fromEnum x) (rRange @r)
+   in ( \((va, vb, idx), _) -> pure (mkNums va, mkNums vb, idx)
+      , \(va, _) -> pure $ mkNums va
+      , \(va, _) -> pure (mkNums va, id)
+      , \_ -> pure ()
+      , \(va, _) -> pure $ mkNums va
+      , \va -> pure $ mkNums va
+      )
+
+toGenConstrXTraverse :: (Monad m) => XTraverse m AddNums (GenConst r) r bst
+toGenConstrXTraverse =
+  ( \((a, b, i), (_, _, from, to, _)) -> pure ((a, b), (from, to), i)
+  , \(is, (i, _)) -> pure (is, i)
+  , \(xv, _) -> pure (xv, id)
+  , \_ -> pure ()
+  , \(xs, i) -> pure (xs, i)
+  , \xv -> pure xv
+  )
+
+data CurrSt = Decide | Undecide deriving (Show, Eq, Ord)
+
+getRCurrSt :: forall r sig m. (Has (State (Map r CurrSt)) sig m, Ord r) => r -> m CurrSt
+getRCurrSt r =
+  gets @(Map r CurrSt) (Map.lookup r) >>= \case
+    Nothing -> error internalError
+    Just v -> pure v
+
+restoreWrapper1 :: forall r sig m a. (Has (State (Map r CurrSt) :+: State r) sig m) => m a -> m a
+restoreWrapper1 m = do
+  s1 <- get @(Map r CurrSt)
+  s2 <- get @r
+  a <- m
+  put s1
+  put s2
+  pure a
+
+checkProtXFold
+  :: forall r bst sig m
+   . (Has (State (Map r CurrSt) :+: State r :+: Error (ProtocolError r bst)) sig m, Eq r, Ord r, Enum r, Bounded r)
+  => XFold m (GenConst r) r bst
+checkProtXFold =
+  ( \((_, (from, to), idx), (msgName, _, _, _, prot)) -> do
+      when (idx == 0) $ do
+        r1 <- get @r
+        if from == r1
+          then pure ()
+          else throwError @(ProtocolError r bst) (BranchFirstMsgMustHaveTheSameSender r1 msgName from)
+      fromCurrSt <- getRCurrSt from
+      when (fromCurrSt == Undecide) (throwError @(ProtocolError r bst) (UndecideStateCanNotSendMsg msgName))
+      modify (Map.insert to Decide)
+      case prot of
+        Terminal _ -> do
+          vals <- gets @(Map r CurrSt) Map.elems
+          when (any (/= Decide) vals) (throwError @(ProtocolError r bst) (TerminalNeedAllRoleDecide msgName))
+        _ -> pure ()
+  , \_ -> pure ()
+  , \(_, (r1, ls)) -> do
+      r1CurrSt <- getRCurrSt r1
+      when (r1CurrSt == Undecide) (throwError @(ProtocolError r bst) (UndecideStateCanNotStartBranch ls))
+      for_ [r | r <- rRange, r /= r1] $ \r -> modify (Map.insert r Undecide)
+      when (length ls < 1) (throwError @(ProtocolError r bst) BranchAtLeastOneBranch)
+      put r1
+      pure (restoreWrapper1 @r)
+  , \_ -> pure ()
+  , \_ -> pure ()
+  , \_ -> pure ()
+  )
+
+genConstrXFold
+  :: forall r bst sig m
+   . (Has (State (IntMap [Int]) :+: State [Int] :+: Writer (Seq C.Constraint) :+: Error (ProtocolError r bst)) sig m, Enum r)
+  => XFold m (GenConst r) r bst
+genConstrXFold =
+  ( \(((is, os), (from, to), index), _) -> do
+      let ifrom = fromEnum from
+          ito = fromEnum to
+          from' = is !! ifrom --- is
+          to' = is !! ito ------- is
+          deleteIndexFromTo ks =
+            fmap snd $ filter (\(idx, _) -> idx /= ifrom && idx /= ito) $ zip [0 ..] ks
+          deleteIndexFrom ks =
+            fmap snd $ filter (\(idx, _) -> idx /= ifrom) $ zip [0 ..] ks
+
+      when (index == 0) $ do
+        branchSts <- get @[Int]
+        tellSeq $ map (uncurry C.Constraint) $ zip (deleteIndexFrom branchSts) (deleteIndexFrom is)
+
+      tellSeq $
+        C.Constraint from' to'
+          : zipWith C.Constraint (deleteIndexFromTo is) (deleteIndexFromTo os)
+  , \((is, i), lb) ->
+      gets (IntMap.lookup @[Int] i) >>= \case
+        Just _ -> throwError @(ProtocolError r bst) (DefLabelMultTimes lb)
+        Nothing -> modify (IntMap.insert i is)
+  , \(is, _) -> do
+      put is
+      pure (restoreWrapper @[Int])
+  , \_ -> pure ()
+  , \((xs, i), gt) -> do
+      gets (IntMap.lookup i) >>= \case
+        Nothing -> throwError @(ProtocolError r bst) (LabelUndefined gt)
+        Just ls -> tellSeq $ zipWith C.Constraint xs ls
+  , \(xs) -> tellSeq $ zipWith C.Constraint xs (cycle [-1])
+  )
+
+replXTraverse :: (Monad m) => C.SubMap -> XTraverse m (GenConst r) (GenConst r) r bst
+replXTraverse sbm =
+  ( \(((a, b), (from, to), i), _) ->
+      pure ((replaceList sbm a, replaceList sbm b), (from, to), i)
+  , \((xs, i), _) -> pure (replaceList sbm xs, i)
+  , \(a, _) -> pure (replaceList sbm a, id)
+  , \_ -> pure ()
+  , \((xs, i), _) -> pure (replaceList sbm xs, i)
+  , \xs -> pure (replaceList sbm xs)
+  )
+
+verifyProtXFold
+  :: forall r bst sig m
+   . (Has (State (IntMap (r, r)) :+: Error (ProtocolError r bst)) sig m, Enum r, Eq r)
+  => XFold m (GenConst r) r bst
+verifyProtXFold =
+  ( \(((is, _), ft@(from, _to), _), _) -> do
+      let from' = is !! fromEnum from
+      res <- gets @(IntMap (r, r)) (IntMap.lookup from')
+      case res of
+        Nothing -> modify (IntMap.insert from' ft)
+        Just ft1 -> when (ft1 /= ft) (throwError @(ProtocolError r bst) AStateOnlyBeUsedForTheSamePair)
+  , \_ -> pure ()
+  , \_ -> pure id
+  , \_ -> pure ()
+  , \_ -> pure ()
+  , \_ -> pure ()
+  )
+
+collectBranchDynValXFold :: (Has (State (Set Int)) sig m, Enum r) => XFold m (GenConst r) r bst
+collectBranchDynValXFold =
+  ( \_ -> pure ()
+  , \_ -> pure ()
+  , \(ls, (r, _)) -> do
+      let ls' = map snd $ filter (\(i, _) -> i /= fromEnum r) $ zip [0 ..] ls
+      modify (`Set.union` (Set.fromList ls'))
+      pure id
+  , \_ -> pure ()
+  , \_ -> pure ()
+  , \_ -> pure ()
+  )
+
+genT
+  :: forall bst sig m
+   . (Has (Reader (Set Int) :+: State bst) sig m)
+  => (bst -> Int -> T bst) -> Int -> m (T bst)
+genT fun i = do
+  dynSet <- ask @(Set Int)
+  if i == -1
+    then pure (TEnd)
+    else
+      if Set.member i dynSet
+        then do
+          bst <- get
+          pure (fun bst i)
+        else pure $ TNum i
+
+genMsgTXTraverse
+  :: forall r bst sig m
+   . (Has (Reader (Set Int) :+: State bst) sig m, Enum r, Eq r, Bounded r)
+  => XTraverse m (GenConst r) (MsgT r bst) r bst
+genMsgTXTraverse =
+  ( \(((is, _), (from, to), vi), _) -> do
+      is' <- forM (zip rRange is) $
+        \(key, i) -> genT @bst (\bst1 i1 -> if key == from then BstList i1 bst1 else TAny i1) i
+      pure (is', (from, to), vi)
+  , \((ls, idx), _) -> do
+      ls' <- mapM (genT (const TAny)) ls
+      pure (ls', idx)
+  , \(ls, (r, _)) -> do
+      ls' <- mapM (\(idx, v) -> genT (if idx == fromEnum r then const TNum else (const TAny)) v) (zip [0 ..] ls)
+      pure (ls', restoreWrapper @bst)
+  , \(_, (bst, _)) -> put bst
+  , \((is, i), _) -> do
+      is' <- mapM (genT @bst (const TAny)) is
+      pure (is', i)
+  , \ls -> pure $ fmap (const TEnd) ls
+  )
+
+getFirstXV :: Protocol (MsgT r bst) r bst -> [T bst]
+getFirstXV = \case
+  Msg (xv, _, _) _ _ _ _ :> _ -> xv
+  Label (xv, _) _ :> _ -> xv
+  Branch xv _ _ -> xv
+  Goto (xv, _) _ -> xv
+  Terminal xv -> xv
+
+genMsgT1XTraverse :: (Monad m, Enum r) => XTraverse m (MsgT r bst) (MsgT1 r bst) r bst
+genMsgT1XTraverse =
+  ( \((is, (from, to), i), (_, _, _, _, prot)) -> do
+      let os = getFirstXV prot
+          from' = fromEnum from
+          to' = fromEnum to
+      pure ((is !! from', os !! from', os !! to'), (from, to), i)
+  , \(a, _) -> pure a
+  , \(a, _) -> pure (a, id)
+  , \(a, _) -> pure a
+  , \(a, _) -> pure a
+  , \a -> pure a
+  )
+
+data PipleResult r bst = PipleResult
+  { msgT :: Protocol (MsgT r bst) r bst
+  , msgT1 :: Protocol (MsgT1 r bst) r bst
+  , dnySet :: Set Int
+  , stBound :: (Int, Int)
+  }
+
+reRank :: Set Int -> Int -> IntMap Int
+reRank branchValSet maxSize =
+  let allSet = Set.insert 0 branchValSet
+      restList = [i | i <- [0 .. maxSize], i `Set.notMember` allSet]
+   in IntMap.fromList $ zip (Set.toList allSet ++ restList) [0 ..]
+
+piple'
+  :: forall r bst sig m
+   . ( Has (Error (ProtocolError r bst)) sig m
+     , Enum r
+     , Bounded r
+     , Eq r
+     , Ord r
+     )
+  => (Tracer r bst -> m ())
+  -> Protocol Creat r bst
+  -> m (PipleResult r bst)
+piple' trace prot0 = do
+  trace (TracerProtocolCreat prot0)
+  (brSet, (maxSzie, (_, idxProt))) <-
+    runState @(Set Int) Set.empty
+      . runState @Int 0
+      . runState @Index (Index 100)
+      $ (xtraverse addIdxXTraverse prot0)
+  trace (TracerProtocolIdx idxProt)
+  trace (TracerReRank (reRank brSet maxSzie))
+  idxProt1 <- xtraverse (reRankXTraverse (reRank brSet maxSzie)) idxProt
+  trace (TracerProtocolIdx idxProt1)
+  prot1 <- xtraverse addNumsXTraverse idxProt1
+  trace (TracerProtocolAddNum prot1)
+  prot2 <- xtraverse toGenConstrXTraverse prot1
+  trace (TracerProtocolGenConst prot2)
+  void
+    . runState @(Map r CurrSt) (Map.fromList $ zip (rRange @r) (cycle [Decide]))
+    . runState @r (error internalError)
+    $ xfold checkProtXFold prot2
+  (constraintList, _) <-
+    runWriter @(Seq C.Constraint)
+      . runState @(IntMap [Int]) (IntMap.empty)
+      . runState @[Int] (error internalError)
+      $ xfold genConstrXFold prot2
+  trace (TracerConstraints constraintList)
+  let (sbm, stBound) = compressSubMap $ C.constrToSubMap $ toList constraintList
+  trace (TracerSubMap sbm)
+  prot3 <- xtraverse (replXTraverse sbm) prot2
+  trace (TracerProtocolGenConstN prot3)
+  verifyResult <- fst <$> runState @(IntMap (r, r)) (IntMap.empty) (xfold verifyProtXFold prot3)
+  trace (TracerVerifyResult verifyResult)
+  dnys <- fst <$> runState @((Set Int)) (Set.empty) (xfold collectBranchDynValXFold prot3)
+  trace (TracerCollectBranchDynVal dnys)
+  prot4 <-
+    fmap snd
+      . runReader @(Set Int) dnys
+      . runState @bst (error internalError)
+      $ (xtraverse genMsgTXTraverse prot3)
+  trace (TracerProtocolMsgT prot4)
+  prot5 <- xtraverse genMsgT1XTraverse prot4
+  trace (TracerProtocolMsgT1 prot5)
+  pure (PipleResult prot4 prot5 dnys stBound)
+
+piple
+  :: forall r bst
+   . (Enum r, Bounded r, Eq r, Ord r)
+  => Protocol Creat r bst
+  -> Either
+      (ProtocolError r bst)
+      (PipleResult r bst)
+piple protocol =
+  run $ runError @(ProtocolError r bst) $ (piple' (const (pure ())) protocol)
+
+pipleWithTracer
+  :: forall r bst
+   . (Enum r, Bounded r, Eq r, Ord r)
+  => Protocol Creat r bst
+  -> ( Seq (Tracer r bst)
+     , Either
+        (ProtocolError r bst)
+        (PipleResult r bst)
+     )
+pipleWithTracer protocol =
+  run
+    . runWriter @(Seq (Tracer r bst))
+    . runError @(ProtocolError r bst)
+    $ (piple' (\w -> tell @(Seq (Tracer r bst)) (Seq.singleton w)) protocol)
+
+genDocXFold
+  :: forall r bst ann sig m
+   . ( Has (Writer [Doc ann]) sig m
+     , Show r
+     , Show bst
+     )
+  => String -> String -> XFold m (MsgT1 r bst) r bst
+genDocXFold rName protName =
+  ( \( ((sendStart, sendEnd, recEnd), (from, to), _)
+      , (cons, args, _, _, _)
+      ) -> do
+        tell @[Doc ann]
+          [ pretty cons
+              <+> "::"
+              <+> pretty (L.intercalate "->" args)
+              <+> (if null args then emptyDoc else "->")
+              <+> "Msg"
+              <+> pretty rName
+              <+> pretty (protName <> "St")
+              <+> parens (pretty $ show sendStart)
+              <+> (pretty $ '\'' : show (from, sendEnd))
+              <+> (pretty $ '\'' : show (to, recEnd))
+          ]
+  , \_ -> pure ()
+  , \_ -> pure (id)
+  , \_ -> pure ()
+  , \_ -> pure ()
+  , \_ -> pure ()
+  )
+
+genDoc :: forall r bst ann. (Show r, Show bst) => String -> String -> Protocol (MsgT1 r bst) r bst -> [Doc ann]
+genDoc rName protName prot =
+  fst $ run $ runWriter @[Doc ann] (xfold (genDocXFold @r @bst @ann rName protName) prot)
+
+genGraph :: (Enum r, Bounded r, Show bst, Ord r, Show r) => StrFillEnv -> PipleResult r bst -> String
+genGraph sfe PipleResult{msgT} = runRender sfe (stMsgT sfe) msgT
diff --git a/src/TypedSession/State/Piple.hs b/src/TypedSession/State/Piple.hs
deleted file mode 100644
--- a/src/TypedSession/State/Piple.hs
+++ /dev/null
@@ -1,411 +0,0 @@
-{-# LANGUAGE AllowAmbiguousTypes #-}
-{-# LANGUAGE ConstraintKinds #-}
-{-# LANGUAGE DeriveFunctor #-}
-{-# LANGUAGE EmptyCase #-}
-{-# LANGUAGE FlexibleContexts #-}
-{-# LANGUAGE GeneralizedNewtypeDeriving #-}
-{-# LANGUAGE LambdaCase #-}
-{-# LANGUAGE MultiWayIf #-}
-{-# LANGUAGE OverloadedStrings #-}
-{-# LANGUAGE PatternSynonyms #-}
-{-# LANGUAGE RankNTypes #-}
-{-# LANGUAGE ScopedTypeVariables #-}
-{-# LANGUAGE TypeAbstractions #-}
-{-# LANGUAGE TypeApplications #-}
-{-# LANGUAGE TypeFamilies #-}
-{-# LANGUAGE TypeOperators #-}
-{-# LANGUAGE UndecidableInstances #-}
-{-# LANGUAGE NoFieldSelectors #-}
-
-module TypedSession.State.Piple where
-
-import Control.Algebra ((:+:))
-import Control.Carrier.Error.Either (runError)
-import Control.Carrier.Fresh.Strict
-import Control.Carrier.Reader (runReader)
-import Control.Carrier.State.Strict
-import Control.Carrier.Writer.Strict (runWriter)
-import Control.Effect.Error
-import Control.Effect.Reader
-import Control.Effect.Writer
-import Control.Monad
-import Data.Foldable (Foldable (toList), for_)
-import Data.IntMap (IntMap)
-import qualified Data.IntMap as IntMap
-import qualified Data.List as L
-import Data.Map (Map)
-import qualified Data.Map as Map
-import Data.Sequence (Seq)
-import qualified Data.Sequence as Seq
-import Data.Set (Set)
-import qualified Data.Set as Set
-import Prettyprinter
-import qualified TypedSession.State.Constraint as C
-import TypedSession.State.Render
-import TypedSession.State.Type
-import TypedSession.State.Utils
-
-------------------------
-
-newtype Index = Index Int deriving (Show, Eq, Ord, Num)
-
-addIdxXTraverse
-  :: forall r bst sig m
-   . ( Has (State Int :+: State Index :+: State (Set Int) :+: Error (ProtocolError r bst)) sig m
-     , Enum r
-     , Bounded r
-     , Ord r
-     )
-  => XTraverse m Creat Idx r bst
-addIdxXTraverse =
-  ( \_ -> do
-      inputIdx <- get @Int
-      modify @Int (+ 1)
-      Index idx <- get @Index
-      modify @Index (+ 1)
-      outputInx <- get @Int
-      pure (inputIdx, outputInx, idx)
-  , const get
-  , \(_, _) -> do
-      inputIdx <- get @Int
-      modify (Set.insert inputIdx)
-      pure (inputIdx, id)
-  , \_ -> do
-      put (Index 0)
-      modify @Int (+ 1)
-  , const get
-  , const get
-  )
-
-reRankXTraverse :: (Monad m) => IntMap Int -> XTraverse m Idx Idx r bst
-reRankXTraverse sbm =
-  ( \((a, b, idx), _) -> pure (replaceVal sbm a, replaceVal sbm b, idx)
-  , \(xs, _) -> pure (replaceVal sbm xs)
-  , \(a, _) -> pure (replaceVal sbm a, id)
-  , \_ -> pure ()
-  , \(xs, _) -> pure (replaceVal sbm xs)
-  , \xs -> pure (replaceVal sbm xs)
-  )
-
-addNumsXTraverse
-  :: forall r bst sig m
-   . ( Has (Error (ProtocolError r bst)) sig m
-     , Enum r
-     , Bounded r
-     , Ord r
-     )
-  => XTraverse m Idx AddNums r bst
-addNumsXTraverse =
-  let mkNums i =
-        let sized = fromEnum (maxBound @r) + 1
-         in fmap (\x -> i * sized + fromEnum x) (rRange @r)
-   in ( \((va, vb, idx), _) -> pure (mkNums va, mkNums vb, idx)
-      , \(va, _) -> pure $ mkNums va
-      , \(va, _) -> pure (mkNums va, id)
-      , \_ -> pure ()
-      , \(va, _) -> pure $ mkNums va
-      , \va -> pure $ mkNums va
-      )
-
-toGenConstrXTraverse :: (Monad m) => XTraverse m AddNums (GenConst r) r bst
-toGenConstrXTraverse =
-  ( \((a, b, i), (_, _, from, to, _)) -> pure ((a, b), (from, to), i)
-  , \(is, (i, _)) -> pure (is, i)
-  , \(xv, _) -> pure (xv, id)
-  , \_ -> pure ()
-  , \(xs, i) -> pure (xs, i)
-  , \xv -> pure xv
-  )
-
-data CurrSt = Decide | Undecide deriving (Show, Eq, Ord)
-
-getRCurrSt :: forall r sig m. (Has (State (Map r CurrSt)) sig m, Ord r) => r -> m CurrSt
-getRCurrSt r =
-  gets @(Map r CurrSt) (Map.lookup r) >>= \case
-    Nothing -> error "np"
-    Just v -> pure v
-
-restoreWrapper1 :: forall r sig m a. (Has (State (Map r CurrSt) :+: State r) sig m) => m a -> m a
-restoreWrapper1 m = do
-  s1 <- get @(Map r CurrSt)
-  s2 <- get @r
-  a <- m
-  put s1
-  put s2
-  pure a
-
-checkProtXFold
-  :: forall r bst sig m
-   . (Has (State (Map r CurrSt) :+: State r :+: Error (ProtocolError r bst)) sig m, Eq r, Ord r, Enum r, Bounded r)
-  => XFold m (GenConst r) r bst
-checkProtXFold =
-  ( \((_, (from, to), idx), (msgName, _, _, _, prot)) -> do
-      when (idx == 0) $ do
-        r1 <- get @r
-        if from == r1
-          then pure ()
-          else throwError @(ProtocolError r bst) (BranchFirstMsgMustHaveTheSameSender r1 msgName from)
-      fromCurrSt <- getRCurrSt from
-      when (fromCurrSt == Undecide) (throwError @(ProtocolError r bst) (UndecideStateCanNotSendMsg msgName))
-      modify (Map.insert to Decide)
-      case prot of
-        Terminal _ -> do
-          vals <- gets @(Map r CurrSt) Map.elems
-          when (any (/= Decide) vals) (throwError @(ProtocolError r bst) (TerminalNeedAllRoleDecide msgName))
-        _ -> pure ()
-  , \_ -> pure ()
-  , \(_, (r1, ls)) -> do
-      r1CurrSt <- getRCurrSt r1
-      when (r1CurrSt == Undecide) (throwError @(ProtocolError r bst) (UndecideStateCanNotStartBranch ls))
-      for_ [r | r <- rRange, r /= r1] $ \r -> modify (Map.insert r Undecide)
-      when (length ls < 1) (throwError @(ProtocolError r bst) BranchAtLeastOneBranch)
-      put r1
-      pure (restoreWrapper1 @r)
-  , \_ -> pure ()
-  , \_ -> pure ()
-  , \_ -> pure ()
-  )
-
-genConstrXFold
-  :: forall r bst sig m
-   . (Has (State (IntMap [Int]) :+: State [Int] :+: Writer (Seq C.Constraint) :+: Error (ProtocolError r bst)) sig m, Enum r)
-  => XFold m (GenConst r) r bst
-genConstrXFold =
-  ( \(((is, os), (from, to), index), _) -> do
-      let ifrom = fromEnum from
-          ito = fromEnum to
-          from' = is !! ifrom --- is
-          to' = is !! ito ------- is
-          deleteIndexFromTo ks =
-            fmap snd $ filter (\(idx, _) -> idx /= ifrom && idx /= ito) $ zip [0 ..] ks
-          deleteIndexFrom ks =
-            fmap snd $ filter (\(idx, _) -> idx /= ifrom) $ zip [0 ..] ks
-
-      when (index == 0) $ do
-        branchSts <- get @[Int]
-        tellSeq $ map (uncurry C.Constraint) $ zip (deleteIndexFrom branchSts) (deleteIndexFrom is)
-
-      tellSeq $
-        C.Constraint from' to'
-          : zipWith C.Constraint (deleteIndexFromTo is) (deleteIndexFromTo os)
-  , \((is, i), lb) ->
-      gets (IntMap.lookup @[Int] i) >>= \case
-        Just _ -> throwError @(ProtocolError r bst) (DefLabelMultTimes lb)
-        Nothing -> modify (IntMap.insert i is)
-  , \(is, _) -> do
-      put is
-      pure (restoreWrapper @[Int])
-  , \_ -> pure ()
-  , \((xs, i), gt) -> do
-      gets (IntMap.lookup i) >>= \case
-        Nothing -> throwError @(ProtocolError r bst) (LabelUndefined gt)
-        Just ls -> tellSeq $ zipWith C.Constraint xs ls
-  , \(xs) -> tellSeq $ zipWith C.Constraint xs (cycle [-1])
-  )
-
-replXTraverse :: (Monad m) => C.SubMap -> XTraverse m (GenConst r) (GenConst r) r bst
-replXTraverse sbm =
-  ( \(((a, b), (from, to), i), _) ->
-      pure ((replaceList sbm a, replaceList sbm b), (from, to), i)
-  , \((xs, i), _) -> pure (replaceList sbm xs, i)
-  , \(a, _) -> pure (replaceList sbm a, id)
-  , \_ -> pure ()
-  , \((xs, i), _) -> pure (replaceList sbm xs, i)
-  , \xs -> pure (replaceList sbm xs)
-  )
-
-collectBranchDynValXFold :: (Has (State (Set Int)) sig m, Enum r) => XFold m (GenConst r) r bst
-collectBranchDynValXFold =
-  ( \_ -> pure ()
-  , \_ -> pure ()
-  , \(ls, (r, _)) -> do
-      let ls' = map snd $ filter (\(i, _) -> i /= fromEnum r) $ zip [0 ..] ls
-      modify (`Set.union` (Set.fromList ls'))
-      pure id
-  , \_ -> pure ()
-  , \_ -> pure ()
-  , \_ -> pure ()
-  )
-
-genT
-  :: forall bst sig m
-   . (Has (Reader (Set Int) :+: State bst) sig m)
-  => (bst -> Int -> T bst) -> Int -> m (T bst)
-genT fun i = do
-  dynSet <- ask @(Set Int)
-  if i == -1
-    then pure (TEnd)
-    else
-      if Set.member i dynSet
-        then do
-          bst <- get
-          pure (fun bst i)
-        else pure $ TNum i
-
-genMsgTXTraverse
-  :: forall r bst sig m
-   . (Has (Reader (Set Int) :+: State bst) sig m, Enum r, Eq r, Bounded r)
-  => XTraverse m (GenConst r) (MsgT r bst) r bst
-genMsgTXTraverse =
-  ( \(((is, _), (from, to), vi), _) -> do
-      is' <- forM (zip rRange is) $
-        \(key, i) -> genT @bst (\bst1 i1 -> if key == from then BstList i1 bst1 else TAny i1) i
-      pure (is', (from, to), vi)
-  , \((ls, idx), _) -> do
-      ls' <- mapM (genT (const TAny)) ls
-      pure (ls', idx)
-  , \(ls, (r, _)) -> do
-      ls' <- mapM (\(idx, v) -> genT (if idx == fromEnum r then const TNum else (const TAny)) v) (zip [0 ..] ls)
-      pure (ls', restoreWrapper @bst)
-  , \(_, (bst, _)) -> put bst
-  , \((is, i), _) -> do
-      is' <- mapM (genT @bst (const TAny)) is
-      pure (is', i)
-  , \ls -> pure $ fmap (const TEnd) ls
-  )
-
-getFirstXV :: Protocol (MsgT r bst) r bst -> [T bst]
-getFirstXV = \case
-  Msg (xv, _, _) _ _ _ _ :> _ -> xv
-  Label (xv, _) _ :> _ -> xv
-  Branch xv _ _ -> xv
-  Goto (xv, _) _ -> xv
-  Terminal xv -> xv
-
-genMsgT1XTraverse :: (Monad m, Enum r) => XTraverse m (MsgT r bst) (MsgT1 r bst) r bst
-genMsgT1XTraverse =
-  ( \((is, (from, to), i), (_, _, _, _, prot)) -> do
-      let os = getFirstXV prot
-          from' = fromEnum from
-          to' = fromEnum to
-      pure ((is !! from', os !! from', os !! to'), (from, to), i)
-  , \(a, _) -> pure a
-  , \(a, _) -> pure (a, id)
-  , \(a, _) -> pure a
-  , \(a, _) -> pure a
-  , \a -> pure a
-  )
-
-data PipleResult r bst = PipleResult
-  { msgT :: Protocol (MsgT r bst) r bst
-  , msgT1 :: Protocol (MsgT1 r bst) r bst
-  , dnySet :: Set Int
-  , stBound :: (Int, Int)
-  }
-
-reRank :: Set Int -> Int -> IntMap Int
-reRank branchValSet maxSize =
-  let allSet = Set.insert 0 branchValSet
-      restList = [i | i <- [0 .. maxSize], i `Set.notMember` allSet]
-   in IntMap.fromList $ zip (Set.toList allSet ++ restList) [0 ..]
-
-piple'
-  :: forall r bst sig m
-   . ( Has (Error (ProtocolError r bst)) sig m
-     , Enum r
-     , Bounded r
-     , Eq r
-     , Ord r
-     )
-  => (Tracer r bst -> m ())
-  -> Protocol Creat r bst
-  -> m (PipleResult r bst)
-piple' trace prot0 = do
-  trace (TracerProtocolCreat prot0)
-  (brSet, (maxSzie, (_, idxProt))) <-
-    runState @(Set Int) Set.empty
-      . runState @Int 0
-      . runState @Index (Index 100)
-      $ (xtraverse addIdxXTraverse prot0)
-  trace (TracerProtocolIdx idxProt)
-  trace (TracerReRank (reRank brSet maxSzie))
-  idxProt1 <- xtraverse (reRankXTraverse (reRank brSet maxSzie)) idxProt
-  trace (TracerProtocolIdx idxProt1)
-  prot1 <- xtraverse addNumsXTraverse idxProt1
-  trace (TracerProtocolAddNum prot1)
-  prot2 <- xtraverse toGenConstrXTraverse prot1
-  trace (TracerProtocolGenConst prot2)
-  void
-    . runState @(Map r CurrSt) (Map.fromList $ zip (rRange @r) (cycle [Decide]))
-    . runState @r undefined
-    $ xfold checkProtXFold prot2
-  (constraintList, _) <-
-    runWriter @(Seq C.Constraint)
-      . runState @(IntMap [Int]) (IntMap.empty)
-      . runState @[Int] undefined
-      $ xfold genConstrXFold prot2
-  trace (TracerConstraints constraintList)
-  let (sbm, stBound) = compressSubMap $ C.constrToSubMap $ toList constraintList
-  trace (TracerSubMap sbm)
-  prot3 <- xtraverse (replXTraverse sbm) prot2
-  trace (TracerProtocolGenConstN prot3)
-  dnys <- fst <$> runState @((Set Int)) (Set.empty) (xfold collectBranchDynValXFold prot3)
-  trace (TracerCollectBranchDynVal dnys)
-  prot4 <-
-    fmap snd
-      . runReader @(Set Int) dnys
-      . runState @bst undefined
-      $ (xtraverse genMsgTXTraverse prot3)
-  trace (TracerProtocolMsgT prot4)
-  prot5 <- xtraverse genMsgT1XTraverse prot4
-  trace (TracerProtocolMsgT1 prot5)
-  pure (PipleResult prot4 prot5 dnys stBound)
-
-piple
-  :: forall r bst
-   . (Enum r, Bounded r, Eq r, Ord r)
-  => Protocol Creat r bst
-  -> Either
-      (ProtocolError r bst)
-      (PipleResult r bst)
-piple protocol =
-  run $ runError @(ProtocolError r bst) $ (piple' (const (pure ())) protocol)
-
-pipleWithTracer
-  :: forall r bst
-   . (Enum r, Bounded r, Eq r, Ord r)
-  => Protocol Creat r bst
-  -> ( Seq (Tracer r bst)
-     , Either
-        (ProtocolError r bst)
-        (PipleResult r bst)
-     )
-pipleWithTracer protocol =
-  run
-    . runWriter @(Seq (Tracer r bst))
-    . runError @(ProtocolError r bst)
-    $ (piple' (\w -> tell @(Seq (Tracer r bst)) (Seq.singleton w)) protocol)
-
-genDocXFold
-  :: forall r bst ann sig m
-   . ( Has (Writer [Doc ann]) sig m
-     , Show r
-     , Show bst
-     )
-  => String -> String -> XFold m (MsgT1 r bst) r bst
-genDocXFold rName protName =
-  ( \( ((sendStart, sendEnd, recEnd), (from, to), _)
-      , (cons, args, _, _, _)
-      ) -> do
-        tell @[Doc ann]
-          [ pretty cons
-              <+> "::"
-              <+> pretty (L.intercalate "->" args)
-              <+> (if null args then emptyDoc else "->")
-              <+> "Msg"
-              <+> pretty rName
-              <+> pretty (protName <> "St")
-              <+> parens (pretty $ show sendStart)
-              <+> (pretty $ '\'' : show (from, sendEnd))
-              <+> (pretty $ '\'' : show (to, recEnd))
-          ]
-  , \_ -> pure ()
-  , \_ -> pure (id)
-  , \_ -> pure ()
-  , \_ -> pure ()
-  , \_ -> pure ()
-  )
-
-genDoc :: forall r bst ann. (Show r, Show bst) => String -> String -> Protocol (MsgT1 r bst) r bst -> [Doc ann]
-genDoc rName protName prot =
-  fst $ run $ runWriter @[Doc ann] (xfold (genDocXFold @r @bst @ann rName protName) prot)
diff --git a/src/TypedSession/State/Render.hs b/src/TypedSession/State/Render.hs
--- a/src/TypedSession/State/Render.hs
+++ b/src/TypedSession/State/Render.hs
@@ -17,11 +17,7 @@
 import Control.Effect.State
 import Control.Effect.Writer
 import Control.Monad (when)
-import Data.IntMap (IntMap)
 import qualified Data.List as L
-import Data.Sequence (Seq)
-import Data.Set (Set)
-import qualified TypedSession.State.Constraint as C
 import TypedSession.State.Type
 import TypedSession.State.Utils
 
@@ -140,18 +136,6 @@
       tell [header]
       (xfold (renderXFold sfe xst) prot)
 
-data Tracer r bst
-  = TracerProtocolCreat (Protocol Creat r bst)
-  | TracerProtocolIdx (Protocol Idx r bst)
-  | TracerReRank (IntMap Int)
-  | TracerProtocolAddNum (Protocol AddNums r bst)
-  | TracerProtocolGenConst (Protocol (GenConst r) r bst)
-  | TracerConstraints (Seq C.Constraint)
-  | TracerSubMap C.SubMap
-  | TracerProtocolGenConstN (Protocol (GenConst r) r bst)
-  | TracerCollectBranchDynVal (Set Int)
-  | TracerProtocolMsgT (Protocol (MsgT r bst) r bst)
-  | TracerProtocolMsgT1 (Protocol (MsgT1 r bst) r bst)
 
 traceWrapper :: String -> String -> String
 traceWrapper desc st =
@@ -212,6 +196,7 @@
     TracerConstraints p -> traceWrapper "Constrains" $ show p
     TracerSubMap p -> traceWrapper "SubMap" $ show p
     TracerProtocolGenConstN p -> traceWrapper "GenConstN" $ show p
+    TracerVerifyResult m -> traceWrapper "VerifyResult Map" $ show m
     TracerCollectBranchDynVal dvs -> traceWrapper "CollectBranchDynVal" $ show dvs
     TracerProtocolMsgT p -> traceWrapper "MsgT" $ show p
     TracerProtocolMsgT1 p -> traceWrapper "MsgT1" $ show p
diff --git a/src/TypedSession/State/Type.hs b/src/TypedSession/State/Type.hs
--- a/src/TypedSession/State/Type.hs
+++ b/src/TypedSession/State/Type.hs
@@ -17,9 +17,13 @@
 module TypedSession.State.Type where
 
 import Control.Monad
+import Data.IntMap (IntMap)
 import Data.Kind (Constraint, Type)
+import Data.Sequence (Seq)
+import Data.Set (Set)
 import Prettyprinter
 import Prettyprinter.Render.String (renderString)
+import qualified TypedSession.State.Constraint as C
 
 type family XMsg eta
 type family XLabel eta
@@ -132,6 +136,7 @@
   | UndecideStateCanNotStartBranch [BranchSt (GenConst r) r bst]
   | TerminalNeedAllRoleDecide String
   | BranchAtLeastOneBranch
+  | AStateOnlyBeUsedForTheSamePair
 
 instance (Show r, Show bst) => Show (ProtocolError r bst) where
   show = \case
@@ -148,6 +153,24 @@
     UndecideStateCanNotStartBranch brs -> "Undecide State can't start branch! " <> show brs
     TerminalNeedAllRoleDecide msgName -> "Msg " <> msgName <> ", Terminal need all role decide!"
     BranchAtLeastOneBranch -> "Branch at least one branch!"
+    AStateOnlyBeUsedForTheSamePair -> "A state can only be used for the same pair of communicators." ++ internalError
+
+internalError :: String
+internalError = "Internal error, please report: https://github.com/sdzx-1/typed-session/issues"
+
+data Tracer r bst
+  = TracerProtocolCreat (Protocol Creat r bst)
+  | TracerProtocolIdx (Protocol Idx r bst)
+  | TracerReRank (IntMap Int)
+  | TracerProtocolAddNum (Protocol AddNums r bst)
+  | TracerProtocolGenConst (Protocol (GenConst r) r bst)
+  | TracerConstraints (Seq C.Constraint)
+  | TracerSubMap C.SubMap
+  | TracerProtocolGenConstN (Protocol (GenConst r) r bst)
+  | TracerVerifyResult (IntMap (r, r))
+  | TracerCollectBranchDynVal (Set Int)
+  | TracerProtocolMsgT (Protocol (MsgT r bst) r bst)
+  | TracerProtocolMsgT1 (Protocol (MsgT1 r bst) r bst)
 
 ------------------------
 
diff --git a/src/TypedSession/State/Utils.hs b/src/TypedSession/State/Utils.hs
--- a/src/TypedSession/State/Utils.hs
+++ b/src/TypedSession/State/Utils.hs
@@ -74,4 +74,4 @@
 replaceList sbm ls = fmap (\k -> fromMaybe k $ IntMap.lookup k sbm) ls
 
 replaceVal :: IntMap Int -> Int -> Int
-replaceVal sbm k = fromMaybe (error "np") $ IntMap.lookup k sbm
+replaceVal sbm k = fromMaybe (error internalError) $ IntMap.lookup k sbm
diff --git a/test/Main.hs b/test/Main.hs
--- a/test/Main.hs
+++ b/test/Main.hs
@@ -5,9 +5,8 @@
 module Main (main) where
 
 import Text.RawString.QQ (r)
-import TypedSession.State.GenDoc (genGraph)
 import TypedSession.State.Parser (runProtocolParser)
-import TypedSession.State.Piple (pipleWithTracer)
+import TypedSession.State.Pipeline (genGraph, pipleWithTracer)
 import TypedSession.State.Render (StrFillEnv (StrFillEnv))
 
 main :: IO ()
@@ -125,6 +124,8 @@
 --   Msg <(([1,1,2],[2,-1,2]),(Client,Server),0)> Stop [] Client Server
 --   Msg <(([2,-1,2],[-1,-1,-1]),(Client,Counter),1)> CStop [] Client Counter
 --   Terminal [-1,-1,-1]
+-- ,--------------------VerifyResult Map-----------------
+-- fromList [(1,(Client,Server)),(2,(Client,Counter)),(3,(Server,Client))]
 -- ,--------------------CollectBranchDynVal-----------------
 -- fromList [1,2]
 -- ,--------------------MsgT-----------------
@@ -451,6 +452,8 @@
 --   Msg <(([2,2,1],[1,0,1]),(Seller,Buyer),0)> NoBook [] Seller Buyer
 --   Msg <(([1,0,1],[0,0,1]),(Buyer,Buyer2),1)> SellerNoBook [] Buyer Buyer2
 --   Goto ([0,0,1],0) 0
+-- ,--------------------VerifyResult Map-----------------
+-- fromList [(0,(Buyer,Seller)),(1,(Buyer,Buyer2)),(2,(Seller,Buyer)),(5,(Buyer,Seller)),(6,(Buyer2,Buyer)),(9,(Buyer,Buyer2)),(10,(Seller,Buyer)),(11,(Seller,Buyer))]
 -- ,--------------------CollectBranchDynVal-----------------
 -- fromList [1,2,5,6,9]
 -- ,--------------------MsgT-----------------
diff --git a/typed-session-state-algorithm.cabal b/typed-session-state-algorithm.cabal
--- a/typed-session-state-algorithm.cabal
+++ b/typed-session-state-algorithm.cabal
@@ -20,7 +20,7 @@
 -- PVP summary:     +-+------- breaking API changes
 --                  | | +----- non-breaking API additions
 --                  | | | +--- code changes with no API change
-version:            0.1.0.2
+version:            0.2.0.0
 
 -- A short (one-line) description of the package.
 synopsis: Automatically generate status for typed-session.
@@ -60,9 +60,7 @@
 
     -- Modules exported by the library.
     exposed-modules:  TypedSession.State.Constraint
-                    , TypedSession.State.Piple
-                    , TypedSession.State.Pattern
-                    , TypedSession.State.GenDoc
+                    , TypedSession.State.Pipeline
                     , TypedSession.State.Type
                     , TypedSession.State.Utils
                     , TypedSession.State.Render