Copy project functionality:
- Implemented functionality to copy existing projects.
Requirement formalization:
- Added formalizations for the following FRETish template keys:
before, -, immediately | within | after. - Updated formalization for persists and occurs to ensure strictness near the end of a scope; for example,
persists(3, p)does not hold if applied within 2 steps of the scope’s end, even ifpholds for the last two timepoints. The same rule applies to occurs. - Introduced temporal logic simplifications - specifically, for past-time,
Z FALSEis now used to designate the first time point instead of! (Y TRUE).
FRET executables:
- Added a build step in the scripts for generating FRET executables on Linux and macOS.
UI improvements:
- Updated the requirement editor dialog to truncate lengthy requirement and project IDs, with tooltips displaying full IDs for truncated entries.
- Added Undo (Command Z/Control Z) and Redo (Command Y/Control Y) to the requirement editor.
- Removed automatic upper-casing of requirement IDs in the Requirement Table.
- Added tooltips for FRET operations in the dashboard.
- Sorted project names alphabetically in the requirement editor.
- Enabled down-arrow navigation in the glossary and template dropdown menus within the requirement editor.
Realizability checking:
- Bumped Kind 2 version to 2.2.0.
- Improved UI to better support handling of projects with multiple components and specifications that can be decomposed into a big number of connected components.
- Improved the performance of the diagnosis algorithm for unrealizable requirements.
Database and export/import support:
- Added functionality to export status data when exporting requirements.
- Implemented support to display an error message when a corrupted JSON file is detected during import.
- Optimized variable entry updates for faster processing in model-db.
Documentation:
- Updated documentation to be clear that the keywords
not in, for the not-in scope, require that the keywordswhenorifmust precedenot in.