Compression d'états dans Spot

From LRDE

Revision as of 17:07, 29 January 2019 by Bot (talk | contribs)
(diff) ← Older revision | Latest revision (diff) | Newer revision → (diff)

Résumé

Pour représenter un système par un automate, il faut sauvegarder toutes les valeurs des variables du système pour chaque état de l'automate. Cela peut prendre beaucoup de place en mémoire lorsqu'il y a beaucoup de variables et/ou d'états, et de fait ralentit le temps d'exécution à cause des défauts de cache. Pour contourner ce problème dans Spot, on utilise une simple compression du tableau contenant les variables d'un étatet ce pour chaque état, ce qui réduit la mémoire utilisée et aussi le temps d'exécution. Dans ce rapport, nous présentons une structure de données qui améliore la compression des variables en utilisant la redondance des valeurs présentes dans différents états, et les différents problèmes rencontrés lors de son ajout dans Spot.