Wrong answer when model checking mucalc with pins2lts-sym

[ningit]

Model checking --mucalc properties with pins2lts-sym sometimes returns wrong answers. As a witness, I attach a modified version of the Sokoban example, where a positive answer is obtained for both <a> p and [a] ¬ p.

$ pins2lts-sym sokoboard.so --mucalc '< "push_left" > { s0 = 1 }' --pg-solve
pins2lts-sym: The result is: true.
$ pins2lts-sym sokoboard.so --mucalc '[ "push_left" ] ! { s0 = 1 }' --pg-solve
pins2lts-sym: The result is: true.

These two results are logically inconsistent. In fact, [push_left] ¬ { s0 = 1 } must not be satisfied according to the specification, and the right answer is obtained using pins2lts-seq and pbespgsolve as described in the ltsmin-mucalc manpage. This behavior is observed both using the 3.0.2 release and building LTSmin from the repository source. Full executions are attached.

Debugging, it can be seen that negated propositions are not checked in the right state. In this case, the subformula ! { s0 = 0 } is not checked in the successor by the push_left action but in the initial state.

[jacopol]

Hi Ningit, Yes, this looks wrong indeed. We will look into this, in order to repair the bug. Kind regards, Jaco van de Pol

…

-- Jaco van de Pol, Prof. of Computer Science Aarhus University + University of Twente From: ningit <notifications@github.com> Sent: Monday, February 10, 2020 2:55 PM To: utwente-fmt/ltsmin <ltsmin@noreply.github.com> Cc: Subscribed <subscribed@noreply.github.com> Subject: [utwente-fmt/ltsmin] Wrong answer when model checking mucalc with pins2lts-sym (#184) Model checking --mucalc properties with pins2lts-sym sometimes returns wrong answers. As a witness, I attach a modified version<https://github.com/utwente-fmt/ltsmin/files/4181129/sokoban.tar.gz> of the Sokoban example<https://github.com/utwente-fmt/ltsmin-tacas2015/tree/master/sokoban>, where a positive answer is obtained for both <a> p and [a] ¬ p. $ pins2lts-sym sokoboard.so --mucalc '< "push_left" > { s0 = 1 }' --pg-solve pins2lts-sym: The result is: true. $ pins2lts-sym sokoboard.so --mucalc '[ "push_left" ] ! { s0 = 1 }' --pg-solve pins2lts-sym: The result is: true. These two results are logically inconsistent. In fact, [push_left] ¬ { s0 = 1 } must not be satisfied according to the specification, and the right answer is obtained using pins2lts-seq and pbespgsolve as described in the ltsmin-mucalc<https://ltsmin.utwente.nl/assets/man/ltsmin-mucalc.html> manpage. This behavior is observed both using the 3.0.2 release and building LTSmin from the repository source. Full executions are attached<https://github.com/utwente-fmt/ltsmin/files/4181137/executions-output.txt>. Debugging, it can be seen that negated propositions are not checked in the right state. In this case, the subformula ! { s0 = 0 } is not checked in the successor by the push_left action but in the initial state. — You are receiving this because you are subscribed to this thread. Reply to this email directly, view it on GitHub<#184?email_source=notifications&email_token=ABTGAZNU4GTK43RLGZWGDQTRCFMCFA5CNFSM4KSOQXWKYY3PNVWWK3TUL52HS4DFUVEXG43VMWVGG33NNVSW45C7NFSM4IMIHLDA>, or unsubscribe<https://github.com/notifications/unsubscribe-auth/ABTGAZLPEV2SK6H7VP46BTTRCFMCFANCNFSM4KSOQXWA>.