Declare 规则的完整分类总结，包含所有核心约束模板及其正式定义、LTL 等价公式和实际应用示例：
1. 存在性约束 (Existence)
| 规则名称 | LTL公式 | 语义说明 | 示例 |
|---|
| Existence(A) | ◇A | A至少出现1次 | 患者必须进行至少1次化验（Existence(LabTest)） |
| Existence2(A) | ◇(A ∧ ◇A) | A至少出现2次 | 订单需经过双重审核（Existence2(Approval)） |
| Absence(A) | ¬◇A | A禁止出现 | 禁止跳过安全检查（Absence(SkipCheck)） |
| Absence2(A) | ¬(A ∧ ◇A) | A最多出现1次 | 每个案例只能提交1次（Absence2(Resubmit)） |
| Exactly1(A) | ◇A ∧ ¬(A ∧ ◇A) | A恰好出现1次 | 手术必须唯一（Exactly1(Surgery)） |
2. 顺序约束 (Ordering)
| 规则名称 | LTL公式 | 语义说明 | 示例 |
|---|
| Response(A,B) | □(A → ◇B) | A后必须有B | 下单后必须付款（Response(Order,Payment)） |
| Precedence(A,B) | ¬B U A | B前必须有A | 付款前需开发票（Precedence(Invoice,Payment)） |
| Succession(A,B) | □(A → ◇B) ∧ □(B → ◇A) | A和B必须成对出现 | 咨询与反馈必须配对（Succession(Consult,Feedback)） |
| AlternateResponse(A,B) | □(A → ◯(¬A U B)) | A后必须有B，且中间不能有A | 检查后必须清洁，中间不能重复检查（AlternateResponse(Inspect,Clean)） |
| ChainResponse(A,B) | □(A → ◯B) | A后必须立即跟B | 扫描后立即验证（ChainResponse(Scan,Verify)） |
3. 选择约束 (Choice)
| 规则名称 | LTL公式 | 语义说明 | 示例 |
|---|
| ExclusiveChoice(A,B) | (◇A ∨ ◇B) ∧ ¬(◇A ∧ ◇B) | 必须选A或B，但不能都选 | 支付方式：信用卡或现金（ExclusiveChoice(CreditCard,Cash)） |
| NotCoExistence(A,B) | ¬(◇A ∧ ◇B) | A和B不能同时出现 | 折扣与优惠券不可并用（NotCoExistence(Discount,Coupon)） |
4. 循环约束 (Repetition)
| 规则名称 | LTL公式 | 语义说明 | 示例 |
|---|
| CoExistence(A,B) | ◇A ↔ ◇B | A和B必须同时出现或都不出现 | 合同签署与公证共存（CoExistence(Sign,Notarize)） |
| RespondedExistence(A,B) | ◇A → ◇B | 如果A出现，则B必须出现 | 投诉必须响应（RespondedExistence(Complaint,Reply)） |
5. 负约束 (Negative)
| 规则名称 | LTL公式 | 语义说明 | 示例 |
|---|
| NotResponse(A,B) | □(A → ¬◇B) | A后禁止出现B | 拒绝后不得再次提交（NotResponse(Reject,Resubmit)） |
| NotPrecedence(A,B) | ¬(¬A U B) | B前禁止出现A | 未经授权禁止访问（NotPrecedence(NoAuth,Access)） |
6. 扩展约束 (Extended)
| 规则名称 | 说明 | 示例 |
|---|
| Init(A) | 流程必须以A开始 | 病例必须从登记开始（Init(Registration)） |
| End(A) | 流程必须以A结束 | 订单必须以交付结束（End(Delivery)） |
| Participation(A) | 所有案例必须包含A | 所有交易必须记录（Participation(Log)） |
| First(A) | A必须是案例的第一个活动 | 首次登录必须验证（First(Verify)） |
7. 带参数的约束
| 规则名称 | 参数说明 | 示例 |
|---|
| Within(A,B).T | A后必须在时间T内发生B | 报警后5分钟内响应（Within(Alert,Response).5min） |
| Timespan(A).T | A的持续时间必须≤T | 审批不得超过24小时（Timespan(Approval).24h） |
8. 资源约束 (Resource)
| 规则名称 | 说明 | 示例 |
|---|
| SameResource(A,B) | A和B必须由同一资源执行 | 医生诊断与开药需同一人（SameResource(Diagnose,Prescribe)） |
| DifferentResource(A,B) | A和B必须由不同资源执行 | 审批与执行需分离（DifferentResource(Approve,Execute)） |
应用场景
| 领域 | 常用约束 | 作用 |
|---|
| 医疗 | ChainResponse(Test, Diagnose) | 确保检验后立即诊断 |
| 金融 | Precedence(KYC, Transaction) | 反洗钱合规 |
| 制造 | AlternateResponse(QC, Repair) | 质量控制闭环 |
| 电子商务 | Within(Order, Payment).24h | 防止未支付订单滞留 |
通过组合这些约束模板，可以构建出覆盖绝大多数业务流程规则的声明式模型。实际应用中，约80%的约束集中在Response、Precedence、Existence三类基础模板上（根据IEEE Task Mining研究报告）。
