Commit e41043cb authored by Maxime Folschette's avatar Maxime Folschette
Browse files

start translating comments in English

parent 061c81d8
......@@ -2,7 +2,7 @@
Implementation of the weakest precondition calculus using Hoare logic
on biological regulatory networks.
Reference:
Reference article:
G. Bernot, J.-P. Comet, Z. Khalis, A. Richard, O. Roux,
A genetically modified Hoare logic,
Theoretical Computer Science,
......
(***
Implémentation du calcul de plus faible précondition à l'aide de logique de Hoare
sur des réseaux de régulation biologique.
Implementation of the weakest precondition calculus using Hoare logic
on biological regulatory networks.
Référence :
Reference article:
G. Bernot, J.-P. Comet, Z. Khalis, A. Richard, O. Roux,
A genetically modified Hoare logic,
Theoretical Computer Science,
2018.
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)
* Les pré-conditions de boucles utilisent des sous-formules à part
(avec des variables « fraiches ») qui ne sont pas impactées par la simplification
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
See the README file for usage notes.
Principle:
This implementation defines grammars and trees to represent properties on
networks and their dynamical states (such as “a=1 AND b>0 OR ...”) and a
simple branching imperative language (increment, decrement, conditional, loop
and quantifiers) with the aim of computing the weakest precondition from given
postcondition and path program, on a given network.
This weakest precondition can also be translated to Answer Set Programming
(ASP) in order to be solved by Clingo 5 (should be also compatible with
Clingo 4; for Clingo 3, it is advised to uncomment the #hide. directive in the
produced script).
Useful functions:
- wp: compute the weakest precondition
- simplify: perform formula simplification
- string_of_formula & string_of_prog_indent: pretty-print a formula or program
- write_example: translate a formula into ASP
- asp_params: print the correspondence between ASP variables and parameters
TODO:
* Model & processes should not be hard-coded in this file
* Purify all functions regarding the model
* Make a weakest While loop invariant calculus
* Finish processings on FreshState (simplifications, etc.)
***)
(****************************)
(*** Fonction utilitaires ***)
(****************************)
(************************)
(*** Common functions ***)
(************************)
open List ;;
(** Fonction identité **)
(** Identity function **)
let id x = x ;;
(** Conversion d'une liste en chaîne de caractères selon une fonction de transformation et un séparateur *)
(** Convert list into string with given separator and element-to-string converter *)
let rec string_of_list conv sep l =
match l with
| [] -> ""
......@@ -76,7 +57,7 @@ let rec string_of_list conv sep l =
let string_of_list_delim conv sep delim1 delim2 l =
delim1 ^ string_of_list conv sep l ^ delim2 ;;
(** Calcul de l'ensemble des parties *)
(** Compute power set *)
let powerset l =
let rec ps lp l =
match l with
......@@ -84,7 +65,7 @@ let powerset l =
| h :: t -> (ps lp t) @ (ps (lp @ [h]) t) in
ps [] l ;;
(** Calcul de l'ensemble des parties ordonné *)
(** Compute oredered power set *)
let powerset_sort l fcompare =
let rec ps lp l fcompare =
match l with
......@@ -92,7 +73,7 @@ let powerset_sort l fcompare =
| h :: t -> (ps lp t fcompare) @ (ps (lp @ [h]) t fcompare) in
ps [] l fcompare ;;
(** Récupération de l'index d'un élément d'une liste *)
(** Get the index of an element in a list *)
let index l a =
let rec index_rec l a n =
match l with
......@@ -102,11 +83,11 @@ let index l a =
(**************************)
(*** Opérateurs communs ***)
(**************************)
(************************)
(*** Common Operators ***)
(************************)
(** Opérateurs logiques *)
(** Logical operators *)
type propop2 =
| And | Or | Impl ;;
type propop1 =
......@@ -114,13 +95,13 @@ type propop1 =
type propop0 =
| True | False ;;
(** Opérateurs logiques et arithmétiques *)
(** Comparison and arithmetic operators *)
type relop2 =
| LE | LT | GE | GT | Eq | NEq ;;
type exprop2 =
| Plus | Minus ;;
(** Conversion des opérateurs en chaînes de caractères pour ASP *)
(** Convert operator into string for ASP *)
let asp_of_relop2 = function
| LE -> "<="
| LT -> "<"
......@@ -132,7 +113,7 @@ let asp_of_exprop2 = function
| Plus -> "+"
| Minus -> "-" ;;
(** Conversion des opérateurs en chaînes de caractères pour affichage *)
(** Convert operator into pretty-printable string *)
let string_of_propop2 = function
| And -> "∧"
| Or -> "∨"
......
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