Skip to content

Commit

Permalink
More readable and informative status bar (#4636)
Browse files Browse the repository at this point in the history
This PR adjusts the proof info shown in the status bar. In particular,
it:
- removes the `branches` info, since this number refers to all of the
internal branchings of the proof, it differs from the number of leaves,
and it is not clear how it is useful to the end-user;
- removes the `terminal` info, since this can be computed from the other
information; it could also be confusing to end-users as to why there are
always two terminal nodes to begin with (final node of `setUp` and
`target`);
- reduces horizontal space so that there is a greater chance that full
status does not overflow and more info can be seen when test name is
large.
  • Loading branch information
PetarMax authored Sep 11, 2024
1 parent b6e638d commit b74cee0
Showing 1 changed file with 1 addition and 5 deletions.
6 changes: 1 addition & 5 deletions pyk/src/pyk/proof/reachability.py
Original file line number Diff line number Diff line change
Expand Up @@ -551,17 +551,13 @@ def one_line_summary(self) -> str:
nodes = len(self.kcfg.nodes)
pending = len(self.pending)
failing = len(self.failing)
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)
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|{branches} branches|{terminal} terminal --- {pending} pending|{passed} passed|{failing} failing|{vacuous} vacuous|{refuted} refuted|{stuck} stuck'
+ f': {nodes} nodes: {pending} pending|{passed} passed|{failing} failing|{vacuous} vacuous|{refuted} refuted|{stuck} stuck'
)

def get_refutation_id(self, node_id: int) -> str:
Expand Down

0 comments on commit b74cee0

Please sign in to comment.