A tool for test case generation based on B machine specifications.