Library Fairisle.Fairisle.SPECIF.ROUND_ROBIN.NextPort



Require Export PortsCompl.
Require Import Arith_Compl.

Set Implicit Arguments.
Unset Strict Implicit.

Section Successor_Modulo_NbPorts.

  Variable i : nat.   Let Inportno := T_Inportno i.
  Let no : Inportno → nat := no_in (i:=i).
  Notation C_Inp := (exist (fun n : nat ⇒ n < i)) (only parsing).

Returns the next successful input port according to the last successful one and according to the number of input ports

 Definition SUC_MODN (last : Inportno) : Inportno :=
   match less_or_eq last with
   | left p ⇒
       exist (fun n : nat ⇒ n < i) (S (no last)) p
   | right p ⇒
       exist (fun n : nat ⇒ n < i) 0 (Ex_n_lt_gen (n:=i) (m:=no last) p)
   end.

End Successor_Modulo_NbPorts.