Discussion :

[Garulfo]

Bonjour,

je me demandais si qqun avait déjà fait un model-checker, si possible en traitement symbolique, avec ocaml ?

Si oui, comment avez vous représenté vos BDDs ?
Personnellement je me suis dit qu'il serait intéressant de garder l'ensemble des nœuds étiquetté par une variable pour me simplifier la vie.

Les variables sont représentées par leurs ordres, et un tableau garde le nom pour l'ordre.

Si qqun y a pensé ou a déjà fait ça, je prend ses commentaires.

[InOCamlWeTrust]

Tu as regardé sur la bosse ?
http://caml.inria.fr//cgi-bin/hump.en.cgi

[gorgonite]

perso, je n'ai jamais vraiment fait de model-checking (la honte pour un type qui fait de l'analyse statique ), mais je pense que tu devrais regarder dans les sources des grands projets comme BLAST

[Garulfo]

Tu as regardé sur la bosse ?
http://caml.inria.fr//cgi-bin/hump.en.cgi

Oui, hélas, je n'ai rien trouvé. C'est mon premier réflexe.

perso, je n'ai jamais vraiment fait de model-checking (la honte pour un type qui fait de l'analyse statique ), mais je pense que tu devrais regarder dans les sources des grands projets comme BLAST

Hum oui je ne connaissais pas ça... je vais voir. Merci.

[DavidDeharbe]

Bonjour,

je me demandais si qqun avait déjà fait un model-checker, si possible en traitement symbolique, avec ocaml ?

Si oui, comment avez vous représenté vos BDDs ?
Personnellement je me suis dit qu'il serait intéressant de garder l'ensemble des nœuds étiquetté par une variable pour me simplifier la vie.

Les variables sont représentées par leurs ordres, et un tableau garde le nom pour l'ordre.

Si qqun y a pensé ou a déjà fait ça, je prend ses commentaires.

Il y a un papier de Bryant, 93 (je crois) sur la mise en oeuvre efficace de BDDs. Sinon, tu peux jeter un coup d'oeil sur ce qui a été fait dans des bibliothèques existantes. Je crois que les BDDs ont aussi été programmé dans le prouveur ACL2, qui est écrit en LISP, et qui peut te donner une bonne indication de comment s'y prendre.

Les solutions que je connais associent en effet à chaque variable l'ensemble des noeuds étiquetés par cette variable. Il est aussi important d'utiliser des caches pour implémenter les opérateurs logiques.

Une caractéristique importante est la canonicité, qui doit être préservée. Pour cela il faut stocker tous les noeuds qui ont déjà été créés. Lors de la création d'un noeud (lors de la construction du résultat d'une opération logique, par exemple), il faut vérifier si celui-ci n'a pas été déjà créé pour éviter de créer un doublon.

David.
--

[Garulfo]

Il y a un papier de Bryant, 93 (je crois) sur la mise en oeuvre efficace de BDDs. [...]
David.
--

Efficient implementation of a BDD package (90)? Je l'ai ...
Sinon j'ai Graph-Based Algorithms for Boolean Function Manipulation de 86.

Je me demandais juste si qqun avait eu qqchose de plus précis pour ocaml ^_^

Merci pour ACP2. Je vais aller voir