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 versionhttps://github.com/utwente-fmt/ltsmin/files/4181129/sokoban.tar.gz of the Sokoban examplehttps://github.com/utwente-fmt/ltsmin-tacas2015/tree/master/sokoban, where a positive answer is obtained for both 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-mucalchttps://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 attachedhttps://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 GitHubhttps://github.com/utwente-fmt/ltsmin/issues/184?email_source=notifications&email_token=ABTGAZNU4GTK43RLGZWGDQTRCFMCFA5CNFSM4KSOQXWKYY3PNVWWK3TUL52HS4DFUVEXG43VMWVGG33NNVSW45C7NFSM4IMIHLDA, or unsubscribehttps://github.com/notifications/unsubscribe-auth/ABTGAZLPEV2SK6H7VP46BTTRCFMCFANCNFSM4KSOQXWA.