From c47859db0d4d759ff34ea4252cb31184ac7536ca Mon Sep 17 00:00:00 2001 From: Noah Watson Date: Tue, 6 Aug 2024 11:15:12 -0500 Subject: [PATCH 1/2] Add # of refuted nodes to status bar display --- pyk/src/pyk/proof/reachability.py | 3 ++- 1 file changed, 2 insertions(+), 1 deletion(-) diff --git a/pyk/src/pyk/proof/reachability.py b/pyk/src/pyk/proof/reachability.py index 53b1b26e586..42c49187b59 100644 --- a/pyk/src/pyk/proof/reachability.py +++ b/pyk/src/pyk/proof/reachability.py @@ -512,9 +512,10 @@ def one_line_summary(self) -> str: terminal = len(self.terminal) stuck = len(self.kcfg.stuck) passed = len([cover for cover in self.kcfg.covers() if cover.target.id == self.target]) + refuted = len(self.node_refutations) return ( super().one_line_summary - + f'|{nodes} nodes|{pending} pending|{passed} passed|{failing} failing|{branches} branches|{vacuous} vacuous|{terminal} terminal|{stuck} stuck' + + f'|{nodes} nodes|{pending} pending|{passed} passed|{failing} failing|{branches} branches|{vacuous} vacuous|{terminal} terminal|{stuck} stuck|{refuted} refuted' ) def get_refutation_id(self, node_id: int) -> str: From 6df6cbc213ffd4649c92571cc52e54f7d9abc1a3 Mon Sep 17 00:00:00 2001 From: Noah Watson Date: Tue, 6 Aug 2024 16:42:20 -0500 Subject: [PATCH 2/2] Group information, give more meaningful definition of branches --- pyk/src/pyk/proof/reachability.py | 6 ++++-- 1 file changed, 4 insertions(+), 2 deletions(-) diff --git a/pyk/src/pyk/proof/reachability.py b/pyk/src/pyk/proof/reachability.py index 42c49187b59..fab28f6cc60 100644 --- a/pyk/src/pyk/proof/reachability.py +++ b/pyk/src/pyk/proof/reachability.py @@ -507,7 +507,9 @@ def one_line_summary(self) -> str: nodes = len(self.kcfg.nodes) pending = len(self.pending) failing = len(self.failing) - branches = len(self.kcfg.ndbranches()) + len(self.kcfg.splits()) + branches = 0 + for branch in self.kcfg.ndbranches() + self.kcfg.splits(): + branches += len(branch.targets) vacuous = len(self.kcfg.vacuous) terminal = len(self.terminal) stuck = len(self.kcfg.stuck) @@ -515,7 +517,7 @@ def one_line_summary(self) -> str: refuted = len(self.node_refutations) return ( super().one_line_summary - + f'|{nodes} nodes|{pending} pending|{passed} passed|{failing} failing|{branches} branches|{vacuous} vacuous|{terminal} terminal|{stuck} stuck|{refuted} refuted' + + f' --- {nodes} nodes|{branches} branches|{terminal} terminal --- {pending} pending|{passed} passed|{failing} failing|{vacuous} vacuous|{refuted} refuted|{stuck} stuck' ) def get_refutation_id(self, node_id: int) -> str: