GitLab

* main.go: Here.

* README.md: Here.

* benchs/extract_results.sh,
benchs/generate-fig.r: Here.

* benchs/run-ltl-bb.sh,
benchs/run-reach-bb.sh: Here

Makefile: here.

* Makefile: Here.

* Makefile, benchs/run-benchmark.sh: Here.

* main.go: Here.

* Makefile: Here.

* boilerplate/main.go: Here.

- The benchmark now accept TIMEOUT=10s to fix the maximum
running time of each test.
- The output is the same, whatever the experience considered
- The logs file are now displayed with then \cr\n

* benchs/run-ltl-bb.sh,
benchs/run-ltl.sh,
benchs/run-reach-bb.sh,
benchs/run-reach.sh: Here.

* benchs/Makefile: Here.

* main.go: Here.

Depending on the layout of the map, one could
stop when encountering prefix only. We should
was the wall set

* tools/formulae.go: Here.

* tools/recursion.go:  Here.

* benchs/run-ltl-bb.sh, benchs/run-ltl.sh: Here.

Avoid systematic computation of the whole State Space
that can be too huge.

* benchs/build.sh: Here.

* main.go: Here.

A new log directory is now generated when bench is in progress,
containing all log files, named with this pattern,
`formula.<FORMULA NB>.[bb.].log`.

To preserve a nice workflow and tracking more efficiently when Makefile
can possibly fail. The current workflow is LTL files, Reach files, LTL
files blackboxed, Reach files blackboxed.

 * benchs/Makefile: Here.

By invoking the make command in benchs, you can now generate a benchmark
for basic LTL and REACH RERS files.

 * benchs/Makefile,
   benchs/run-ltl.sh,
   benchs/run-reach.sh: Here.

Multidimensional arrays are not treated yet, so a panic is triggered if
go2pins encounters one.

 * transform/checktype.go : Here.

To avoid collision since we modify IndexExpr and nested IndexExpr, we
now use a map to check if the element has already been modified.

 * transform/double_brackets.go: Here.

Blackbox can now handle global array.

 * main.go : Here.

Double brackets transform can now handle IndexExpr using IndexExpr
recusrively in order to use an array as an index.

 * transform/double_brackets.go : Here.

If blackbox is set to auto, the blackbox functions are defined with the
formula.

 * main.go,
   tools/formulae.go : Here.

Go2Pins now accepts a second argument, a formula to run directly
modelchecking on it.

 * main.go : Here.

By calling go2pins with rers, it will automatically detect the RERS
input values.

 * benchs/run-blackbox/test.sh,
   main.go,
   tools/rers.go : Here.

A little script to compare the formulae auto detecting blackbox
efficiency, it output the result for both blackbox and non blackbox
file.

 * benchs/run-blackbox-test.sh : Here.

In order to make easier the use of blackbox, for a given file, if we
pass a formulae file to go2pins, it will automatically set the functions
to be blackboxed.

In order to avoid conflict with global variables defined after assigning
to it, LocalVariableAssignments has been corrected.

 * main.go,
   transform/localvariableassignments.go : Here.