Commit 99ebae12 authored by Maxime Folschette's avatar Maxime Folschette
Browse files

extensive README and comments (in French)

parent 624a3b4d
Implémentation du calcul de plus faible précondition à l'aide de logique de Hoare
sur des réseaux de régulation biologique.
Référence :
G. Bernot, J.-P. Comet, Z. Khalis, A. Richard, O. Roux,
A genetically modified Hoare logic,
Theoretical Computer Science,
2018.
ISSN: 0304-3975
DOI: https://doi.org/10.1016/j.tcs.2018.02.003
Principe :
Définit des langages d'arbres pour représenter des propriétés sur les réseaux
(formules du type « a = 1 ET b > 0 OU ... »)
et un langage impératif simple (incrémentation, conditionnelle, boucles, et quantificateurs)
dans l'objectif de calculer une plus faible précondition à partir d'une postcondition
et d'un programme donnés, sur un réseau donné.
La plus faible précondition peut aussi être exportée en Answer Set Programming (ASP)
pour être résolue avec Clingo 3.
Requis :
OCaml (testé sur la version 4.02.0)
Clingo 3 (testé sur la version 3.0.5)
Attention, les scripts ne sont pas compatibles avec les versions 4 et 5 de Clingo
Fichier principal : main.ml
---------------------------
Usage :
ocaml main.ml
Sorties : tests manuels dans le programme (à l'écran) et programmes ASP
permettant l'énumération des états initiaux et paramétrisations compatibles.
Le modèle doit être modifié « en dur » dans la section « Informations du BRN ».
Les résultats (calcul de plus faible précondition, simplifications, etc.) sont à écrire
à la fin du programme dans les sections « Bac à sable ».
Un exemple est déjà implémenté (quelques applications tirées du papier de référence).
Sorties : tests sur l'exemple courant : affichage des formules obtenues (à l'écran)
et production de programmes en Answer Set Programming (ASP) destinés à être résolus
par Clingo 3 énumération les états initiaux et paramétrisations compatibles.
Le modèle doit actuellement être modifié à la main dans le programme
(section « Informations du BRN »).
Limitation : il faut pour le moment définir un invariant explicite
pour les boulces (Tant que) bien que le papier de référence donne une méthode permettant
de calculer un plus faible invariant.
......
(***
Implémentation du calcul de plus faible précondition à l'aide de logique de Hoare
sur des réseaux de régulation biologique.
Référence :
G. Bernot, J.-P. Comet, Z. Khalis, A. Richard, O. Roux,
A genetically modified Hoare logic,
Theoretical Computer Science,
2018.
ISSN: 0304-3975
DOI: https://doi.org/10.1016/j.tcs.2018.02.003
Cf. documentation du fichier README
Principe :
Définit des langages d'arbres pour représenter des propriétés sur les réseaux
(formules du type « a = 1 ET b > 0 OU ... »)
et un langage impératif simple (incrémentation, conditionnelle, boucles, et quantificateurs)
dans l'objectif de calculer une plus faible précondition à partir d'une postcondition
et d'un programme donnés, sur un réseau donné.
La plus faible précondition peut aussi être exportée en Answer Set Programming (ASP)
pour être résolue avec Clingo 3.
Utilisation :
Le modèle doit être modifié « en dur » dans la section « Informations du BRN ».
Les résultats (calcul de plus faible précondition, simplifications, etc.) sont à écrire
à la fin du programme dans les sections « Bac à sable ».
Un exemple est déjà implémenté (quelques applications tirés du papier de référence).
Le programme est fonctionnel et peut être exécuté par la commande :
ocaml main.ml
Limitations théoriques :
* Il faut pour le moment définir un invariant explicite pour les boulces (Tant que)
Limitations techniques :
* Le modèle et les traitements doivent être implémentés « en dur » dans le code
* La résolution par Clingo peut être très longue pour certaines formules
* La sortie de Clingo peut être difficile à lire
Fonctions utiles :
- wp : calcule la plus faible précondition associée à une postcondition et un programme donnés
- simplify : simplifie une formule de type précondition ou postcondition, grâce
à des propriétés logiques simples comme les règles de De Morgan
- string_of_formula : traduit une formule en chaîne de caractères affichable
- string_of_prog_indent : idem pour un programma impératif (avec indentations)
- write_example : traduit une formule en ASP et l'écrit dans un fichier
- asp_params : affiche la correspondance entre les variables ASP et les paramètres du modèle
TODO :
* Trouver une solution (parsing de fichier ?) pour ne plus modifier les données en dur
* « Purifier » les fonctions
* Faire un calcul automatique de plus faible invariant pour les boulces
* Terminer les traitements des FreshState (simplifications, etc.)
* Passer à Clingo 5
***)
(****************************)
(*** Fonction utilitaires ***)
(****************************)
......
Supports Markdown
0% or .
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment