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

Hugo Moreau authored Apr 11, 2021 and Etienne Renault committed Apr 20, 2021

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

Hugo Moreau authored Apr 11, 2021 and Etienne Renault committed Apr 20, 2021

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.

Hugo Moreau authored Apr 02, 2021 and Etienne Renault committed Apr 20, 2021

 * benchs/Makefile: Here.

Hugo Moreau authored Apr 01, 2021 and Etienne Renault committed Apr 20, 2021

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.

Hugo Moreau authored Mar 30, 2021 and Etienne Renault committed Apr 20, 2021

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

 * transform/checktype.go : Here.

Hugo Moreau authored Mar 30, 2021 and Etienne Renault committed Apr 20, 2021

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.

Hugo Moreau authored Mar 29, 2021 and Etienne Renault committed Apr 20, 2021

Blackbox can now handle global array.

 * main.go : Here.

Hugo Moreau authored Mar 29, 2021 and Etienne Renault committed Apr 20, 2021

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

 * transform/double_brackets.go : Here.

Hugo Moreau authored Mar 22, 2021 and Etienne Renault committed Apr 20, 2021

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

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

Hugo Moreau authored Mar 22, 2021 and Etienne Renault committed Apr 20, 2021

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

 * main.go : Here.

Hugo Moreau authored Mar 14, 2021 and Etienne Renault committed Apr 20, 2021

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

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

Hugo Moreau authored Mar 14, 2021 and Etienne Renault committed Apr 20, 2021

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.

Hugo Moreau authored Mar 14, 2021 and Etienne Renault committed Apr 20, 2021

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.

Hugo Moreau authored Mar 03, 2021 and Etienne Renault committed Apr 20, 2021

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

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

Hugo Moreau authored Mar 02, 2021 and Etienne Renault committed Apr 20, 2021

results was created according to the size of the caller and not the
results function. It is now corrected.

 * transform/cfg/linkresults.go : Here.

Hugo Moreau authored Mar 02, 2021 and Etienne Renault committed Apr 20, 2021

 * tests/innercall.go,
   tests/expected,
   transform/innercall.go : Here.

Hugo Moreau authored Mar 01, 2021 and Etienne Renault committed Apr 20, 2021

 * tests/expected,
   tests/multiplecallassign.go, tests/passes/innercall.go : Here.

Hugo Moreau authored Mar 01, 2021 and Etienne Renault committed Apr 20, 2021

Handling multiple func call as assignments by creating a tmp variables.

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

Hugo Moreau authored Mar 01, 2021 and Etienne Renault committed Apr 20, 2021

 * main.go : Here.

Hugo Moreau authored Mar 01, 2021 and Etienne Renault committed Apr 20, 2021

 * transform/arithmeticcall.go : Here.

Hugo Moreau authored Mar 01, 2021 and Etienne Renault committed Apr 20, 2021

Using a function call as a function args was failing before.

 * transform/cfg/linkresults.go : Here.