Atelier B建模铁路联锁系统：添加列车后不变量无法证明求助

问题背景 #

使用Atelier B的B方法对铁路联锁系统进行形式化规约，核心规则为：同一区域同一时间仅能有一列列车。其中区域是位置集合，train_areas定义为从列车到位置集合幂集的全函数：train_areas : trains --> POW(LOCATION)。

定义的不变量形式 #

为保证无位置被多列列车占用，定义了三种等价的不变量形式：

• 形式1（针对列车对）：

  !(t1, t2). (t1 : trains & t2 : trains & t1 /= t2 => train_areas(t1) /\ train_areas(t2) = {})
  

  含义：任意两列不同列车的区域位置集合交集为空。
• 形式2（针对值域集合）：

  !(locs1, locs2).(locs1 : ran(train_areas) & locs2 : ran(train_areas) & locs1 /= locs2 => locs1 /\ locs2 = {})
  

  含义：train_areas值域中任意两个不同位置集合的交集为空。
• 形式3（针对单列车与其他列车并集）：

  !tt. (tt : trains => train_areas(tt) /\ union(ran(train_areas) - {train_areas(tt)}) = {})
  

  含义：任意列车的区域与其他所有列车区域的并集交集为空。

当前代码与问题 #

AddTrain操作已通过多个前置条件确保新位置loc未被现有列车区域占用，但执行train_areas := train_areas \/ {tt |-> {loc}}更新后，Atelier B无法证明上述不变量保持成立。

完整Atelier B机器代码：

MACHINE APSTrackside
SETS
    AREA ; LOCATION ; TRAIN    
VARIABLES
    areas, train_locations, trains, train_areas
INVARIANT
    trains <: TRAIN &
    
    // Every train area is associated with a set of locations
    train_areas : trains --> POW(LOCATION) &

    // Every area is associated with a set of locations
    areas : AREA --> POW(LOCATION) &
    
    // Every train is associated with a location
    train_locations : trains --> LOCATION &
    
    // Every train needs to be assigned a set of locations in train_areas
    !tt.(tt : trains => train_locations(tt) : train_areas(tt)) &
    
    // There can only be one train in any one area at the same time
    // Here is the problem    
    !(locs1, locs2).(locs1 : ran(train_areas) & locs2 : ran(train_areas) & locs1 /= locs2 
        => locs1 /\ locs2 = {})
    
INITIALISATION
    trains := {} ||
    train_locations := {} ||
    train_areas := {} ||
    areas := %area.(area : AREA | {ll | ll:LOCATION})
    
OPERATIONS    
    AddTrain(tt, loc) =
    PRE
        tt : TRAIN &
        loc : LOCATION &
        tt /: trains &
        
        // The location is not in any currently set up train area
        !train.(train : trains => {loc} /\ train_areas(train) = {}) &
        !locs.(locs : ran(train_areas) => loc /: locs) &
        loc /: union(ran(train_areas)) &
        
        // Ensure the location is not already occupied by any train
        !train.(train : dom(train_areas) => loc /: train_areas(train)) &
        
        // Ensure the new train's location doesn't overlap with any existing train's area
        !(tt1).(tt1 : trains => loc /: train_areas(tt1)) &
        
        // There is no other train at this location
        !tt.(tt : trains => loc /= train_locations(tt))
    THEN
        trains := trains \/ {tt} ||
        train_locations := train_locations \/ {tt |-> loc} ||
        // Here is the problem
        train_areas := train_areas \/ {tt |-> {loc}}
    END
END

工具生成的待证不变量形式（更新后）：

tt1 : trains \/ {tt} 
=>
(train_areas \/ {tt |-> {loc}})(tt1) /\ 
union(ran(train_areas \/ {tt |-> {loc}}) 
-s ({(train_areas \/ {tt |-> {loc}})(tt1)})) = {}

原因分析 #

1. 不变量形式的证明友好性不足：当前使用的形式2（基于值域集合）需要证明两个维度：原有值域内的集合仍满足交集为空，以及新加入的{loc}与原有值域所有集合交集为空。虽然前置条件已覆盖后者，但Atelier B的自动证明器难以自动关联“列车的区域”和“值域中的集合”之间的映射关系，导致逻辑链断裂。
2. 冗余前置条件干扰：多个前置条件（如!train.(train : trains => {loc} /\ train_areas(train) = {})与loc /: union(ran(train_areas))）是等价的，冗余的表述会分散证明器的注意力，增加自动推导的复杂度。
3. 值域操作的间接性：ran(train_areas)是派生集合，证明器需要额外步骤推导“新加入的{loc}不在原有值域中”或“与原有值域所有集合无交集”，而直接针对列车定义域的不变量（形式1）无需这层间接推导。

解决方案 #

方案1：切换为更易证明的不变量形式 #

将不变量替换为形式1（针对列车对），该形式直接关联train_areas的定义域（列车），与AddTrain的前置条件逻辑链更直接：

!(t1, t2). (t1 : trains & t2 : trains & t1 /= t2 => train_areas(t1) /\ train_areas(t2) = {})

证明逻辑：

• 原有列车对的不变性由初始不变量保证；
• 新列车tt与任意现有列车t的区域交集为空，直接由前置条件{loc} /\ train_areas(t) = {}保证（因为train_areas(tt)就是{loc}），证明器可直接推导。

方案2：简化前置条件并添加中间断言 #

若坚持使用形式2的不变量，可简化前置条件为最直接的等价表述，并在操作中添加中间断言帮助证明器分步推导：
修改后的AddTrain操作：

OPERATIONS    
    AddTrain(tt, loc) =
    PRE
        tt : TRAIN &
        loc : LOCATION &
        tt /: trains &
        // 保留最直接的前置条件，其余等价条件可删除
        loc /: union(ran(train_areas)) &
        !tt.(tt : trains => loc /= train_locations(tt))
    THEN
        // 添加中间断言，明确新区域与现有区域无交集
        ASSERT {loc} /\ union(ran(train_areas)) = {};
        trains := trains \/ {tt} ||
        train_locations := train_locations \/ {tt |-> loc} ||
        train_areas := train_areas \/ {tt |-> {loc}}
    END
END

断言会引导证明器先确认核心事实，再推导值域的不变性。

方案3：细化不变量的拆分表述 #

可将形式2的不变量拆分为两个更具体的子不变量（拆分后证明器更易处理）：

// 原有值域内的集合仍满足无交集
!(locs1, locs2).(locs1 : ran(train_areas) & locs2 : ran(train_areas) & locs1 /= locs2 => locs1 /\ locs2 = {}) &
// 每个列车的区域都是唯一的（避免不同列车映射到同一区域集合）
!t1,t2.(t1:trains & t2:trains & t1/=t2 => train_areas(t1)/=train_areas(t2))

不过该方案仅在存在不同列车映射到同一区域集合的场景下有意义，对于当前需求，方案1是最优选择。

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