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.1.0.2 + +*New protocol check function. + ## 0.1.0.1 *Fix st min value must be -1. diff --git a/src/TypedSession/State/Piple.hs b/src/TypedSession/State/Piple.hs --- a/src/TypedSession/State/Piple.hs +++ b/src/TypedSession/State/Piple.hs @@ -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) 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 @@ -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 = () diff --git a/test/Main.hs b/test/Main.hs --- a/test/Main.hs +++ b/test/Main.hs @@ -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 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.1 +version: 0.1.0.2 -- A short (one-line) description of the package. synopsis: Automatically generate status for typed-session.