Behind the Scenes

Input

The process starts with a user-generated TLA+ specification, which passes through SANY.

Intermediate Representation

Assuming syntactic correctness, we identify operators, constants and variables/parameters and assign unique IDs to all expressions and sub-expressions occurring in the specification. Their purpose is to serve as primary keys in various databases used by plugins (e.g. for type information, scoping information, substitution chains, etc.).

Plugins

While the intermediate representation is very basic, the ID system is versatile in the sense that it allows for various kinds of detailed analysis later on. It is usually the case that a specific user is interested in some, but not all, information that our tool provides. Therefore, the plugin system was devised to eliminate redundant computation. Each plugin performs one very specific task and any number of plugins may be combined into a plugin chain, as long as interdependencies of plugins are respected.

Examples of plugins include:

• Boolean Analysis: Checks for non-boolean terms in boolean operators (e.g. FALSE v "abc").
• Name Structure: Expands the basic OperatorEx, ConstantEx, Name distinctions of the internal representation, distinguishes parameters, function expressions, variables, etc.
• Type Inference: If possible, assigns type information to expressions.
• Rich Type Inference: Explicitly distinguishes tuples, records, sequences, etc., which are typed as functions.
• Scope Information: ...
• Abstraction: ...
• Source Tracing: Follows the ID substitution chain and identifies the original code in the specification file, that has been transformed into the given expression.
• ...

Plugin Chains

TODO, UPLOAD PICTURES