module CSPM.LTS.Deadlock
(
findDeadlock
)
where
import CSPM.CoreLanguage
import CSPM.FiringRules.Rules
import CSPM.FiringRules.Verifier (viewProcAfter)
import CSPM.FiringRules.FieldConstraints (computeTransitions)
import CSPM.Interpreter (INT, Digest)
import CSPM.Interpreter.Hash
import Control.Monad
import Control.Monad.Trans.State
import Control.Monad.Trans.Class
import qualified Data.Set as Set
import Data.Set (Set)
type Path = ([Rule INT], Process INT)
type BM a = StateT (Set Digest) (Either [Rule INT]) a
findDeadlock ::
Sigma INT
-> Process INT
-> Maybe [Rule INT]
findDeadlock sigma process
= case evalStateT (wave [([],process)]) Set.empty of
Right () -> Nothing
Left p -> Just p
where
wave :: [Path] -> BM ()
wave [] = return ()
wave w = mapM expandPath w >>= wave . concat
expandPath :: Path -> BM [Path]
expandPath (path, node) = do
t <- isOldNode node
if t then return []
else do
let rules = computeTransitions sigma node
when (null rules) $ lift $ Left $ reverse path
return $ map (\r -> (r:path , viewProcAfter r)) rules
isOldNode :: Process INT -> BM Bool
isOldNode n = do
let h = hash n
s <- get
let res = Set.member h s
put $ Set.insert h s
return res