如何在Alloy中检查两个持续时间重叠

Question

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

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;
   }
}

Answer 1

我认为合金在这种情况下更喜欢关系情况。请注意，Time是（有序）集合。所以在2个时间原子之间有许多其他时间原子。即范围是一组时间。然后重叠就是它们的设定值的简单重叠。即如果他们有任何共同的时间。由于每个有序原子都具有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