CSPM.LTS.MkLtsDFS

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

Documentation

dfsStep :: Sigma INT -> DFSState -> (DFSState, Bool)

perform one iteration of the DFS loop

mkLtsDFS :: Bool -> Maybe Double -> Sigma INT -> Process INT -> IO (LTS, Bool)

Generate an LTS with a DFS