[GH-96] T1.2.1 QuickCheck state machine tests, added example.

Makefile

@@ -22,4 +22,8 @@ test-ghci: ## Run repl on test suites
 test-ghcid: ## Run ghcid on test suites
 	@ghcid --command "stack ghci $(PROJECT_NAME):lib $(PROJECT_NAME):test:$(PROJECT_NAME)-test --ghci-options=-fobject-code"
 
-.PHONY: stylish-haskell ghcid ghcid-test run-test test-ghci test-ghcid help
+test-ghcid-nix: ## Run ghcid on test suites with Nix
+	#NUM_PROC = $(nproc --all) # Either try to fetch the real num of cores or default to 4
+	@ghcid --command="stack ghci --test --main-is cardano-shell:test:cardano-shell-test --nix -j12"
+
+.PHONY: stylish-haskell ghcid ghcid-test run-test test-ghci test-ghcid help

cardano-shell.cabal

@@ -175,7 +175,7 @@ executable cardano-launcher
                        -Wincomplete-record-updates
                        -Wincomplete-uni-patterns
                        -Wredundant-constraints
-                       -Wpartial-fields                      
+                       -Wpartial-fields
 
 test-suite cardano-shell-test
   type: exitcode-stdio-1.0
@@ -186,6 +186,7 @@ test-suite cardano-shell-test
   if !os(windows)
     other-modules:
       NodeIPCSpec
+      NodeIPCSMSpec
 
   hs-source-dirs:
       test
@@ -199,6 +200,10 @@ test-suite cardano-shell-test
     , safe-exceptions
     -- quickcheck
     , QuickCheck
+    , quickcheck-state-machine >= 0.6
+    -- required because of QSM
+    , tree-diff
+    , stm
     , hspec
     , hspec-contrib
     , concurrency
@@ -208,7 +213,7 @@ test-suite cardano-shell-test
   default-extensions:  NoImplicitPrelude
                        OverloadedStrings
 
-  ghc-options:         -Wall
+  ghc-options:         
                        -Werror
                        -Wcompat
                        -Wincomplete-record-updates

stack.yaml

@@ -40,6 +40,8 @@ packages:
 # using the same syntax as the packages field.
 # (e.g., acme-missiles-0.3)
 extra-deps:
+  - quickcheck-state-machine-0.6.0 # Used a specific dependency, new release.
+
   - git: https://github.com/input-output-hk/cardano-prelude
     commit: 2256fd727c5f92e6218afdcf8cddf6e01c4a9dcd
     subdirs:
@@ -60,11 +62,8 @@ extra-deps:
       - .
 
   - katip-0.7.0.0@sha256:4b30d0643e18d01a3fd264d3d75921b49b2f464336a52fa46fa049107ebbfe04
-
   - time-units-1.0.0@sha256:27cf54091c4a0ca73d504fc11d5c31ab4041d17404fe3499945e2055697746c1
-
   - ekg-0.4.0.15@sha256:f52d7c00654d72d2ab988255f30adba95a52484ac310bab9c136c64732e69f4b
-
   - ekg-json-0.1.0.6@sha256:4ff2e9cac213a5868ae8b4a7c72a16a9a76fac14d944ae819b3d838a9725569b
 
   - ekg-prometheus-adapter-0.1.0.4

test/NodeIPCSMSpec.hs

@@ -0,0 +1,176 @@
+{-# LANGUAGE DataKinds          #-}
+{-# LANGUAGE DeriveAnyClass     #-}
+{-# LANGUAGE DeriveGeneric      #-}
+{-# LANGUAGE FlexibleInstances  #-}
+{-# LANGUAGE KindSignatures     #-}
+{-# LANGUAGE LambdaCase         #-}
+{-# LANGUAGE PolyKinds          #-}
+{-# LANGUAGE StandaloneDeriving #-}
+
+module NodeIPCSMSpec
+    ( mkEnv
+    , prop_echoOK
+    , prop_echoParallelOK
+    ) where
+
+import           Cardano.Prelude
+
+import           Control.Concurrent.STM (TVar, newTVarIO, readTVar, writeTVar)
+
+import           Data.Kind (Type)
+import           Data.TreeDiff (ToExpr (..))
+
+import           GHC.Generics (Generic, Generic1)
+import           Prelude
+import           Test.QuickCheck (Gen, Property, arbitrary, oneof, (===))
+import           Test.QuickCheck.Monadic (monadicIO)
+
+import           Test.StateMachine
+import           Test.StateMachine.Types
+import qualified Test.StateMachine.Types.Rank2 as Rank2
+
+------------------------------------------------------------------------
+
+-- | Echo API.
+
+data Env = Env
+    { _buf :: TVar (Maybe String) }
+
+-- | Create a new environment.
+mkEnv :: IO Env
+mkEnv = Env <$> newTVarIO Nothing
+
+-- | Input a string. Returns 'True' iff the buffer was empty and the given
+-- string was added to it.
+input :: Env -> String -> IO Bool
+input (Env mBuf) str = atomically $ do
+    res <- readTVar mBuf
+    case res of
+        Nothing -> writeTVar mBuf (Just str) >> return True
+        Just _  -> return False
+
+-- | Output the buffer contents.
+output :: Env -> IO (Maybe String)
+output (Env mBuf) = atomically $ do
+    res <- readTVar mBuf
+    writeTVar mBuf Nothing
+    return res
+
+------------------------------------------------------------------------
+
+-- | Spec for echo.
+
+prop_echoOK :: Property
+prop_echoOK = forAllCommands smUnused Nothing $ \cmds -> monadicIO $ do
+    env <- liftIO $ mkEnv
+    let echoSM' = echoSM env
+    (hist, _, res) <- runCommands echoSM' cmds
+    prettyCommands echoSM' hist (res === Ok)
+
+prop_echoParallelOK :: Bool -> Property
+prop_echoParallelOK problem = forAllParallelCommands smUnused $ \cmds -> monadicIO $ do
+    env <- liftIO $ mkEnv
+    let echoSM' = echoSM env
+    let n | problem   = 2
+          | otherwise = 1
+    prettyParallelCommands cmds =<< runParallelCommandsNTimes n echoSM' cmds
+
+smUnused :: StateMachine Model Action IO Response
+smUnused = echoSM $ error "used env during command generation"
+
+echoSM :: Env -> StateMachine Model Action IO Response
+echoSM env = StateMachine
+    { initModel         = Empty
+    -- ^ At the beginning of time nothing was received.
+    , transition        = mTransitions
+    , precondition      = mPreconditions
+    , postcondition     = mPostconditions
+    , generator         = mGenerator
+    , invariant         = Nothing
+    , shrinker          = mShrinker
+    , semantics         = mSemantics
+    , mock              = mMock
+    , distribution      = Nothing
+    }
+    where
+      mTransitions :: Model r -> Action r -> Response r -> Model r
+      mTransitions Empty   (In str) _   = Buf str
+      mTransitions (Buf _) Echo     _   = Empty
+      mTransitions Empty   Echo     _   = Empty
+      -- TODO: qcsm will match the case below. However we don't expect this to happen!
+      mTransitions (Buf str) (In _)   _ = Buf str -- Dummy response
+          -- error "This shouldn't happen: input transition with full buffer"
+
+      -- | There are no preconditions for this model.
+      mPreconditions :: Model Symbolic -> Action Symbolic -> Logic
+      mPreconditions _ _ = Top
+
+      -- | Post conditions for the system.
+      mPostconditions :: Model Concrete -> Action Concrete -> Response Concrete -> Logic
+      mPostconditions Empty     (In _) InAck     = Top
+      mPostconditions (Buf _)   (In _) ErrFull   = Top
+      mPostconditions _         (In _) _         = Bot
+      mPostconditions Empty     Echo   ErrEmpty  = Top
+      mPostconditions Empty     Echo   _         = Bot
+      mPostconditions (Buf str) Echo   (Out out) = str .== out
+      mPostconditions (Buf _)   Echo   _         = Bot
+
+      -- | Generator for symbolic actions.
+      mGenerator :: Model Symbolic -> Maybe (Gen (Action Symbolic))
+      mGenerator _ =  Just $ oneof
+          [ In <$> arbitrary
+          , return Echo
+          ]
+
+      -- | Trivial shrinker.
+      mShrinker :: Model Symbolic -> Action Symbolic -> [Action Symbolic]
+      mShrinker _ _ = []
+
+      -- | Here we'd do the dispatch to the actual SUT.
+      mSemantics :: Action Concrete -> IO (Response Concrete)
+      mSemantics (In str) = do
+          success <- input env str
+          return $ if success
+                   then InAck
+                   else ErrFull
+      mSemantics Echo = maybe ErrEmpty Out <$> output env
+
+      -- | What is the mock for?
+      mMock :: Model Symbolic -> Action Symbolic -> GenSym (Response Symbolic)
+      mMock Empty (In _)   = return InAck
+      mMock (Buf _) (In _) = return ErrFull
+      mMock Empty Echo     = return ErrEmpty
+      mMock (Buf str) Echo = return (Out str)
+
+deriving instance ToExpr (Model Concrete)
+
+-- | The model contains the last string that was communicated in an input
+-- action.
+data Model (r :: Type -> Type)
+    = -- | The model hasn't been initialized.
+      Empty
+    | -- | Last input string (a buffer with size one).
+      Buf String
+  deriving (Eq, Show, Generic)
+
+-- | Actions supported by the system.
+data Action (r :: Type -> Type)
+    = -- | Input a string, which should be echoed later.
+      In String
+      -- | Request a string output.
+    | Echo
+  deriving (Show, Generic1, Rank2.Foldable, Rank2.Traversable, Rank2.Functor, CommandNames)
+
+-- | The system gives a single type of output response, containing a string
+-- with the input previously received.
+data Response (r :: Type -> Type)
+    = -- | Input acknowledgment.
+      InAck
+      -- | The previous action wasn't an input, so there is no input to echo.
+      -- This is: the buffer is empty.
+    | ErrEmpty
+      -- | There is already a string in the buffer.
+    | ErrFull
+      -- | Output string.
+    | Out String
+  deriving (Show, Generic1, Rank2.Foldable, Rank2.Traversable, Rank2.Functor)

test/Spec.hs

@@ -8,7 +8,7 @@ import           Cardano.Prelude
 import           Control.Concurrent.Classy (MonadConc)
 import           Control.Exception.Safe (throwM)
 import           Test.DejaFu (abortsNever, deadlocksNever, exceptionsNever)
-import           Test.Hspec (Spec, describe, hspec)
+import           Test.Hspec (Spec, describe, hspec, it)
 import           Test.Hspec.Contrib.HUnit (fromHUnitTest)
 import           Test.HUnit.DejaFu (testDejafu)
 import           Test.QuickCheck (Gen, arbitraryASCIIChar, choose, frequency,
@@ -20,13 +20,15 @@ import           Cardano.Shell.Types (CardanoFeature (..))
 
 import           DhallConfigSpec (dhallConfigSpec, mkConfigSpec)
 import           NodeIPCSpec (nodeIPCSpec)
+import           NodeIPCSMSpec
 
 -- | Entry point for tests.
 main :: IO ()
 main = hspec $ do
     describe "App should have no concurrency issues" validConcurrencySpec
     describe "Dhall configurations" dhallConfigSpec
     describe "Cardano configurations" mkConfigSpec
+    describe "NodeIPC state machine example" $ it "check the example works" prop_echoOK
     describe "NodeIPC" nodeIPCSpec
 
 -- | A valid concurrency specification.