如何在Alloy中检查两个时间段重叠？附代码实现与Time处理疑问

Great question! Let's break this down into two clear parts: translating your overlap logic into an Alloy predicate, and explaining how Alloy handles temporal ordering for your Time signature.

Handling Time in Alloy #

By default, Alloy treats your Time signature as a set of unordered atoms—there's no inherent "before" or "after" relationship unless you define it. To enable time comparisons, the easiest approach is to use Alloy's built-in util/ordering module. This module adds a strict linear order (lt) to the Time sig, plus handy helper functions like first, last, next, and prev to navigate the timeline.

Implementing the isTimeOverlap Predicate #

Your core overlap logic translates directly to Alloy. The rule is simple: two durations overlap if the start of one is not after the end of the other, and vice versa. Here's a complete implementation, including a helper for non-strict comparisons (matching your original <= logic):

// Import the ordering module to add temporal order to Time
open util/ordering[Time]

sig Time {}

sig Duration {
    startTime : one Time,
    endTime : one Time,
    // Optional but critical: Ensure valid durations (start time comes before end time)
    inv : startTime < endTime
}

// Helper function for non-strict less-than-or-equal comparison
fun lte[t1, t2 : Time] : Bool {
    t1.lt[t2] || t1 = t2
}

// Your overlap predicate
pred isTimeOverlap[a, b : Duration] {
    lte[a.startTime, b.endTime] && lte[b.startTime, a.endTime]
}

// Alternative: Inline the logic without the helper function
pred isTimeOverlapInline[a, b : Duration] {
    (a.startTime.lt[b.endTime] || a.startTime = b.endTime) && 
    (b.startTime.lt[a.endTime] || b.startTime = a.endTime)
}

Key Details: #

• Valid Duration Invariant: The inv clause in the Duration sig ensures no duration has an end time earlier than its start time. This eliminates nonsensical cases from your analysis.
• Strict vs Non-Strict Overlap: Your original code includes cases where one duration ends exactly when the other starts. If you wanted strict overlap (no "touching" durations), just replace the non-strict checks with strict lt comparisons.

Testing the Predicate #

To verify the logic works, run this command to generate instances of overlapping durations:

run isTimeOverlap for 2 Duration, 4 Time

Alloy will display visual instances where two durations overlap, so you can confirm the predicate behaves as expected.

内容的提问来源于stack exchange，提问作者Hari