Skip to content

Commit 7c8fa96

Browse files
authored
Merge pull request #12 from goblint/fix_json_configs
Fix td3.json and td4 json config files
2 parents d8ba560 + 78806c1 commit 7c8fa96

File tree

7 files changed

+34
-36
lines changed

7 files changed

+34
-36
lines changed

index/conf/td3.json

Lines changed: 11 additions & 12 deletions
Original file line numberDiff line numberDiff line change
@@ -17,18 +17,17 @@
1717
"dbg": {
1818
"debug": false
1919
},
20-
"exp": {
21-
"solver": {
22-
"td3": {
23-
"restart": {
24-
"wpoint": {
25-
"enabled": false,
26-
"once": true
27-
}
28-
},
29-
"abort": false,
30-
"abort-verify": false
31-
}
20+
"solver": "td3",
21+
"solvers": {
22+
"td3": {
23+
"restart": {
24+
"wpoint": {
25+
"enabled": false,
26+
"once": true
27+
}
28+
},
29+
"abort": false,
30+
"abort-verify": false
3231
}
3332
},
3433
"incremental": {

index/conf/td4.json

Lines changed: 11 additions & 12 deletions
Original file line numberDiff line numberDiff line change
@@ -17,18 +17,17 @@
1717
"dbg": {
1818
"debug": false
1919
},
20-
"exp": {
21-
"solver": {
22-
"td3": {
23-
"restart": {
24-
"wpoint": {
25-
"enabled": true,
26-
"once": false
27-
}
28-
},
29-
"abort": false,
30-
"abort-verify": false
31-
}
20+
"solver": "td3",
21+
"solvers": {
22+
"td3": {
23+
"restart": {
24+
"wpoint": {
25+
"enabled": true,
26+
"once": false
27+
}
28+
},
29+
"abort": false,
30+
"abort-verify": false
3231
}
3332
},
3433
"incremental": {

index/defs/performance.yaml

Lines changed: 2 additions & 2 deletions
Original file line numberDiff line numberDiff line change
@@ -5,5 +5,5 @@ incremental: true
55
FromScratch:
66
Restart: --enable incremental.restart.sided.enabled
77
Reluctant: --enable incremental.restart.sided.enabled --enable incremental.reluctant.on
8-
Abort: --enable incremental.restart.sided.enabled --enable exp.solver.td3.abort
9-
Both: --enable incremental.restart.sided.enabled --enable incremental.reluctant.on --enable exp.solver.td3.abort
8+
Abort: --enable incremental.restart.sided.enabled --enable solvers.td3.abort
9+
Both: --enable incremental.restart.sided.enabled --enable incremental.reluctant.on --enable solvers.td3.abort

index/defs/precision.yaml

Lines changed: 2 additions & 2 deletions
Original file line numberDiff line numberDiff line change
@@ -5,5 +5,5 @@ incremental: true
55
FromScratch:
66
Incremental:
77
RestartGlob: --enable incremental.restart.sided.enabled
8-
RestartLocs: --enable exp.solver.td3.restart.wpoint.enabled
9-
RestartBoth: --enable exp.solver.td3.restart.wpoint.enabled --enable incremental.restart.sided.enabled
8+
RestartLocs: --enable solvers.td3.restart.wpoint.enabled
9+
RestartBoth: --enable solvers.td3.restart.wpoint.enabled --enable incremental.restart.sided.enabled

index/defs/restarting.yaml

Lines changed: 2 additions & 2 deletions
Original file line numberDiff line numberDiff line change
@@ -3,7 +3,7 @@ compare: true
33
incremental: true
44

55
FromScratch:
6-
Incremental: --disable exp.solver.td3.restart.wpoint.enabled
7-
RestartGlob: --disable exp.solver.td3.restart.wpoint.enabled --enable incremental.restart.sided.enabled
6+
Incremental: --disable solvers.td3.restart.wpoint.enabled
7+
RestartGlob: --disable solvers.td3.restart.wpoint.enabled --enable incremental.restart.sided.enabled
88
RestartLocs:
99
RestartBoth: --enable incremental.restart.sided.enabled

index/defs/td3and4.yaml

Lines changed: 5 additions & 5 deletions
Original file line numberDiff line numberDiff line change
@@ -3,8 +3,8 @@ compare: true
33
incremental: false
44

55
TD3:
6-
TD3-Abort: --enable exp.solver.td3.abort
7-
TD3-Verify: --enable exp.solver.td3.abort --enable exp.solver.td3.abort-verify
8-
TD4: --enable exp.solver.td3.restart.wpoint.enabled --disable exp.solver.td3.restart.wpoint.once
9-
TD4-Abort: --enable exp.solver.td3.restart.wpoint.enabled --disable exp.solver.td3.restart.wpoint.once --enable exp.solver.td3.abort
10-
TD4-Verify: --enable exp.solver.td3.restart.wpoint.enabled --disable exp.solver.td3.restart.wpoint.once --enable exp.solver.td3.abort --enable exp.solver.td3.abort-verify
6+
TD3-Abort: --enable solvers.td3.abort
7+
TD3-Verify: --enable solvers.td3.abort --enable solvers.td3.abort-verify
8+
TD4: --enable solvers.td3.restart.wpoint.enabled --disable solvers.td3.restart.wpoint.once
9+
TD4-Abort: --enable solvers.td3.restart.wpoint.enabled --disable solvers.td3.restart.wpoint.once --enable solvers.td3.abort
10+
TD4-Verify: --enable solvers.td3.restart.wpoint.enabled --disable solvers.td3.restart.wpoint.once --enable solvers.td3.abort --enable solvers.td3.abort-verify

update_bench_incremental.rb

Lines changed: 1 addition & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -156,7 +156,7 @@ def print_res (i)
156156

157157
if ARGV[2].nil?
158158
puts 'You must run command with timout, conf, and at least one benchmark set, e.g.:'
159-
puts './update_bench_incremental.rb 60 index/defs/interactive.yaml index/sets/posix.yaml'
159+
puts './update_bench_incremental.rb 60 index/defs/incremental.yaml index/sets/posix.yaml'
160160
exit 1
161161
end
162162

0 commit comments

Comments
 (0)