Investigate workstation_resupply_2.tlsf

[gaperez64]

This is the first time I find a benchmark we cannot solve with the default settings. Perhaps the value of k is too low?

[michaelcadilhac]

That's correct; a value of K=12 works, but K=11 is too small. This is realizable.

Compare:

$ ./src/acacia-bonsai -c REAL -F ../tests/ltl/syntcomp24/workstation_resupply_2.ltl --ins occupied_1,occupied_0 --outs alive,resupply,pick_up_part,outside_station_1,outside_station_0,outside_stockroom,station_1,station_0,stockroom -v -K 11 --Kmin 11
[real] Formula: !(!(GF!Xoccupied_0 & GF!Xoccupied_1) | (alive & !(G(!alive | ((stockroom -> (!outside_station_0 & !outside_station_1 & !outside_stockroom & !station_0 & !station_1)) & (station_0 -> (!outside_station_0 & !outside_station_1 & !outside_stockroom & !station_1 & !stockroom)) & (station_1 -> (!outside_station_0 & !outside_station_1 & !outside_stockroom & !station_0 & !stockroom)) & (outside_stockroom -> (!outside_station_0 & !outside_station_1 & !station_0 & !station_1 & !stockroom)) & (outside_station_0 -> (!outside_station_1 & !outside_stockroom & !station_0 & !station_1 & !stockroom)) & (outside_station_1 -> (!outside_station_0 & !outside_stockroom & !station_0 & !station_1 & !stockroom)))) -> (G(!alive | ((!X(alive & occupied_0) & X(alive & station_0)) -> !X(alive & X(alive & occupied_0)))) & G(!alive | ((!X(alive & occupied_1) & X(alive & station_1)) -> !X(alive & X(alive & occupied_1)))))) & (alive U G!alive)) | (alive & G(!alive | ((stockroom -> (!outside_station_0 & !outside_station_1 & !outside_stockroom & !station_0 & !station_1)) & (station_0 -> (!outside_station_0 & !outside_station_1 & !outside_stockroom & !station_1 & !stockroom)) & (station_1 -> (!outside_station_0 & !outside_station_1 & !outside_stockroom & !station_0 & !stockroom)) & (outside_stockroom -> (!outside_station_0 & !outside_station_1 & !station_0 & !station_1 & !stockroom)) & (outside_station_0 -> (!outside_station_1 & !outside_stockroom & !station_0 & !station_1 & !stockroom)) & (outside_station_1 -> (!outside_station_0 & !outside_stockroom & !station_0 & !station_1 & !stockroom)))) & (alive U G!alive) & F(alive & resupply & station_0) & F(alive & resupply & station_1) & G(!alive | ((stockroom -> (X(!alive | stockroom) | X(!alive | outside_stockroom))) & (station_0 -> (X(!alive | station_0) | X(!alive | outside_station_0))) & (station_1 -> (X(!alive | station_1) | X(!alive | outside_station_1))) & (outside_stockroom -> (X(!alive | stockroom) | X(!alive | outside_stockroom) | X(!alive | outside_station_0) | X(!alive | outside_station_1))) & (outside_station_0 -> (X(!alive | outside_stockroom) | X(!alive | station_0) | X(!alive | outside_station_0) | X(!alive | outside_station_1))) & (outside_station_1 -> (X(!alive | outside_stockroom) | X(!alive | outside_station_0) | X(!alive | station_1) | X(!alive | outside_station_1))))) & G(!alive | ((X(alive & occupied_0) -> !station_0) & (X(alive & occupied_1) -> !station_1))) & G(!alive | (pick_up_part -> stockroom)) & G(!alive | (resupply -> (station_0 | station_1))) & (((!alive | !resupply) U pick_up_part) | G(!alive | !resupply)) & G(!alive | (resupply -> X(alive & (((!alive | !resupply) U pick_up_part) | G(!alive | !resupply)))))))
[real] Translating formula done in 0.0208626 seconds
[real] Automaton has 84 states and 1 colors
[real] Preprocessing done in 6.2382e-05 seconds
[real] DPA has 84 states
[real] Bounded states: 38 / 84 = 45%
[real] Computation of boolean states in 0.00069422seconds , found 46 nonboolean states.
[real] Bitset threshold set at 48
[real] Safety game created in 0.000723906 seconds
[real] Time disregarding Spot translation: 0.00078872 seconds
[real] Not fully solved -> extra solve
[real] Bitset threshold set at 48
[real] IOS Precomputer with invariant 1...
[real] Make actions...
[real] Fetching IO actions
[real] INPUT: !occupied_0 & !occupied_1 #ACTIONS: 93
[real] INPUT: !occupied_0 & occupied_1 #ACTIONS: 83
[real] INPUT: occupied_0 & occupied_1 #ACTIONS: 77
[real] INPUT: occupied_0 & !occupied_1 #ACTIONS: 83
[real] INPUT GAIN: 4/4 = 100%
[real] IO GAIN: 336/2048 = 16%
[real] Loop# 1, F of size 1
[real] Loop# 2, F of size 2
[real] Loop# 3, F of size 3
[real] Loop# 4, F of size 4
[real] Loop# 5, F of size 5
[real] Loop# 6, F of size 6
[real] Loop# 7, F of size 7
[real] Loop# 8, F of size 8
[real] Loop# 9, F of size 9
[real] Loop# 10, F of size 10
[real] Loop# 11, F of size 11
[real] Loop# 12, F of size 23
[real] Loop# 13, F of size 43
[real] Loop# 14, F of size 205
[real] Loop# 15, F of size 272
[real] Loop# 16, F of size 185
[real] Loop# 17, F of size 418
[real] Loop# 18, F of size 303
[real] Loop# 19, F of size 286
[real] Loop# 20, F of size 346
[real] Loop# 21, F of size 465
[real] Loop# 22, F of size 333
[real] Loop# 23, F of size 495
[real] Loop# 24, F of size 382
[real] Loop# 25, F of size 255
[real] Loop# 26, F of size 406
[real] Loop# 27, F of size 345
[real] Loop# 28, F of size 280
[real] Loop# 29, F of size 349
[real] Loop# 30, F of size 312
[real] Loop# 31, F of size 401
[real] Loop# 32, F of size 301
[real] Loop# 33, F of size 237
[real] Loop# 34, F of size 264
[real] Loop# 35, F of size 262
[real] Safety game solved in 18.8245 seconds
[real] returning 3
UNKNOWN

and

$ ./src/acacia-bonsai -c REAL -F ../tests/ltl/syntcomp24/workstation_resupply_2.ltl --ins occupied_1,occupied_0 --outs alive,resupply,pick_up_part,outside_station_1,outside_station_0,outside_stockroom,station_1,station_0,stockroom -v -K 12 --Kmin 12                                                           
[real] Formula: !(!(GF!Xoccupied_0 & GF!Xoccupied_1) | (alive & !(G(!alive | ((stockroom -> (!outside_station_0 & !outside_station_1 & !outside_stockroom & !station_0 & !station_1)) & (station_0 -> (!outside_station_0 & !outside_station_1 & !outside_stockroom & !station_1 & !stockroom)) & (station_1 -> (!outside_station_0 & !outside_station_1 & !outside_stockroom & !station_0 & !stockroom)) & (outside_stockroom -> (!outside_station_0 & !outside_station_1 & !station_0 & !station_1 & !stockroom)) & (outside_station_0 -> (!outside_station_1 & !outside_stockroom & !station_0 & !station_1 & !stockroom)) & (outside_station_1 -> (!outside_station_0 & !outside_stockroom & !station_0 & !station_1 & !stockroom)))) -> (G(!alive | ((!X(alive & occupied_0) & X(alive & station_0)) -> !X(alive & X(alive & occupied_0)))) & G(!alive | ((!X(alive & occupied_1) & X(alive & station_1)) -> !X(alive & X(alive & occupied_1)))))) & (alive U G!alive)) | (alive & G(!alive | ((stockroom -> (!outside_station_0 & !outside_station_1 & !outside_stockroom & !station_0 & !station_1)) & (station_0 -> (!outside_station_0 & !outside_station_1 & !outside_stockroom & !station_1 & !stockroom)) & (station_1 -> (!outside_station_0 & !outside_station_1 & !outside_stockroom & !station_0 & !stockroom)) & (outside_stockroom -> (!outside_station_0 & !outside_station_1 & !station_0 & !station_1 & !stockroom)) & (outside_station_0 -> (!outside_station_1 & !outside_stockroom & !station_0 & !station_1 & !stockroom)) & (outside_station_1 -> (!outside_station_0 & !outside_stockroom & !station_0 & !station_1 & !stockroom)))) & (alive U G!alive) & F(alive & resupply & station_0) & F(alive & resupply & station_1) & G(!alive | ((stockroom -> (X(!alive | stockroom) | X(!alive | outside_stockroom))) & (station_0 -> (X(!alive | station_0) | X(!alive | outside_station_0))) & (station_1 -> (X(!alive | station_1) | X(!alive | outside_station_1))) & (outside_stockroom -> (X(!alive | stockroom) | X(!alive | outside_stockroom) | X(!alive | outside_station_0) | X(!alive | outside_station_1))) & (outside_station_0 -> (X(!alive | outside_stockroom) | X(!alive | station_0) | X(!alive | outside_station_0) | X(!alive | outside_station_1))) & (outside_station_1 -> (X(!alive | outside_stockroom) | X(!alive | outside_station_0) | X(!alive | station_1) | X(!alive | outside_station_1))))) & G(!alive | ((X(alive & occupied_0) -> !station_0) & (X(alive & occupied_1) -> !station_1))) & G(!alive | (pick_up_part -> stockroom)) & G(!alive | (resupply -> (station_0 | station_1))) & (((!alive | !resupply) U pick_up_part) | G(!alive | !resupply)) & G(!alive | (resupply -> X(alive & (((!alive | !resupply) U pick_up_part) | G(!alive | !resupply)))))))
[real] Translating formula done in 0.0208839 seconds
[real] Automaton has 84 states and 1 colors
[real] Preprocessing done in 6.3919e-05 seconds
[real] DPA has 84 states
[real] Bounded states: 38 / 84 = 45%
[real] Computation of boolean states in 0.000766755seconds , found 46 nonboolean states.
[real] Bitset threshold set at 48
[real] Safety game created in 0.000796763 seconds
[real] Time disregarding Spot translation: 0.000862931 seconds
[real] Not fully solved -> extra solve
[real] Bitset threshold set at 48
[real] IOS Precomputer with invariant 1...
[real] Make actions...
[real] Fetching IO actions
[real] INPUT: !occupied_0 & !occupied_1 #ACTIONS: 93
[real] INPUT: !occupied_0 & occupied_1 #ACTIONS: 83
[real] INPUT: occupied_0 & occupied_1 #ACTIONS: 77
[real] INPUT: occupied_0 & !occupied_1 #ACTIONS: 83
[real] INPUT GAIN: 4/4 = 100%
[real] IO GAIN: 336/2048 = 16%
[real] Loop# 1, F of size 1
[real] Loop# 2, F of size 2
[real] Loop# 3, F of size 3
[real] Loop# 4, F of size 4
[real] Loop# 5, F of size 5
[real] Loop# 6, F of size 6
[real] Loop# 7, F of size 7
[real] Loop# 8, F of size 8
[real] Loop# 9, F of size 9
[real] Loop# 10, F of size 10
[real] Loop# 11, F of size 11
[real] Loop# 12, F of size 12
[real] Loop# 13, F of size 24
[real] Loop# 14, F of size 44
[real] Loop# 15, F of size 59
[real] Loop# 16, F of size 263
[real] Loop# 17, F of size 152
[real] Loop# 18, F of size 167
[real] Loop# 19, F of size 238
[real] Loop# 20, F of size 156
[real] Loop# 21, F of size 174
[real] Loop# 22, F of size 164
[real] Loop# 23, F of size 208
[real] Loop# 24, F of size 375
[real] Loop# 25, F of size 811
[real] Loop# 26, F of size 320
[real] Loop# 27, F of size 332
[real] Loop# 28, F of size 317
[real] Loop# 29, F of size 286
[real] Loop# 30, F of size 270
[real] Loop# 31, F of size 231
[real] Loop# 32, F of size 222
[real] Loop# 33, F of size 222
[real] Loop# 34, F of size 222
[real] Loop# 35, F of size 223
[real] Safety game solved in 16.9112 seconds
[real] returning 0
REALIZABLE

I'm inclined to close the issue.

[gaperez64]

Yes, now that it is confirmed we should probably just increase the default K to 12.