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.