Formi's Features

The intuitive YAML-based editor enables users to quickly define models through textual input. At the same time, the portable format can be used to store and share models.

On-the-fly validation warns about issues, such as non-total functions, but does not prevent model checking if possible.

Interactive graphs visualize model domains, constants, functions, and relations. Touch input and mouse input are supported. Zooming and panning ensure that even the largest models can be inspected.

Formulas are parsed in real-time, with helpful error messages for syntax errors.

The ASTs of formulas are visualized and display operator precedence. Any non-terminal node can be expanded and collapsed to reveal or hide sub-formulas respectively.

Every evaluation step of the recursive model checking algorithm is represented as a node in the evaluation tree. This ensures that results are always tangible.

A checkmark indicates that the (sub-)formula must be modelled by the model, a cross represents the opposite. The colors green and red show whether the actual result matches the expected result or not.