search

jonnybest / Alloy2RelSMT

This is Alloy2RelSMT, a converter. It translates Alloy models into SMT files with a specific relational theory.
1 stars 0 forks source link

making TCL workable and restoring fileSystem #31

Closed jonnybest closed 11 years ago

jonnybest commented 11 years ago

Since the introduction of the "corrected" TCL lemma, the fileSystem benchmark is broken. See it here:

http://rise4fun.com/Z3/2U2

jonnybest commented 11 years ago

I traced this issue back to the line FSO = Root.*entries in filesystem. The reflexive transitive closure is currently translated with the call to translateExpr_p(ue.sub.closure().plus(ExprConstant.IDEN), letBindings, atomVars) ref. While this may be the correct implementation, it is not compatible with the lemmas that we use now.

This is probably not a bug. There are two possible solutions to work around this fault:

  1. reimplement transitive closure as a function and install the "original transitive closure lemma"
  2. find and implement a new lemma which links the functions union_2, transClos and IDEN.
jonnybest commented 11 years ago

fixed in 509130bf7fed9f70ba02e8fa0f803f52f67bcd7a