MkLtsDFS.hs

----------------------------------------------------------------------------
-- |
-- Module      :  CSPM.LTS.mkLtsDFS
-- Copyright   :  (c) Fontaine 2011
-- License     :  BSD3
--
-- Maintainer  :  Fontaine@cs.uni-duesseldorf.de
-- Stability   :  experimental
-- Portability :  GHC-only
--
-- Compute the labled transition system of a process.
-- Uses depth first search and runs in the IO-Monad.
-- A Timeout can be set and the function can return a partial LTS
----------------------------------------------------------------------------
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

-- | Generate an LTS with a DFS
{-# WARNING mkLtsDFS "mkLts leaks memory: TODO : fix this" #-}
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)

-- | perform one iteration of the DFS loop
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