ImProve examples.
- buildGCD :: IO ()
- counter :: Stmt ()
- verifyCounter :: IO ()
- arbiterSpec :: (E Bool, E Bool, E Bool) -> (E Bool, E Bool, E Bool) -> Stmt ()
- arbiter :: Name -> ((E Bool, E Bool, E Bool) -> Stmt (E Bool, E Bool, E Bool)) -> Stmt ()
- arbiter1 :: (E Bool, E Bool, E Bool) -> Stmt (E Bool, E Bool, E Bool)
- arbiter2 :: (E Bool, E Bool, E Bool) -> Stmt (E Bool, E Bool, E Bool)
- arbiter3 :: (E Bool, E Bool, E Bool) -> Stmt (E Bool, E Bool, E Bool)
- verifyArbiters :: IO ()
- buildArbiters :: IO ()
- runAll :: IO ()
Documentation
Verify the counter
example.
arbiterSpec :: (E Bool, E Bool, E Bool) -> (E Bool, E Bool, E Bool) -> Stmt ()Source
Arbiter specification.
arbiter :: Name -> ((E Bool, E Bool, E Bool) -> Stmt (E Bool, E Bool, E Bool)) -> Stmt ()Source
Binding an arbiter implemenation to the arbiter specification.
arbiter1 :: (E Bool, E Bool, E Bool) -> Stmt (E Bool, E Bool, E Bool)Source
An arbiter implementation.
arbiter2 :: (E Bool, E Bool, E Bool) -> Stmt (E Bool, E Bool, E Bool)Source
An another arbiter implementation.
arbiter3 :: (E Bool, E Bool, E Bool) -> Stmt (E Bool, E Bool, E Bool)Source
Yet another arbiter implementation.
Verify the different arbiter implementations.
Build the different arbiter implementations.