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