Wrong result on TSLMT benchmark robot-tasks.tslmt

[raynadimitrova]

Hello,

Congratulations on the acceptance of your paper at CAV 2026!

When looking at results.csv in your artifact, we noticed that the "unrealizable" result by Issy (in the table given as issy3-tsl) for the benchmark robot-tasks.tslmt is incorrectly marked as "wrong".

According to the semantics of TSL, the specification in robot-tasks.tslmt is indeed unrealizable. To see this, consider an initial state where x=1 and y=1, along with some inputs that satisfy the assumption. In this case, the guarantee requires that all of the updates [x <- i_x] , [x <- sub x i1()] , [y <- i_y] , [y <- y] must be true simultaneously. This is not possible, since [x <- i_x] and [x <- sub x i1()] cannot both be satisfied at the same time (the same holds for the updates to y too). The reason for this is that the terms i_x and sub x i1() are syntactically different. As defined by the semantics of TSL, updates are checked syntactically (see page 617 in https://link.springer.com/content/pdf/10.1007/978-3-030-25540-4_35.pdf). This means that for initial state <x=1,y=1> and some inputs that satisfy the assumption, the guarantee cannot be satisfied, and hence the specification is unrealizable.

In conclusion, the "unrealizable" result reported by Issy is in fact correct, while the "realizable" result reported by sweap (as sweap-tsl in the table) is wrong. We kindly ask that any report of this in your paper be corrected in the final version.

Best regards,
Rayna

[lou1306]

Dear Rayna,
Thank you! And thank you for pointing out the issue.

It appears that Sweap and Issy were evaluating two variants of this benchmarks. Sweap's problem is under the benchmarks/raboniel directory and Issy's problem is in benchmarks/tslmt2rpg. This was supposed to be simply due to slightly different syntax accepted by the tool, but at some point the benchmarks diverged. (The "Raboniel" features a few X operators missing from the other version. This might affect realisability).

We are going to investigate further, and we will make sure to correct the final version accordingly.

Best,
Luca

[raynadimitrova]

Dear Luca,

Thanks for the quick response and for looking into and addressing the issue.

Best regards,
Rayna

[lou1306]

Dear Rayna,
We fixed the benchmark in the sweap repository (commit e3b611c). Now the benchmark is realisable (as was supposed to be when we introduced it, in CAV'25) and Issy correctly recognises it as such.

We also added support for "tslmt2rpg/Issy-flavoured" TSLMT syntax (commit c35e5cf), which hopefully should prevent these kinds of mistakes from happening in the future.

We updated this repository to reflect those changes, by changing the Dockerfile and the archive with the results that will appear in the final version. We will shortly revise the Zenodo entry as well.