特定の要素を順番に指定するには - 合金のutil orderingを使用しますか？

Question

私の意図は、日付を順番に指定することです。最初の要素として 'd = request.begin'を初期化し、順序の最後の要素として 'd' 'を初期化しました。次のコードでは、 'd1 = d.next'、 'd2 = d1.next'、および 'd3 = d2.next'を定義します。さらに、私は図書館でutilの注文を呼びました。 'open util/ordering [Date] as DateOrder'をクリックします。ただし、コードを実行する際にインスタンスが見つかりません。誰も私にコードの問題点を教えてもらえますか？

open util/ordering [Date] as DateOrder 

    abstract sig resource {} 

    one sig Tour extends resource {date : one Date, destination : tour_destination} 
    one sig tour_destination {} 

    pred holiday [disjoint d,d1,d2,d3,d": some Date , r:Request, t:Tour] { 
    r.begin = d and r.end = d" 
    t.date = d or t.date = d1 or t.date = d2 or t.date = d3 or t.date = d" 
    d != d"} 

    sig Date{} 

    pred init [d:Date]{d= Request.begin} 

    fact traces { 
    init [first] 
    let d" = last | one d : Date - last | 
    let d1 = d.next, d2 = d1.next, d3 = d2.next | 
     lone t: Tour, r: Request| 
      holiday [d,d1,d2,d3,d",r,t]} 

    one sig Request{tour_request: one Tour,begin: one Date, end: one Date} 


    run holiday 

Answer 1

必ずしも問題ではありません。与えられたコードは良いかもしれませんが、それが表すモデルは矛盾するかもしれません（したがって、合金はインスタンスを見つけることができません）。完全なモデルは提示されておらず、どの述語が実行されているかに関する十分な詳細情報もないので、この答えは何が間違っているのかを推測します。

声明

one d: Date - last 

はあなたのために矛盾が発生しているようです。順序のインポートのため、このようなステートメントは、Dateシグネチャのインスタンスが2つあるユニバースに対してのみ一貫している可能性があります。

例としてoneがsomeによって置き換えられた場合、合金は、以下のモデルのインスタンスの多くを見つける：

open util/ordering [Date] 

sig Request{ 
    begin: lone Date 
} 

sig Date{} 

pred init [d:Date]{d= Request.begin} 

fact traces { 
    init [first] 
    let d" = last | some d : Date - last | 
    let d1 = d.next, d2 = d1.next, d3 = d2.next | 
    d1 in Date && d2 in Date && d3 in Date && d" in Date 
} 

run {} for 4 but 1 Request