Using LTL formulae to check system states in quickcheck-state-machine

Sketch_QSM_LTL.hs

{-# LANGUAGE FlexibleInstances  #-}
{-# LANGUAGE GADTs              #-}
{-# LANGUAGE KindSignatures     #-}
{-# LANGUAGE RecordWildCards    #-}
{-# LANGUAGE StandaloneDeriving #-}

module Main where

import           Data.IORef
import           Data.TreeDiff
import           System.IO.Unsafe

import           Test.QuickCheck               (Gen)
import           Test.QuickCheck               as QC
import           Test.QuickCheck.Monadic       as QC
import           Test.StateMachine
import qualified Test.StateMachine.Types       as SM
import qualified Test.StateMachine.Types.Rank2 as Rank2

{-------------------------------------------------------------------------------
  System under test
-------------------------------------------------------------------------------}

systemState :: IORef Int
{-# NOINLINE systemState #-}
systemState = unsafePerformIO $ newIORef undefined

reset :: IO ()
reset = writeIORef systemState 0

-- | Precondition: system must be reset first
incr :: IO ()
incr = modifyIORef' systemState (+ 1)

getState :: IO Int
getState = readIORef systemState

{-------------------------------------------------------------------------------
  "LTL" formula (simplified to triviality)
-------------------------------------------------------------------------------}

data LTL = Eq Int LTL | OK | Falsified
  deriving Show

step :: Int -> LTL -> LTL
step n (Eq n' f)
     | n == n'   = f
     | otherwise = Falsified
step _ OK        = OK
step _ Falsified = Falsified

isFalsified :: LTL -> Bool
isFalsified Falsified = True
isFalsified _         = False

{-------------------------------------------------------------------------------
  Generator
-------------------------------------------------------------------------------}

generator :: Model Symbolic -> Maybe (Gen (Cmd Symbolic))
generator InitModel            = Just $ return Reset
generator (SymbModel DidReset) = Just $ elements [Reset, Incr]

{-------------------------------------------------------------------------------
  Tests
-------------------------------------------------------------------------------}

-- Abstract state we need to know which commands we can generate
-- For this simple example it suffices to know that we did a reset .
data AbstractState = DidReset
  deriving (Show)

-- Our concrete sate during runnig the test are the formulas we want to check
-- We just keep track of a single one for simplicity
type ConcreteState = LTL

-- The formula we want to evaluate
initFormula :: LTL
initFormula = Eq 1 $ Eq 3 $ OK

data Model (r :: * -> *) where
  InitModel :: Model r
  SymbModel :: AbstractState -> Model Symbolic
  ConcModel :: ConcreteState -> Model Concrete

deriving instance Show (Model r)

data Cmd (r :: * -> *) = Reset | Incr
  deriving Show

instance CommandNames Cmd where
  cmdName Reset = "r"
  cmdName Incr  = "i"
  cmdNames _ = ["r", "i"]

data Resp (r :: * -> *) where
  ConcResp :: Int -> Resp Concrete
  SymbResp :: Resp Symbolic

deriving instance Show (Resp r)

semantics' :: Cmd Concrete -> IO ()
semantics' Reset = reset
semantics' Incr  = incr

semantics :: Cmd Concrete -> IO (Resp Concrete)
semantics cmd = semantics' cmd >> ConcResp <$> getState

transition :: Model r -> Cmd r -> Resp r -> Model r
transition  InitModel     Reset  SymbResp    = SymbModel DidReset
transition  InitModel     Reset (ConcResp _) = ConcModel $ initFormula
transition  InitModel     Incr   _           = error "impossible"
transition (SymbModel st) _      SymbResp    = SymbModel st
transition (ConcModel st) _     (ConcResp r) = ConcModel $ step r st

-- Precondition simply states that incr is not valid in the init model
precondition :: Model Symbolic -> Cmd Symbolic -> Logic
precondition InitModel Incr = Bot
precondition _         _    = Top

-- Postcondition says no formulas must have been falsified
postcondition :: Model Concrete -> Cmd Concrete -> Resp Concrete -> Logic
postcondition  InitModel     _  _           = Top
postcondition (ConcModel st) _ (ConcResp r) = Boolean $ not (isFalsified $ step r st)

mock :: Model Symbolic -> Cmd Symbolic -> GenSym (Resp Symbolic)
mock _ _ = return SymbResp

sm :: StateMachine Model Cmd IO Resp
sm = StateMachine {
      initModel     = InitModel
    , transition    = transition
    , precondition  = precondition
    , postcondition = postcondition
    , invariant     = Nothing
    , generator     = generator
    , distribution  = Nothing
    , shrinker      = \_ _ -> []
    , semantics     = semantics
    , mock          = mock
    }

{-------------------------------------------------------------------------------
  ToExpr instances so q-s-m can show how model evolves
  We cheat and just use the Show instance
-------------------------------------------------------------------------------}

instance ToExpr (Model Concrete) where
  toExpr = defaultExprViaShow

{-------------------------------------------------------------------------------
  Some additional type class requirements
  These are trivial due to how we instantiated q-s-m (we make no use of vars)
-------------------------------------------------------------------------------}

instance Rank2.Functor Cmd where
  fmap _ Reset = Reset
  fmap _ Incr  = Incr

instance Rank2.Foldable Cmd where
  foldMap _ _ = mempty

instance Rank2.Traversable Cmd where
  traverse _ Reset = pure Reset
  traverse _ Incr  = pure Incr

instance Rank2.Foldable Resp where
  foldMap _ _ = mempty

{-------------------------------------------------------------------------------
  Top-level test
-------------------------------------------------------------------------------}

prop_sequential :: QC.Property
prop_sequential =
    forAllCommands sm Nothing $ \cmds ->
      QC.monadicIO $ do
        (hist, _model, res) <- runCommands sm cmds
        prettyCommands sm hist $ res QC.=== Ok

main :: IO ()
main = quickCheck prop_sequential