more

LICENSE

@@ -1,6 +1,6 @@
 MIT License
 
-Copyright (c) 2022 Symbiont Inc.
+Copyright (c) 2022-2023 Symbiont Inc.
 
 Permission is hereby granted, free of charge, to any person obtaining a
 copy of this software and associated documentation files (the

app/Main.hs

@@ -1,101 +1,6 @@
 module Main where
 
-import Control.Exception (assert)
-import Control.Monad (unless)
-import System.Environment
-import System.Exit (die)
-
-import Part05.ClientGenerator
-import Part05.ErrorReporter
-import Part05.EventLoop
-import Part05.StateMachine
-import Part05.Configuration
-import Part05.Codec
-import Part05.Debug
-import Part05.Deployment
-import Part05.Network
-import Part05.Random
-import Part05.History
-import Part05.Time
-
-import qualified Part04.LineariseWithFault as Part4
-
-import qualified Part05.ViewstampReplication.Machine as VR
-import Part05.ViewstampReplication.Test.ClientGenerator (vrGeneratorSchema)
-import Part05.ViewstampReplication.Test.Model (smI, step, initModel, markFailure)
-
-------------------------------------------------------------------------
-
-runMany :: [Seed] -> (Seed -> IO Bool) -> IO ()
-runMany origxs f = go (1 :: Int) origxs
-  where
-  go _i [] = return ()
-  go i (x:xs) = do
-    putStrLn $ "Running iteration: " ++ show i ++ " Seed " ++ show (unSeed x)
-    res <- f x
-    if res
-      then go (succ i) xs
-      else do
-        die $ "Failed iteration: " ++ show i ++ " : Seed " ++ show (unSeed x)
+import Part05.LibMain (libMain)
 
 main :: IO ()
-main = do
-  args <- getArgs
-  case args of
-    ["--simulation"] -> do
-      h <- newHistory
-      _collector <- eventLoopSimulation (Seed 0) echoAgenda h [SomeCodecSM idCodec echoSM] NoGenerator
-      _history <- readHistory h
-      putStrLn "Can't print history yet, need Show/Pretty constraints for parameters..."
-    ["vr", "--simulation", seed, fp] -> do
-      h <- newHistory
-      let
-        nodes = map NodeId [0..4]
-        delta = 15 -- time for primary to do re-broadcast
-        vrSM me = VR.vrSM (filter (/= me) nodes) me delta [] smI
-        printItem label prefix thing =
-          putStrLn $ "\x1b[33m" <> label <> ":\x1b[0m " <> prefix <> show thing
-        printE (HistEvent' d (HistEvent n bs inp as msgs)) = do
-          putStrLn "\n\x1b[32mNew Entry\x1b[0m"
-          printItem "Node" " " n
-          printItem "State before" "\n" bs
-          printItem "Input" (case d of { DidDrop -> "\x1b[31m[DROPPED]\x1b[0m "; DidArrive -> " "}) inp
-          printItem "State after" "\n" as
-          printItem "Sent messages" "" ""
-          mapM_ (\x -> putStrLn $ "  " <> show x) msgs
-        fs = FailureSpec (NetworkFaults 0.15)
-        seed' = read seed
-        endTime = addTimeSeconds 3600 epoch
-      collector <- eventLoopFaultySimulation (Seed seed') (VR.agenda endTime) h fs
-        [ SomeCodecSM VR.vrCodec (vrSM me) | me <- nodes] vrGeneratorSchema
-      history <- readHistory h
-      mapM_ printE history
-      -- let's print the errors again so they are easier to see.
-      reportedErrors <- readFromCollector collector
-      unless (null reportedErrors) (putStrLn "")
-      mapM_ putStrLn reportedErrors
-      writeDebugFile fp history
-      let bbHistory = markFailure (blackboxFailHistory (fmap heEvent history))
-      assert (Part4.linearise step initModel bbHistory) (return ())
-    ["vr", "--simulation-explore"] -> do
-      seeds <- generateSeeds 10
-      runMany seeds $ \ seed -> do
-        h <- newHistory
-        let
-          nodes = map NodeId [0..4]
-          delta = 15 -- time for primary to do re-broadcast
-          vrSM me = VR.vrSM (filter (/= me) nodes) me delta [] smI
-          fs = FailureSpec (NetworkFaults 0.15)
-          endTime = addTimeSeconds 3600 epoch
-        collector <- eventLoopFaultySimulation seed (VR.agenda endTime) h fs
-          [ SomeCodecSM VR.vrCodec (vrSM me) | me <- nodes] vrGeneratorSchema
-        history <- readHistory h
-        -- let's print the errors again so they are easier to see.
-        reportedErrors <- readFromCollector collector
-        unless (null reportedErrors) (putStrLn "")
-        mapM_ putStrLn reportedErrors
-        let bbHistory = markFailure (blackboxFailHistory (fmap heEvent history))
-            isValid = Part4.linearise step initModel bbHistory
-        print bbHistory
-        return (null reportedErrors && isValid)
-    _otherwise       -> eventLoopProduction [SomeCodecSM idCodec echoSM]
+main = libMain

property-based-testing-stateful-systems.cabal

@@ -17,7 +17,7 @@ license:            MIT
 license-file:       LICENSE
 author:             Stevan Andjelkovic and Daniel Gustafsson
 maintainer:         symbiont-stevan-andjelkovic@users.noreply.github.com
-copyright:          Copyright (c) 2022 Symbiont Inc.
+copyright:          Copyright (c) 2022-2023 Symbiont Inc.
 category:           Testing
 extra-source-files:
   CHANGELOG.md
@@ -84,6 +84,7 @@ library
     Part05.EventLoop
     Part05.EventQueue
     Part05.History
+    Part05.LibMain
     Part05.Network
     Part05.Options
     Part05.Random
@@ -120,12 +121,6 @@ library
 
 executable part5
   main-is:          Main.hs
-
-  -- Modules included in this executable, other than Main.
-  -- other-modules:
-
-  -- LANGUAGE extensions used by modules in this package.
-  -- other-extensions:
   build-depends:
     , base
     , property-based-testing-stateful-systems

src/Part05/LibMain.hs

@@ -0,0 +1,101 @@
+module Part05.LibMain (libMain) where
+
+import Control.Exception (assert)
+import Control.Monad (unless)
+import System.Environment
+import System.Exit (die)
+
+import Part05.ClientGenerator
+import Part05.ErrorReporter
+import Part05.EventLoop
+import Part05.StateMachine
+import Part05.Configuration
+import Part05.Codec
+import Part05.Debug
+import Part05.Deployment
+import Part05.Network
+import Part05.Random
+import Part05.History
+import Part05.Time
+
+import qualified Part04.LineariseWithFault as Part4
+
+import qualified Part05.ViewstampReplication.Machine as VR
+import Part05.ViewstampReplication.Test.ClientGenerator (vrGeneratorSchema)
+import Part05.ViewstampReplication.Test.Model (smI, step, initModel, markFailure)
+
+------------------------------------------------------------------------
+
+runMany :: [Seed] -> (Seed -> IO Bool) -> IO ()
+runMany origxs f = go (1 :: Int) origxs
+  where
+  go _i [] = return ()
+  go i (x:xs) = do
+    putStrLn $ "Running iteration: " ++ show i ++ " Seed " ++ show (unSeed x)
+    res <- f x
+    if res
+      then go (succ i) xs
+      else do
+        die $ "Failed iteration: " ++ show i ++ " : Seed " ++ show (unSeed x)
+
+libMain :: IO ()
+libMain = do
+  args <- getArgs
+  case args of
+    ["--simulation"] -> do
+      h <- newHistory
+      _collector <- eventLoopSimulation (Seed 0) echoAgenda h [SomeCodecSM idCodec echoSM] NoGenerator
+      _history <- readHistory h
+      putStrLn "Can't print history yet, need Show/Pretty constraints for parameters..."
+    ["vr", "--simulation", seed, fp] -> do
+      h <- newHistory
+      let
+        nodes = map NodeId [0..4]
+        delta = 15 -- time for primary to do re-broadcast
+        vrSM me = VR.vrSM (filter (/= me) nodes) me delta [] smI
+        printItem label prefix thing =
+          putStrLn $ "\x1b[33m" <> label <> ":\x1b[0m " <> prefix <> show thing
+        printE (HistEvent' d (HistEvent n bs inp as msgs)) = do
+          putStrLn "\n\x1b[32mNew Entry\x1b[0m"
+          printItem "Node" " " n
+          printItem "State before" "\n" bs
+          printItem "Input" (case d of { DidDrop -> "\x1b[31m[DROPPED]\x1b[0m "; DidArrive -> " "}) inp
+          printItem "State after" "\n" as
+          printItem "Sent messages" "" ""
+          mapM_ (\x -> putStrLn $ "  " <> show x) msgs
+        fs = FailureSpec (NetworkFaults 0.15)
+        seed' = read seed
+        endTime = addTimeSeconds 3600 epoch
+      collector <- eventLoopFaultySimulation (Seed seed') (VR.agenda endTime) h fs
+        [ SomeCodecSM VR.vrCodec (vrSM me) | me <- nodes] vrGeneratorSchema
+      history <- readHistory h
+      mapM_ printE history
+      -- let's print the errors again so they are easier to see.
+      reportedErrors <- readFromCollector collector
+      unless (null reportedErrors) (putStrLn "")
+      mapM_ putStrLn reportedErrors
+      writeDebugFile fp history
+      let bbHistory = markFailure (blackboxFailHistory (fmap heEvent history))
+      assert (Part4.linearise step initModel bbHistory) (return ())
+    ["vr", "--simulation-explore"] -> do
+      seeds <- generateSeeds 10
+      runMany seeds $ \ seed -> do
+        h <- newHistory
+        let
+          nodes = map NodeId [0..4]
+          delta = 15 -- time for primary to do re-broadcast
+          vrSM me = VR.vrSM (filter (/= me) nodes) me delta [] smI
+          fs = FailureSpec (NetworkFaults 0.15)
+          endTime = addTimeSeconds 3600 epoch
+        collector <- eventLoopFaultySimulation seed (VR.agenda endTime) h fs
+          [ SomeCodecSM VR.vrCodec (vrSM me) | me <- nodes] vrGeneratorSchema
+        history <- readHistory h
+        -- let's print the errors again so they are easier to see.
+        reportedErrors <- readFromCollector collector
+        unless (null reportedErrors) (putStrLn "")
+        mapM_ putStrLn reportedErrors
+        let bbHistory = markFailure (blackboxFailHistory (fmap heEvent history))
+            isValid = Part4.linearise step initModel bbHistory
+        print bbHistory
+        return (null reportedErrors && isValid)
+    _otherwise       -> eventLoopProduction [SomeCodecSM idCodec echoSM]

src/Part05/StateMachine.hs

@@ -28,6 +28,22 @@ newtype TimerId = TimerId Int
 type SMStep state message response
   = state -> StdGen -> ([Output response message], state, StdGen)
 
+-- The state machine type is a bit more complex what we've seen previously:
+--
+--   * input and output types are parameters so that applications with different
+--     message types can written;
+--   * inputs are split into client requests (synchronous) and internal messages
+--     (asynchrous);
+--   * a step in the SM can returns several outputs, this is useful for
+--     broadcasting;
+--   * outputs can also set and reset timers, which is necessary for
+--     implementing retry logic;
+--   * when the timers expire the event loop will call the SM's timeout handler
+--     (`smTimeout`);
+--   * in addition to the state we also thread through a seed, `StdGen`, so that
+--     the SM can generate random numbers;
+--   * there's also an initisation step (`smInit`) to set up the SM before it's
+--     put to work.
 data SM state request message response = SM
   { smState   :: state
   , smInit    :: SMStep state message response

src/Part05/StateMachineDSL.hs

@@ -21,6 +21,9 @@ import Part05.Time
 
 ------------------------------------------------------------------------
 
+-- The DSL allows us to use do syntax, do `send`s or register timers anywhere
+-- rather than return a list outputs, as well as add pre-conditions via guards
+-- and do early returns.
 type SMM s msg resp a =
   ContT Guard (StateT s (StateT StdGen (Writer [Output resp msg]))) a