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

some expressions don't translate properly #24

Closed jonnybest closed 12 years ago

jonnybest commented 12 years ago

in the predicate

// complete hack to simulate behavior of code to set freeList
pred setFreeList[hs, hs_: HeapState] {
  // especially hackish
  hs_.freeList.*(hs_.left) in (Node - hs.marked)
  all n: Node |
    (n !in hs.marked) => {
      no hs_.right[n]
      hs_.left[n] in (hs_.freeList.*(hs_.left))
      n in hs_.freeList.*(hs_.left)
    } else {
      hs_.left[n] = hs.left[n]
      hs_.right[n] = hs.right[n]
    }
  hs_.marked = hs.marked
}

there are some formulas which produce invalid output. the output currently looks like this:

(assert
  (forall ((hs Rel1)(hs_ Rel1)) (= (setFreeList hs hs_) (and 
    (subset_1 (join_1x2 (join_1x2 hs_ freeList) (reflTransClos (join_1x3 hs_ left))) (diff_1 Node (join_1x2 hs marked)))
    (forall ((n Atom)) (=> (in_1 n Node) \if((not (in_1 n (join_1x2 hs marked)))) \then((and 
    (not (some_1 (join_1x2 (a2r_1 n) (join_1x3 hs_ right))))
    (subset_1 (join_1x2 (a2r_1 n) (join_1x3 hs_ left)) (join_1x2 (join_1x2 hs_ freeList) (reflTransClos (join_1x3 hs_ left))))
    (in_1 n (join_1x2 (join_1x2 hs_ freeList) (reflTransClos (join_1x3 hs_ left))))
  )) \else((and (= (join_1x2 (a2r_1 n) (join_1x3 hs_ left)) (join_1x2 (a2r_1 n) (join_1x3 hs left))) (= (join_1x2 (a2r_1 n) (join_1x3 hs_ right)) (join_1x2 (a2r_1 n) (join_1x3 hs right)))))))
    (= (join_1x2 hs_ marked) (join_1x2 hs marked))
  )))
)

The expected output is something without "\then" and "\if" and "\else".

jonnybest commented 12 years ago

this issue comes from a if-then-else expressions. ite-expressions are supported in SMT but not yet implemented in this project.

jonnybest commented 12 years ago

expected output

(assert
  (forall ((hs Rel1)(hs_ Rel1)) (= (setFreeList hs hs_) (and 
    (subset_1 (join_1x2 (join_1x2 hs_ freeList) (reflTransClos (join_1x3 hs_ left))) (diff_1 Node (join_1x2 hs marked)))
    (forall ((n Atom)) (=> (in_1 n Node) 
    (ite (not (in_1 n (join_1x2 hs marked)))
    (and 
        (not (some_1 (join_1x2 (a2r_1 n) (join_1x3 hs_ right))))
        (subset_1 (join_1x2 (a2r_1 n) (join_1x3 hs_ left)) (join_1x2 (join_1x2 hs_ freeList) (reflTransClos (join_1x3 hs_ left))))
        (in_1 n (join_1x2 (join_1x2 hs_ freeList) (reflTransClos (join_1x3 hs_ left))))
    )
    (and (= (join_1x2 (a2r_1 n) (join_1x3 hs_ left)) (join_1x2 (a2r_1 n) (join_1x3 hs left))) (= (join_1x2 (a2r_1 n) (join_1x3 hs_ right)) (join_1x2 (a2r_1 n) (join_1x3 hs right)))))))
    (= (join_1x2 hs_ marked) (join_1x2 hs marked))
  )))
)