content: -----------------------------------------------------------------------------
  -- |
  -- Module    : Documentation.SBV.Examples.Lists.BoundedMutex
  -- Copyright : (c) Levent Erkok
  -- License   : BSD3
  -- Maintainer: erkokl@gmail.com
  -- Stability : experimental
  --
  -- Proves a simple mutex algorithm correct up to a given bound.
  -----------------------------------------------------------------------------
  
  {-# LANGUAGE FlexibleInstances   #-}
  {-# LANGUAGE ScopedTypeVariables #-}
  {-# LANGUAGE TemplateHaskell     #-}
  {-# LANGUAGE TypeApplications    #-}
  
  {-# OPTIONS_GHC -Wall -Werror #-}
  
  module Documentation.SBV.Examples.Lists.BoundedMutex where
  
  import Data.SBV
  import Data.SBV.Control
  
  -- | Each agent can be in one of the three states
  data State = Idle     -- ^ Regular work
             | Ready    -- ^ Intention to enter critical state
             | Critical -- ^ In the critical state
             deriving Show
  
  -- | Make 'State' a symbolic enumeration
  mkSymbolic [''State]
  
  -- | The mutex property holds for two sequences of state transitions, if they are not in
  -- their critical section at the same time.
  mutex :: [SState] -> [SState] -> SBool
  mutex p1s p2s = sAnd $ zipWith (\p1 p2 -> p1 ./= sCritical .|| p2 ./= sCritical) p1s p2s
  
  -- | A sequence is valid upto a bound if it starts at 'Idle', and follows the mutex rules. That is:
  --
  --    * From 'Idle' it can switch to 'Ready' or stay 'Idle'
  --    * From 'Ready' it can switch to 'Critical' if it's its turn
  --    * From 'Critical' it can either stay in 'Critical' or go back to 'Idle'
  --
  -- The variable @me@ identifies the agent id.
  validSequence :: Integer -> [SInteger] -> [SState] -> SBool
  validSequence _  []     _           = sTrue
  validSequence _  _      []          = sTrue
  validSequence me pturns procs@(p:_) = sAnd [ sIdle .== p
                                             , check pturns procs sIdle
                                             ]
     where check []           _          _    = sTrue
           check _            []         _    = sTrue
           check (turn:turns) (cur:rest) prev = ok .&& check turns rest cur
             where ok = ite (prev .== sIdle)                          (cur `sElem` [sIdle, sReady])
                      $ ite (prev .== sReady .&& turn .== literal me) (cur `sElem` [sCritical])
                      $ ite (prev .== sCritical)                      (cur `sElem` [sCritical, sIdle])
                                                                      (cur `sElem` [prev])
  
  -- | The mutex algorithm, coded implicitly as an assignment to turns. Turns start at @1@, and at each stage is either
  -- @1@ or @2@; giving preference to that process. The only condition is that if either process is in its critical
  -- section, then the turn value stays the same. Note that this is sufficient to satisfy safety (i.e., mutual
  -- exclusion), though it does not guarantee liveness.
  validTurns :: [SInteger] -> [SState] -> [SState] -> SBool
  validTurns []                    _        _        = sTrue
  validTurns turns@(firstTurn : _) process1 process2 = firstTurn .== 1 .&& check (zip3 turns process1 process2) 1
    where check []                     _    = sTrue
          check ((cur, p1, p2) : rest) prev =   cur `sElem` map literal [1, 2]
                                            .&& (p1 .== sCritical .|| p2 .== sCritical .=> cur .== prev)
                                            .&& check rest cur
  
  -- | Check that we have the mutex property so long as 'validSequence' and 'validTurns' holds; i.e.,
  -- so long as both the agents and the arbiter act according to the rules. The check is bounded up-to-the
  -- given concrete bound; so this is an example of a bounded-model-checking style proof. We have:
  --
  -- >>> checkMutex 20
  -- All is good!
  checkMutex :: Int -> IO ()
  checkMutex b = runSMT $ do
                    p1    :: [SState]   <- mapM (\i -> free ("p1_" ++ show i)) [1 .. b]
                    p2    :: [SState]   <- mapM (\i -> free ("p2_" ++ show i)) [1 .. b]
                    turns :: [SInteger] <- mapM (\i -> free ("t_"  ++ show i)) [1 .. b]
  
                    -- Ensure that both sequences and the turns are valid
                    constrain $ validSequence 1 turns p1
                    constrain $ validSequence 2 turns p2
                    constrain $ validTurns      turns p1 p2
  
                    -- Try to assert that mutex does not hold. If we get a
                    -- counter example, we would've found a violation!
                    constrain $ sNot $ mutex p1 p2
  
                    query $ do cs <- checkSat
                               case cs of
                                 Unk    -> error "Solver said Unknown!"
                                 DSat{} -> error "Solver said delta-satisfiable!"
                                 Unsat  -> io . putStrLn $ "All is good!"
                                 Sat    -> do io . putStrLn $ "Violation detected!"
                                              do p1V <- mapM getValue p1
                                                 p2V <- mapM getValue p2
                                                 ts  <- mapM getValue turns
  
                                                 io . putStrLn $ "P1: " ++ show p1V
                                                 io . putStrLn $ "P2: " ++ show p2V
                                                 io . putStrLn $ "Ts: " ++ show ts
  
  -- | Our algorithm is correct, but it is not fair. It does not guarantee that a process that
  -- wants to enter its critical-section will always do so eventually. Demonstrate this by
  -- trying to show a bounded trace of length 10, such that the second process is ready but
  -- never transitions to critical. We have:
  --
  -- >>> notFair 10
  -- Fairness is violated at bound: 10
  -- P1: [Idle,Idle,Ready,Critical,Idle,Ready,Critical,Critical,Idle,Ready]
  -- P2: [Idle,Ready,Ready,Ready,Ready,Ready,Ready,Ready,Ready,Ready]
  -- Ts: [1,1,1,1,1,1,1,1,1,1]
  --
  -- As expected, P2 gets ready but never goes critical since the arbiter keeps picking
  -- P1 unfairly. (You might get a different trace depending on what z3 happens to produce!)
  --
  -- Exercise for the reader: Change the 'validTurns' function so that it alternates the turns
  -- from the previous value if neither process is in critical. Show that this makes the 'notFair'
  -- function below no longer exhibits the issue. Is this sufficient? Concurrent programming is tricky!
  notFair :: Int -> IO ()
  notFair b = runSMT $ do p1    :: [SState]   <- mapM (\i -> free ("p1_" ++ show i)) [1 .. b]
                          p2    :: [SState]   <- mapM (\i -> free ("p2_" ++ show i)) [1 .. b]
                          turns :: [SInteger] <- mapM (\i -> free ("t_"  ++ show i)) [1 .. b]
  
                          -- Ensure that both sequences and the turns are valid
                          constrain $ validSequence 1 turns p1
                          constrain $ validSequence 2 turns p2
                          constrain $ validTurns    turns p1 p2
  
                          -- Ensure that the second process becomes ready in the second cycle:
                          constrain $ p2 !! 1 .== sReady
  
                          -- Find a trace where p2 never goes critical
                          -- counter example, we would've found a violation!
                          constrain $ sNot $ sCritical `sElem` p2
  
                          query $ do cs <- checkSat
                                     case cs of
                                       Unk    -> error "Solver said Unknown!"
                                       DSat{} -> error "Solver said delta-satisfiable!"
                                       Unsat  -> error "Solver couldn't find a violating trace!"
                                       Sat    -> do io . putStrLn $ "Fairness is violated at bound: " ++ show b
                                                    do p1V <- mapM getValue p1
                                                       p2V <- mapM getValue p2
                                                       ts  <- mapM getValue turns
  
                                                       io . putStrLn $ "P1: " ++ show p1V
                                                       io . putStrLn $ "P2: " ++ show p2V
                                                       io . putStrLn $ "Ts: " ++ show ts
  
  {- HLint ignore module "Reduce duplication" -}
  