Fastest is a model-based testing tool that works with specifications written in the Z notation.
The tool implements[1] the Test Template Framework (TTF) proposed by Phil Stocks and David Carrington.
The user first needs to load a Z specification written in LaTeX format verifying the ISO standard.
Each leaf predicate is evaluated on each element of this Cartesian product until one satisfies the predicate (meaning that an abstract test case was found) or until it is exhausted (meaning that either the test class is unsatisfiable or the finite model is inadequate).
In the last case, the user has the chance to assist the tool in finding the right finite model or to prune the test class because it is unsatisfiable.