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.