SpecForge знакомит с языком темпоральных спецификаций Lilo через практический пример. Lilo — expression-based язык для гибридных систем. В нём есть примитивные типы Bool, Int, Float, String, обычные арифметические операторы и операторы сравнения, но главная фишка — темпоральные операторы. always φ означает, что φ истинно во все будущие моменты времени, eventually φ — что φ станет истинным когда-нибудь в будущем, past φ и historically φ смотрят в прошлое. Интервалы уточняют сроки: eventually[0, 10] φ говорит, что φ сбудется в пределах 10 временных единиц.
Спецификации собираются в системы. Система объявляется ключевым словом system и группирует сигналы, параметры, типы, определения и сами спецификации. Сигналы меняются во времени (signal temperature: Float), параметры статичны (param max_temp: Float). В примере разбирают system temperature_sensor с сигналами temperature и humidity, параметрами min_temperature и max_temperature. Спецификация temperature_in_bounds проверяет через импортированную функцию in_bounds, что температура в границах, а always_in_bounds оборачивает её в always. Спецификация humidity_correlation требует, чтобы при нормальной температуре (15–35°) влажность держалась в пределах 20–80%. emergency_condition фиксирует критические выходы (<5° или >45°), а recovery_spec настаивает: после срабатывания аварийного условия температура должна вернуться в норму в течение 10 единиц времени — eventually[0, 10] (temperature >= 15.0 && temperature <= 35.0).
Всё это пишется прямо в VSCode с расширением SpecForge, которое даёт подсветку, проверку типов и предупреждения. Дальше можно запускать анализы. Monitor берёт записанный трейс из файла данных и оценивает спецификацию — результат выглядит как дерево, где видно, истинна спецификация или ложна в каждый момент, можно проваливаться в подвыражения и смотреть подсказки. Анализ сохраняется и позже открывается заново. Exemplify генерирует примеры трасс, удовлетворяющих спецификациям — полезно для понимания корректного поведения или отладки самих требований. Falsify ищет контрпримеры, если есть модель системы; фальсификатор прописывается в specforge.toml, и при обнаружении нарушения показывается то же дерево мониторинга. Export выгружает спецификации в другие форматы, например .json. Есть ещё Animate для визуализации поведения, а запускать анализы можно и из Jupyter ноутбуков через Python SDK.