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.
  • FSYNC -> Full synchrone
  • SSYNC -> Semi synchrone
  • ASYNC -> Asynchrone

exemple :

Sync := ASYNC 

• Space := Permet de définir l'espace dans le quel vont évoluer les robots.
  • R -> une seul dimension
  • mR X -> mille-feuille d'une dimension, correspondant par exemple à X routes parallèles, X peut ne pas être renseigné.
  • R2 -> plan
  • mR2 X -> mille-feuille de plan, correspondant à 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 tel que n/x avec n le nombre de robot
  • [id1;id2;id3] -> liste d'entier correspondant aux id des Byzantins

exemple :

Byzantine := 5

• 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 être interrompu et commencer un nouveau cycle LCM

Rigidity := Flexible delta 

• 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.

exemple :

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
    • 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 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 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:

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 ê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 := Location;Light