This release adds R2U2 runtime monitor generation, strengthens test case generation and realizability checking, and improves documentation throughout.

R2U2 Runtime Monitoring Integration

• FRET can now generate specifications in Mission-time Linear Temporal Logic (MLTL), which serve as direct inputs to the R2U2 runtime monitoring tool for generating C monitors.
• This feature was contributed by Collins Aerospace under a Corporate Contributor License Agreement (CLA).

Requirements Editor

• Improved the toggle bar for switching between probabilistic and non-probabilistic modes.
• Added PRISM syntax as an output option for generated formalizations.
• Enhanced the quality and clarity of generated English semantic explanations.

Test Case Generation:

• Added compatibility with NuSMV 2.7.0.
• Tests generated with Kind 2 can now be loaded and inspected directly in the simulator.
• Added an option to configure the length of generated test cases when using the NuSMV engine.
• Improved error handling and output log messages for better diagnostics.

Realizability Checking:

• Improved robustness and output message logs in the presence of errors.
• Adjusted tooltip of 'Simulate Realizable Requirements' option to not appear when JKind has been selected as engine.
• Fixed intricate case where diagnosis table was not properly sorting requirements after deselecting a requirement that was part of the viewed conflict.
• Strengthened the JKind dependency check to verify all required scripts from the installation.

Documentation:

• Extended Notes section in the installation manual to use Github's NOTE Alert type in order to improve content readability and visibility.
• Added documentation for built-in functions.
• Updated Test Case Generation docs to reflect new features and latest supported dependency versions.
• Updated Realizability Checking docs to clarify supported dependency versions.
• Fixed a broken link to the Troubleshooting section in the README.

1. Probabilistic Requirement Specification and Formalization

• Introduced support for probabilistic requirements, enabling the specification of uncertainty - crucial for autonomous systems.
• Extended the FRETish language with a probability field for direct probabilistic constraint specification.
• Automated the formalization of probabilistic requirements as Probabilistic Computational Tree Logic Star (PCTL*) formulas.
  • PCTL* formulas are generated in a compositional manner, promoting extensibility and maintainability of the tool.
  • The generated PCTL* formulas adhere to the syntax of the PRISM property specification language, facilitating connection with the PRISM and other probabilistic model checkers.

2. Requirement-Based Test Case Generation

• Automated the test case generation from FRETish requirements based on test obligation formulas, leveraging the FLIP requirements coverage metric to ensure comprehensive testing.
• Integrated two test generation engines:
  • Kind 2: for past-time LTL formulas
  • NuSMV: for future- and past-time LTL formulas.
• Added multiple export options:
  • Test cases (from both Kind 2 and NuSMV) can be exported in JSON format.
  • Test obligation formulas, the core of the test generation process, can be exported in Lustre or SMV syntax.
• Enabled visualization of NuSMV-generated tests using the FRET simulator (LTLSIM), to visually and interactively inspect and validate the generated tests.

3. Revamped Analysis Portal

• Added a 'Complete' column to the variables mapping table for mandatory variable information specification.
• Implemented asynchronous diagnosis of unrealizable results for improved efficiency.
• Enhanced tooltip behavior for realizable requirement simulations.

4. Revamped LTLSIM Simulator

• Enabled multi-trace display with varying lengths within a single window.
• Added trace export/import functionality in JSON and CSV formats.
• Improved trace annotation and selection features.
• Enhanced integration for visualizing realizability counterexamples.
• Included an hourglass cursor for visual feedback of NuSMV processing.

5. Installation & Infrastructure

• Adopted Apache 2.0 licensing for FRET.
• Improved robustness of realizability checking to accommodate JSON format variations across Kind 2 versions.
• Updated .deb dependencies in Dockerfile for Ubuntu 24.04 compatibility.
• Revised WSL installation guide with latest system requirements.
• Bumped dependencies, including the nodegyp package.

6. User Manual & Documentation

• Expanded and improved the user manual documentation.
• Added Lockheed Martin case study requirements and a step-by-step test obligation generation guide for Lustre/Simulink.

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 if p holds for the last two timepoints. The same rule applies to occurs.
• Introduced temporal logic simplifications - specifically, for past-time, Z FALSE is 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 keywords when or if must precede not in.

Command Line Interface (CLI) for FRET:

• Support for realizability checking through the CLI.
• Support for generating formalizations for a FRETish requirement.

FRETish language:

• Extended FRETish expressiveness with finally timing finally in past time is the dual of immediately in future time.

Requirement editor:

• Fixed and enhanced hot key functionality and text group selection using mouse actions as follows:
  • Shift + Left/Right Arrow will highlight characters to the left/right.
  • For requirements taking up more than one line, Shift + Up/Down Arrow will highlight everything starting from the cursor to the same position of the above/below line.
  • Shift + Home/End will highlight everything starting from the cursor to the beginning/end of the line.
  • Home key puts the cursor in the beginning of the line.
  • End key puts the cursor at the end of the line.
  • Command + Shift + Left/Right Arrow will accumulate highlight a word to the left/right.
  • Fixed bug in Command + Shift + Left Arrow.
  • Fixed bug in selecting texts with the mouse (click and drag) to the left.

Publicly available case study examples:

• Made the following case studies available to our users:
  • Lift Plus Cruise aircraft.
  • Finite State Machine component of an aircraft.
  • Liquid Mixer.

Code redesign:

• The import and export of requirements, variables, realizability and LTLSim simulator reports in previous versions uses Node.js file system methods. For versatility (using FRET both as an Electron App and as a CLI), we changed the import and export functionalities to use download and upload Web APIs. These changes were made for requirements, variables, and realizability reports except in the external tools mode.

Node package upgrades:

• Bumped jest, jest-unit.
• Bumped level down.
• Bumped follow-redirects.
• Bumped node-sass.
• Bumped slate, slate-history, slate-react.
• Bumped ejs.
• Replaced archiver and csvtojson with file-saver, csv and jszip.

Analysis portal:

• Improved behavior in Variable mapping when assignments of internal variables refer to non existing variables.

Installation options and guides:

• Added new installation guide for Windows systems using Windows Subsystem for Linux (WSL).
• Added scripts to build executables for Mac, Windows and Linux systems.

LTLSIM (FRET simulator):

• Simulator now recognizes both NuSMV and nusmv executable names.
• Code reorganization and clean up.

FRETish language:

• Increased expressiveness of FRETish by adding continual conditions (non edge-triggered) - e.g., “GF a” formulas can now be expressed.
• Added diagrammatic and textual explanations to describe continual conditions in the UI of FRET.
• Updated requirement parser to recognize reserved words by NuSMV and to return feedback to the user.
• Updated requirement parser to return error message for trailing unparsed input.

Package upgrades:

• Upgraded Node to version 18.
• Upgraded Electron to version 27.
• Upgraded Webpack to version 5.
• Upgraded archiver to latest version (j352).

Realizability checking:

• Added support for identifying assumptions by substring in requirementID.

LTLSim (FRET simulator):

• Updated interface of simulator to make it more user-friendly.

Requirement search:

• Added Enter key functionality in Search bar.
• Updated Search bar to reset search when changing project.

Documentation:

• Updated FRETish manual to describe all newly added features.
• Updated publication lists to include work with FRET by external researchers/users.

Core FRET:

• Redesigned code to support client server architecture. New architecture allows easier integration of third party code.
• Added import/export functionality for variables.
• Added functionality to choose input database before starting FRET.

Support of analysis tools:

• Updated Kind 2 exit code handling for realizability checking to support Kind 2 v.1.9.0 or later.
• Updated Matlab/Simulink script for FRET glossary generation.

Documentation:

• Updated Windows installation guide.
• Updated manual and FRET publication list.

What is new in FRET v2.6

Requirements language and formalization:

• Updated display of formalizations in Requirement Editor to include formalizations for infinite traces in Future time.
• Extended FRETish with "at the next/previous occurrence of p, q".

Requirement editor:

• Added state machine requirement templates.
• Improved ext execution mode for running requirement editor as standalone tool that allows easy integration with external tools.

Installation with Docker:

• Updated installation instructions and added Docker image for Linux users.

Documentation:

• Updated FRET manual.
• Updated FRET publication list.

What is new in FRET v2.5

Realizability checking:

• Users can now simulate realizable requirements. Currently this action is available only when using the JKind engine option. An example execution trace that satisfies all requirements is provided as additional feedback.

Requirements Formalization:

• A period can now be used at the end of a requirement sentence.
• Improved message returned to the users when the requirement is in free form (quoted), stating that it will not be formalized.

What is new in FRET v2.4

Realizability checking:

• Users can now save and load realizability checking and diagnosis reports using the graphical interface.
• Extended the interface to allow selection of subsets of requirements in a given system component.
• Changed default realizability checking engine to Kind 2.

Requirements Formalization:

• Fixed handling of Boolean constants in FRETish.
• Predicate preBool is now properly mapped to temporal operators Y or Z, depending on the initial value.

What is new in FRET v2.3

Requirement editor:

• Added node script (npm run ext) for running requirement editor as standalone tool to facilitate integration with external tools.
• Extended editor to support identifiers with periods, percents, and double-quotes.
• Fixed translation of xor, equivalence, and mod operators.

Generation of analysis code and realizability checking:

• Added predefined auxiliary functions for Lustre code generation (e.g., absolute value, min, max).