Constant variable substitution, loop unroll pass + dpor code cleanup #202
Conversation
# Conflicts: # subprojects/xcfa/xcfa-cli/src/main/java/hu/bme/mit/theta/xcfa/cli/XcfaCli.kt
# Conflicts: # subprojects/xcfa/xcfa-analysis/src/main/java/hu/bme/mit/theta/xcfa/analysis/por/XcfaDporLts.kt
There was a problem hiding this comment.
Why was this change necessary? How come this used to be so complicated, and now an ID equivalence is enough?
There was a problem hiding this comment.
Well, I have no idea why this was so complicated beforehand. I can see no reason for the ID equivalence check being an incorrect way of determining the equivalence of ArgNodes as long as IDs are unique (if we compare ArgNodes from different ARGs, it may be wrong; though I do not see such a use case). On the other hand, the former complicated way resulted in a depth-first ARG search from the given ArgNode (cf. line 284 in the old version comparing outEdges and line 33 comparing the targets of ArgEdges).
(We had a conversation about this issue on the 15th of June; also with @AdamZsofi).
There was a problem hiding this comment.
Based on git blame, you are the author of the original equivalence check, so you may have the reasons for implementing equivalence check this way.
e9defab (fixed link)
There was a problem hiding this comment.
I see, I've made these changes in e9defab. The reason for them was that even if you fully re-build an ARG from a model a second time, due to mismatched IDs, the two ARG's comparison would fail. I think that with this simplified version, the problem would reappear, and we'd have some problems with ARG comparisons, e.g., in the progress check of @AdamZsofi. Of course we can mitigate it some other way, I don't think it's acceptable that a DFS search should run at every ArgNode comparison.
There was a problem hiding this comment.
Let's move this topic to our next in-person meeting. I think we will need to come up with a solution that neither breaks existing functionality nor does it place such a burden on performance.
There was a problem hiding this comment.
(also, @AdamZsofi: some tests would be nice, so that similar changes are reflected in the CT pipeline's success!)
There was a problem hiding this comment.
I omit this change from this PR but I have created the issue #203 about ArgNode comparison.
|
Also, feel free to merge the PR without waiting for all the tests - this PR does not target master, so we can merge it and fix it in #198. |
The somewhat messy code used for the TSE article is cleaned up and contributed in this pull request.