Skip to content
Snippets Groups Projects
Commit b61a8b96 authored by Pierre Roux's avatar Pierre Roux
Browse files

Improve documentation

parent ba30e140
Branches
No related tags found
No related merge requests found
Hide whitespace changes
Inline Side-by-side
RminStruct.v
+ 38
− 16
View file @ b61a8b96
(* Copyright : Lucien Rakotomalala, Pierre Roux and Marc Boyer. *)
(******************************************************************************)
(* Build dioid instances used in network calculus. *)
(* *)
(* F == set of functions nnR -> Rbar *)
(* *)
(* Fup == the dioid's set *)
(* Fup_min x y == first dioid's operator <-> minimum between x y forall t *)
(* Fup_min_conv == dioid's second operator <-> the min-plus convolution *)
(* between x and y *)
(* Fup_zero == dioid's zero element <-> the infinite function *)
(* Fup_one == dioid's unit element <-> the function that is zero at zero *)
(* and infinite otherwise *)
(* Fup_leP == use this if you want to switch an inequality to dioid to F *)
(* unfoldFup == use this lemma to switch between dioid and Fplus. *)
(******************************************************************************)
From HB Require Import structures.
From mathcomp Require Import ssreflect ssrfun ssrbool eqtype order ssrnat.
From mathcomp Require Import choice seq bigop ssralg ssrnum rat.
......@@ -24,6 +8,44 @@ From mathcomp.dioid Require Import HB_wrappers dioid.
From mathcomp.dioid Require Import complete_lattice complete_dioid.
Require Import nngenum.
(******************************************************************************)
(* Dioid instances used in network calculus. *)
(* *)
(* * number dioids *)
(* R+ == {nonneg R} *)
(* Q == rat *)
(* Q+ == {nonneg Q} *)
(* Q+* == {posnum Q} *)
(* \bar R and {nonnege R} are equipped with a complete lattice canonical *)
(* structure, first law is min, second law is addition, zero element is +oo *)
(* and unit element is 0. *)
(* *)
(* * functions dioids *)
(* F == functions R+ -> \bar R *)
(* Fplus == functions f in F such that for all x, 0 <= f x *)
(* Fup == functions f in Fplus that are non decreasing *)
(* F0up == functions f in Fup such that f 0 = 0 *)
(* The first three types are equipped with a complete dioid canonical *)
(* structure, first law is pointwise minimum, second law is min-plus *)
(* convolution, zero element is the constant function +oo and unit element is *)
(* the function equal to +oo everywhere except in 0 where it is 0. *)
(* The last type is *not* a dioid. *)
(* *)
(* * pointwise addition of functions *)
(* Moreover, F is equipped with a pointwise addition F_plus with neutral *)
(* element F_0, accessible with following notations in scope F_scope (%F): *)
(* f + g == pointwise addition of functions f and g *)
(* f / g == deconvolution in dioid F *)
(* -f == pointwise opposite of f *)
(* f - g == pointwise subtraction of f and g *)
(* \sum == notation for sum with bigop *)
(* *)
(* * other operators *)
(* Fup_shift_l f d == the function in Fup equal to (f : Fup) shifted by d *)
(* (i.e., t |-> f (t + d)) *)
(* pseudo_inv_inf_nnR f == y |-> inf{ x | y <= f x } *)
(******************************************************************************)
Set Implicit Arguments.
Unset Strict Implicit.
Unset Printing Implicit Defensive.
......
arrival_curves.v
+ 10
− 11
View file @ b61a8b96
(* Copyright : Lucien Rakotomalala, Pierre Roux and Marc Boyer. *)
(******************************************************************************)
(* Definiton and properties of arrival curves in Network Calculus *)
(* *)
(* is_maximal_arrival A alpha <-> alpha is an arrival curve *)
(* for the data flow A *)
(* *)
(* maximal_arrival_deconv{1,2} state that A / A *)
(* is the smallest arrival curve for A *)
(* *)
(******************************************************************************)
From mathcomp Require Import ssreflect ssrfun ssrbool eqtype order ssrnat.
From mathcomp Require Import choice seq fintype finfun bigop ssralg ssrnum rat.
From mathcomp.analysis Require Import reals ereal nngnum posnum boolp classical_sets.
......@@ -20,6 +9,16 @@ Require Import nngenum RminStruct.
Require Import cumulative_curves.
Require Import NCCoq.usual_functions.
(******************************************************************************)
(* Arrival curves in Network Calculus *)
(* *)
(* is_maximal_arrival A alpha <-> alpha is an arrival curve *)
(* for the data flow A *)
(* *)
(* maximal_arrival_deconv{1,2} state that A / A *)
(* is the smallest arrival curve for A *)
(******************************************************************************)
Set Implicit Arguments.
Unset Strict Implicit.
Unset Printing Implicit Defensive.
......
cumulative_curves.v
+ 24
− 16
View file @ b61a8b96
(******************************************************************************)
(* Data flows for network calculus. *)
(* *)
(* We define the main object studied by network calculus. *)
(* A flow cumulative function is a function from R+ to R+, *)
(* non-decreasing, null at 0 and left continuous.It represents the total *)
(* amount of data of a flow at *)
(* some observation point up to observation time.See [DNC18, §1.3] *)
(* *)
(* flow_cc == the type for data flows *)
(** A flow cumulative curve is a function R+ -> R+ that
- is non-decreasing;
- takes value 0 in 0;
- is left-continuous. *)
(* *)
(******************************************************************************)
(* Copyright : Lucien Rakotomalala, Pierre Roux and Marc Boyer. *)
From mathcomp Require Import ssreflect ssrfun ssrbool eqtype order ssrnat.
From mathcomp Require Import choice seq bigop ssralg ssrnum rat.
......@@ -22,6 +7,29 @@ From mathcomp.dioid Require Import HB_wrappers dioid.
From mathcomp.dioid Require Import complete_lattice complete_dioid.
Require Import nngenum RminStruct.
(******************************************************************************)
(* Data flows for network calculus. *)
(* *)
(* We define the main object studied by network calculus. *)
(* A data flow cumulative function is a function from R+ to R+, *)
(* non-decreasing, null at 0 and left continuous. It represents the total *)
(* amount of data of a flow at some observation point up to observation time. *)
(* *)
(* flow_cc == the type for data flows, functions in Fup that: *)
(* * are equal to 0 at 0; *)
(* * are left-continuous; *)
(* * only take finite values. *)
(* flow_cc are equipped with a coercion to Fup *)
(* f%:fcc == the function in R+ -> R+ equal to f : flow_cc *)
(* left_cont_closure f == the left continuous closure of f, i.e. *)
(* t |-> sup{ f u | u < t } *)
(* *)
(* flow_cc iq equipped with an addition flow_cc_plus with neutral element *)
(* flow_cc_0 and following notations in scope flow_cc_scope (%C): *)
(* f + g == pointwise addition of functions f and g *)
(* \sum == notation for sum with bigop *)
(******************************************************************************)
Set Implicit Arguments.
Unset Strict Implicit.
Unset Printing Implicit Defensive.
......
0% or .
You are about to add 0 people to the discussion. Proceed with caution.
Please register or to comment