search

jrclogic / SMCDEL

A symbolic model checker for Dynamic Epistemic Logic.
https://w4eg.de/malvin/illc/smcdelweb
GNU General Public License v2.0
39 stars 9 forks source link

do not simplify simStep (Dk _ Bot) #41

Closed m4lvin closed 3 months ago

m4lvin commented 4 months ago

Similar to https://github.com/jrclogic/SMCDEL/issues/39 this simplification is wrong because it is not a valid equivalence in K.

https://github.com/jrclogic/SMCDEL/blob/b71711d6aea1cae5fe10c96a0862016d3a3c1528/src/SMCDEL/Language.hs#L547

ToDo:

m4lvin commented 3 months ago

Fixed in https://github.com/jrclogic/SMCDEL/commit/f6ecaf08154a36b6c79744c52b0dac4b45b3cb6e