atom-0.1.3: A DSL for embedded hard realtime applications.




data Model Source

A model of a scheduled program for model checking.

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

Create a model from a scheduled program.

test :: IO ()Source

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 ()