GitLab

programs to be used from the command line.

nb : -exe no longer exist. use -old to get the old algo.

Also, add the oracle outputs in the '.rif'.

  - Add support to handle several oracles.
  - Add a info command
  - Don't create a tmp dir in the direct mode.
  - Do not overwrite rif file, unless --overwrite-output is used
  - Add a ec_exe mode for rp that les one plus aby rif based exec to bu plugged.
  - Clean all tables to make sure that lutin result are reproductible when not
    quitting lurettetop (was not necessary in the old mode...).
  nb : this has broken some of the non-reg test.
  - and more...

Some improvements in the Lutin manual.

 - fix the coverage stuff that was not working
 - add an 'info' command that display a sum-up of the test parameters
 - add support to compile Lustre V4 programs

Moreover, we now use the direct mdoe in the non-reg tests !!

remove useless options: -boot, -oracle, -cov*

Also, split LustreRun in 2: LutinRun and LustreRun, so that check-rif compiles.

- changes in the verbosity level, or in lutin files were not taken inti account
- propagate the verbosity level to the lutin interpreter

send the Alices inputs, without any "#step i/ #outs" ; hence the
scanf at the Alices side was not working.

not display the list of options whena bad option is provided.

too big integers. Also, set the default min and max for vars to biggers values.

Still no reg test.

Most of the change will be undone latter, because my plan is to use lurettetop
instead, and therefore to remove all those warts in Lutin. However, as this is
currently working, I take a snapshot before breaking everything.

nb : non-reg test don't event pass.

In the short term, it will be the only supported mode. The idea is to
run lurette test session without generating any lurette_exe
executable.

It's not finished, but yet usable.

In particular, split Run into Run and RunBin.

- put the seed and the lutin version on stdour (as stderr) so that it appears in the .rif file
- add a '#' before "The oracle returned false at step" in the rif file
- Replace every occurence of "the oracle is violated" by "the oracle returned false".
- Display more information in lutin and check-rif when an oracle returned false.

Instead, add an integer suffix to the file name, e.g.,

  lutin -rif toto.rif (...)

will generate the file toto-2.rif if toto.rif and toto-1.rif already
exist.

This was done by moving most of the code from checkRif.ml to
lustreRun.ml (new module) and coverage.ml, so that checkRif only
contains administration stuff (dealing with options) plus a simple
top-level loop.

I've added some tests in exemple/lutin/oracle.

Try to push the reusable part of the code in the coverage and
LustreRun modules, so that chekRif.ml only contains administration
stuff (dealing with options) plus a simple top-level loop.

The rationale would be to be able to reuse that stuff from lutin for
instance.

full tail rec algo abandoned (for the time being)

- Add an option to specify the dir where to put generated C files in.
- Propagate all lutin options in the C part that fork the lutin interpreter
(-rif, -precision, -node, -boot)
- use the Sys.argv.(0) as the lutin interpreter to be called (to make sure
the same lutin is used and to be able to specify the full path in the C
file if needed).