diff --git a/results/011encoding+SetAddDel-apalache-0.18.2-SNAPSHOT.csv b/results/011encoding+SetAddDel-apalache-0.18.2-SNAPSHOT.csv new file mode 100644 index 0000000..da49ea5 --- /dev/null +++ b/results/011encoding+SetAddDel-apalache-0.18.2-SNAPSHOT.csv @@ -0,0 +1,17 @@ +01:no,02:tool,03:status,04:time_sec,05:depth,05:mem_kb,10:ninit_trans,11:ninit_trans,12:ncells,13:nclauses,14:navg_clause_len +1,apalache,NoError,3,0,189296,0,0,4,3,4 +2,apalache,NoError,3,0,185536,0,0,31,37,10 +3,apalache,NoError,3,0,191256,0,0,73,98,13 +4,apalache,NoError,4,0,198616,0,0,123,179,14 +5,apalache,NoError,9,0,198804,0,0,181,280,15 +6,apalache,NoError,80,0,205948,0,0,247,401,16 +7,apalache,NoError,643,0,241908,0,0,321,542,17 +8,apalache,NoError,6557,0,424544,0,0,403,703,18 +9,apalache,NoError,4,0,185872,0,0,5,5,5 +10,apalache,NoError,4,0,187944,0,0,51,61,12 +11,apalache,NoError,4,0,198916,0,0,139,172,17 +12,apalache,NoError,5,0,201580,0,0,259,327,22 +13,apalache,NoError,6,0,226988,0,0,411,526,27 +14,apalache,NoError,159,0,246840,0,0,595,769,32 +15,apalache,Timeout,7200,0,3760,0,0,730,962,36 +16,apalache,Timeout,7200,0,3464,0,0,776,1035,38 diff --git a/results/011encoding+SetAddDel-apalache-mem-log.svg b/results/011encoding+SetAddDel-apalache-mem-log.svg new file mode 100644 index 0000000..5b46d5f --- /dev/null +++ b/results/011encoding+SetAddDel-apalache-mem-log.svg @@ -0,0 +1,1388 @@ + + + + + + + + 2021-12-13T12:56:08.381787 + image/svg+xml + + + Matplotlib v3.5.0, https://matplotlib.org/ + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + diff --git a/results/011encoding+SetAddDel-apalache-mem.svg b/results/011encoding+SetAddDel-apalache-mem.svg new file mode 100644 index 0000000..a99edb5 --- /dev/null +++ b/results/011encoding+SetAddDel-apalache-mem.svg @@ -0,0 +1,1286 @@ + + + + + + + + 2021-12-13T12:56:09.764611 + image/svg+xml + + + Matplotlib v3.5.0, https://matplotlib.org/ + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + diff --git a/results/011encoding+SetAddDel-apalache-ncells.svg b/results/011encoding+SetAddDel-apalache-ncells.svg new file mode 100644 index 0000000..abfa22e --- /dev/null +++ b/results/011encoding+SetAddDel-apalache-ncells.svg @@ -0,0 +1,1406 @@ + + + + + + + + 2021-12-13T12:56:10.898491 + image/svg+xml + + + Matplotlib v3.5.0, https://matplotlib.org/ + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + diff --git a/results/011encoding+SetAddDel-apalache-nclauses.svg b/results/011encoding+SetAddDel-apalache-nclauses.svg new file mode 100644 index 0000000..70a8338 --- /dev/null +++ b/results/011encoding+SetAddDel-apalache-nclauses.svg @@ -0,0 +1,1290 @@ + + + + + + + + 2021-12-13T12:56:12.050359 + image/svg+xml + + + Matplotlib v3.5.0, https://matplotlib.org/ + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + diff --git a/results/011encoding+SetAddDel-apalache-time-log.svg b/results/011encoding+SetAddDel-apalache-time-log.svg new file mode 100644 index 0000000..756a76b --- /dev/null +++ b/results/011encoding+SetAddDel-apalache-time-log.svg @@ -0,0 +1,1455 @@ + + + + + + + + 2021-12-13T12:56:05.775311 + image/svg+xml + + + Matplotlib v3.5.0, https://matplotlib.org/ + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + diff --git a/results/011encoding+SetAddDel-apalache-time.svg b/results/011encoding+SetAddDel-apalache-time.svg new file mode 100644 index 0000000..19c9733 --- /dev/null +++ b/results/011encoding+SetAddDel-apalache-time.svg @@ -0,0 +1,1347 @@ + + + + + + + + 2021-12-13T12:56:07.239768 + image/svg+xml + + + Matplotlib v3.5.0, https://matplotlib.org/ + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + diff --git a/results/011encoding+SetAddDel-report.md b/results/011encoding+SetAddDel-report.md new file mode 100644 index 0000000..6810897 --- /dev/null +++ b/results/011encoding+SetAddDel-report.md @@ -0,0 +1,70 @@ +# Results of 011encoding+SetAddDel-apalache + + +## 1. Awesome plots + +### 1.1. Time (logarithmic scale) + +![time-log](011encoding+SetAddDel-apalache-time-log.svg "Time Log") + +### 1.2. Time (linear) + +![time-log](011encoding+SetAddDel-apalache-time.svg "Time Log") + +### 1.3. Memory (logarithmic scale) + +![mem-log](011encoding+SetAddDel-apalache-mem-log.svg "Memory Log") + +### 1.4. Memory (linear) + +![mem](011encoding+SetAddDel-apalache-mem.svg "Memory Log") + +### 1.5. Number of arena cells (linear) + +![ncells](011encoding+SetAddDel-apalache-ncells.svg "Number of arena cells") + +### 1.6. Number of SMT clauses (linear) + +![nclauses](011encoding+SetAddDel-apalache-nclauses.svg "Number of SMT clauses") + +## 2. Input parameters + +no | filename | tool | timeout | init | inv | next | args +----|--------------------------------|------------|-----------|--------|-------|--------|----------------------------------------------------- +1 | array-encoding/SetAddDel.tla | apalache | 2h | Init | Inv | Next | --smt-encoding=arrays --length=0 --cinit=CInit0 +2 | array-encoding/SetAddDel.tla | apalache | 2h | Init | Inv | Next | --smt-encoding=arrays --length=2 --cinit=CInit2 +3 | array-encoding/SetAddDel.tla | apalache | 2h | Init | Inv | Next | --smt-encoding=arrays --length=4 --cinit=CInit4 +4 | array-encoding/SetAddDel.tla | apalache | 2h | Init | Inv | Next | --smt-encoding=arrays --length=6 --cinit=CInit6 +5 | array-encoding/SetAddDel.tla | apalache | 2h | Init | Inv | Next | --smt-encoding=arrays --length=8 --cinit=CInit8 +6 | array-encoding/SetAddDel.tla | apalache | 2h | Init | Inv | Next | --smt-encoding=arrays --length=10 --cinit=CInit10 +7 | array-encoding/SetAddDel.tla | apalache | 2h | Init | Inv | Next | --smt-encoding=arrays --length=12 --cinit=CInit12 +8 | array-encoding/SetAddDel.tla | apalache | 2h | Init | Inv | Next | --smt-encoding=arrays --length=14 --cinit=CInit14 +9 | array-encoding/SetAddDel.tla | apalache | 2h | Init | Inv | Next | --smt-encoding=oopsla19 --length=0 --cinit=CInit0 +10 | array-encoding/SetAddDel.tla | apalache | 2h | Init | Inv | Next | --smt-encoding=oopsla19 --length=2 --cinit=CInit2 +11 | array-encoding/SetAddDel.tla | apalache | 2h | Init | Inv | Next | --smt-encoding=oopsla19 --length=4 --cinit=CInit4 +12 | array-encoding/SetAddDel.tla | apalache | 2h | Init | Inv | Next | --smt-encoding=oopsla19 --length=6 --cinit=CInit6 +13 | array-encoding/SetAddDel.tla | apalache | 2h | Init | Inv | Next | --smt-encoding=oopsla19 --length=8 --cinit=CInit8 +14 | array-encoding/SetAddDel.tla | apalache | 2h | Init | Inv | Next | --smt-encoding=oopsla19 --length=10 --cinit=CInit10 +15 | array-encoding/SetAddDel.tla | apalache | 2h | Init | Inv | Next | --smt-encoding=oopsla19 --length=12 --cinit=CInit12 +16 | array-encoding/SetAddDel.tla | apalache | 2h | Init | Inv | Next | --smt-encoding=oopsla19 --length=14 --cinit=CInit14 + +## 3. Detailed results: 011encoding+SetAddDel-apalache-0.18.2-SNAPSHOT.csv + +01:no | 02:tool | 03:status | 04:time_sec | 05:depth | 05:mem_kb | 10:ninit_trans | 11:ninit_trans | 12:ncells | 13:nclauses | 14:navg_clause_len +-------|------------|-------------|---------------|------------|-------------|------------------|------------------|-------------|---------------|-------------------- +1 | apalache | NoError | 3s | 0 | 184MB | 0 | 0 | 4.0 | 3.0 | 4.0 +2 | apalache | NoError | 3s | 0 | 181MB | 0 | 0 | 31 | 37 | 10 +3 | apalache | NoError | 3s | 0 | 186MB | 0 | 0 | 73 | 98 | 13 +4 | apalache | NoError | 4s | 0 | 193MB | 0 | 0 | 123 | 179 | 14 +5 | apalache | NoError | 9s | 0 | 194MB | 0 | 0 | 181 | 280 | 15 +6 | apalache | NoError | 1m01s | 0 | 201MB | 0 | 0 | 247 | 401 | 16 +7 | apalache | NoError | 10m | 0 | 236MB | 0 | 0 | 321 | 542 | 17 +8 | apalache | NoError | 1h01m | 0 | 414MB | 0 | 0 | 403 | 703 | 18 +9 | apalache | NoError | 4s | 0 | 181MB | 0 | 0 | 5.0 | 5.0 | 5.0 +10 | apalache | NoError | 4s | 0 | 183MB | 0 | 0 | 51 | 61 | 12 +11 | apalache | NoError | 4s | 0 | 194MB | 0 | 0 | 139 | 172 | 17 +12 | apalache | NoError | 5s | 0 | 196MB | 0 | 0 | 259 | 327 | 22 +13 | apalache | NoError | 6s | 0 | 221MB | 0 | 0 | 411 | 526 | 27 +14 | apalache | NoError | 2m02s | 0 | 241MB | 0 | 0 | 595 | 769 | 32 +15 | apalache | Timeout | 2h02m | 0 | 3.0MB | 0 | 0 | 730 | 962 | 36 +16 | apalache | Timeout | 2h02m | 0 | 3.0MB | 0 | 0 | 776 | 1.0K | 38