GoKawiilThis section is a quick introduction to SpecForge’s main capabilities through a hands-on example. We’ll explore how to write specifications in the Lilo language and analyze them using SpecForge’s VSCode extension.
Lilo is an expression-based temporal specification language designed for hybrid systems. Here are the key concepts:
Primitive Types: Bool , Int , Float , and String
Operators: Standard arithmetic ( + , - , * , / ), comparisons ( == , < , > , etc.), and logical operators ( && , || , => )
Temporal Operators: Lilo’s distinguishing feature is its rich set of temporal logic operators:
always φ : φ is true at all future times
: is true at all future times eventually φ : φ is true at some future time
: is true at some future time past φ : φ was true at some past time
: was true at some past time historically φ : φ was true at all past times
These operators can be qualified with time intervals, e.g., eventually[0, 10] φ means φ becomes true within 10 time units. More operators are available.
... continue reading