## Cours OFA (13.04.2021) Amine Hadjiat, Sebastien Chassot ---- ## Etat actuel du projet - on part d'une map 2D - modéliser le comportement des agents - modéliser le comportement des joueurs - modéliser les interractions (attaques, recharge) - vérifier certaines propriétés (points de vie) ---- ### 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 ---- ### constantes  ---- ### player  ---- ### checkpoints  ---- ### premiers tests de propriétés   ---- ### travaux futurs - Ajout d'un agent. - Intéractions entre le joueur et l'agent. - Réflexions sur les nouvelles propriétés à vérifier - Par exemple : le joueur parvient-il à atteindre le dernier checkpoint avec au moins 250 HP ? --- ## Cours OFA (20.04.2021) Amine Hadjiat, Sebastien Chassot ---- ## Etat actuel du projet - le comportement du joueur fonctionne - le comportement des agents fonctionne - le mécanisme des niveaux fonctionne - travail sur la modélisation des attaques ---- ### Travail de la semaine - correction du message d'erreur :  - en vérifiant certaines propriétés, mise en doute du modèle - inverstigation pour comprendre le comportement - réécriture du modèle en DTMC ----  ----  ----  ----  ---- ### Nouveau modèle  ----  ----  ----  ---- ### Travaux futurs - Création de sous-modèles plus complexes. --- ## Cours OFA (27.04.2021) Amine Hadjiat, Sebastien Chassot ---- ## Etat actuel du projet - modélisation d'un nouveau modèle d'attaques - le modèle est déjà trop complexe - en simplifiant le modèle (supression du mecanisme de défense) - test de quelques propriétes - script python pour lancer les simulations et tester des propriétés ---- ## Nouveau modèle - conception d'un système de combat tour par tour entre deux joueurs et un ennemi. - chacun peut attaquer avec une certaines probabilité et un ordre non déterministe. - les coups peuvent soit être normaux, critiques ou manqués. - l'objectif est d'obtenir une probabilité de 60% de gagner le combat. ---- ## Les contants  ---- ## Modules contrôleur d'attaque  ---- ## Modules players  ---- ## Modules boss  ---- ## Reward frappes critiques  ---- ## Probabilités  ---- ## Script python - lancer des simulations - lancer des modélisations - à étendre suivant les besoins ---- ## Suite du projet - explorer le fonctionnement de PRISM --- ## Cours OFA (04.05.2021) Amine Hadjiat, Sebastien Chassot ---- ## Etat actuel du projet - modifications mineurs des modèles - machines d'états du modèle agent (map) - machines d'états du modèle attack - schéma de transitions (simplifiés) ---- <!-- .slide: style="font-size: 10px;" -->  ---- ## Mouvements player  ---- ## Level controller  ----  ----  ----  ---- ## Travaux futurs liés à PRISM - faire des modèles simples pour tester l'impact de la taille des domaines de variables - essayer de lancer en MTBDD et en hybrid pour voir les différences de temps --- ## Cours OFA (11.05.2021) Amine Hadjiat, Sebastien Chassot ---- ## Etat actuel du projet <!-- .slide: style="font-size: 24px;" --> - Observations sur le fonctionnement de PRISM - Model checking probabiliste - premet d'obtenir rapidement une aproximation de probabilité - Model checking - sparse - MTBDD - hybrid ---- ## Observations <!-- .slide: style="font-size: 24px;" --> - le range des variables détermine le nombre bits pour les représenter - PRISM utilise 2 types : boolean et int - le nombre de transitions est lié au nombre de terminaisons (MTBDD) ---- ## Representation des données <!-- .slide: style="font-size: 20px;" --> ``` a : [17..23] init 17; b : [5..8] init 6; ``` - représentation sur 3 bits $$a = [17 \cdots 23] \Longleftrightarrow a' = [0 \cdots 5] = [(000)_2, \cdots, (101)_2] $$ - représentation sur 2 bits $$b = [5 \cdots 8] \Longleftrightarrow a' = [0 \cdots 3] = [(00)_2, (01)_2, (10)_2, (11)_2]$$ - toutes les variables sont concaténées dans un seul vecteur $$a=3,b=2 = (01110)_2$$ ---- ## LUT states => variable ### matrice states ``` // avec n=6, x=[n..n+10], y=[1..6] (x,y) 0:(6,1) ... 5:(6,6) 6:(7,1) ... 12:(8,1) ... 18:(9,1) ... 60:(16,1) ... 65:(16,6) ``` ---- ## Opérations <!-- .slide: style="font-size: 16px;" --> $$[x_0,x_1,\cdots, x_n, y_0, \cdots, y_m, z_0, \cdots,z_p]$$ $$ [ X_{pre}, Y_{pre}, Z_{pre} ]_{1,m+n+p} \cdot A = [ X_{pre}, Y_{pre}, Z_{pre} ]_{1,m+n+p} \cdot \begin{bmatrix} I_{m,m} & 0 & 0 \\ 0 & A_{Y_{n,n}} & 0\\ 0 & 0 & I_{p,p} \\ \end{bmatrix} = [ X_{pre} Y_{post} Z_{pre} ]_{1,m+n+p}$$ ---- ## Chaque transition utilise une ou plusieurs applications <!-- .slide: style="font-size: 24px;" --> ``` [] (cond1) -> 0.5 : (level'=0) + 0.25 : (level'=1) + 0.25 : (level'=2); [] (cond2) -> 0.5 : (x'=x) + 0.25 : (x'=x+1) + 0.25 : (x'=x-1); [] (cond3) -> 0.5 : (x'=2*x) + 0.5 : (x'=3*x); ``` ---- ## Travaux futurs liés à PRISM <!-- .slide: style="font-size: 24px;" --> - mieux comprendre les MTBDD --- ## Cours OFA (18.05.2021) Amine Hadjiat, Sebastien Chassot ---- ## Etat actuel du projet <!-- .slide: style="font-size: 24px;" --> - travail sur le rapport - review du plan du rapport ---- ## PRISM - transitions <!-- .slide: style="font-size: 24px;" -->  ----