search

Pathemeous / Symbolic-Gossip

Symbolic Model Checker for the Gossip Problem
GNU General Public License v2.0
2 stars 0 forks source link

Fix/transparent #9

Closed Pathemeous closed 5 months ago

Pathemeous commented 5 months ago

Fixes two bugs in the Transparent Transformer:

  1. calling has for the own secret (such a proposition does not exist)
  2. the pre-checks of the transformer update failed. In particular, the event law ($\Theta^+$) failed due to the lack of an event proposition while the law required it. The transformer should most likely only add the single proposition relating to the call that it is transforming.