-----------------------------------------------------------------------------
-- |
-- 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 DeriveAnyClass      #-}
{-# LANGUAGE DeriveDataTypeable  #-}
{-# LANGUAGE FlexibleContexts    #-}
{-# LANGUAGE OverloadedLists     #-}
{-# LANGUAGE ScopedTypeVariables #-}
{-# LANGUAGE StandaloneDeriving  #-}
{-# LANGUAGE TemplateHaskell     #-}

{-# 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 (Int -> State
State -> Int
State -> [State]
State -> State
State -> State -> [State]
State -> State -> State -> [State]
(State -> State)
-> (State -> State)
-> (Int -> State)
-> (State -> Int)
-> (State -> [State])
-> (State -> State -> [State])
-> (State -> State -> [State])
-> (State -> State -> State -> [State])
-> Enum State
forall a.
(a -> a)
-> (a -> a)
-> (Int -> a)
-> (a -> Int)
-> (a -> [a])
-> (a -> a -> [a])
-> (a -> a -> [a])
-> (a -> a -> a -> [a])
-> Enum a
$csucc :: State -> State
succ :: State -> State
$cpred :: State -> State
pred :: State -> State
$ctoEnum :: Int -> State
toEnum :: Int -> State
$cfromEnum :: State -> Int
fromEnum :: State -> Int
$cenumFrom :: State -> [State]
enumFrom :: State -> [State]
$cenumFromThen :: State -> State -> [State]
enumFromThen :: State -> State -> [State]
$cenumFromTo :: State -> State -> [State]
enumFromTo :: State -> State -> [State]
$cenumFromThenTo :: State -> State -> State -> [State]
enumFromThenTo :: State -> State -> State -> [State]
Enum, State
State -> State -> Bounded State
forall a. a -> a -> Bounded a
$cminBound :: State
minBound :: State
$cmaxBound :: State
maxBound :: State
Bounded)

-- | Make 'State' a symbolic enumeration
mkSymbolicEnumeration ''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 :: [SBV State] -> [SBV State] -> SBool
mutex [SBV State]
p1s [SBV State]
p2s = [SBool] -> SBool
sAnd ([SBool] -> SBool) -> [SBool] -> SBool
forall a b. (a -> b) -> a -> b
$ (SBV State -> SBV State -> SBool)
-> [SBV State] -> [SBV State] -> [SBool]
forall a b c. (a -> b -> c) -> [a] -> [b] -> [c]
zipWith (\SBV State
p1 SBV State
p2 -> SBV State
p1 SBV State -> SBV State -> SBool
forall a. EqSymbolic a => a -> a -> SBool
./= SBV State
sCritical SBool -> SBool -> SBool
.|| SBV State
p2 SBV State -> SBV State -> SBool
forall a. EqSymbolic a => a -> a -> SBool
./= SBV State
sCritical) [SBV State]
p1s [SBV State]
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 :: Integer -> [SInteger] -> [SBV State] -> SBool
validSequence Integer
_  []     [SBV State]
_           = SBool
sTrue
validSequence Integer
_  [SInteger]
_      []          = SBool
sTrue
validSequence Integer
me [SInteger]
pturns procs :: [SBV State]
procs@(SBV State
p:[SBV State]
_) = [SBool] -> SBool
sAnd [ SBV State
sIdle SBV State -> SBV State -> SBool
forall a. EqSymbolic a => a -> a -> SBool
.== SBV State
p
                                           , [SInteger] -> [SBV State] -> SBV State -> SBool
check [SInteger]
pturns [SBV State]
procs SBV State
sIdle
                                           ]
   where check :: [SInteger] -> [SBV State] -> SBV State -> SBool
check []           [SBV State]
_          SBV State
_    = SBool
sTrue
         check [SInteger]
_            []         SBV State
_    = SBool
sTrue
         check (SInteger
turn:[SInteger]
turns) (SBV State
cur:[SBV State]
rest) SBV State
prev = SBool
ok SBool -> SBool -> SBool
.&& [SInteger] -> [SBV State] -> SBV State -> SBool
check [SInteger]
turns [SBV State]
rest SBV State
cur
           where ok :: SBool
ok = SBool -> SBool -> SBool -> SBool
forall a. Mergeable a => SBool -> a -> a -> a
ite (SBV State
prev SBV State -> SBV State -> SBool
forall a. EqSymbolic a => a -> a -> SBool
.== SBV State
sIdle)                          (SBV State
cur SBV State -> [SBV State] -> SBool
forall a. EqSymbolic a => a -> [a] -> SBool
`sElem` [Item [SBV State]
SBV State
sIdle, Item [SBV State]
SBV State
sReady])
                    (SBool -> SBool) -> SBool -> SBool
forall a b. (a -> b) -> a -> b
$ SBool -> SBool -> SBool -> SBool
forall a. Mergeable a => SBool -> a -> a -> a
ite (SBV State
prev SBV State -> SBV State -> SBool
forall a. EqSymbolic a => a -> a -> SBool
.== SBV State
sReady SBool -> SBool -> SBool
.&& SInteger
turn SInteger -> SInteger -> SBool
forall a. EqSymbolic a => a -> a -> SBool
.== Integer -> SInteger
forall a. SymVal a => a -> SBV a
literal Integer
me) (SBV State
cur SBV State -> [SBV State] -> SBool
forall a. EqSymbolic a => a -> [a] -> SBool
`sElem` [Item [SBV State]
SBV State
sCritical])
                    (SBool -> SBool) -> SBool -> SBool
forall a b. (a -> b) -> a -> b
$ SBool -> SBool -> SBool -> SBool
forall a. Mergeable a => SBool -> a -> a -> a
ite (SBV State
prev SBV State -> SBV State -> SBool
forall a. EqSymbolic a => a -> a -> SBool
.== SBV State
sCritical)                      (SBV State
cur SBV State -> [SBV State] -> SBool
forall a. EqSymbolic a => a -> [a] -> SBool
`sElem` [Item [SBV State]
SBV State
sCritical, Item [SBV State]
SBV State
sIdle])
                                                                    (SBV State
cur SBV State -> [SBV State] -> SBool
forall a. EqSymbolic a => a -> [a] -> SBool
`sElem` [Item [SBV State]
SBV State
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 :: [SInteger] -> [SBV State] -> [SBV State] -> SBool
validTurns []                    [SBV State]
_        [SBV State]
_        = SBool
sTrue
validTurns turns :: [SInteger]
turns@(SInteger
firstTurn : [SInteger]
_) [SBV State]
process1 [SBV State]
process2 = SInteger
firstTurn SInteger -> SInteger -> SBool
forall a. EqSymbolic a => a -> a -> SBool
.== SInteger
1 SBool -> SBool -> SBool
.&& [(SInteger, SBV State, SBV State)] -> SInteger -> SBool
forall {a}.
(SymVal a, Num a) =>
[(SBV a, SBV State, SBV State)] -> SBV a -> SBool
check ([SInteger]
-> [SBV State] -> [SBV State] -> [(SInteger, SBV State, SBV State)]
forall a b c. [a] -> [b] -> [c] -> [(a, b, c)]
zip3 [SInteger]
turns [SBV State]
process1 [SBV State]
process2) SInteger
1
  where check :: [(SBV a, SBV State, SBV State)] -> SBV a -> SBool
check []                     SBV a
_    = SBool
sTrue
        check ((SBV a
cur, SBV State
p1, SBV State
p2) : [(SBV a, SBV State, SBV State)]
rest) SBV a
prev =   SBV a
cur SBV a -> [SBV a] -> SBool
forall a. EqSymbolic a => a -> [a] -> SBool
`sElem` (a -> SBV a) -> [a] -> [SBV a]
forall a b. (a -> b) -> [a] -> [b]
map a -> SBV a
forall a. SymVal a => a -> SBV a
literal [a
Item [a]
1, a
Item [a]
2]
                                          SBool -> SBool -> SBool
.&& (SBV State
p1 SBV State -> SBV State -> SBool
forall a. EqSymbolic a => a -> a -> SBool
.== SBV State
sCritical SBool -> SBool -> SBool
.|| SBV State
p2 SBV State -> SBV State -> SBool
forall a. EqSymbolic a => a -> a -> SBool
.== SBV State
sCritical SBool -> SBool -> SBool
.=> SBV a
cur SBV a -> SBV a -> SBool
forall a. EqSymbolic a => a -> a -> SBool
.== SBV a
prev)
                                          SBool -> SBool -> SBool
.&& [(SBV a, SBV State, SBV State)] -> SBV a -> SBool
check [(SBV a, SBV State, SBV State)]
rest SBV a
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 :: Int -> IO ()
checkMutex Int
b = Symbolic () -> IO ()
forall a. Symbolic a -> IO a
runSMT (Symbolic () -> IO ()) -> Symbolic () -> IO ()
forall a b. (a -> b) -> a -> b
$ do
                  [SBV State]
p1    :: [SState]   <- (Int -> SymbolicT IO (SBV State))
-> [Int] -> SymbolicT IO [SBV State]
forall (t :: * -> *) (m :: * -> *) a b.
(Traversable t, Monad m) =>
(a -> m b) -> t a -> m (t b)
forall (m :: * -> *) a b. Monad m => (a -> m b) -> [a] -> m [b]
mapM (\Int
i -> String -> SymbolicT IO (SBV State)
forall a. SymVal a => String -> Symbolic (SBV a)
free (String
"p1_" String -> ShowS
forall a. [a] -> [a] -> [a]
++ Int -> String
forall a. Show a => a -> String
show Int
i)) [Int
Item [Int]
1 .. Int
Item [Int]
b]
                  [SBV State]
p2    :: [SState]   <- (Int -> SymbolicT IO (SBV State))
-> [Int] -> SymbolicT IO [SBV State]
forall (t :: * -> *) (m :: * -> *) a b.
(Traversable t, Monad m) =>
(a -> m b) -> t a -> m (t b)
forall (m :: * -> *) a b. Monad m => (a -> m b) -> [a] -> m [b]
mapM (\Int
i -> String -> SymbolicT IO (SBV State)
forall a. SymVal a => String -> Symbolic (SBV a)
free (String
"p2_" String -> ShowS
forall a. [a] -> [a] -> [a]
++ Int -> String
forall a. Show a => a -> String
show Int
i)) [Int
Item [Int]
1 .. Int
Item [Int]
b]
                  [SInteger]
turns :: [SInteger] <- (Int -> SymbolicT IO SInteger) -> [Int] -> SymbolicT IO [SInteger]
forall (t :: * -> *) (m :: * -> *) a b.
(Traversable t, Monad m) =>
(a -> m b) -> t a -> m (t b)
forall (m :: * -> *) a b. Monad m => (a -> m b) -> [a] -> m [b]
mapM (\Int
i -> String -> SymbolicT IO SInteger
forall a. SymVal a => String -> Symbolic (SBV a)
free (String
"t_"  String -> ShowS
forall a. [a] -> [a] -> [a]
++ Int -> String
forall a. Show a => a -> String
show Int
i)) [Int
Item [Int]
1 .. Int
Item [Int]
b]

                  -- Ensure that both sequences and the turns are valid
                  SBool -> Symbolic ()
forall a. QuantifiedBool a => a -> Symbolic ()
forall (m :: * -> *) a.
(SolverContext m, QuantifiedBool a) =>
a -> m ()
constrain (SBool -> Symbolic ()) -> SBool -> Symbolic ()
forall a b. (a -> b) -> a -> b
$ Integer -> [SInteger] -> [SBV State] -> SBool
validSequence Integer
1 [SInteger]
turns [SBV State]
p1
                  SBool -> Symbolic ()
forall a. QuantifiedBool a => a -> Symbolic ()
forall (m :: * -> *) a.
(SolverContext m, QuantifiedBool a) =>
a -> m ()
constrain (SBool -> Symbolic ()) -> SBool -> Symbolic ()
forall a b. (a -> b) -> a -> b
$ Integer -> [SInteger] -> [SBV State] -> SBool
validSequence Integer
2 [SInteger]
turns [SBV State]
p2
                  SBool -> Symbolic ()
forall a. QuantifiedBool a => a -> Symbolic ()
forall (m :: * -> *) a.
(SolverContext m, QuantifiedBool a) =>
a -> m ()
constrain (SBool -> Symbolic ()) -> SBool -> Symbolic ()
forall a b. (a -> b) -> a -> b
$ [SInteger] -> [SBV State] -> [SBV State] -> SBool
validTurns      [SInteger]
turns [SBV State]
p1 [SBV State]
p2

                  -- Try to assert that mutex does not hold. If we get a
                  -- counter example, we would've found a violation!
                  SBool -> Symbolic ()
forall a. QuantifiedBool a => a -> Symbolic ()
forall (m :: * -> *) a.
(SolverContext m, QuantifiedBool a) =>
a -> m ()
constrain (SBool -> Symbolic ()) -> SBool -> Symbolic ()
forall a b. (a -> b) -> a -> b
$ SBool -> SBool
sNot (SBool -> SBool) -> SBool -> SBool
forall a b. (a -> b) -> a -> b
$ [SBV State] -> [SBV State] -> SBool
mutex [SBV State]
p1 [SBV State]
p2

                  Query () -> Symbolic ()
forall a. Query a -> Symbolic a
query (Query () -> Symbolic ()) -> Query () -> Symbolic ()
forall a b. (a -> b) -> a -> b
$ do CheckSatResult
cs <- Query CheckSatResult
checkSat
                             case CheckSatResult
cs of
                               CheckSatResult
Unk    -> String -> Query ()
forall a. HasCallStack => String -> a
error String
"Solver said Unknown!"
                               DSat{} -> String -> Query ()
forall a. HasCallStack => String -> a
error String
"Solver said delta-satisfiable!"
                               CheckSatResult
Unsat  -> IO () -> Query ()
forall a. IO a -> Query a
io (IO () -> Query ()) -> (String -> IO ()) -> String -> Query ()
forall b c a. (b -> c) -> (a -> b) -> a -> c
. String -> IO ()
putStrLn (String -> Query ()) -> String -> Query ()
forall a b. (a -> b) -> a -> b
$ String
"All is good!"
                               CheckSatResult
Sat    -> do IO () -> Query ()
forall a. IO a -> Query a
io (IO () -> Query ()) -> (String -> IO ()) -> String -> Query ()
forall b c a. (b -> c) -> (a -> b) -> a -> c
. String -> IO ()
putStrLn (String -> Query ()) -> String -> Query ()
forall a b. (a -> b) -> a -> b
$ String
"Violation detected!"
                                            do [State]
p1V <- (SBV State -> QueryT IO State) -> [SBV State] -> QueryT IO [State]
forall (t :: * -> *) (m :: * -> *) a b.
(Traversable t, Monad m) =>
(a -> m b) -> t a -> m (t b)
forall (m :: * -> *) a b. Monad m => (a -> m b) -> [a] -> m [b]
mapM SBV State -> QueryT IO State
forall a. SymVal a => SBV a -> Query a
getValue [SBV State]
p1
                                               [State]
p2V <- (SBV State -> QueryT IO State) -> [SBV State] -> QueryT IO [State]
forall (t :: * -> *) (m :: * -> *) a b.
(Traversable t, Monad m) =>
(a -> m b) -> t a -> m (t b)
forall (m :: * -> *) a b. Monad m => (a -> m b) -> [a] -> m [b]
mapM SBV State -> QueryT IO State
forall a. SymVal a => SBV a -> Query a
getValue [SBV State]
p2
                                               [Integer]
ts  <- (SInteger -> QueryT IO Integer)
-> [SInteger] -> QueryT IO [Integer]
forall (t :: * -> *) (m :: * -> *) a b.
(Traversable t, Monad m) =>
(a -> m b) -> t a -> m (t b)
forall (m :: * -> *) a b. Monad m => (a -> m b) -> [a] -> m [b]
mapM SInteger -> QueryT IO Integer
forall a. SymVal a => SBV a -> Query a
getValue [SInteger]
turns

                                               IO () -> Query ()
forall a. IO a -> Query a
io (IO () -> Query ()) -> (String -> IO ()) -> String -> Query ()
forall b c a. (b -> c) -> (a -> b) -> a -> c
. String -> IO ()
putStrLn (String -> Query ()) -> String -> Query ()
forall a b. (a -> b) -> a -> b
$ String
"P1: " String -> ShowS
forall a. [a] -> [a] -> [a]
++ [State] -> String
forall a. Show a => a -> String
show [State]
p1V
                                               IO () -> Query ()
forall a. IO a -> Query a
io (IO () -> Query ()) -> (String -> IO ()) -> String -> Query ()
forall b c a. (b -> c) -> (a -> b) -> a -> c
. String -> IO ()
putStrLn (String -> Query ()) -> String -> Query ()
forall a b. (a -> b) -> a -> b
$ String
"P2: " String -> ShowS
forall a. [a] -> [a] -> [a]
++ [State] -> String
forall a. Show a => a -> String
show [State]
p2V
                                               IO () -> Query ()
forall a. IO a -> Query a
io (IO () -> Query ()) -> (String -> IO ()) -> String -> Query ()
forall b c a. (b -> c) -> (a -> b) -> a -> c
. String -> IO ()
putStrLn (String -> Query ()) -> String -> Query ()
forall a b. (a -> b) -> a -> b
$ String
"Ts: " String -> ShowS
forall a. [a] -> [a] -> [a]
++ [Integer] -> String
forall a. Show a => a -> String
show [Integer]
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 :: Int -> IO ()
notFair Int
b = Symbolic () -> IO ()
forall a. Symbolic a -> IO a
runSMT (Symbolic () -> IO ()) -> Symbolic () -> IO ()
forall a b. (a -> b) -> a -> b
$ do [SBV State]
p1    :: [SState]   <- (Int -> SymbolicT IO (SBV State))
-> [Int] -> SymbolicT IO [SBV State]
forall (t :: * -> *) (m :: * -> *) a b.
(Traversable t, Monad m) =>
(a -> m b) -> t a -> m (t b)
forall (m :: * -> *) a b. Monad m => (a -> m b) -> [a] -> m [b]
mapM (\Int
i -> String -> SymbolicT IO (SBV State)
forall a. SymVal a => String -> Symbolic (SBV a)
free (String
"p1_" String -> ShowS
forall a. [a] -> [a] -> [a]
++ Int -> String
forall a. Show a => a -> String
show Int
i)) [Int
Item [Int]
1 .. Int
Item [Int]
b]
                        [SBV State]
p2    :: [SState]   <- (Int -> SymbolicT IO (SBV State))
-> [Int] -> SymbolicT IO [SBV State]
forall (t :: * -> *) (m :: * -> *) a b.
(Traversable t, Monad m) =>
(a -> m b) -> t a -> m (t b)
forall (m :: * -> *) a b. Monad m => (a -> m b) -> [a] -> m [b]
mapM (\Int
i -> String -> SymbolicT IO (SBV State)
forall a. SymVal a => String -> Symbolic (SBV a)
free (String
"p2_" String -> ShowS
forall a. [a] -> [a] -> [a]
++ Int -> String
forall a. Show a => a -> String
show Int
i)) [Int
Item [Int]
1 .. Int
Item [Int]
b]
                        [SInteger]
turns :: [SInteger] <- (Int -> SymbolicT IO SInteger) -> [Int] -> SymbolicT IO [SInteger]
forall (t :: * -> *) (m :: * -> *) a b.
(Traversable t, Monad m) =>
(a -> m b) -> t a -> m (t b)
forall (m :: * -> *) a b. Monad m => (a -> m b) -> [a] -> m [b]
mapM (\Int
i -> String -> SymbolicT IO SInteger
forall a. SymVal a => String -> Symbolic (SBV a)
free (String
"t_"  String -> ShowS
forall a. [a] -> [a] -> [a]
++ Int -> String
forall a. Show a => a -> String
show Int
i)) [Int
Item [Int]
1 .. Int
Item [Int]
b]

                        -- Ensure that both sequences and the turns are valid
                        SBool -> Symbolic ()
forall a. QuantifiedBool a => a -> Symbolic ()
forall (m :: * -> *) a.
(SolverContext m, QuantifiedBool a) =>
a -> m ()
constrain (SBool -> Symbolic ()) -> SBool -> Symbolic ()
forall a b. (a -> b) -> a -> b
$ Integer -> [SInteger] -> [SBV State] -> SBool
validSequence Integer
1 [SInteger]
turns [SBV State]
p1
                        SBool -> Symbolic ()
forall a. QuantifiedBool a => a -> Symbolic ()
forall (m :: * -> *) a.
(SolverContext m, QuantifiedBool a) =>
a -> m ()
constrain (SBool -> Symbolic ()) -> SBool -> Symbolic ()
forall a b. (a -> b) -> a -> b
$ Integer -> [SInteger] -> [SBV State] -> SBool
validSequence Integer
2 [SInteger]
turns [SBV State]
p2
                        SBool -> Symbolic ()
forall a. QuantifiedBool a => a -> Symbolic ()
forall (m :: * -> *) a.
(SolverContext m, QuantifiedBool a) =>
a -> m ()
constrain (SBool -> Symbolic ()) -> SBool -> Symbolic ()
forall a b. (a -> b) -> a -> b
$ [SInteger] -> [SBV State] -> [SBV State] -> SBool
validTurns    [SInteger]
turns [SBV State]
p1 [SBV State]
p2

                        -- Ensure that the second process becomes ready in the second cycle:
                        SBool -> Symbolic ()
forall a. QuantifiedBool a => a -> Symbolic ()
forall (m :: * -> *) a.
(SolverContext m, QuantifiedBool a) =>
a -> m ()
constrain (SBool -> Symbolic ()) -> SBool -> Symbolic ()
forall a b. (a -> b) -> a -> b
$ [SBV State]
p2 [SBV State] -> Int -> SBV State
forall a. HasCallStack => [a] -> Int -> a
!! Int
1 SBV State -> SBV State -> SBool
forall a. EqSymbolic a => a -> a -> SBool
.== SBV State
sReady

                        -- Find a trace where p2 never goes critical
                        -- counter example, we would've found a violation!
                        SBool -> Symbolic ()
forall a. QuantifiedBool a => a -> Symbolic ()
forall (m :: * -> *) a.
(SolverContext m, QuantifiedBool a) =>
a -> m ()
constrain (SBool -> Symbolic ()) -> SBool -> Symbolic ()
forall a b. (a -> b) -> a -> b
$ SBool -> SBool
sNot (SBool -> SBool) -> SBool -> SBool
forall a b. (a -> b) -> a -> b
$ SBV State
sCritical SBV State -> [SBV State] -> SBool
forall a. EqSymbolic a => a -> [a] -> SBool
`sElem` [SBV State]
p2

                        Query () -> Symbolic ()
forall a. Query a -> Symbolic a
query (Query () -> Symbolic ()) -> Query () -> Symbolic ()
forall a b. (a -> b) -> a -> b
$ do CheckSatResult
cs <- Query CheckSatResult
checkSat
                                   case CheckSatResult
cs of
                                     CheckSatResult
Unk    -> String -> Query ()
forall a. HasCallStack => String -> a
error String
"Solver said Unknown!"
                                     DSat{} -> String -> Query ()
forall a. HasCallStack => String -> a
error String
"Solver said delta-satisfiable!"
                                     CheckSatResult
Unsat  -> String -> Query ()
forall a. HasCallStack => String -> a
error String
"Solver couldn't find a violating trace!"
                                     CheckSatResult
Sat    -> do IO () -> Query ()
forall a. IO a -> Query a
io (IO () -> Query ()) -> (String -> IO ()) -> String -> Query ()
forall b c a. (b -> c) -> (a -> b) -> a -> c
. String -> IO ()
putStrLn (String -> Query ()) -> String -> Query ()
forall a b. (a -> b) -> a -> b
$ String
"Fairness is violated at bound: " String -> ShowS
forall a. [a] -> [a] -> [a]
++ Int -> String
forall a. Show a => a -> String
show Int
b
                                                  do [State]
p1V <- (SBV State -> QueryT IO State) -> [SBV State] -> QueryT IO [State]
forall (t :: * -> *) (m :: * -> *) a b.
(Traversable t, Monad m) =>
(a -> m b) -> t a -> m (t b)
forall (m :: * -> *) a b. Monad m => (a -> m b) -> [a] -> m [b]
mapM SBV State -> QueryT IO State
forall a. SymVal a => SBV a -> Query a
getValue [SBV State]
p1
                                                     [State]
p2V <- (SBV State -> QueryT IO State) -> [SBV State] -> QueryT IO [State]
forall (t :: * -> *) (m :: * -> *) a b.
(Traversable t, Monad m) =>
(a -> m b) -> t a -> m (t b)
forall (m :: * -> *) a b. Monad m => (a -> m b) -> [a] -> m [b]
mapM SBV State -> QueryT IO State
forall a. SymVal a => SBV a -> Query a
getValue [SBV State]
p2
                                                     [Integer]
ts  <- (SInteger -> QueryT IO Integer)
-> [SInteger] -> QueryT IO [Integer]
forall (t :: * -> *) (m :: * -> *) a b.
(Traversable t, Monad m) =>
(a -> m b) -> t a -> m (t b)
forall (m :: * -> *) a b. Monad m => (a -> m b) -> [a] -> m [b]
mapM SInteger -> QueryT IO Integer
forall a. SymVal a => SBV a -> Query a
getValue [SInteger]
turns

                                                     IO () -> Query ()
forall a. IO a -> Query a
io (IO () -> Query ()) -> (String -> IO ()) -> String -> Query ()
forall b c a. (b -> c) -> (a -> b) -> a -> c
. String -> IO ()
putStrLn (String -> Query ()) -> String -> Query ()
forall a b. (a -> b) -> a -> b
$ String
"P1: " String -> ShowS
forall a. [a] -> [a] -> [a]
++ [State] -> String
forall a. Show a => a -> String
show [State]
p1V
                                                     IO () -> Query ()
forall a. IO a -> Query a
io (IO () -> Query ()) -> (String -> IO ()) -> String -> Query ()
forall b c a. (b -> c) -> (a -> b) -> a -> c
. String -> IO ()
putStrLn (String -> Query ()) -> String -> Query ()
forall a b. (a -> b) -> a -> b
$ String
"P2: " String -> ShowS
forall a. [a] -> [a] -> [a]
++ [State] -> String
forall a. Show a => a -> String
show [State]
p2V
                                                     IO () -> Query ()
forall a. IO a -> Query a
io (IO () -> Query ()) -> (String -> IO ()) -> String -> Query ()
forall b c a. (b -> c) -> (a -> b) -> a -> c
. String -> IO ()
putStrLn (String -> Query ()) -> String -> Query ()
forall a b. (a -> b) -> a -> b
$ String
"Ts: " String -> ShowS
forall a. [a] -> [a] -> [a]
++ [Integer] -> String
forall a. Show a => a -> String
show [Integer]
ts

{- HLint ignore module "Reduce duplication" -}