Function TIME-RANGE.END-TIME

• Defined in theory: Jat-generic
• Source code: job-assignment-generic.lisp

Slots on this function:

Documentation:

(TR-END-TIME 'tr) denotes an end time of a time range tr.

Instance-Of: Function

Arity: 2

Domain: Time-range

Range: Time-point

Other Related Axioms:

(Tp= (Tp+ (Time-Range.Start-Time ?Time-Range)
          (Time-Range.Duration ?Time-Range))
     (Time-Range.End-Time ?Time-Range))

(=> (Time-Range ?Time-Range)
    (Tp= (Tp+ (Time-Range.Start-Time ?Time-Range)
              (Time-Range.Duration ?Time-Range))
         (Time-Range.End-Time ?Time-Range)))

(=> (Time-Range.End-Time $X $Y) (Time-Point $Y))

(=> (Time-Range.End-Time $X $Y) (Time-Range $X))

(<=> (Before ?Tr1 ?Tr2)
     (Tp< (Time-Range.End-Time ?Tr1) (Time-Range.Start-Time ?Tr2)))

(<=> (After ?Tr1 ?Tr2)
     (Tp< (Time-Range.End-Time ?Tr2) (Time-Range.Start-Time ?Tr1)))

(<=> (Equals ?Tr1 ?Tr2)
     (And (Tp= (Time-Range.Start-Time ?Tr1)
               (Time-Range.Start-Time ?Tr2))
          (Tp= (Time-Range.End-Time ?Tr1) (Time-Range.End-Time ?Tr2))))

(<=> (During ?Tr1 ?Tr2)
     (And (Tp> (Time-Range.Start-Time ?Tr1)
               (Time-Range.Start-Time ?Tr2))
          (Tp< (Time-Range.End-Time ?Tr1) (Time-Range.End-Time ?Tr2))))

(<=> (Overlaps ?Tr1 ?Tr2)
     (And (Tp< (Time-Range.Start-Time ?Tr1)
               (Time-Range.Start-Time ?Tr2))
          (Tp< (Time-Range.Start-Time ?Tr2)
               (Time-Range.End-Time ?Tr1))
          (Tp< (Time-Range.End-Time ?Tr1) (Time-Range.End-Time ?Tr2))))

(<=> (Starts ?Tr1 ?Tr2)
     (And (Tp= (Time-Range.Start-Time ?Tr1)
               (Time-Range.Start-Time ?Tr2))
          (Tp< (Time-Range.End-Time ?Tr1) (Time-Range.End-Time ?Tr2))))

(<=> (Finishes ?Tr1 ?Tr2)
     (And (Tp> (Time-Range.Start-Time ?Tr1)
               (Time-Range.Start-Time ?Tr2))
          (Tp= (Time-Range.End-Time ?Tr1) (Time-Range.End-Time ?Tr2))))

(=> (= (Tr+ ?Tr1 ?Duration) ?Tr2)
    (= (Tp+ (Time-Range.End-Time ?Tr1) ?Duration)
       (Time-Range.End-Time ?Tr2)))