名称: specify 描述: 使用TLA+、SysML或状态机为组件或行为创建形式化规范。用于安全关键系统。允许工具: Read, Glob, Grep, Write, Skill, Task 参数提示: <topic> [–format <tla+|sysml|state-machine|uml>]

/specify 命令

为系统组件、行为和算法创建形式化规范。

使用方式

/specify "分布式锁协议"
/specify "订单生命周期" format=state-machine
/specify "车辆控制系统" format=sysml
/specify "共识算法" format=tla+

工作流程

步骤 1: 分析主题

解析规范主题并确定：

正在指定什么（协议、生命周期、系统、算法）
要捕获的关键属性（安全性、活跃性、结构）
适当的形式化方法

步骤 2: 选择规范格式

如果未指定格式，基于主题自动检测：

主题模式	推荐格式
“协议”, “共识”, “分布式”	TLA+
“生命周期”, “状态”, “工作流”	状态机
“系统”, “硬件”, “嵌入式”	SysML
“交互”, “流程”, “序列”	UML

步骤 3: 调用适当技能

加载相关技能：

tla-specification 用于 TLA+ 规范
state-machine-design 用于状态机
sysml-modeling 用于 SysML 模型
uml-modeling 用于 UML 图

步骤 4: 收集需求

如果在有规范的项目中工作：

在 docs/requirements/ 中搜索相关需求
检查现有领域模型
查找相关 ADRs

步骤 5: 生成规范

创建形式化规范，包括：

核心规范（TLA+ 模块、SysML 图、状态机）
文档和注释
验证方法（如果适用）
实施指导

步骤 6: 输出结果

交付：

选定格式的规范
图表可视化（PlantUML/Mermaid）
文档化关键属性
使用说明

格式特定输出

TLA+

--------------------------- MODULE TopicName ---------------------------
EXTENDS Integers, Sequences
CONSTANTS ...
VARIABLES ...
Init == ...
Next == ...
Spec == Init /\ [][Next]_vars
Safety == ...
Liveness == ...
=============================================================================

状态机

@startuml
[*] --> Initial
Initial --> Active : trigger
Active --> Completed : complete
Completed --> [*]
@enduml

SysML

@startuml
class "<<block>>
SystemName" as System {
  values
  --
  parts
  --
  operations
}
@enduml

示例

分布式锁

/specify "带领导选举的分布式锁" format=tla+

输出: 带有互斥安全性属性和最终授予活跃性属性的 TLA+ 模块。

订单生命周期

/specify "电子商务订单生命周期"

输出: 显示草稿 → 已提交 → 已支付 → 已发货 → 已交付状态的状态机图，带有转换和守卫。

车辆系统

/specify "自动驾驶车辆感知系统" format=sysml

输出: 显示传感器、处理器和数据流的 SysML BDD，带有参数约束。

集成

该命令与以下集成：

企业架构: 链接到 ADRs
需求获取: 追踪到需求
系统设计: 与架构对齐

名称: specify 描述: 使用TLA+、SysML或状态机为组件或行为创建形式化规范。用于安全关键系统。 允许工具: Read, Glob, Grep, Write, Skill, Task 参数提示: <topic> [–format <tla+|sysml|state-machine|uml>]