How to develop an algorithm to automatically generate states?

sdzx-1 commented 2 months ago

User describes the protocol and automatically generates Msg. The initial idea is to generate constraints through protocols, and constraints generate replacement tables.

pp :: [P BookRole]
pp =
  [ Buyer :-> Seller
  , Seller :-> Buyer
  , Buyer :-> Buyer2
  , Buyer2 :-> Buyer
  , Buyer :-> Seller
  , Seller :-> Buyer
  , Buyer :-> Buyer2
  , Buyer2 :-> Buyer
  , Buyer :-> Seller
  , Seller :-> Buyer
  ]

allRoles' :: [BookRole]
allRoles' = [Buyer2, Seller, Buyer]

v2 :: String
v2 = unlines $ "st" : render allRoles' bookRoleToInt (zip [0 ..] pp)

{-
>>> error v2
*** Exception: st
0                             0                             2                             
| <-- someMsg                 |                                                           
3                             3                             2                             
| someMsg -->                 |                                                           
6                             2                             2                             
                              | someMsg -->                 |                             
6                             10                            10                            
                              | <-- someMsg                 |                             
6                             6                             14                            
| <-- someMsg                 |                                                           
15                            15                            14                            
| someMsg -->                 |                                                           
18                            14                            14                            
                              | someMsg -->                 |                             
18                            22                            22                            
                              | <-- someMsg                 |                             
18                            18                            26                            
| <-- someMsg                 |                                                           
27                            27                            26                            
| someMsg -->                 |                                                           
-}

sdzx-1 commented 2 months ago

data BookRole
  = Buyer
  | Seller
  | Buyer2
  deriving (Show)

bookRoleToInt :: BookRole -> Int
bookRoleToInt = \case
  Buyer -> 0
  Seller -> 1
  Buyer2 -> 2

p :: R BookRole ()
p =
  (Buyer --> Seller) "Title"
    :> Branch
      [ branchVal "BookNotFound" $
          (Buyer <-- Seller) "BookNotFoun"
            :> (Buyer --> Buyer2) "SellerNotFoundBook"
            :> terminal
      , branchVal "BookFound" $
          (Buyer <-- Seller) "Price"
            :> (Buyer --> Buyer2) "PriceToBuyer2"
            :> (Buyer <-- Buyer2) "HalfPrice"
            :> Branch
              [ branchVal "EnoughBudget" $
                  ( (Buyer --> Seller) "Afford"
                      :> (Buyer <-- Seller) "Data"
                      :> (Buyer --> Buyer2) "Success"
                      :> terminal
                  )
              , branchVal "NotEnoughBudget" $
                  ( (Buyer --> Seller) "NotBuy"
                      :> (Buyer --> Buyer2) "Failed"
                      :> terminal
                  )
              ]
      ]

p' :: R BookRole Int
p' = snd $ runIdentity $ runFresh 0 $ addIndex p

rcs = M.genSubMap $ rToConstrs 3 bookRoleToInt p'

p'' :: R BookRole [Int]
p'' =
  fmap (fmap (\i -> fromMaybe i $ IntMap.lookup i rcs)) $
    addSt 3 $
      snd $
        runIdentity $
          runFresh 0 $
            addIndex p

v2 :: [Char]
v2 =
  "st\n"
    ++ render
      [Buyer, Seller, Buyer2]
      bookRoleToInt
      (\is -> [CenterFill ((i + 1) * width) ' ' (show v) | (i, v) <- zip [0 ..] is])
      p''

{-

>>> error v2
\*** Exception: st
------------------Buyer--------------Seller--------------Buyer2-----------------
                   0                   0                   2
        Title      |        --->       |
    ------------------------------BookNotFound------------------------------
                   3                   3                   2
     BookNotFoun   |        <---       |
                   2                   -1                  2
   SellerNotFoundB |                  --->                 |
                   -1                  -1                  -1
                                    Terminal

    --------------------------------BookFound-------------------------------
                   3                   3                   2
        Price      |        <---       |
                   2                   16                  2
    PriceToBuyer2  |                  --->                 |
                   18                  16                  18
      HalfPrice    |                  <---                 |
        --------------------------EnoughBudget--------------------------
                   16                  16                  23
       Afford      |        --->       |
                   24                  24                  23
        Data       |        <---       |
                   23                  -1                  23
       Success     |                  --->                 |
                   -1                  -1                  -1
                                    Terminal

        -------------------------NotEnoughBudget------------------------
                   16                  16                  23
       NotBuy      |        --->       |
                   23                  -1                  23
       Failed      |                  --->                 |
                   -1                  -1                  -1
                                    Terminal

-}

sdzx-1 commented 2 months ago

Finally got here！！！

p :: R BookRole ()
p =
  (Buyer --> Seller) "Title"
    :> Branch
      ()
      [ branchVal "BookNotFound" $
          (Buyer <-- Seller) "BookNotFoun"
            :> (Buyer --> Buyer2) "SellerNotFoundBook"
            :> terminal
      , branchVal "BookFound" $
          (Buyer <-- Seller) "Price"
            :> (Buyer --> Buyer2) "PriceToBuyer2"
            :> (Buyer <-- Buyer2) "HalfPrice"
            :> Branch
              ()
              [ branchVal "EnoughBudget" $
                  ( (Buyer --> Seller) "Afford"
                      :> (Buyer <-- Seller) "Data"
                      :> (Buyer --> Buyer2) "Success"
                      :> terminal
                  )
              , branchVal "NotEnoughBudget" $
                  ( (Buyer --> Seller) "NotBuy"
                      :> (Buyer --> Buyer2) "Failed"
                      :> terminal
                  )
              ]
      ]

{-
-----------------Buyer---------------Seller--------------Buyer2-----------------
                   S0                  S0                 S1 s
       Title       |        --->       |
                  S2 s                S2 s                S1 s
    ------------------------------BookNotFound------------------------------
                  S2 s          S2 BookNotFound           S1 s
    BookNotFoun    |        <---       |
            S1 BookNotFound           End                 S1 s
  SellerNotFoundB  |                  --->                 |
                  End                 End                 End
                                    Terminal

    -------------------------------BookFound--------------------------------
                  S2 s            S2 BookFound            S1 s
       Price       |        <---       |
              S1 BookFound            S3 s                S1 s
   PriceToBuyer2   |                  --->                 |
                   S4                 S3 s                 S4
     HalfPrice     |                  <---                 |
                  S3 s                S3 s                S5 s
        --------------------------EnoughBudget--------------------------
            S3 EnoughBudget           S3 s                S5 s
       Afford      |        --->       |
                   S6                  S6                 S5 s
        Data       |        <---       |
            S5 EnoughBudget           End                 S5 s
      Success      |                  --->                 |
                  End                 End                 End
                                    Terminal

        ------------------------NotEnoughBudget-------------------------
           S3 NotEnoughBudget         S3 s                S5 s
       NotBuy      |        --->       |
           S5 NotEnoughBudget         End                 S5 s
       Failed      |                  --->                 |
                  End                 End                 End
                                    Terminal

-}

sdzx-1 commented 2 months ago

https://github.com/sdzx-1/communication-protocol-state-algorithm

sdzx-1 / typed-communication-protocol

How to develop an algorithm to automatically generate states? #2