Article URL: https://docs.imiron.io/v/0.5.10/en/tour.html Comments URL: https://news.ycombinator.com/item?id=49095628 Points: 26 # Comments: 1

This 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: Operators: Standard arithmetic (+, -, *, /), comparisons (==, <, >, etc.), and logical operators (&&, ||, =>) Temporal Operators: Lilo’s distinguishing feature is its rich set of temporal logic operators: These operators can be qualified with time intervals, e.g., eventually[0, 10] φ means φ becomes true within 10 time units. More operators are available. A system file begins with a system declaration like system temperature_control and contains all the declarations for that system. We’ll use a temperature control system as our running example. This example project is available in the releases. The system monitors temperature and humidity sensors, with specifications ensuring values remain within safe ranges: The VSCode extension provides support for writing Lilo code, syntax highlighting, type-checking, warnings, spec satisfiability, etc.: