choiceBad :: Config ()
choiceBad
  = Config { cTypes = [mTT, mOK]
           , cUnfold = []
           , cSets   = []
           , cProcs = [ (tpid0, choiceMaster)
                      , (tpid1, choiceSlave)
                      ]
           }
    where
      choiceMaster = Send tpid1 [ (mTT, Send tpid1 [ (mTT, Skip ())
                                                     , (mOK, Skip ())
                                                     ] ())
                                 , (mOK, Send tpid1 [ (mTT, Skip ())
                                                     , (mOK, Skip ())
                                                     ] ())
                                   ] ()
      choiceSlave = Recv [ (mTT, Recv [ (mTT, Skip ()) ] ())
                          , (mOK, Recv [ (mOK, Skip ()) ] ())
                          ] ()

---
choiceBad :: Config ()
choiceBad
  = Config { cTypes = [mTT, mOK]
           , cUnfold = []
           , cSets   = []
           , cProcs = [ (tpid0, choiceMaster)
                      , (tpid1, choiceSlave)
                      ]
           }
    where
      choiceMaster = Send tpid1 [ (mTT, Send tpid1 [ (mTT, Skip ())
                                                     , (mOK, Skip ())
                                                     ] ())
                                 , (mOK, Send tpid1 [ (mTT, Skip ())
                                                     , (mOK, Skip ())
                                                     ] ())
                                   ] ()
      choiceSlave = Recv [ (mTT, Recv [ (mTT, Skip ()) ] ())
                          , (mOK, Recv [ (mOK, Skip ()) ] ())
                          ] ()

---
choiceBad
  = Config { cTypes = [mTT, mOK]
           , cUnfold = []
           , cSets   = []
           , cProcs = [ (tpid0, choiceMaster)
                      , (tpid1, choiceSlave)
                      ]
           }
    where
      choiceMaster = Send tpid1 [ (mTT, Send tpid1 [ (mTT, Skip ())
                                                     , (mOK, Skip ())
                                                     ] ())
                                 , (mOK, Send tpid1 [ (mTT, Skip ())
                                                     , (mOK, Skip ())
                                                     ] ())
                                   ] ()
      choiceSlave = Recv [ (mTT, Recv [ (mTT, Skip ()) ] ())
                          , (mOK, Recv [ (mOK, Skip ()) ] ())
                          ] ()

---