快捷键 按 ← 或 → 在章节之间导航 按 S 或 / 在书中搜索 按 ? 显示此帮助 按 Esc 隐藏此帮助 旋风游览 本节是对 SpecForge 主要功能的快速介绍，采用动手示例。我们将探讨如何使用 Lilo 语言编写规范，并使用 SpecForge 的 VSCode 扩展进行分析。 Lilo 语言：简要介绍 Lilo 是一种基于表达式的时间规范语言，专为混合系统设计。以下是关键概念： 基本类型：Bool、Int、Float 和 String 运算符：标准算术（+、-、*、/）、比较（==、<、> 等）和逻辑运算符（&&、||、=>） 时间运算符：Lilo 的一个显著特点是它丰富的时间逻辑运算符： - 总是 φ：φ 在所有未来时刻为真 - 最终 φ：φ 在某个未来时刻为真 - 过去 φ：φ 在某个过去时刻为真 - 历史上 φ：φ 在所有过去时刻为真 这些运算符可以用时间区间进行限定，例如，eventually[0, 10] φ 表示 φ 在 10 个时间单位内为真。 系统：Lilo 规范被组织成系统，系统将以下内容分组在一起： - 信号 s：时间变化的输入值（如，信号 temperature: Float） - 参数 s：非时间性参数，不随时间变化（如，param max_temp: Float） - 类型 s：用于结构化数据定义的自定义类型 - 定义：可重用的定义和辅助函数 - 规范：应当为该系统成立的要求 系统文件以像 system temperature_control 这样的系统声明开始，包含该系统的所有声明。有关语言的全面指南，请参阅 Lilo 语言章节。 运行示例 我们将使用温度控制系统作为我们的运行示例。此示例项目可在发布版本中获得。该系统监控温度和湿度传感器，规范确保值保持在安全范围内： system temperature_sensor // 温度监控规范 // 此规范定义了温度传感器系统的安全要求 import util use { in_bounds } signal temperature: Float signal humidity: Float param min_temperature: Float param max_temperature: Float #[disable(redundancy)] spec temperature_in_bounds = in_bounds(temperature, min_temperature, max_temperature) spec always_in_bounds = always temperature_in_bounds // 当温度在正常范围时，湿度应合理 spec humidity_correlation = always ((temperature >= 15.0 && temperature <= 35.0) => (humidity >= 20.0 && humidity <= 80.0)) // 紧急情况 - 温度超过临界阈值 spec emergency_condition = temperature < 5.0 || temperature > 45.0 // 恢复规范 - 紧急情况后，系统应稳定 spec recovery_spec = always (emergency_condition => eventually[0, 10] (temperature >= 15.0 && temperature <= 35.0)) VSCode 扩展提供了支持编写 Lilo 代码、语法高亮、类型检查、警告、规范可满足性等功能。 规范分析 一旦您为系统编写了规范，SpecForge VSCode 扩展提供了多种分析功能： - 监视：检查记录的系统行为是否满足规范 - 示例化：生成满足规范的示例轨迹 - 验证：搜索违反规范的反例，相对于某个模型 - 导出：将规范转换为其他格式（.json、.lilo 等） - 动画：可视化规范行为随时间的变化 这可以直接在 VSCode 中完成，或在使用 Python SDK 的 Jupyter notebook 中完成。我们将在此直接在 VSCode 中进行分析。VSCode 指南详细介绍了所有功能。 监视 监视检查记录在数据文件中的实际系统行为是否满足您的规范。您提供记录的轨迹数据，SpecForge 将其与规范进行评估。导航到规范选择屏幕，单击您要监视的规范的分析按钮。在从下拉菜单中选择数据文件后，单击运行分析。结果是该规范的分析监视树：规范的整体结果显示在顶部。在其下方，您可以深入到规范的子表达式，以理解在任何给定时间使规范为真的因素。将鼠标悬停在任何信号上会显示一个弹出窗口，解释该时刻的结果，并突出显示子表达式结果信号的相关片段。分析可以保存。要这样做，请单击保存分析按钮，并选择一个位置以保存分析。然后，您可以导航到该分析文件并在 VSCode 中再次打开它。该分析也会在规范状态菜单中显示，位于相关规范下。 示例化 示例分析生成示例轨迹，以展示满足行为。这对于：理解...