Wie spezifiziert man die spezifischen Elemente in der Reihenfolge - mit util Bestellung in Alloy?

Question

Meine Absicht hier ist, Datum in der Reihenfolge anzugeben. Beginne mit d, gefolgt von d1, d2, d3 und end mit d ". Ich habe 'd = request.begin' als erstes Element initialisiert, während 'd' 'das letzte Element in der Reihenfolge ist. In den folgenden Codes definiere ich 'd1 = d.next', 'd2 = d1.next' und 'd3 = d2.next'. Außerdem habe ich die util-Bestellung in der Bibliothek aufgerufen; 'open util/ordern [Datum] als DateOrder'. Bei der Ausführung der Codes wurde jedoch keine Instanz gefunden. Könnte mich bitte jemand wissen lassen, was das Problem mit den Codes ist?

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

Es gibt nicht unbedingt ein Problem. Der angegebene Code ist vielleicht in Ordnung, aber das Modell, das er repräsentiert, könnte inkonsistent sein (daher kann Alloy keine Instanz finden). Beachten Sie, dass diese Antwort versucht zu raten, was falsch sein könnte, da Sie nicht das vollständige Modell und nicht genügend Details zu diesem Prädikat angegeben haben.

Es scheint, dass die Aussage

one d: Date - last 

die Inkonsistenz für Sie verursacht. Beachten Sie, dass eine solche Anweisung aufgrund des Imports der Reihenfolge nur für Universen konsistent sein kann, die über zwei Instanzen der Datumssignatur verfügen.

Als Beispiel wenn one durch some ersetzt wird, findet Legierung viele Instanzen für das folgende Modell:

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