如何在Alloy 6中指定简洁的全局框架条件？

我正在学习《Formal Software Design with Alloy 6》的协议设计章节，做时态流程建模时，想简化谓词里的框架条件。

示例场景 #

假设员工（Employee）可登录机器（Machine），所处位置为Machine或测量室（MeasureRoom）；Machine有NoLogin、Work、Measuring三种状态，包含activeTool（活动工具）和tools（工具集合）。

模型代码 #

enum MachineState { NoLogin, Work, Measuring }

abstract sig Location {}

some sig Tool {}

one sig Machine extends Location {
  var login: lone Employee,
  var state: one MachineState,
  var tools: some Tool,
  var activeTool: lone Tool
}

one sig NotAtWork extends Location {}

one sig MeasureRoom extends Location {}

one sig Employee {
  var location: one Location
}

初始状态定义 #

fact init {
  Employee.location = NotAtWork

  no Machine.login
  Machine.state = NoLogin

  Machine.tools = Tool
  no Machine.activeTool
}

状态转换谓词（含冗余框架条件） #

pred login {
  Machine.state = NoLogin // 守卫条件

  // 状态变更效果
  Machine.state' = Work
  Machine.login' = Employee
  Employee.location' = Machine
}

pred measuring_begin {
  Machine.state = Work // 守卫条件

  // 状态变更效果
  Machine.state' = Measuring
  Employee.location' = MeasureRoom
  
  // 框架条件 - 如何简化这些冗余代码？
  Machine.login' = Machine.login
  Machine.tools' = Machine.tools
  Machine.activeTool' = Machine.activeTool
}

pred measuring_end {
  Machine.state = Measuring // 守卫条件

  // 状态变更效果
  Machine.state' = Work
  Employee.location' = Machine

  // 框架条件 - 如何简化这些冗余代码？
  Machine.login' = Machine.login
  Machine.tools' = Machine.tools
  Machine.activeTool' = Machine.activeTool
}


fact transition {
    always (
        login or measuring_begin or measuring_end
    )
}

run example {
    eventually measuring_end
}

具体问题 #

有没有办法写出简洁的框架条件，确保新状态除了指定的变更效果外，和原状态完全一致？我知道谓词只是定义未来状态的搜索条件，不是直接修改状态，不确定这种简化是否可行。

Alloy 6提供了几种实用方式来简化这类框架条件，避免重复声明未变更的字段：

1. 使用only关键字指定仅变更的字段 #

这是最简洁且符合需求的方式，Alloy的时态语义支持用only块明确标记允许变化的字段，未被标记的所有可变字段（带var修饰）都会自动保持原值。

修改后的measuring_begin和measuring_end谓词可以简化为：

pred measuring_begin {
  Machine.state = Work // 守卫条件

  // 仅指定需要变更的字段，其余字段自动保持原状态
  only {
    Machine.state' = Measuring
    Employee.location' = MeasureRoom
  }
}

pred measuring_end {
  Machine.state = Measuring // 守卫条件

  only {
    Machine.state' = Work
    Employee.location' = Machine
  }
}

only块的核心作用就是保证：只有块内声明的字段能在状态转换中改变，所有其他可变字段必须与原状态一致，完全匹配你想要的效果。

2. 定义通用辅助谓词封装不变逻辑 #

如果多个谓词需要复用“保持某些字段不变”的逻辑，可以封装一个辅助谓词：

pred machineFieldsUnchanged[m: Machine] {
  m.login' = m.login
  m.tools' = m.tools
  m.activeTool' = m.activeTool
}

然后在转换谓词中直接调用：

pred measuring_begin {
  Machine.state = Work
  Machine.state' = Measuring
  Employee.location' = MeasureRoom
  machineFieldsUnchanged[Machine]
}

这种方式适合字段较多、且多个谓词需要保持相同字段不变的场景。

3. 批量声明不变字段集合 #

如果需要保持不变的字段是固定一组，也可以用集合批量声明：

// 提取Machine的可变字段集合
fun machineVarFields[m: Machine] { m.login, m.tools, m.activeTool }

pred measuring_begin {
  Machine.state = Work
  Machine.state' = Measuring
  Employee.location' = MeasureRoom
  // 批量指定集合内的字段保持不变
  machineVarFields[Machine]' = machineVarFields[Machine]
}

不过这种方式可读性不如only关键字，推荐优先使用第一种方案。

内容的提问来源于stack exchange，提问作者Matija Sirk