typed-session-state-algorithm 0.1.0.1 → 0.1.0.2

raw patch · 5 files changed

+171/−129 lines, 5 filesPVP: major bump suggested

API removals or changes: PVP suggests a major version bump

API changes (from Hackage documentation)

Files

• CHANGELOG.md +4/−0
• src/TypedSession/State/Piple.hs +77/−33
• src/TypedSession/State/Type.hs +20/−14
• test/Main.hs +69/−81
• typed-session-state-algorithm.cabal +1/−1

@@ -1,5 +1,9 @@ # Revision history for typed-session-state-algorithm +## 0.1.0.2++*New protocol check function.+ ## 0.1.0.1  *Fix st min value must be -1. 

@@ -3,6 +3,7 @@ {-# LANGUAGE DeriveFunctor #-} {-# LANGUAGE EmptyCase #-} {-# LANGUAGE FlexibleContexts #-}+{-# LANGUAGE GeneralizedNewtypeDeriving #-} {-# LANGUAGE LambdaCase #-} {-# LANGUAGE MultiWayIf #-} {-# LANGUAGE OverloadedStrings #-}@@ -28,10 +29,12 @@ import Control.Effect.Reader import Control.Effect.Writer import Control.Monad-import Data.Foldable (Foldable (toList))+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)@@ -44,9 +47,11 @@  ------------------------ +newtype Index = Index Int deriving (Show, Eq, Ord, Num)+ addIdxXTraverse   :: forall r bst sig m-   . ( Has (State Int :+: State (Set Int) :+: Error (ProtocolError r bst)) sig m+   . ( Has (State Int :+: State Index :+: State (Set Int) :+: Error (ProtocolError r bst)) sig m      , Enum r      , Bounded r      , Ord r@@ -56,21 +61,25 @@   ( \_ -> do       inputIdx <- get @Int       modify @Int (+ 1)+      Index idx <- get @Index+      modify @Index (+ 1)       outputInx <- get @Int-      pure (inputIdx, outputInx)+      pure (inputIdx, outputInx, idx)   , const get   , \(_, _) -> do       inputIdx <- get @Int       modify (Set.insert inputIdx)       pure (inputIdx, id)-  , \_ -> modify @Int (+ 1)+  , \_ -> 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), _) -> pure (replaceVal sbm a, replaceVal sbm b)+  ( \((a, b, idx), _) -> pure (replaceVal sbm a, replaceVal sbm b, idx)   , \(xs, _) -> pure (replaceVal sbm xs)   , \(a, _) -> pure (replaceVal sbm a, id)   , \_ -> pure ()@@ -80,7 +89,7 @@  addNumsXTraverse   :: forall r bst sig m-   . ( Has (State Int :+: Error (ProtocolError r bst)) sig m+   . ( Has (Error (ProtocolError r bst)) sig m      , Enum r      , Bounded r      , Ord r@@ -90,27 +99,10 @@   let mkNums i =         let sized = fromEnum (maxBound @r) + 1          in fmap (\x -> i * sized + fromEnum x) (rRange @r)-   in ( \((va, vb), _) -> do-          idx <- get @Int-          modify @Int (+ 1)-          pure (mkNums va, mkNums vb, idx)+   in ( \((va, vb, idx), _) -> pure (mkNums va, mkNums vb, idx)       , \(va, _) -> pure $ mkNums va-      , \(va, (r, ls)) -> do-          let len = length ls-          -- At least two branches.-          when (len < 2) (throwError (AtLeastTwoBranches (Branch va r ls)))-          void $ runState @(Maybe r) Nothing $ forM_ ls $ \(BranchSt _ _ prot) -> do-            -- The first message of each branch must have the same receiver and sender.-            case getFirstMsgInfo prot of-              Nothing -> throwError (BranchNoMsg prot)-              Just (from, _) -> do-                when (from /= r) $-                  throwError (BranchFirstMsgMustHaveTheSameSender prot)-            -- Each branch sender must send (directly or indirectly) a message to all other receivers to notify the state change.-            let receivers = L.nub $ L.sort $ r : (fmap snd $ getAllMsgInfo prot)-            when (receivers /= [minBound .. maxBound]) (throwError (BranchNotNotifyAllOtherReceivers prot))-          pure (mkNums va, id)-      , \_ -> put @Int 0+      , \(va, _) -> pure (mkNums va, id)+      , \_ -> pure ()       , \(va, _) -> pure $ mkNums va       , \va -> pure $ mkNums va       )@@ -125,6 +117,55 @@   , \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)@@ -271,20 +312,23 @@   -> m (PipleResult r bst) piple' trace prot0 = do   trace (TracerProtocolCreat prot0)-  (brSet, (maxSzie, idxProt)) <--    runState @(Set Int) Set.empty $-      runState @Int 0 (xtraverse addIdxXTraverse 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 <--    fmap snd-      . runState @Int 100-      $ xtraverse addNumsXTraverse 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)

@@ -125,23 +125,29 @@  -- | ProtocolError data ProtocolError r bst-  = AtLeastTwoBranches (Protocol Idx r bst)-  | DefLabelMultTimes Int+  = DefLabelMultTimes Int   | LabelUndefined Int-  | BranchNoMsg (Protocol Idx r bst)-  | BranchFirstMsgMustHaveTheSameSender (Protocol Idx r bst)-  | BranchNotNotifyAllOtherReceivers (Protocol Idx r bst)+  | BranchFirstMsgMustHaveTheSameSender r String r+  | UndecideStateCanNotSendMsg String+  | UndecideStateCanNotStartBranch [BranchSt (GenConst r) r bst]+  | TerminalNeedAllRoleDecide String+  | BranchAtLeastOneBranch  instance (Show r, Show bst) => Show (ProtocolError r bst) where   show = \case-    AtLeastTwoBranches prot -> "At least two branches are required\n" <> show prot-    DefLabelMultTimes msgOrLabel -> "Defining Label multiple times\n" <> show msgOrLabel-    LabelUndefined prot -> "Label Undefined\n" <> show prot-    BranchNoMsg prot -> "Branch No Msg\n" <> show prot-    BranchFirstMsgMustHaveTheSameSender prot ->-      "The first message of each branch must have the same sender.\n" <> show prot-    BranchNotNotifyAllOtherReceivers prot ->-      "Each branch sender must send (directly or indirectly) a message to all other receivers to notify the state change.\n" <> show prot+    DefLabelMultTimes msgOrLabel -> "Defining Label multiple times: " <> show msgOrLabel+    LabelUndefined prot -> "Label Undefined: " <> show prot+    BranchFirstMsgMustHaveTheSameSender psender msgName from ->+      "The first message of each branch must have the same sender. Sender: "+        <> show psender+        <> " But Msg: "+        <> msgName+        <> "'s sender is "+        <> show from+    UndecideStateCanNotSendMsg msgName -> "Msg " <> msgName <> " error, Undecide State can't send msg!"+    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!"  ------------------------ @@ -156,7 +162,7 @@  data Idx -type instance XMsg Idx = (Int, Int)+type instance XMsg Idx = (Int, Int, Int) type instance XLabel Idx = Int type instance XBranch Idx = Int type instance XBranchSt Idx = ()

@@ -7,10 +7,8 @@ import Text.RawString.QQ (r) import TypedSession.State.GenDoc (genGraph) import TypedSession.State.Parser (runProtocolParser)-import TypedSession.State.Pattern-import TypedSession.State.Piple (PipleResult (..), piple, pipleWithTracer)-import TypedSession.State.Render (StrFillEnv (StrFillEnv), defaultStrFilEnv)-import TypedSession.State.Type (Creat, Protocol)+import TypedSession.State.Piple (pipleWithTracer)+import TypedSession.State.Render (StrFillEnv (StrFillEnv))  main :: IO () main = putStrLn "Test suite not yet implemented."@@ -63,13 +61,13 @@ -- Label 0 0 -- [Branch] 0 Client --   * BranchSt () STrue---   Msg <(1,2)> AddOne [] Client Counter---   Msg <(2,3)> Ping [Int, Int, Int] Client Server---   Msg <(3,4)> Pong [] Server Client+--   Msg <(1,2,0)> AddOne [] Client Counter+--   Msg <(2,3,1)> Ping [Int, Int, Int] Client Server+--   Msg <(3,4,2)> Pong [] Server Client --   Goto 4 0 --   * BranchSt () SFalse---   Msg <(5,6)> Stop [] Client Server---   Msg <(6,7)> CStop [] Client Counter+--   Msg <(5,6,0)> Stop [] Client Server+--   Msg <(6,7,1)> CStop [] Client Counter --   Terminal 7 -- ,--------------------ReRank----------------- -- fromList [(0,0),(1,1),(2,2),(3,3),(4,4),(5,5),(6,6),(7,7)]@@ -77,13 +75,13 @@ -- Label 0 0 -- [Branch] 0 Client --   * BranchSt () STrue---   Msg <(1,2)> AddOne [] Client Counter---   Msg <(2,3)> Ping [Int, Int, Int] Client Server---   Msg <(3,4)> Pong [] Server Client+--   Msg <(1,2,0)> AddOne [] Client Counter+--   Msg <(2,3,1)> Ping [Int, Int, Int] Client Server+--   Msg <(3,4,2)> Pong [] Server Client --   Goto 4 0 --   * BranchSt () SFalse---   Msg <(5,6)> Stop [] Client Server---   Msg <(6,7)> CStop [] Client Counter+--   Msg <(5,6,0)> Stop [] Client Server+--   Msg <(6,7,1)> CStop [] Client Counter --   Terminal 7 -- ,--------------------AddNum----------------- -- Label [0,1,2] 0@@ -159,15 +157,13 @@ -- -------------------------------------Client--------------Server-------------Counter -- LABEL 0                                S0                 S1 s                S2 s --   [Branch Client]                      S0                 S1 s                S2 s---     * BranchSt STrue --     AddOne                        {S2 STrue}->            S1 s               ->S2 s---     Ping                           S1 STrue->            ->S1 s               S2 s---     Pong                              S3<-                <-S3                S2 s---     Goto 0                             S0                 S1 s                S2 s---     * BranchSt SFalse+--       Ping                         S1 STrue->            ->S1 s               S2 s+--       Pong                            S3<-                <-S3                S2 s+--       Goto 0                           S0                 S1 s                S2 s --     Stop                         {S1 SFalse}->           ->S1 s               S2 s---     CStop                         S2 SFalse->             End                ->S2 s---     ~ Terminal                        End                 End                 End+--       CStop                       S2 SFalse->             End                ->S2 s+--       Terminal                        End                 End                 End  data Role   = Buyer@@ -276,75 +272,75 @@ --   Goto () 0 -- ,--------------------Idx----------------- -- Label 0 0--- Msg <(0,1)> Title [String] Buyer Seller+-- Msg <(0,1,100)> Title [String] Buyer Seller -- [Branch] 1 Seller --   * BranchSt () Found---   Msg <(2,3)> Price [Int] Seller Buyer+--   Msg <(2,3,0)> Price [Int] Seller Buyer --   [Branch] 3 Buyer --     * BranchSt () Two---     Msg <(4,5)> PriceToBuyer2 [Int] Buyer Buyer2+--     Msg <(4,5,0)> PriceToBuyer2 [Int] Buyer Buyer2 --     [Branch] 5 Buyer2 --       * BranchSt () NotSupport---       Msg <(6,7)> NotSupport1 [] Buyer2 Buyer---       Msg <(7,8)> TwoNotBuy [] Buyer Seller+--       Msg <(6,7,0)> NotSupport1 [] Buyer2 Buyer+--       Msg <(7,8,1)> TwoNotBuy [] Buyer Seller --       Goto 8 0 --       * BranchSt () Support---       Msg <(9,10)> SupportVal [Int] Buyer2 Buyer+--       Msg <(9,10,0)> SupportVal [Int] Buyer2 Buyer --       [Branch] 10 Buyer --         * BranchSt () Enough---         Msg <(11,12)> TwoAccept [] Buyer Seller---         Msg <(12,13)> TwoDate [Int] Seller Buyer---         Msg <(13,14)> TwoSuccess [Int] Buyer Buyer2+--         Msg <(11,12,0)> TwoAccept [] Buyer Seller+--         Msg <(12,13,1)> TwoDate [Int] Seller Buyer+--         Msg <(13,14,2)> TwoSuccess [Int] Buyer Buyer2 --         Goto 14 0 --         * BranchSt () NotEnough---         Msg <(15,16)> TwoNotBuy1 [] Buyer Seller---         Msg <(16,17)> TwoFailed [] Buyer Buyer2+--         Msg <(15,16,0)> TwoNotBuy1 [] Buyer Seller+--         Msg <(16,17,1)> TwoFailed [] Buyer Buyer2 --         Terminal 17 --     * BranchSt () One---     Msg <(18,19)> OneAccept [] Buyer Seller---     Msg <(19,20)> OneDate [Int] Seller Buyer---     Msg <(20,21)> OneSuccess [Int] Buyer Buyer2+--     Msg <(18,19,0)> OneAccept [] Buyer Seller+--     Msg <(19,20,1)> OneDate [Int] Seller Buyer+--     Msg <(20,21,2)> OneSuccess [Int] Buyer Buyer2 --     Goto 21 0 --   * BranchSt () NotFound---   Msg <(22,23)> NoBook [] Seller Buyer---   Msg <(23,24)> SellerNoBook [] Buyer Buyer2+--   Msg <(22,23,0)> NoBook [] Seller Buyer+--   Msg <(23,24,1)> SellerNoBook [] Buyer Buyer2 --   Goto 24 0 -- ,--------------------ReRank----------------- -- fromList [(0,0),(1,1),(2,5),(3,2),(4,6),(5,3),(6,7),(7,8),(8,9),(9,10),(10,4),(11,11),(12,12),(13,13),(14,14),(15,15),(16,16),(17,17),(18,18),(19,19),(20,20),(21,21),(22,22),(23,23),(24,24)] -- ,--------------------Idx----------------- -- Label 0 0--- Msg <(0,1)> Title [String] Buyer Seller+-- Msg <(0,1,100)> Title [String] Buyer Seller -- [Branch] 1 Seller --   * BranchSt () Found---   Msg <(5,2)> Price [Int] Seller Buyer+--   Msg <(5,2,0)> Price [Int] Seller Buyer --   [Branch] 2 Buyer --     * BranchSt () Two---     Msg <(6,3)> PriceToBuyer2 [Int] Buyer Buyer2+--     Msg <(6,3,0)> PriceToBuyer2 [Int] Buyer Buyer2 --     [Branch] 3 Buyer2 --       * BranchSt () NotSupport---       Msg <(7,8)> NotSupport1 [] Buyer2 Buyer---       Msg <(8,9)> TwoNotBuy [] Buyer Seller+--       Msg <(7,8,0)> NotSupport1 [] Buyer2 Buyer+--       Msg <(8,9,1)> TwoNotBuy [] Buyer Seller --       Goto 9 0 --       * BranchSt () Support---       Msg <(10,4)> SupportVal [Int] Buyer2 Buyer+--       Msg <(10,4,0)> SupportVal [Int] Buyer2 Buyer --       [Branch] 4 Buyer --         * BranchSt () Enough---         Msg <(11,12)> TwoAccept [] Buyer Seller---         Msg <(12,13)> TwoDate [Int] Seller Buyer---         Msg <(13,14)> TwoSuccess [Int] Buyer Buyer2+--         Msg <(11,12,0)> TwoAccept [] Buyer Seller+--         Msg <(12,13,1)> TwoDate [Int] Seller Buyer+--         Msg <(13,14,2)> TwoSuccess [Int] Buyer Buyer2 --         Goto 14 0 --         * BranchSt () NotEnough---         Msg <(15,16)> TwoNotBuy1 [] Buyer Seller---         Msg <(16,17)> TwoFailed [] Buyer Buyer2+--         Msg <(15,16,0)> TwoNotBuy1 [] Buyer Seller+--         Msg <(16,17,1)> TwoFailed [] Buyer Buyer2 --         Terminal 17 --     * BranchSt () One---     Msg <(18,19)> OneAccept [] Buyer Seller---     Msg <(19,20)> OneDate [Int] Seller Buyer---     Msg <(20,21)> OneSuccess [Int] Buyer Buyer2+--     Msg <(18,19,0)> OneAccept [] Buyer Seller+--     Msg <(19,20,1)> OneDate [Int] Seller Buyer+--     Msg <(20,21,2)> OneSuccess [Int] Buyer Buyer2 --     Goto 21 0 --   * BranchSt () NotFound---   Msg <(22,23)> NoBook [] Seller Buyer---   Msg <(23,24)> SellerNoBook [] Buyer Buyer2+--   Msg <(22,23,0)> NoBook [] Seller Buyer+--   Msg <(23,24,1)> SellerNoBook [] Buyer Buyer2 --   Goto 24 0 -- ,--------------------AddNum----------------- -- Label [0,1,2] 0@@ -532,34 +528,26 @@ -- LABEL 0                                S0                  S0                 S1 s --   Title                               S0->                ->S0                S1 s --   [Branch Seller]                     S2 s                 S3                 S1 s---     * BranchSt Found --     Price                            S2 s<-           <-{S2 Found}            S1 s---     [Branch Buyer]                     S4                 S5 s                S1 s---       * BranchSt Two---       PriceToBuyer2                {S1 Two}->             S5 s               ->S1 s---       [Branch Buyer2]                 S6 s                S5 s                 S7---         * BranchSt NotSupport---         NotSupport1                  S6 s<-               S5 s         <-{S6 NotSupport}---         TwoNotBuy               S5 NotSupport->          ->S5 s               S1 s---         Goto 0                         S0                  S0                 S1 s---         * BranchSt Support---         SupportVal                   S6 s<-               S5 s           <-{S6 Support}---         [Branch Buyer]                 S8                 S5 s                S9 s---           * BranchSt Enough---           TwoAccept              {S5 Enough}->           ->S5 s               S9 s---           TwoDate                    S10<-               <-S10                S9 s---           TwoSuccess              S9 Enough->              S0                ->S9 s+--       [Branch Buyer]                   S4                 S5 s                S1 s+--         PriceToBuyer2              {S1 Two}->             S5 s               ->S1 s+--           [Branch Buyer2]             S6 s                S5 s                 S7+--             NotSupport1              S6 s<-               S5 s         <-{S6 NotSupport}+--               TwoNotBuy         S5 NotSupport->          ->S5 s               S1 s+--               Goto 0                   S0                  S0                 S1 s+--             SupportVal               S6 s<-               S5 s           <-{S6 Support}+--               [Branch Buyer]           S8                 S5 s                S9 s+--                 TwoAccept        {S5 Enough}->           ->S5 s               S9 s+--                   TwoDate            S10<-               <-S10                S9 s+--                   TwoSuccess      S9 Enough->              S0                ->S9 s+--                   Goto 0               S0                  S0                 S1 s+--                 TwoNotBuy1      {S5 NotEnough}->         ->S5 s               S9 s+--                   TwoFailed      S9 NotEnough->           End                ->S9 s+--                   Terminal            End                 End                 End+--         OneAccept                  {S5 One}->            ->S5 s               S1 s+--           OneDate                    S11<-               <-S11                S1 s+--           OneSuccess                S1 One->               S0                ->S1 s --           Goto 0                       S0                  S0                 S1 s---           * BranchSt NotEnough---           TwoNotBuy1            {S5 NotEnough}->         ->S5 s               S9 s---           TwoFailed              S9 NotEnough->           End                ->S9 s---           ~ Terminal                  End                 End                 End---       * BranchSt One---       OneAccept                    {S5 One}->            ->S5 s               S1 s---       OneDate                        S11<-               <-S11                S1 s---       OneSuccess                    S1 One->               S0                ->S1 s---       Goto 0                           S0                  S0                 S1 s---     * BranchSt NotFound --     NoBook                           S2 s<-         <-{S2 NotFound}           S1 s---     SellerNoBook                 S1 NotFound->             S0                ->S1 s---     Goto 0                             S0                  S0                 S1 s+--       SellerNoBook               S1 NotFound->             S0                ->S1 s+--       Goto 0                           S0                  S0                 S1 s

@@ -20,7 +20,7 @@ -- PVP summary:     +-+------- breaking API changes --                  | | +----- non-breaking API additions --                  | | | +--- code changes with no API change-version:            0.1.0.1+version:            0.1.0.2  -- A short (one-line) description of the package. synopsis: Automatically generate status for typed-session.