如何按顺序指定特定元素 - 在 Alloy 中使用 util 排序？

Question

我这里的目的是按顺序指定日期。从 d 开始，然后是 d1、d2、d3，并以 d 结束。我已经将 '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

不一定有问题。给定的代码可能没问题，但它表示的模型可能不一致（因此 Alloy 找不到任何实例）。请注意，由于您没有提供完整的模型，也没有足够的细节说明您是哪个谓词运行，此答案试图猜测可能有什么问题。

好像是这个说法

one d: Date - last

给你造成不一致。请注意，由于排序的导入，此类声明可能仅对具有 2 个日期签名实例的 Universe 是一致的。

例如，如果将one替换为some，Alloy会为以下模型找到很多实例：

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

如何按顺序指定特定元素 - 在 Alloy 中使用 util 排序？

How to specify the specific elements in order - using util ordering in Alloy?

alloy