首页 文章

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

提问于
浏览 次
1

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

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 回答

  • 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
    回复于

相关问题