Skip to content

Recursive analysis - #28

Merged
jdreier merged 16 commits into
tamarin-prover:masterfrom
zoaient:recursive_analysis
Aug 1, 2025
Merged

Recursive analysis#28
jdreier merged 16 commits into
tamarin-prover:masterfrom
zoaient:recursive_analysis

Conversation

@zoaient

@zoaient zoaient commented Jul 25, 2025

Copy link
Copy Markdown

Recursive Analysis

Recursive Analysis has been implemented.

  • Symbols imported from other Tamarin files are no longer reported as errors.
  • Syntax highlighting has been updated
  • Few wellformedness Checks has been updated as well of a few tests
  • 2 new unitary tests to test wellformedness checks with symbols imported from another file.

splib and spthy files

  • This plugin supports two file types:
    • spthy is the default format for Tamarin files.
    • splib files are library files that do not contain the theory name, "begin" and "end". They can be imported using include "file.splib".
  • Non spthy or splib files that are labeled as Tamarin files are considered as spthy files , unless they are imported and considered instead as splib files.

@jdreier
jdreier merged commit f3f5380 into tamarin-prover:master Aug 1, 2025
2 checks passed
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment

Labels

None yet

Projects

None yet

Development

Successfully merging this pull request may close these issues.

2 participants