hoare-fol

Implementation of the weakest precondition calculus using Hoare logic
on biological regulatory networks.

Documentation:
  M. Folschette,
  The Hoare-fol Tool,
  technical report, 2019.
  https://hal.archives-ouvertes.fr/hal-02409801v1

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).

Reference article:
  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

Requirements:
  OCaml (requires 4.03.0, tested with version 4.09.0)
  Clingo 5 (tested with version 5.4.0)



Main file: main.ml
------------------

Usage:
  ocaml main.ml

Model and processes specification:
  For the moment, the model has to be “hard-coded” in this file under the
  section “BRN 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).