Wie bekomme ich das nächste Element in einer Seq (Sequenz)?

Question

Ein Flugzeug fliegt eine Sequenz von Beinen. Jedes Bein muss von einem geeigneten nächsten Bein gefolgt werden. A NextLegTable enthält die entsprechenden (Leg -> Leg) Paare.

Also, jedes Paar Beine in einem Flug muss in der NextLegTable sein. Ich habe diese Einschränkung in der folgenden Fact implementiert.

Hier ist eine Beschreibung meiner Umsetzung: Jedes Paar Beine (leg und leg'), so dass indexOf(leg) + 1 = indexOf(leg') im NextLegTable sein muss. Scheinbar ist diese Herangehensweise falsch, da ich "keine Instanzen" bekomme.

Was ist der richtige Ansatz? Wie finde ich bei einem Bein das nächste Bein in der Sequenz?

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

Dies sind die beiden Linien zu sehen: Der Versuch wird

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

Diese Lösung, die derzeit eine Instanz zu finden, wo alle Legs eines Flight, die eine andere Leg folgen, werden auch in der NextLegTable sig gezeigt. Sie haben ihm jedoch nicht gesagt, dass er diese Mappings tatsächlich in den Tisch legen soll. Sie müssen sagen, dass, wenn ein Leg andere Leg folgt, setzen Leg -> Leg' in NextLegTable:

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

Das das Programm erzählt die Zuordnungen in den Tisch zu legen, wenn die erste Bedingung erfüllt ist.