## Cours OFA (30.03.2021) ### Introduction - fin d'étude du tutorial dynamic power magement - nouvelle idée de projet Amine Hadjiat, Sebastien Chassot --- ## dynamic power magement CTMC - ajout de reward au modèle - plot de différentes propriétés ---- ### Reward/Cost ```verilog rewards "queue_size" true : q; endrewards rewards "lost" [request] q=q_max : 1; endrewards rewards "power" sp=0 : 0.13; sp=1 : 0.95; sp=2 : 2.15; [sleep2idle] true : 7; [idle2sleep] true : 0.067; endrewards ``` ---- ### Reward/Cost (lost) ![](https://i.imgur.com/bQQAyO9.png) ---- ### Reward/Cost (power) ![](https://i.imgur.com/H9uxsJ8.png) --- ## Proposition projet - on part d'une map 2D - modéliser le comportement des agents (déterministe) - modéliser le comportement des joueurs (déterministe) - modéliser les interractions (attaques, recharge) - vérifier certaines propriétés (points de vie) - objectif du projet ---- ### La map ```verilog // CONSTANTS const int n; // size of the grid ``` ```verilog // position x1 : [1..n] init 1; // x position of agent y1 : [1..n] init 1; // y position of agent ``` ---- ### modéliser comportement agents (déterministe) - déplacement en direction du player - puissance d'attaque selon progression player - temps de recharge - agents réveillés selon level du player ```verilog // reach player [] x1 < x_player & !(x1=x_player+1) -> rate_agent : (x1'=x1+1); [] y1 < y_player & !(y1=y_player+1) -> rate_agent : (y1'=y1+1); ``` ---- ### agent's state transition diagram ![](https://i.imgur.com/tHGysZ0.png) ---- ### modéliser le comportement du player (déterministe) - plusieurs checkpoints dans la map - objectif du player : atteindre le dernier checkpoint - à chaque checkpoint atteint - un signal est envoyé aux agents - level du player augmenté ```verilog [player_attacked] abs(x_playe-x1) <= 1 -> rate_attack : player_hit=1; ``` ---- ### player's state transition diagram ![](https://i.imgur.com/hQwQWxz.png) ---- ### vérification de certaines propriétés - le player se fait attaquer trop souvent (vitesse, nombre d'agents, temps de recharge) - les attaques sont trop/pas assez puissantes - montée en level en fonction de la position des checkpoints ---- ### objectif du projet - créer un modèle pour évaluer les difficultés : - la durée de vie du joueur est-elle suffisante ? - le nombre d'agents et leur puissance d'attaque sont-ils raisonnables ? - adapter la difficulté en fonction de différentes propriétés mesurées
{"metaMigratedAt":"2023-06-15T21:53:35.020Z","metaMigratedFrom":"YAML","title":"Présentation Outils formels avancés","breaks":true,"slideOptions":"{\"theme\":\"beige\",\"transition\":\"fade\"}","contributors":"[{\"id\":\"87a387b1-d175-4f51-acdf-da3806d318b3\",\"add\":3020,\"del\":2598},{\"id\":\"1ce810ad-6106-4d65-be6c-781d56daa8b7\",\"add\":2882,\"del\":534}]"}
    290 views
   Owned this note