Как проверить, что две длительности времени перекрываются в Alloy

У меня есть следующие подписи и предикат для проверки двух перекрытий продолжительности времени

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

Я хочу реализовать следующую логику в Alloy (как предикат isTimeOverlap). Есть ли какой-то особый способ обработки Time в Alloy?

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

alloy
person Hari    schedule 02.01.2018    source источник

Ответы (1)


arrow_upward
1
arrow_downward

Я думаю, что в данном случае сплав предпочитает отношения. Обратите внимание, что Time — это (упорядоченный) набор. Таким образом, между двумя атомами времени находится ряд других атомов времени. т.е. диапазон представляет собой набор времени. В этом случае перекрытие является простым перекрытием их заданных значений. т.е. если у них есть общее Время. Поскольку каждый упорядоченный атом имеет функцию 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
person Peter Kriens    schedule 02.01.2018