Skip to content
New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

Refactor edge structure for merging node #4600

Closed
wants to merge 3 commits into from

Conversation

Stevengre
Copy link
Contributor

Merging nodes will combine several edges into one. To ensure no loss of information, we need to make sure that a single edge can store multiple pieces of data. However, modifying the Edge structure has wide-ranging implications. Even though I’ve added rule and depth as properties to minimize this impact, it still has broad effects.

@Stevengre Stevengre self-assigned this Aug 21, 2024
@Stevengre Stevengre marked this pull request as draft August 21, 2024 04:09
@Stevengre
Copy link
Contributor Author

This is the primary change.

k/pyk/src/pyk/kcfg/kcfg.py

Lines 205 to 207 in 0b3669f

depths: tuple[int, ...]
rules_list: tuple[tuple[str, ...], ...]
csubsts: tuple[CSubst, ...]

I’ve tried to update all the affected methods, but I’m unsure what changes should be made to the following: KCFGShow and KCFGViewer.

k/pyk/src/pyk/kcfg/show.py

Lines 132 to 136 in 0b3669f

def _print_edge(edge: KCFG.Edge) -> list[str]:
if edge.depth == 1:
return ['(' + str(edge.depth) + ' step)']
else:
return ['(' + str(edge.depth) + ' steps)']

elif type(self._element) is KCFG.Edge:

elif type(self._element) is KCFG.Edge:

Additionally, will this update affect KaaS?

@Stevengre Stevengre marked this pull request as ready for review August 21, 2024 06:14
Comment on lines 202 to +207
class Edge(EdgeLike):
source: KCFG.Node
target: KCFG.Node
depth: int
rules: tuple[str, ...]
depths: tuple[int, ...]
rules_list: tuple[tuple[str, ...], ...]
csubsts: tuple[CSubst, ...]
Copy link
Contributor

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

I'm not sure we can manage a breaking change of this scale across our stack at this point.

Is there a reasonable way to merge edges with loss of information? (E.g. take the the maximum depth, etc.)

Copy link
Contributor Author

@Stevengre Stevengre Aug 21, 2024

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

I’ve added two properties to mitigate this issue, ensuring that previous access to depth and rule continues to work as expected.

k/pyk/src/pyk/kcfg/kcfg.py

Lines 209 to 215 in 0b3669f

@property
def depth(self) -> int:
return max(self.depths)
@property
def rules(self) -> tuple[str, ...]:
return single(self.rules_list)

What they should return can be further evaluated.

Copy link
Contributor

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

to_dict and from_dict still changes though, and as implemented, proofs written before the change will no longer be usable with this version.

We could still

  1. Update the old format on the first read, or
  2. Support both formats

but we should really think about if adding this complexity is worth it right now.

Copy link
Contributor

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

If losing information is not an option for your use case, you could still add a new class MergedEdge(EdgeLike) that contains a tuple[Edge, ...].

Copy link
Contributor Author

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

Thank you for your suggestion! I think introducing a new class is a good idea. It won’t disrupt the existing proofs and will preserve the information that would otherwise be lost. However, we’ll still need to modify KCFGShow and KCFGViewer to adapt to this change, but the adjustments required will be much smaller.

Copy link
Contributor Author

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

Moreover, we need to change the as_rule and as_rules to make this new Edge class work correctly for the CSE.

Copy link
Contributor Author

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

If that implementation is better, I will close this PR and work that then. What do you think?

Copy link
Member

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

I like the MergeEdge idea!

@Stevengre Stevengre closed this Aug 22, 2024
rv-jenkins pushed a commit that referenced this pull request Aug 27, 2024
Here is the alternative implementation for [this
PR](#4600).

- commit 1: introduce the new class `MergedEdge`
- commit 2: add `to_rule` function to `MergedEdge` for CSE
- commit 3: add corresponding functions like `Edge` for `MergedEdge`
- commit 4: modify `Edge.to_rule` related functions for CSE
- commit 5: modify KCFGShow for MergedEdge
- commit 6: modify KCFGViewer for MergedEdge
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment
Labels
None yet
Projects
None yet
Development

Successfully merging this pull request may close these issues.

3 participants