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 Control.Monad
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
void $ 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