PREREQUISE

- recent Linux installation
- full lustre install for "make test"
- a tiny lustre distrib is provided in ./bin
  which is sufficient for proofs, just put
  it in your path

How does it work ?
------------------

- we only consider configs with a 2-robots tower plus a single robot
- only the single robot moves 

Encoding 
--------

- nodes of the grid are numbered like that:

  678
  345
  012

- the position of the tower is "hot-encoded" by a 9-Boolean array
  (tower in pos "i" <=> d[i] /\ ! d[j] for all j <> i)

- the position of the single is "hot-encoded" by a 9-Boolean array
  (single in pos "i" <=> u[i] /\ ! u[j] for all j <> i)

Identifying configs
-------------------

- an "actual" config is a pair (d,u) wher d<>u, thus
  there are 9*8 = 72 actual configs

- among these configs some are undistinguishable modulo symetry
  The classes are COMPUTED by "make_lustre.ml", in order to avoid
  hand-made mistakes.
  => these classe are nbcls (=12, proven by construction)
  => a particular config is choosen in each class,
     these nbcls configs are called "canonical"

- Visited classes are hot-encoded by nbcls-Boolean array
  => the function "actual config -> class" is AUTOMATICALY
  generated  by "make_lustre.ml", in order to avoid hand-made mistakes.

Proof Program
-------------

- we write a reactive program (in lustre) with:
  * 4 inputs: m1, p1, m3, p3, encoding the "desired" moves of the single robot
  * a variable d encoding the pos of the tower, set to a constant d0
  * a variable u encoding the pos of the single, initialized to a constant u0
    inputs (required moves) are considered in sequence:
    if m1, and the move is correct then single moves left
    else if p1, and the move is correct then single moves right 
    else if m3, and the move is correct then single moves down
    else if p3, and the move is correct then single moves up

  In addition, the program manages several variables to keep trace
  of the execution:
  * viewed = 9-Boolean array encoding the visited nodes
  * cls = nb-cls array encoding the classes visited at least once
  * cls2 = nb-cls array encoding the classes visited at least twice
  * stuck = (Boolean) cls2 is not fully false (some class has been visited twice)
  * viewed_count = (binary-encoded int) the number of visited nodes
    (caridnal of viewwd)

  At last, the program computes a "flag":
  * ok = (stuck => (viewed_count <= 6))
    i.e. if some class has been visited twice, then not more than 

  => N.B. as soon as stuck becomes true, the whole program is "freezed"
     in order to avoid unnecessary exploration

Proof
-----

- we use an invariant checker (specialized model-checker) checking that:
  * starting in a valid config (d0,u0),
    and whatever be an arbitrary long sequence of inputs,
    ok remains always true  
    (i.e. (stuck => (viewed_count <= 6)) is an invariant of any execution)

N.B. This proof can be splitted into 12 (nbcls) smaller proofs, one
     for each canonical initial config, in order to limit the state-space
     explotion (less than 9s cpu for the 12 proofs).
     However, the model-checker was able to perform the whole proof
     in less than 16s cpu.

ubuntu/Intel Xeon 2.67Ghz 8Gb ram