From 27cfc9d280243c3e463e9ab295f253704f3b6c9b Mon Sep 17 00:00:00 2001 From: Petar Maksimovic Date: Mon, 28 Aug 2023 09:16:33 +0200 Subject: [PATCH 1/3] fixing incorrect removal of terminal nodes --- src/pyk/kcfg/exploration.py | 5 +++-- 1 file changed, 3 insertions(+), 2 deletions(-) diff --git a/src/pyk/kcfg/exploration.py b/src/pyk/kcfg/exploration.py index f86f9405f..c10ce46aa 100644 --- a/src/pyk/kcfg/exploration.py +++ b/src/pyk/kcfg/exploration.py @@ -54,8 +54,8 @@ def add_terminal(self, node_id: NodeIdLike) -> None: self._terminal.add(self.kcfg._resolve(node_id)) # Unmarking a given node as terminal - def remove_terminal(self, node_id: NodeIdLike) -> None: - self._terminal.discard(self.kcfg._resolve(node_id)) + def remove_terminal(self, node_id: int) -> None: + self._terminal.discard(node_id) # # Lifted KCFG functions that may affect terminal nodes @@ -63,6 +63,7 @@ def remove_terminal(self, node_id: NodeIdLike) -> None: # Removing a given node def remove_node(self, node_id: NodeIdLike) -> None: + node_id = self.kcfg._resolve(node_id) self.kcfg.remove_node(node_id) self.remove_terminal(node_id) From 1927d14135289e011f483c3e414e4c4f391e552c Mon Sep 17 00:00:00 2001 From: devops Date: Mon, 28 Aug 2023 07:18:24 +0000 Subject: [PATCH 2/3] Set Version: 0.1.430 --- package/version | 2 +- pyproject.toml | 2 +- 2 files changed, 2 insertions(+), 2 deletions(-) diff --git a/package/version b/package/version index ae6c98f07..74ef6681c 100644 --- a/package/version +++ b/package/version @@ -1 +1 @@ -0.1.429 +0.1.430 diff --git a/pyproject.toml b/pyproject.toml index a583cf03a..f33ea1870 100644 --- a/pyproject.toml +++ b/pyproject.toml @@ -4,7 +4,7 @@ build-backend = "poetry.core.masonry.api" [tool.poetry] name = "pyk" -version = "0.1.429" +version = "0.1.430" description = "" authors = [ "Runtime Verification, Inc. ", From 664bdb2308ebe9be92634d3cf40ae0844d41d9ea Mon Sep 17 00:00:00 2001 From: Petar Maksimovic Date: Mon, 28 Aug 2023 09:38:09 +0200 Subject: [PATCH 3/3] not removing init or target, removing infinite loop --- src/pyk/proof/reachability.py | 10 +++++++--- 1 file changed, 7 insertions(+), 3 deletions(-) diff --git a/src/pyk/proof/reachability.py b/src/pyk/proof/reachability.py index ddbedb03d..3a20026a5 100644 --- a/src/pyk/proof/reachability.py +++ b/src/pyk/proof/reachability.py @@ -122,6 +122,10 @@ def shortest_path_to(self, node_id: NodeIdLike) -> tuple[KCFG.Successor, ...]: assert spb is not None return spb + def prune(self, node_id: NodeIdLike, keep_nodes: Iterable[NodeIdLike] = ()) -> list[int]: + pruned_nodes = super().prune(node_id, keep_nodes=list(keep_nodes) + [self.init, self.target]) + return pruned_nodes + @staticmethod def read_proof(id: str, proof_dir: Path) -> APRProof: proof_path = proof_dir / f'{hash_str(id)}.json' @@ -427,7 +431,7 @@ def is_failing(self, node_id: NodeIdLike) -> bool: return super().is_failing(node_id) and not self.is_bounded(node_id) def prune(self, node_id: NodeIdLike, keep_nodes: Iterable[NodeIdLike] = ()) -> list[int]: - pruned_nodes = self.prune(node_id, keep_nodes=keep_nodes) + pruned_nodes = super().prune(node_id, keep_nodes=keep_nodes) for nid in pruned_nodes: self.remove_bounded(nid) return pruned_nodes @@ -495,8 +499,8 @@ def from_claim_with_bmc_depth( def add_bounded(self, nid: NodeIdLike) -> None: self._bounded.add(self.kcfg._resolve(nid)) - def remove_bounded(self, node_id: NodeIdLike) -> None: - self._bounded.discard(self.kcfg._resolve(node_id)) + def remove_bounded(self, node_id: int) -> None: + self._bounded.discard(node_id) @property def summary(self) -> CompositeSummary: