如何将元素添加到总函数中，同时确保不存在到该元素的其他映射？

Question

我试图在 Atelier B 中用 B 方法正式指定一个铁路联锁系统。最基本的概念非常简单：可以为火车分配一个位置和一个区域。 一个区域同一时间内只能有一趟列车。该区域只是一组位置，定义为映射到位置集幂集的列车元素的总函数：

train_areas : trains --> POW(LOCATION)

。为了确保没有位置映射到两列火车，一个不变量应该类似于

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

对于每两趟列车，列车在 train_areas 中映射到的位置集的交集应该是一个空集。 我也尝试过这样表达：

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

对于 train_areas 变量范围内包含的每两组位置（不相同），位置的交集应为空集。 也可以这样表示：

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

对于所有列车元素，train_areas 中映射到列车的位置与 train_areas 中映射到的位置范围减去映射到相关列车的位置的交集应该是一个空集。

现在我想添加一列火车。火车需要有自己的位置，并且该位置当然需要包含在火车在 train_areas 中映射到的一组位置中。我确保该位置尚未包含在 train_areas 集中，如下所示：

!train.(train : trains => {loc} /\ train_areas(train) = {})

对于所有火车元素，新添加的位置和已经从train_areas中的火车映射到的位置的交集是一个空集。我还以我能想到的所有其他方式添加了这个条件来表达它。尽管如此，当向 train_areas 变量添加新映射时，Atelier B 无法证明上述不变量成立，如下所示

train_areas := train_areas \/ {tt |-> {loc}}

（train_areas 中所有内容和新火车及其位置幂集的联合）.

由于某种原因，即使多次检查新的火车位置

loc

不存在于train_areas中，在将

{tt |-> {loc}}

添加到train_areas后，仍无法证明没有两列火车映射到train_areas中的同一位置。有人可以帮助我更好地理解 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)})) = {}

Answer 1

我没有查看完整的机器，但也许问题已经在一开始了：

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

您错过了说明

t1

和

t2

是不同的火车。应该是

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