module CSPM.LTS.MkLtsDFS
(
dfsStep
,mkLtsDFS
)
where
import CSPM.CoreLanguage
import CSPM.FiringRules.Rules
import CSPM.FiringRules.Verifier (viewProcAfter)
import CSPM.FiringRules.FieldConstraints (computeTransitions)
import CSPM.Interpreter (INT)
import CSPM.LTS.LTS
import qualified Data.Map as Map
import System.Timeout as Timeout
import Control.Exception
import Data.IORef
mkLtsDFS :: Bool -> Maybe Double -> Sigma INT -> Process INT -> IO (LTS, Bool)
mkLtsDFS progressReport maxTime sigma process = do
ltsPtr <- newIORef ([mkLtsNode process],Map.empty)
let tout = case maxTime of
Nothing -> (1)
Just seconds -> round $ seconds * 1000000
res <- Timeout.timeout tout $ dfsLoop ltsPtr sigma
case res of
Nothing -> do
state <- readIORef ltsPtr
return (snd state, False)
Just () -> do
state <- readIORef ltsPtr
return (snd state, True)
dfsLoop :: IORef DFSState -> Sigma INT -> IO ()
dfsLoop ltsPtr sigma = loop
where
loop = do
lts <- fmap snd $ readIORef ltsPtr
evaluate lts
finish <- atomicModifyIORef ltsPtr $ dfsStep sigma
if finish then return () else loop
type DFSState = ([LtsNode],LTS)
dfsStep :: Sigma INT -> DFSState -> (DFSState,Bool)
dfsStep _ ([],lts) = (([],lts),True)
dfsStep sigma (proc:restQueue,lts)
= if proc `Map.member` lts
then ((restQueue,lts),False)
else ((newQueue,newLts),False)
where
transitions :: [Rule INT]
transitions = computeTransitions sigma $ nodeProcess proc
newNodes = map (mkLtsNode . viewProcAfter) transitions
newLts = Map.insert proc transitions lts
newQueue = newNodes ++ restQueue