{-# LANGUAGE DeriveAnyClass #-}
{-# LANGUAGE DeriveDataTypeable #-}
{-# 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
import Data.SBV.List ((.!!))
import qualified Data.SBV.List as L
import qualified Data.SBV.Tools.BoundedList as L
data State = Idle
| Ready
| Critical
mkSymbolicEnumeration ''State
type SState = SBV State
idle :: SState
idle :: SBV State
idle = State -> SBV State
forall a. SymVal a => a -> SBV a
literal State
Idle
ready :: SState
ready :: SBV State
ready = State -> SBV State
forall a. SymVal a => a -> SBV a
literal State
Ready
critical :: SState
critical :: SBV State
critical = State -> SBV State
forall a. SymVal a => a -> SBV a
literal State
Critical
mutex :: Int -> SList State -> SList State -> SBool
mutex :: Int -> SList State -> SList State -> SBool
mutex i :: Int
i p1s :: SList State
p1s p2s :: SList State
p2s = Int -> SList Bool -> SBool
L.band Int
i (SList Bool -> SBool) -> SList Bool -> SBool
forall a b. (a -> b) -> a -> b
$ Int
-> (SBV State -> SBV State -> SBool)
-> SList State
-> SList State
-> SList Bool
forall a b c.
(SymVal a, SymVal b, SymVal c) =>
Int -> (SBV a -> SBV b -> SBV c) -> SList a -> SList b -> SList c
L.bzipWith Int
i (\p1 :: SBV State
p1 p2 :: SBV State
p2 -> SBV State
p1 SBV State -> SBV State -> SBool
forall a. EqSymbolic a => a -> a -> SBool
./= SBV State
critical SBool -> SBool -> SBool
.|| SBV State
p2 SBV State -> SBV State -> SBool
forall a. EqSymbolic a => a -> a -> SBool
./= SBV State
critical) SList State
p1s SList State
p2s
validSequence :: Int -> Integer -> SList Integer -> SList State -> SBool
validSequence :: Int -> Integer -> SList Integer -> SList State -> SBool
validSequence b :: Int
b me :: Integer
me pturns :: SList Integer
pturns proc :: SList State
proc = [SBool] -> SBool
sAnd [ SList State -> SInteger
forall a. SymVal a => SList a -> SInteger
L.length SList State
proc SInteger -> SInteger -> SBool
forall a. EqSymbolic a => a -> a -> SBool
.== Int -> SInteger
forall a b. (Integral a, Num b) => a -> b
fromIntegral Int
b
, SBV State
idle SBV State -> SBV State -> SBool
forall a. EqSymbolic a => a -> a -> SBool
.== SList State -> SBV State
forall a. SymVal a => SList a -> SBV a
L.head SList State
proc
, Int -> SList Integer -> SList State -> SBV State -> SBool
forall t.
(Eq t, Num t) =>
t -> SList Integer -> SList State -> SBV State -> SBool
check Int
b SList Integer
pturns SList State
proc SBV State
idle
]
where check :: t -> SList Integer -> SList State -> SBV State -> SBool
check 0 _ _ _ = SBool
sTrue
check i :: t
i ts :: SList Integer
ts ps :: SList State
ps prev :: SBV State
prev = let (cur :: SBV State
cur, rest :: SList State
rest) = SList State -> (SBV State, SList State)
forall a. SymVal a => SList a -> (SBV a, SList a)
L.uncons SList State
ps
(turn :: SInteger
turn, turns :: SList Integer
turns) = SList Integer -> (SInteger, SList Integer)
forall a. SymVal a => SList a -> (SBV a, SList a)
L.uncons SList Integer
ts
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
idle) (SBV State
cur SBV State -> [SBV State] -> SBool
forall a. EqSymbolic a => a -> [a] -> SBool
`sElem` [Item [SBV State]
SBV State
idle, Item [SBV State]
SBV State
ready])
(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
ready 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
critical])
(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
critical) (SBV State
cur SBV State -> [SBV State] -> SBool
forall a. EqSymbolic a => a -> [a] -> SBool
`sElem` [Item [SBV State]
SBV State
critical, Item [SBV State]
SBV State
idle])
(SBV State
cur SBV State -> [SBV State] -> SBool
forall a. EqSymbolic a => a -> [a] -> SBool
`sElem` [Item [SBV State]
SBV State
prev])
in SBool
ok SBool -> SBool -> SBool
.&& t -> SList Integer -> SList State -> SBV State -> SBool
check (t
it -> t -> t
forall a. Num a => a -> a -> a
-1) SList Integer
turns SList State
rest SBV State
cur
validTurns :: Int -> SList Integer -> SList State -> SList State -> SBool
validTurns :: Int -> SList Integer -> SList State -> SList State -> SBool
validTurns b :: Int
b turns :: SList Integer
turns process1 :: SList State
process1 process2 :: SList State
process2 = [SBool] -> SBool
sAnd [ SList Integer -> SInteger
forall a. SymVal a => SList a -> SInteger
L.length SList Integer
turns SInteger -> SInteger -> SBool
forall a. EqSymbolic a => a -> a -> SBool
.== Int -> SInteger
forall a b. (Integral a, Num b) => a -> b
fromIntegral Int
b
, 1 SInteger -> SInteger -> SBool
forall a. EqSymbolic a => a -> a -> SBool
.== SList Integer -> SInteger
forall a. SymVal a => SList a -> SBV a
L.head SList Integer
turns
, Int
-> SList Integer -> SList State -> SList State -> SInteger -> SBool
forall a t.
(Ord a, Num t, Num a, Eq t, SymVal a) =>
t -> SList a -> SList State -> SList State -> SBV a -> SBool
check Int
b SList Integer
turns SList State
process1 SList State
process2 1
]
where check :: t -> SList a -> SList State -> SList State -> SBV a -> SBool
check 0 _ _ _ _ = SBool
sTrue
check i :: t
i ts :: SList a
ts proc1 :: SList State
proc1 proc2 :: SList State
proc2 prev :: SBV a
prev = SBV a
cur SBV a -> [SBV a] -> SBool
forall a. EqSymbolic a => a -> [a] -> SBool
`sElem` [1, 2]
SBool -> SBool -> SBool
.&& (SBV State
p1 SBV State -> SBV State -> SBool
forall a. EqSymbolic a => a -> a -> SBool
.== SBV State
critical SBool -> SBool -> SBool
.|| SBV State
p2 SBV State -> SBV State -> SBool
forall a. EqSymbolic a => a -> a -> SBool
.== SBV State
critical SBool -> SBool -> SBool
.=> SBV a
cur SBV a -> SBV a -> SBool
forall a. EqSymbolic a => a -> a -> SBool
.== SBV a
prev)
SBool -> SBool -> SBool
.&& t -> SList a -> SList State -> SList State -> SBV a -> SBool
check (t
it -> t -> t
forall a. Num a => a -> a -> a
-1) SList a
rest SList State
p1s SList State
p2s SBV a
cur
where (cur :: SBV a
cur, rest :: SList a
rest) = SList a -> (SBV a, SList a)
forall a. SymVal a => SList a -> (SBV a, SList a)
L.uncons SList a
ts
(p1 :: SBV State
p1, p1s :: SList State
p1s) = SList State -> (SBV State, SList State)
forall a. SymVal a => SList a -> (SBV a, SList a)
L.uncons SList State
proc1
(p2 :: SBV State
p2, p2s :: SList State
p2s) = SList State -> (SBV State, SList State)
forall a. SymVal a => SList a -> (SBV a, SList a)
L.uncons SList State
proc2
checkMutex :: Int -> IO ()
checkMutex :: Int -> IO ()
checkMutex b :: Int
b = Symbolic () -> IO ()
forall a. Symbolic a -> IO a
runSMT (Symbolic () -> IO ()) -> Symbolic () -> IO ()
forall a b. (a -> b) -> a -> b
$ do
SList State
p1 :: SList State <- String -> Symbolic (SList State)
forall a. SymVal a => String -> Symbolic (SList a)
sList "p1"
SList State
p2 :: SList State <- String -> Symbolic (SList State)
forall a. SymVal a => String -> Symbolic (SList a)
sList "p2"
SList Integer
turns :: SList Integer <- String -> Symbolic (SList Integer)
forall a. SymVal a => String -> Symbolic (SList a)
sList "turns"
SBool -> Symbolic ()
forall (m :: * -> *). SolverContext m => SBool -> m ()
constrain (SBool -> Symbolic ()) -> SBool -> Symbolic ()
forall a b. (a -> b) -> a -> b
$ Int -> Integer -> SList Integer -> SList State -> SBool
validSequence Int
b 1 SList Integer
turns SList State
p1
SBool -> Symbolic ()
forall (m :: * -> *). SolverContext m => SBool -> m ()
constrain (SBool -> Symbolic ()) -> SBool -> Symbolic ()
forall a b. (a -> b) -> a -> b
$ Int -> Integer -> SList Integer -> SList State -> SBool
validSequence Int
b 2 SList Integer
turns SList State
p2
SBool -> Symbolic ()
forall (m :: * -> *). SolverContext m => SBool -> m ()
constrain (SBool -> Symbolic ()) -> SBool -> Symbolic ()
forall a b. (a -> b) -> a -> b
$ Int -> SList Integer -> SList State -> SList State -> SBool
validTurns Int
b SList Integer
turns SList State
p1 SList State
p2
SBool -> Symbolic ()
forall (m :: * -> *). SolverContext m => SBool -> 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
$ Int -> SList State -> SList State -> SBool
mutex Int
b SList State
p1 SList 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
Unk -> String -> Query ()
forall a. HasCallStack => String -> a
error "Solver said Unknown!"
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
$ "All is good!"
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
$ "Violation detected!"
do [State]
p1V <- SList State -> Query [State]
forall a. SMTValue a => SBV a -> Query a
getValue SList State
p1
[State]
p2V <- SList State -> Query [State]
forall a. SMTValue a => SBV a -> Query a
getValue SList State
p2
[Integer]
ts <- SList Integer -> Query [Integer]
forall a. SMTValue a => SBV a -> Query a
getValue SList Integer
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
$ "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
$ "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
$ "Ts: " String -> ShowS
forall a. [a] -> [a] -> [a]
++ [Integer] -> String
forall a. Show a => a -> String
show [Integer]
ts
notFair :: Int -> IO ()
notFair :: Int -> IO ()
notFair b :: Int
b = Symbolic () -> IO ()
forall a. Symbolic a -> IO a
runSMT (Symbolic () -> IO ()) -> Symbolic () -> IO ()
forall a b. (a -> b) -> a -> b
$ do SList State
p1 :: SList State <- String -> Symbolic (SList State)
forall a. SymVal a => String -> Symbolic (SList a)
sList "p1"
SList State
p2 :: SList State <- String -> Symbolic (SList State)
forall a. SymVal a => String -> Symbolic (SList a)
sList "p2"
SList Integer
turns :: SList Integer <- String -> Symbolic (SList Integer)
forall a. SymVal a => String -> Symbolic (SList a)
sList "turns"
SBool -> Symbolic ()
forall (m :: * -> *). SolverContext m => SBool -> m ()
constrain (SBool -> Symbolic ()) -> SBool -> Symbolic ()
forall a b. (a -> b) -> a -> b
$ Int -> Integer -> SList Integer -> SList State -> SBool
validSequence Int
b 1 SList Integer
turns SList State
p1
SBool -> Symbolic ()
forall (m :: * -> *). SolverContext m => SBool -> m ()
constrain (SBool -> Symbolic ()) -> SBool -> Symbolic ()
forall a b. (a -> b) -> a -> b
$ Int -> Integer -> SList Integer -> SList State -> SBool
validSequence Int
b 2 SList Integer
turns SList State
p2
SBool -> Symbolic ()
forall (m :: * -> *). SolverContext m => SBool -> m ()
constrain (SBool -> Symbolic ()) -> SBool -> Symbolic ()
forall a b. (a -> b) -> a -> b
$ Int -> SList Integer -> SList State -> SList State -> SBool
validTurns Int
b SList Integer
turns SList State
p1 SList State
p2
SBool -> Symbolic ()
forall (m :: * -> *). SolverContext m => SBool -> m ()
constrain (SBool -> Symbolic ()) -> SBool -> Symbolic ()
forall a b. (a -> b) -> a -> b
$ SList State
p2 SList State -> SInteger -> SBV State
forall a. SymVal a => SList a -> SInteger -> SBV a
.!! 1 SBV State -> SBV State -> SBool
forall a. EqSymbolic a => a -> a -> SBool
.== SBV State
ready
SBool -> Symbolic ()
forall (m :: * -> *). SolverContext m => SBool -> 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
$ Int -> SBV State -> SList State -> SBool
forall a. (Eq a, SymVal a) => Int -> SBV a -> SList a -> SBool
L.belem Int
b SBV State
critical SList 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
Unk -> String -> Query ()
forall a. HasCallStack => String -> a
error "Solver said Unknown!"
Unsat -> String -> Query ()
forall a. HasCallStack => String -> a
error "Solver couldn't find a violating trace!"
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
$ "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 <- SList State -> Query [State]
forall a. SMTValue a => SBV a -> Query a
getValue SList State
p1
[State]
p2V <- SList State -> Query [State]
forall a. SMTValue a => SBV a -> Query a
getValue SList State
p2
[Integer]
ts <- SList Integer -> Query [Integer]
forall a. SMTValue a => SBV a -> Query a
getValue SList Integer
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
$ "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
$ "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
$ "Ts: " String -> ShowS
forall a. [a] -> [a] -> [a]
++ [Integer] -> String
forall a. Show a => a -> String
show [Integer]
ts
{-# ANN module ("HLint: ignore Reduce duplication" :: String) #-}