Library probsa.util.etime

(* --------------------------- Reals and SSReflect -------------------------- *)
From mathcomp Require Import ssreflect ssrnat ssrbool eqtype.

(* ---------------------------------- Prosa --------------------------------- *)
From prosa.behavior Require Import time.

(* ---------------------------------- Main ---------------------------------- *)

Extended time (etime) defines an extended timeline where a time instant can be one of the following three options: (1) Undef representing unspecified time (e.g., if a job does not arrive in a given evolution), (2) Fin n representing a finite time measured by a natural number n, and (3) Infty representing infinite time (e.g., if a job never completes).

Inductive etime := Undef | Fin (n : nat) | Infty.

Definition etime_eqdef (tb1 tb2 : etime) :=
  match tb1, tb2 with
  | Undef, Undef ⇒ true
  | Infty, Infty ⇒ true
  | Fin n1, Fin n2 ⇒ n1 == n2
  | _, _ ⇒ false
  end.

Lemma eqn_etime : Equality.axiom etime_eqdef.

Canonical etime_eqMixin := EqMixin eqn_etime.
Canonical etime_eqType := Eval hnf in EqType etime etime_eqMixin.

When an extended time instant is compared to a normal time instant, we use the following convention: (1) Undef ≤ t for any time instant t, (2) Fin x > t iff x > t, and Infty > t for any time instant t.

Definition exceeds (X : etime) (t : instant) : bool :=
  match X with
  | Undef ⇒ false
  | Fin x ⇒ (x > t)%N
  | Infty ⇒ true
  end.