GitLab

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

- Split check-rif.ml into check-rif.ml and coverage.ml.
- Add a section dedicated to check-rif in the Lutin manual, in the tool section.
- Use the ocaml Arg module to deal with command-line args.
- Take advantage of the fact that an ec file only have one node.
- Store/update the corevage info in a .cov file

was too small.

The idea is that Rif_base does not depend on any other module while
Rif keeps its interface but relies on Rif_base for its implementation.

Propagate some changes in the gnuplot syntax in gnuplot-rif. This will break old version of gnuplot. Sigh. Also, make -wxt the default behavior of gnuplot-rif.

Fix a bug (probably introduced in 0b0203fe) where the path of the env file was not explicit which prevent Makefile.lurette to find it. \n ps : it is no more possible to use a list of file in the env slot ; but who cares now that Lutin is usable from Lurette?

deterministic subset seems to work

Conflicts:
	source/Lutin/Makefile.lutin
	source/Lutin/main.ml