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

Hugo Moreau authored Feb 24, 2021 and Etienne Renault committed Apr 20, 2021

 * main.go,
   tools/blackbox.go,
   transform/global.go,
   transform/postglobal.go : Here.

Hugo Moreau authored Feb 21, 2021 and Etienne Renault committed Apr 20, 2021

The blackbox package now import structs only if the blackboxed contains
global variables, it was importing it everytime before.

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

Hugo Moreau authored Feb 21, 2021 and Etienne Renault committed Apr 20, 2021

it appeared that not blackbox function call were modified anyway. It is
now fixed.

 * tools/blackbox.go : Here.

Hugo Moreau authored Feb 21, 2021 and Etienne Renault committed Apr 20, 2021

Blackboxed functions are now able to handle global variables, by using
G2PState as a reference.

 * main.go,
   tools/blackbox.go,
   transform/checktype.go, transform/global.go,
   transform/globaltostate.go, transform/localvariableassignments.go,
   transform/postglobal.go : Here.

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

For future global variable access via `Blackbox`, all type generated by
Go2Pins are now stored in a dedicated package `structs`.
All convenient modifications has been done to let Go2Pins in a valid
state.

 * boilerplate/Makefile, boilerplate/main.go,
   boilerplate/structs/structs.go,
   decl/decl.go,
   main.go,
   tools/blackbox.go,
   transform/meta.go : Here.

Hugo Moreau authored Feb 17, 2021 and Etienne Renault committed Apr 20, 2021

Getter and Setter were added twice.

 * transform/global.go : Here.

Hugo Moreau authored Feb 15, 2021 and Etienne Renault committed Apr 20, 2021

Global var can be placed in all the file and not necessarily before its
actual using. So it is now detected before applying the transform.

 * main.go,
   transform/global.go,
   transform/preglobal.go : Here.

Hugo Moreau authored Feb 15, 2021 and Etienne Renault committed Apr 20, 2021

Currently all tests are passing, except `after.go`, we can create global
variable everywhere in the file, patch will come soon.

 * tests/global/ : Here.