Skip to content
This repository has been archived by the owner on Feb 1, 2020. It is now read-only.

KLabelConstants not unique in KEQ #2409

Open
kheradmand opened this issue Apr 3, 2018 · 0 comments
Open

KLabelConstants not unique in KEQ #2409

kheradmand opened this issue Apr 3, 2018 · 0 comments

Comments

@kheradmand
Copy link
Contributor

kheradmand commented Apr 3, 2018

I am trying to use KEQ for establishing equivalence between two programs written in two languages:

module COMMON
syntax Vals ::= @nil 
...
endmodule

module L1
imports COMMON
...
endmodule

module L2
imports COMMON
...
endmodule

details here

I am not getting the result I expect. One problem is that the following equality does not hold:
@nil(.KList@BASIC-K) =? @nil(.KList@BASIC-K).
The reason is that the two @nils have different KLables (with different ordinal numbers but the same hash code).

image
image

I was wondering what the problem may be.

@daejunpark any ideas ?

Sign up for free to subscribe to this conversation on GitHub. Already have an account? Sign in.
Labels
None yet
Projects
None yet
Development

No branches or pull requests

1 participant