如何获取 seq（序列）中的下一项？

Question

一架飞机飞行一系列腿。每条腿之后必须有适当的下一条腿。 NextLegTable 包含适当的 (Leg -> Leg) 对。

因此，航班中的每对腿都必须在NextLegTable 中。我在下面的Fact 中实现了这个约束。

这里是对我的实现的描述：每对腿（leg 和leg'），例如indexOf(leg) + 1 = indexOf(leg')，必须在NextLegTable 中。显然这种方法是错误的，因为我得到“没有实例”。

什么是正确的方法？给定一条腿，我如何在序列中找到它的下一条腿？

sig Flight {
    legs: seq Leg
}

sig Leg {}

one sig NextLegTable {
    nextLeg: Leg -> Leg
}

fact Flight_legs_In_NexLegTable {
    all f: Flight |
        all leg, leg': Leg { 
            leg in f.legs.elems
            leg' in f.legs.elems 
            plus[f.legs.idxOf[leg], 1] =  f.legs.idxOf[leg']
            (leg -> leg') in NextLegTable.nextLeg
        }
}

pred Show (f: Flight) {#f.legs > 1} 
run Show

Answer 1

这是要查看的两行代码：

    plus[f.legs.idxOf[leg], 1] =  f.legs.idxOf[leg']
    (leg -> leg') in NextLegTable.nextLeg

此解决方案当前正在尝试查找一个实例，其中 Flight 的所有 Legs 跟随另一个 Leg 也显示在 NextLegTable sig 中。但是，您并没有告诉它实际将这些映射放入表中。你需要说，当Leg 跟随另一个Leg 时，将Leg -> Leg' 放入NextLegTable：

(plus[f.legs.idxOf[leg], 1] =  f.legs.idxOf[leg']) =>
(leg -> leg') in NextLegTable.nextLeg

这告诉程序在满足第一个条件时将映射放入表中。