env + typo

Readme.md

 # DSL pour Robotique en Essaim
 
+### Environnement 
+  Ocaml 4.13
+  Dune 3.15
+  Coq 8.15
+
+
+
 ### Valeurs possibles pour chaque éléments de la description de l'environnement :
 
 - Sync := Permet de définir le type de synchronisation.
@@ -14,68 +21,83 @@ Sync := ASYNC
 
 - Space := Permet de définir l'espace dans le quel vont évoluer les robots.
   - R  -> une seul dimension
-  - Rm -> millefeuille d'une dimension, correspondant par exemple a x routes paralelles
+  - mR X -> mille-feuille d'une dimension, correspondant par exemple a X routes parallèles, X peut ne pas être renseigné.
   - R2 -> plan 
-  - R2m -> millefeuille de plan, correspondant a des plan sur plusieurs etages
-  - Ring n -> correspond a un anneau Z/nZ 
+  - mR2 X -> mille-feuille de plan, correspondant a des plan sur X étages, X peut ne pas être renseigné. 
+  - Ring n -> correspond a un anneau Z/nZ, n peut ne pas être renseigné.
 
 exemple :
 ```
 Space := Ring 5
 ```
+
 - Byzantine := Permet de déclarer le nombre de Byzantins ou directement les robots qui le sont via leur id.
-  - x -> un entier correspondant à la proportion de Byzantins
+  - x -> un entier correspondant à la proportion de Byzantins tel que n/x avec n le nombre de robot
   - [id1;id2;id3] -> liste d'entier correspondant aux id des Byzantins
+
 ```
-exemple : Byzantine := [1;2;7;8]
+exemple : Byzantine := 5
 ```
-- Rigidity: Défini si le robot peut etre interrompu lors de son déplacement
+
+- Rigidity: Défini si le robot peut être interrompu lors de son déplacement
         - Rigide -> Le robot finit sont déplacement avant de recommencer un cycle LCM
-        - Flexible f -> f est une variable est correspond a la distance minimal que le robot va parcourir avant de pouvoir etre interrompu et commencer un nouveau cycle LCM
+        - Flexible f -> f est une variable est correspond a la distance minimal que le robot va parcourir avant de pouvoir être interrompu et commencer un nouveau cycle LCM
+
 ```
 Rigidity := Flexible delta 
 ```
 
-Couleur : Red; Blue; Yellow; Green; Purple; Orange
-- Robot := Permet de definir des champs privés et publiques pour le robot, il est necessaire de lister les éléments privés puis les éléments publiques
-    - Private : Champ 1; Champ 2; ...
-    - Public : Champ 3; Champ 4; ...
+- Robot := Permet de définir des champs privés et publiques pour le robot, il est nécessaire de lister les éléments privés puis les éléments publiques
+- Private : Champ 1; Champ 2; ...
+- Public : Champ 3; Champ 4; ...
+
+Pour la lumière : 
+ - Internal Light 
+ - External Light
+ - Full Light
+
+Les champs, ainsi que les couleurs des lumière sont au choix de l'utilisateur.
+
 
-Les champs sont définis par l'utilisateur, et peuvent prendre des valeurs ou non.
 exemple :
+
 ```
-Robot := Private :  Temperature; Coordonnee [5;1.8]
+Robot := Private :  Temperature; Internal Light [Rouge;Noir]
          Public : Id; Batterie
-```            
+
+```
+
 - Sensors := Permet de définir les capteurs des robots, et les fonction de degradations sur informations reçues
   Default :
   - **Range** : Correspond à la distance de vue des robots
-    - F Byzantinull       -> Le robot à une range ilimité 
+    - Full       -> Le robot à une range illimité 
     - Limited d  -> range limité à un delta
-    - K_Rand d k -> range limité à un delta + capable de voir k robots au dela de delta choisie rand
-    - K_enemy d k -> range limité à un delta + capable de voir k robots au dela de delta choisie par un ennemie
+    - K_Rand d k -> range limité à un delta + capable de voir k robots au delà de delta choisie rand
+    - K_enemy d k -> range limité à un delta + capable de voir k robots au delà de delta choisie par un ennemie
   - **Opacity**: Correspond à l'opacité des robots
     - Opaque -> les robots derrières un autre robot ne sont pas visibles
     - Transparent -> les robots derrières un autre robot sont visibles
-  - **Multiplicity** : Correspond à la détection de la multiplicité et la ditance de detection
-    - No  -> les robots ne detectent pas la multiplicité
-    - Weak -> les robots detectent si il y a 1 ou plusieurs robots 
-    - Strong -> les robots detectent le nombre exacte de robots 
+  - **Multiplicity** : Correspond à la détection de la multiplicité et la distance de detection
+    - No  -> les robots ne détectent pas la multiplicité
+    - Weak -> les robots détectent si il y a 1 ou plusieurs robots 
+    - Strong -> les robots détectent le nombre exacte de robots 
     - Local -> detection a leur position
     - Global -> detection sur toutes les positions observés
   
 On peut aussi utiliser les capacités/champs renseignés en **PUBLIC** dans Robot
 
-                            
-exemple: 
+
+exemple:
 ```
-Sensors := Range : Limited 5; Multi : Weak Local; 
+Sensors := Range : Limited r; 
+           Multi : Weak Local; 
            Opacity : Opaque;
            Batterie : (fun x -> if x > 50 then 100 else 50);
 ```
 
-- ActivelyUpdate :=  Permet de définir les champs de robots qui vont pouvoir etre modifié par le robogram, Location est par defaut.
+- ActivelyUpdate :=  Permet de définir les champs de robots qui vont pouvoir être modifié par le robogram, Location est par défaut, mais doit être indiqué si il y a plus d'un champs mis à jour
+
 ```
-ActivelyUpdate := Light
+ActivelyUpdate := Location;Light
 ```