Check.hs

{-# LANGUAGE DeriveAnyClass     #-}
{-# LANGUAGE DeriveDataTypeable #-}

module Check where

import Data.SBV
import Data.Generics

-- One of three states we can be in
data State  = S0 | S1 | S2 deriving (Eq, Ord, Show, Read, Data, SymWord, HasKind)
type SState = SBV State

-- Allowed actions
data Action =  A | B deriving (Eq, Ord, Show, Read, Data, SymWord, HasKind)
type SAction = SBV Action

-- Env is the current value of the state, and the value of x
data Env = Env { state :: SState
               , x     :: SInteger
               }

-- Tells SBV how to merge two states, boiler-plate
instance Mergeable Env where
  symbolicMerge l t (Env sa xa) (Env sb xb) = Env (symbolicMerge l t sa sb)
                                                  (symbolicMerge l t xa xb)

-- Move to a new state
move :: Env -> State -> Env
move e s = e{state = literal s}

-- Run through a bunch of choices; return the original unchanged if non of them are true
choose :: Env -> [(SBool, Env)] -> Env
choose initEnv = go
  where go []          = initEnv
        go ((t, n):as) = ite t n (go as)

-- Helpers
ifA, ifB :: SAction -> SBool
ifA act = act .== literal A
ifB act = act .== literal B

-- State 0
s0 :: Env -> SAction -> Env
s0 e a = choose e [ (ifA a &&& x e .> 100, move e S1)
                  , (ifB a               , move e S2)
                  ]

-- State 1
s1 :: Env -> SAction -> Env
s1 e a = choose e [ (ifA a, move e S2)
                  , (ifB a, move e S0)
                  ]

-- State 2
s2 :: Env -> SAction -> Env
s2 e a = choose e [ (ifA a, move e S0)
                  , (ifB a, move e S1)
                  ]

-- The transition relation
transition :: Env -> SAction -> Env
transition e a = choose e [ (state e .== literal S0, s0 e a)
                          , (state e .== literal S1, s1 e a)
                          , (state e .== literal S2, s2 e a)
                          ]

-- Run a sequence of actions
run :: Env -> [SAction] -> Env
run = foldl transition

-- Question: How can we reach the target, starting at S0, in n actions
canReach :: Int -> State -> Predicate
canReach n target = do initX <- free "initialX"
                       as <- mapM (\i -> free ("a" ++ show i)) [0..n-1]
                       let final = run (Env (literal S0) initX) as
                       return $ state final .== literal target

-- Run a reachability query, and print results. Try upto a maximum depth.
reachableBy :: Int -> State -> IO ()
reachableBy lim target = go 0
  where go i | i > lim = putStrLn $ "Giving up. Cannot reach at depth " ++ show lim
             | True    = do putStrLn $ "Checking at depth " ++ show i
                            res <- sat $ canReach i target
                            if modelExists res
                               then do putStrLn "Found a solution:"
                                       print res
                               else go (i+1)

-- See if we can reach S2 in at most 5 moves
main :: IO ()
main = reachableBy 5 S2

-- Output:
--
-- *Check> main
-- Checking at depth 0
-- Checking at depth 1
-- Found a solution:
-- Satisfiable. Model:
--   initialX = 0 :: Integer
--   a0       = B :: Action
--
-- Which shows that S2 is reacable in 1 action (B), where X is 0. (The value of X doesn't really
-- matter in this case, but SBV will always give you one.)