FRET public release v2.9.1

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.

FRET public release v2.9.0

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.

FRET public release v2.8.0

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.

FRET public release v2.7.0

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.

FRET Public release v2.6

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.

FRET public release v2.5

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.

FRET public release v2.4

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.

FRET public release v2.3

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).

FRET public release v2.2

What is new in FRET v2.2

Requirement semantics:

• Extended the requirements assistant to display multiple formalizations.

Installation & Infrastructure:

• Updated dependencies: FRET now works with both Python 2.x and 3.x.
• Upgraded node to v16.

Regression testing:

• Added support for testing with the playwright framework.

FRET public release v2.1

What is new in FRET v2.1

Analysis portal:

• Integrated FRET with the Kind 2 analysis tool for checking realizability;
• Connected realizability analysis with LTLSIM for simulation of conflicting requirements in unrealizable specifications.

LTLSIM:

• Significantly extended the simulator to handle non-boolean variables, to show multiple requirements and to load/save execution traces.

FRET language:

• Added predicates that express temporal conditions, such as persisted(3 ticks, too_hot).
• Added predicates that refer to the previous value of a variable, such as preInt(0, velocity).
• See the FRET manual section on temporal conditions.