Apply Automated Reasoning techniques to the IPL model, including:
Generating a state map via Region Decomposition to see the explorable state sequences.
Performing reachability analysis to find out if certain scenarios are unreachable from state transitions implied by previous scenarios.
Integrate with the IPL Extension to explore the generated models.
Requirements
The IPL Extension (and its dependencies) is recommended to fully utilise formalized code.
The Cucumber Extension is recommended to provide symbol analysis on Gherkin files.
Extension Settings
You can configure SpecLogician with the following settings:
imandra.specLogician.apiKey: Set your Imandra Universe API key here. By default, this is inferred from the IMANDRA_API_KEY environment variable and then from the contents of ~/.config/imandra/api_key (or ~/.config/imandrax/api_key).
FAQ
You may want to silence warnings in cucumber files, as cucumber will highlight stuff yellow if there is no matching code implementation, which is not relevant to the specific purpose of this plugin. You can do this via adding .vscode/settings.json with
If you encounter an unusual state that seems difficult to fix, you can clear the entire state of the extension by invoking imandra-spec-logician.clear-cache via SpecLogician: Clear the cache (WARNING). Notice that this clears all existing formalizations and generated files. The usage of this command should be a last resort.
