Testing simple state transition checking with SBV

readme.md

problem 0
BMC: Iteration: 0
BMC: Iteration: 1
BMC: Iteration: 2
BMC: Iteration: 3
BMC: Iteration: 4
BMC: Iteration: 5
BMC: Solution found at iteration 5
Right (5,[S (Stopped,10),S (Down,8),S (Down,6),S (Down,4),S (Down,2),S (Down,0)])
> problem 1
BMC: Iteration: 0
BMC: Iteration: 1
BMC: Iteration: 2
BMC: Iteration: 3
BMC: Iteration: 4
BMC: Iteration: 5
BMC: Iteration: 6
BMC: Solution found at iteration 6
Right (6,[S (Stopped,10),S (Up,11),S (Down,9),S (Down,7),S (Down,5),S (Down,3),S (Down,1)])

teste-sbv-state-model-checking.hs

{-# LANGUAGE DeriveAnyClass        #-}
{-# LANGUAGE DeriveDataTypeable    #-}
{-# LANGUAGE DeriveFoldable        #-}
{-# LANGUAGE DeriveFunctor         #-}
{-# LANGUAGE DeriveTraversable     #-}
{-# LANGUAGE FlexibleInstances     #-}
{-# LANGUAGE MultiParamTypeClasses #-}
{-# LANGUAGE StandaloneDeriving    #-}
{-# LANGUAGE TemplateHaskell       #-}
{-# LANGUAGE TupleSections         #-}

import           Data.SBV
import           Data.SBV.Control
import           Data.SBV.List      ((.:))
import           Data.SBV.Tools.BMC

data Dir = Up | Down | Stopped

mkSymbolicEnumeration ''Dir

data S a = S a deriving (Functor, Foldable, Traversable, Show)

instance EqSymbolic Dir where
  Up .== Up = sTrue
  Down .== Down = sTrue
  _ .== _ = sFalse

instance (EqSymbolic a) => EqSymbolic (S a) where
  (S s1) .== (S s2) = s1 .== s2

instance Fresh IO (S ((SDir, SInteger))) where
  fresh = do
    d <- freshVar_
    x <- freshVar_
    pure (S (d, x))

instance Queriable IO (S (SDir, SInteger)) (S (Dir, Integer)) where
  create = S <$> ((,) <$> freshVar_ <*> freshVar_)
  project (S (sd, si)) = S <$> ((,) <$> project sd <*> project si)
  embed (S (sd, si)) = S <$> ((,) <$> embed sd <*> embed si)

problem :: Integer -> IO (Either String (Int, [S (Dir, Integer)]))
problem target = bmc (Just 10) True (pure ()) initial trans goal
  where
    initial :: S ((SDir, SInteger)) -> SBool
    initial (S (d, x)) = x .== 10 .&& d .== literal Stopped

    trans (S (d, x)) = [ S (literal Up, x + 1)
                        , S (literal Down, x - 2)
                        ]

    goal (S (d, x)) = x .== literal target