如何检查合金中的两个持续时间重叠答案

【问题标题】：How to check two Time durations overlaps in Alloy如何检查合金中的两个持续时间重叠
【发布时间】：2018-01-02 10:14:29
【问题描述】：

我有以下签名和谓词来检查两个持续时间重叠

sig Time{}
sig Duration{
   startTime : one Time,
   endTime : one Time
}
pred isTimeOverlap[a, b : Duration] {
//
}

我想在 Alloy 中实现以下逻辑（作为谓词 isTimeOverlap）。有什么具体的方法来处理合金中的时间

function Boolean isTimeOverlapp(Time $time1start, Time $time1end, Time $time2start, Time $time2end) {
   if(($time1start <= $time2end) && ($time2start <= $time1end)) {
        return TRUE;
   } else {
        return FALSE;
   }
}

【问题讨论】：

标签： alloy

【解决方案1】：

我认为在这种情况下合金更喜欢关系情况。请注意，时间是一个（有序的）集合。因此，在 2 个时间原子之间还有许多其他时间原子。 IE。范围是时间的集。重叠是它们设定值的简单重叠。 IE。如果他们有共同的时间。由于每个有序原子都有一个nexts 函数，因此您可以轻松计算范围的成员。

open util/ordering[Time]

sig Time {}


let range[s,e] = (s + s.nexts) - e.nexts // inclusive bounds i.e. [s,e]
let overlap[s1,e1,s2,e2] = some (range[s1,e1] & range[s2,e2])

check {


    // [t0,t0] ∩ [t0,tn]
    overlap[ first, first, first, last ] 

    // [t0,t1] ∩ [t1,tn]
    overlap[ first, first.next, first.next, last ]

    // [t0,t1] ∩ [t0,tn]
    overlap[ first, first.next, first, last ]

    // [t0,t1] ∩ [t0,t1]
    overlap[ first, first.next, first, first.next ] 

    // not ( [t1,t0] ∩ [t0,t1] )
    not overlap[ first.next, first, first, last ]

    // not ( [t0,t1] ∩ [t2,tn] )
    not overlap[ first, first.next, first.next.next, last ] 

    // reflexive
    all t1, t2, t3,  t4 : Time | overlap[t1,t2,t3,t4] <=> overlap[t3,t4,t1,t2]
} for 10

【讨论】：