Commit 061c81d8 authored by Maxime Folschette's avatar Maxime Folschette
Browse files

README translated to English

parent 9928b434
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 5 (devrait aussi être compatible avec Clingo 4 ; pour Clingo 3, décommenter la directive #hide. dans le script produit).
Requis :
OCaml (testé sur la version 4.02.0)
Clingo 5 (testé sur la version 5.4.0)
Fichier principal : main.ml
---------------------------
Usage :
Implementation of the weakest precondition calculus using Hoare logic
on biological regulatory networks.
Reference:
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
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).
Requirements:
OCaml (tested with version 4.02.0)
Clingo 5 (tested with version 5.4.0)
Main file: main.ml
------------------
Usage:
ocaml main.ml
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 5 (énumération les états initiaux et paramétrisations compatibles).
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.
Script : run-all.sh
-------------------
Usage :
sh run-all.sh [suffixe]
Sorties : exécute chaque script ASP (entension *.lp, par ex. : script.lp)
trouvé dans le dossier courant et écrit les résultats dans autant de fichiers
(par ex. : script.lp[suffixe].out).
Model and processes specification:
For the moment, the model has to be “hard-coded” in this file under the
section “Network Description”.
The processes (computation of the weakest precondition, simplifying, etc.)
also have to be written at the end of this file in the “Sandbox” sections.
An example is already implemented (some applications on a toy example from the
reference article).
Output:
Performs some tests on the toy example and prints the result formulas on
screen.
These formulas are also translated as ASP logic programs written in .lp files
intended to be solved by Clingo 5 (enumeration of compatible initial states
and parametrizations).
You can execute Clingo on a script with the following command:
clingo 0 script.lp
Main limitations:
- The invariants has to be explicitly given for While loops, although the
reference article gives a method to compute a weakest invariant.
- Simplification of formulas does not apply to parts of the weakest
precondition that are derived from a While loop.
These two limitations can be fixed.
Script: run-all.sh
------------------
Usage:
sh run-all.sh [suffix]
Output:
Executes each ASP script (extension *.lp, e.g. script.lp) found in the current
folder with Clingo and writes the results in as many files using the suffix
and a .out extension (e.g., script.lp[suffix].out).
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