## 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)

----
### Reward/Cost (power)

---
## 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

----
### 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

----
### 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}]"}