{-# LANGUAGE TemplateHaskell #-}
{-# LANGUAGE StandaloneDeriving #-}
{-# LANGUAGE DeriveDataTypeable #-}
{-# LANGUAGE DeriveAnyClass #-}
{-# LANGUAGE ScopedTypeVariables #-}
{-# LANGUAGE OverloadedLists #-}
module Documentation.SBV.Examples.Lists.BoundedMutex where
import Data.SBV
import Data.SBV.Control
import qualified Data.SBV.List as L
import qualified Data.SBV.List.Bounded as L
data State = Idle
| Ready
| Critical
mkSymbolicEnumeration ''State
type SState = SBV State
idle :: SState
idle = literal Idle
ready :: SState
ready = literal Ready
critical :: SState
critical = literal Critical
mutex :: Int -> SList State -> SList State -> SBool
mutex i p1s p2s = L.band i $ L.bzipWith i (\p1 p2 -> p1 ./= critical ||| p2 ./= critical) p1s p2s
validSequence :: Int -> Integer -> SList Integer -> SList State -> SBool
validSequence b me pturns proc = bAnd [ L.length proc .== fromIntegral b
, idle .== L.head proc
, check b pturns proc idle
]
where check 0 _ _ _ = true
check i ts ps prev = let (cur, rest) = L.uncons ps
(turn, turns) = L.uncons ts
ok = ite (prev .== idle) (cur `sElem` [idle, ready])
$ ite (prev .== ready &&& turn .== literal me) (cur `sElem` [critical])
$ ite (prev .== critical) (cur `sElem` [critical, idle])
$ (cur `sElem` [prev])
in ok &&& check (i-1) turns rest cur
validTurns :: Int -> SList Integer -> SList State -> SList State -> SBool
validTurns b turns process1 process2 = bAnd [ L.length turns .== fromIntegral b
, 1 .== L.head turns
, check b turns process1 process2 1
]
where check 0 _ _ _ _ = true
check i ts proc1 proc2 prev = cur `sElem` [1, 2]
&&& (p1 .== critical ||| p2 .== critical ==> cur .== prev)
&&& check (i-1) rest p1s p2s cur
where (cur, rest) = L.uncons ts
(p1, p1s) = L.uncons proc1
(p2, p2s) = L.uncons proc2
checkMutex :: Int -> IO ()
checkMutex b = runSMT $ do
p1 :: SList State <- sList "p1"
p2 :: SList State <- sList "p2"
turns :: SList Integer <- sList "turns"
constrain $ validSequence b 1 turns p1
constrain $ validSequence b 2 turns p2
constrain $ validTurns b turns p1 p2
constrain $ bnot $ mutex b p1 p2
query $ do cs <- checkSat
case cs of
Unk -> error "Solver said Unknown!"
Unsat -> io . putStrLn $ "All is good!"
Sat -> do io . putStrLn $ "Violation detected!"
do p1V <- getValue p1
p2V <- getValue p2
ts <- getValue turns
io . putStrLn $ "P1: " ++ show p1V
io . putStrLn $ "P2: " ++ show p2V
io . putStrLn $ "Ts: " ++ show ts