セットのセットで注文を実装する方法は？

Question

航空機が着陸する空港に近づくと、航空機の接近手順は移行に分割されます。各トランジションは一連の脚で構成されています。

sig Transition { 
    legs: set Leg 
} 
sig Leg {} 

トランジション内の脚のセットが発注されます。各トランジションでは、トランジションの最初のレッグ、トランジションの最後のレッグにアクセスできるようにしたいので、トランジションでは脚から脚までナビゲートしたいと思っています。したがって、私は最初、最後、そして次の関数が必要です。

これを実装する最も簡単な方法は何ですか？私は実装が動作しているが、もっと簡単なことがあるのだろうかと思う。シーケンス番号への私の実装を関連付け、各脚：

open util/ordering [SequenceNumber] 
sig SequenceNumber {} 

sig Transition { 
    legs: Leg one -> one SequenceNumber 
} 

その後、私は私自身の効用関数を作成：

fun First (t: Transition): Leg { 
    t.legs.(min [Leg.(t.legs)]) 
} 

fun Last (t: Transition): Leg { 
    t.legs.(max [Leg.(t.legs)]) 
} 

fun Next (t: Transition, leg: Leg): Leg { 
    t.legs.(next [leg.(t.legs)]) 
} 

私はあなたが私に簡単な解決策を示すことができる期待しています。

Answer 1

seq Legと組み込みシーケンス述語&の機能を使用しないのはなぜですか？