scyther-proof-0.3.0: Automatic generation of Isabelle/HOL correctness proofs for security protocols.

Control.Monad.BoundedDFS

Contents

Description

A monad for implemented bounded depth-first-search and branch-and-bound search.

Synopsis

Costful operations

class Monad m => MonadCost c m | m -> c whereSource

A monad with integer operation cost recording.

Methods

updateCost :: (c -> c) -> m ()Source

Mark the cost of the current operation.

Unbounded depth-first-search

newtype UnboundedDFS c a Source

An unbounded depth-first search monad for searches formulated using MonadPlus.

Constructors

UnboundedDFS 

Fields

runUnboundedDFS :: Maybe a
 

Bounded depth-first-search

newtype BoundedDFS c a Source

A cost bounded depth-first search monad.

All choices are handled committing and there is no differentiation between failure due to cost overrun and other failures.

Constructors

BoundedDFS 

Fields

unBoundedDFS :: ReaderT (c -> Bool) (StateT c Maybe) a
 

runBoundedDFS :: BoundedDFS c a -> (c -> Bool) -> c -> Maybe (a, c)Source

Run a cost bounded depth-first search.

evalBoundedDFS :: BoundedDFS c a -> (c -> Bool) -> c -> Maybe aSource

Evaluate a cost bounded depth-first search.

execBoundedDFS :: BoundedDFS c a -> (c -> Bool) -> c -> Maybe cSource

Execute a cost bounded depth-first search.

Branch-and-bound search

newtype BranchAndBound c a Source

A branch and bound monad for finding results with the smallest costs.

Constructors

BranchAndBound 

Fields

unBranchAndBound :: ReaderT (c -> Bool) (StateT c Maybe) a
 

runBranchAndBound :: Cost c => BranchAndBound c a -> c -> Maybe (a, c)Source

Run a branch and bound search.

evalBranchAndBound :: Cost c => BranchAndBound c a -> c -> Maybe aSource

Evaluate a branch and bound search.

execBranchAndBound :: Cost c => BranchAndBound c a -> c -> Maybe cSource

Execute a branch and bound search.