Commits · master · Spot / go2pins

23 Dec, 2020 5 commits

bench: propagate use of multithreading · 380f320f
Etienne Renault authored Dec 23, 2020
```
* benchs/run-benchmark.sh: Here.
```
380f320f
go2pins: enable multithreading for backends · ec0f2d13
Etienne Renault authored Dec 23, 2020
```
* Makefile,
benchs/run-benchmark.sh,
boilerplate/main.go: Here.
```
ec0f2d13

benchs: fix 2020 benchmark formulae · 2eaa308e

Etienne Renault authored Dec 23, 2020

In the latest version of RERS, the inputs is
slightly modified, our script failed the translation

* benchs/RERS/2020-Problem1-ltl.go.formulae.txt,
benchs/RERS/2020-Problem2-ltl.go.formulae.txt,
benchs/RERS/2020-Problem4-ltl.go.formulae.txt,
benchs/RERS/2020-Problem5-ltl.go.formulae.txt,
benchs/RERS/2020-Problem7-ltl.go.formulae.txt: Here.

2eaa308e

benchs: stop&go is now available · 3d7e9c92

Etienne Renault authored Dec 23, 2020

Our cluster is configured (using SLURM) to limit
jobs longer than 24h. This is a PITA since our
benchmark (in sequential) last more than 24 hours.
This patch allows stop and go on the benchmark

* benchs/run-benchmark.sh: Here.

3d7e9c92

benchs: add missing numbering · a2c874b4
Etienne Renault authored Dec 23, 2020
```
* benchs/run-benchmark.sh: Here.
```
a2c874b4

21 Dec, 2020 5 commits

benchs: restore transpilation · b9f2a12f
Etienne Renault authored Dec 21, 2020
```
* benchs/run-benchmark.sh: Here.
```
b9f2a12f
benchs: update scripts · 42f56cbf
Etienne Renault authored Dec 21, 2020

42f56cbf
benchs: fix variable name during RERS formulae conversion · 060775de
Etienne Renault authored Dec 21, 2020
```
* benchs/RERS/ltlrers2go.sh: Here.
```
060775de

bench: fix to correct variable name · 0cbebb87

Etienne Renault authored Dec 21, 2020

* benchs/RERS/2016-Problem1-ltl.go.formulae.txt,
benchs/RERS/2016-Problem2-ltl.go.formulae.txt,
benchs/RERS/2016-Problem4-ltl.go.formulae.txt,
benchs/RERS/2016-Problem5-ltl.go.formulae.txt,
benchs/RERS/2016-Problem7-ltl.go.formulae.txt,
benchs/RERS/2017-Problem1-ltl.go.formulae.txt,
benchs/RERS/2017-Problem2-ltl.go.formulae.txt,
benchs/RERS/2017-Problem4-ltl.go.formulae.txt,
benchs/RERS/2017-Problem5-ltl.go.formulae.txt,
benchs/RERS/2017-Problem7-ltl.go.formulae.txt,
benchs/RERS/2018-Problem1-ltl.go.formulae.txt,
benchs/RERS/2018-Problem2-ltl.go.formulae.txt,
benchs/RERS/2018-Problem4-ltl.go.formulae.txt,
benchs/RERS/2018-Problem5-ltl.go.formulae.txt,
benchs/RERS/2018-Problem7-ltl.go.formulae.txt,
benchs/RERS/2019-Problem1-ltl.go.formulae.txt,
benchs/RERS/2019-Problem2-ltl.go.formulae.txt,
benchs/RERS/2019-Problem4-ltl.go.formulae.txt,
benchs/RERS/2019-Problem5-ltl.go.formulae.txt,
benchs/RERS/2019-Problem7-ltl.go.formulae.txt: Here.

0cbebb87

bench: fix timing options · ad6feb7a
Etienne Renault authored Dec 21, 2020
```
* benchs/run-benchmark.sh: Here;
```
ad6feb7a

18 Dec, 2020 3 commits

benchs: add part about LTL · 85c0e480
Etienne Renault authored Dec 18, 2020
```
*  benchs/run-benchmark.sh: Here.
```
85c0e480

benchs: add rers LTL problem · a48adae0

Etienne Renault authored Dec 18, 2020

benchs/RERS/2016-Problem1-ltl.go,
benchs/RERS/2016-Problem1-ltl.go.formulae.txt,
benchs/RERS/2016-Problem2-ltl.go,
benchs/RERS/2016-Problem2-ltl.go.formulae.txt
benchs/RERS/2016-Problem4-ltl.go,
benchs/RERS/2016-Problem4-ltl.go.formulae.txt,
benchs/RERS/2016-Problem5-ltl.go,
benchs/RERS/2016-Problem5-ltl.go.formulae.txt,
benchs/RERS/2016-Problem7-ltl.go,
benchs/RERS/2016-Problem7-ltl.go.formulae.txt,
benchs/RERS/2017-Problem1-ltl.go,
benchs/RERS/2017-Problem1-ltl.go.formulae.txt,
benchs/RERS/2017-Problem2-ltl.go,
benchs/RERS/2017-Problem2-ltl.go.formulae.txt,
benchs/RERS/2017-Problem4-ltl.go,
benchs/RERS/2017-Problem4-ltl.go.formulae.txt,
benchs/RERS/2017-Problem5-ltl.go,
benchs/RERS/2017-Problem5-ltl.go.formulae.txt,
benchs/RERS/2017-Problem7-ltl.go,
benchs/RERS/2017-Problem7-ltl.go.formulae.txt,
benchs/RERS/2018-Problem1-ltl.go,
benchs/RERS/2018-Problem1-ltl.go.formulae.txt,
benchs/RERS/2018-Problem2-ltl.go,
benchs/RERS/2018-Problem2-ltl.go.formulae.txt,
benchs/RERS/2018-Problem4-ltl.go,
benchs/RERS/2018-Problem4-ltl.go.formulae.txt,
benchs/RERS/2018-Problem5-ltl.go,
benchs/RERS/2018-Problem5-ltl.go.formulae.txt,
benchs/RERS/2018-Problem7-ltl.go,
benchs/RERS/2018-Problem7-ltl.go.formulae.txt,
benchs/RERS/2019-Problem1-ltl.go,
benchs/RERS/2019-Problem1-ltl.go.formulae.txt,
benchs/RERS/2019-Problem2-ltl.go,
benchs/RERS/2019-Problem2-ltl.go.formulae.txt,
benchs/RERS/2019-Problem4-ltl.go,
benchs/RERS/2019-Problem4-ltl.go.formulae.txt,
benchs/RERS/2019-Problem5-ltl.go,
benchs/RERS/2019-Problem5-ltl.go.formulae.txt,
benchs/RERS/2019-Problem7-ltl.go,
benchs/RERS/2019-Problem7-ltl.go.formulae.txt,
benchs/RERS/2020-Problem1-ltl.go,
benchs/RERS/2020-Problem1-ltl.go.formulae.txt,
benchs/RERS/2020-Problem2-ltl.go,
benchs/RERS/2020-Problem2-ltl.go.formulae.txt,
benchs/RERS/2020-Problem4-ltl.go,
benchs/RERS/2020-Problem4-ltl.go.formulae.txt,
benchs/RERS/2020-Problem5-ltl.go,
benchs/RERS/2020-Problem5-ltl.go.formulae.txt,
benchs/RERS/2020-Problem7-ltl.go,
benchs/RERS/2020-Problem7-ltl.go.formulae.txt: Here.

a48adae0

benchs: automatic extraction from RERS · 6d7731d7
Etienne Renault authored Dec 18, 2020
```
* benchs/RERS/ltlrers2go.sh: Here.
```
6d7731d7

09 Dec, 2020 7 commits

benchs: include correctness specification · fb7266af
Etienne Renault authored Dec 09, 2020
```
* benchs/run-benchmark.sh: Here.
```
fb7266af

benchs: add specification files · 01d90331

Etienne Renault authored Dec 09, 2020

* benchs/RERS/2016-Problem10-reach.go.formulae.txt,
benchs/RERS/2016-Problem11-reach.go.formulae.txt,
benchs/RERS/2016-Problem12-reach.go.formulae.txt,
benchs/RERS/2016-Problem14-reach.go.formulae.txt,
benchs/RERS/2016-Problem15-reach.go.formulae.txt,
benchs/RERS/2017-Problem10-reach.go.formulae.txt,
benchs/RERS/2017-Problem11-reach.go.formulae.txt,
benchs/RERS/2017-Problem12-reach.go.formulae.txt,
benchs/RERS/2017-Problem14-reach.go.formulae.txt,
benchs/RERS/2017-Problem15-reach.go.formulae.txt: Here.

01d90331

benchs: script used to extract behviour from solutions · d91ef1cf
Etienne Renault authored Dec 09, 2020
```
* benchs/RERS/extract_rers_behaviors.sh: Here.
```
d91ef1cf
benchs: reset golang cache · 0353bde0
Etienne Renault authored Dec 09, 2020
```
* benchs/run-benchmark.sh: Here.
```
0353bde0
benchs: update benchmark filenames · 3e42010e
Etienne Renault authored Dec 09, 2020
```
* benchs/run-benchmark.sh: Here.
```
3e42010e

benchs: rename properly RERS to avoid confusion · ce43d7bb

Etienne Renault authored Dec 09, 2020

* benchs/RERS/2016-Problem10.go -> benchs/RERS/2016-Problem10-reach.go
* benchs/RERS/2016-Problem11.go -> benchs/RERS/2016-Problem11-reach.go
* benchs/RERS/2016-Problem12.go -> benchs/RERS/2016-Problem12-reach.go
* benchs/RERS/2016-Problem14.go -> benchs/RERS/2016-Problem14-reach.go
* benchs/RERS/2016-Problem15.go -> benchs/RERS/2016-Problem15-reach.go
* benchs/RERS/2017-Problem10.go -> benchs/RERS/2017-Problem10-reach.go
* benchs/RERS/2017-Problem11.go -> benchs/RERS/2017-Problem11-reach.go
* benchs/RERS/2017-Problem12.go -> benchs/RERS/2017-Problem12-reach.go
* benchs/RERS/2017-Problem14.go -> benchs/RERS/2017-Problem14-reach.go
* benchs/RERS/2017-Problem15.go -> benchs/RERS/2017-Problem15-reach.go
* benchs/RERS/2018-Problem10.go -> benchs/RERS/2018-Problem10-reach.go
* benchs/RERS/2018-Problem11.go -> benchs/RERS/2018-Problem11-reach.go
* benchs/RERS/2019-Problem11.go -> benchs/RERS/2019-Problem11-reach.go
* benchs/RERS/2019-Problem12.go -> benchs/RERS/2019-Problem12-reach.go
* benchs/RERS/2019-Problem14.go -> benchs/RERS/2019-Problem14-reach.go
* benchs/RERS/2019-Problem15.go -> benchs/RERS/2019-Problem15-reach.go

ce43d7bb

boilerplate: modelcheck return 1 in case of counterexample · 712d7763
Etienne Renault authored Dec 09, 2020
```
* boilerplate/main.go: Here.
```
712d7763

08 Dec, 2020 2 commits
- tests: remove useless make command · 7578f4f8
  Etienne Renault authored Dec 08, 2020
```
*  tests/run.sh: Here.
```
  7578f4f8
- output: ease user's life · 4096a93e
  Etienne Renault authored Dec 08, 2020
```
Typing "make -C output" is now obsolete

* boilerplate/main.go,
main.go: Here.
```
  4096a93e
20 Nov, 2020 2 commits
- recursion: make distinction between callexp and cast · 2d5a8045
  Etienne Renault authored Nov 20, 2020
```
* tools/recursion.go: Here.
```
  2d5a8045
- rewrite blackbox and recursion using reflection · bd269bd3
  Etienne Renault authored Nov 20, 2020
```
* main.go,
tools/blackbox.go,
tools/callgraph.go,
tools/extract_blackboxes/main.go,
tools/recursion.go: Here.
```
  bd269bd3
17 Nov, 2020 1 commit
- rewrite unroll recursion with reflection · 2bad8a3e
  Etienne Renault authored Nov 17, 2020
```
* tools/extract_blackboxes/main.go: Here.
```
  2bad8a3e
13 Jul, 2020 2 commits
- boilerplate: fix compability with Spot's dev version · b175b0a9
  Etienne Renault authored Jul 13, 2020
```
* boilerplate/main.go: Here.
```
  b175b0a9
- go2pins-mc: change default display · 0cad5bd5
  Etienne Renault authored Jul 13, 2020
```
* main.go: Here.
```
  0cad5bd5
28 Apr, 2020 4 commits
- Bump version 0.1b (aka Brubeck-Take5) · b9248987
  Etienne Renault authored Apr 28, 2020
```
* .last-cl-gen, ChangeLog, NEWS.txt, main.go: Here.
```
  b9248987
- go2pins: add Changelog generator · 72c35f5e
  Etienne Renault authored Apr 28, 2020
```
* Makefile, build-aux/gitlog-to-changelog : Here.
```
  72c35f5e
- bench: report time and memory · 06641dfe
  Etienne Renault authored Apr 28, 2020
```
* benchs/run-benchmark.sh: Here.
```
  06641dfe
- benchs: fix example for blackbox · 0eb9eb63
  Etienne Renault authored Apr 28, 2020
```
Commit 4536a3ae modifies (significantly) the size of the
state space. Consequently the current benchmark has been
adapted to run on a reasonnable computer.

* benchs/sqrt_prime_fibo.go: Here.
```
  0eb9eb63
27 Apr, 2020 9 commits
- beem: remove hanoi · a8b459a5
  Etienne Renault authored Apr 27, 2020
```
According to discusion #14.

* benchs/BEEM/hanoi.1.go: Here.
```
  a8b459a5
- boilerplate: do not force clang · 1e996e0c
  Etienne Renault authored Apr 27, 2020
```
* boilerplate/Makefile: Here.
```
  1e996e0c
- benchs: add BEEM inspired benchmark · 776ec909
  Etienne Renault authored Apr 27, 2020
```
* benchs/BEEM/adding.1.go,
benchs/BEEM/adding.2.go,
benchs/BEEM/adding.3.go,
benchs/BEEM/adding.4.go,
benchs/BEEM/hanoi.1.go: Here.
```
  776ec909
- debug: add transformation to ease debuging · 89dc1405
  Etienne Renault authored Apr 24, 2020
```
* main.go, transform/debug.go: Here.
```
  89dc1405
- visitor: fix typo · 911fd354
  Etienne Renault authored Apr 24, 2020
```
*  transform/visitor.go: Here.
```
  911fd354
- cfg: fix slice bounds of range error · b99fe8b9
  Etienne Renault authored Apr 24, 2020
```
* transform/cfg/build.go: Here.
```
  b99fe8b9
- desugararray: no special case for index 0 · c8c1c3f7
  Etienne Renault authored Apr 24, 2020
```
The previous code considered index 0 as a special case.
Thus the transformation wasn't go-compiliant after this
pass which was bad.

* transform/desugararray.go: Here.
```
  c8c1c3f7
- gitignore: ignore ltlrec · 9a3041b6
  Etienne Renault authored Apr 23, 2020
```
* .gitignore: Here.
```
  9a3041b6
- desugararray: rename pass · f678c54d
  Etienne Renault authored Apr 22, 2020
```
* Rename transform/arraytreatment.go
to transform/desugararray.go: Here.
```
  f678c54d