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.