Language.Atom.Verification

Documentation

data Model

A model of a scheduled program for model checking.

model :: Schedule -> [UV] -> [UA] -> Model

Create a model from a scheduled program.

test :: IO ()

A list of assertions captured by a model. assertions :: Model -> [Name]

Bounded model checking starting from the initial state. boundedModelChecking :: Model -> Int -> Name -> IO (Maybe Witness)

K-induction model checking given a min and a max k-depth. kInduction :: Model -> Int -> Int -> Name -> IO ()