diff --git a/Readme.md b/Readme.md index c9c7fe228cca8d812178588771479678ec287f54..ff717394980cb8541215bd0384acb98353b8ff1d 100644 --- a/Readme.md +++ b/Readme.md @@ -1,5 +1,12 @@ # 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 ```