如何獲得序列（序列）中的下一個項目？

Question

飛機飛行的一系列腿。每條腿都必須跟着一條合適的下一條腿。 A 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 

該解決方案目前正在試圖找到這樣的情況：即遵循另一Leg一個Flight的所有Legs在NextLegTable SIG也顯示。但是，你沒有告訴它實際上把這些映射放到表中。你需要說的是，當一個Leg接踵而來Leg，把Leg -> Leg'到NextLegTable：

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

這告訴程序只要滿足第一個條件的映射放到桌子上。