diff --git a/pate_binja/pate.py b/pate_binja/pate.py index d43e35f8..011f91ce 100644 --- a/pate_binja/pate.py +++ b/pate_binja/pate.py @@ -384,17 +384,23 @@ def extract_graph_rec(self, eqCond = ConditionTrace(ccontent) match this: case 'Asserted': - #print('Found asserted cond for ', cfar_parent.id) + print('Found asserted cond for', cfar_parent.id) if cfar_parent.assertedConditionTrace: cfar_parent.assertedConditionTrace.update(ccontent) else: cfar_parent.assertedConditionTrace = ConditionTrace(ccontent) - case 'Equivalence Condition Assumed': - #print('Found assumed cond for ', cfar_parent.id) + case 'Assumed': + print('Found assumed cond for', cfar_parent.id) if cfar_parent.assumedConditionTrace: cfar_parent.assumedConditionTrace.update(ccontent) else: cfar_parent.assumedConditionTrace = ConditionTrace(ccontent) + case 'Equivalence Condition Assumed': + print('Found equivalance conditions for', cfar_parent.id) + if cfar_parent.equivalenceConditionTrace: + cfar_parent.equivalenceConditionTrace.update(ccontent) + else: + cfar_parent.equivalenceConditionTrace = ConditionTrace(ccontent) self.command('up') # Consume result of up, but do not need it @@ -896,6 +902,18 @@ def pprint_node_contents(self, pre: str = '', out: IO = sys.stdout, show_ce_trac elif self.exit_meta_data.get(n, {}).get('event_trace'): pprint_node_event_trace(self.exit_meta_data[n]['event_trace'], 'Witness Trace', pre + ' ', out) + # Indicate if there are conditions traces + conditionTraceTypes = [] + if self.equivalenceConditionTrace: + conditionTraceTypes.append('equivalence') + if self.assertedConditionTrace: + conditionTraceTypes.append('asserted') + if self.assumedConditionTrace: + conditionTraceTypes.append('assumed') + if conditionTraceTypes: + out.write('Condition traces for: ') + out.write(', '.join(conditionTraceTypes)) + def pprint_node_domain(self, pre: str = '', out: IO = sys.stdout, show_ce_trace: bool = False): if self.predomain: diff --git a/pate_binja/view.py b/pate_binja/view.py index bef338d2..7aa76400 100644 --- a/pate_binja/view.py +++ b/pate_binja/view.py @@ -218,13 +218,15 @@ def ask_user(self, prompt: str, choices: list[str], replay_choice: Optional[str] execute_on_main_thread_and_wait(lambda: self.pate_widget.ask_user(prompt, choices, replay_choice is not None)) if replay_choice: execute_on_main_thread_and_wait(lambda: self.pate_widget.cmd_field.setText(replay_choice + ' (replay)')) - #Wait for user to respond to prompt. This happens on the GUI thread. + + # Wait for user to respond which happens on the GUI thread. urc = self.pate_widget.user_response_condition with urc: while self.pate_widget.user_response is None: urc.wait() choice = self.pate_widget.user_response self.pate_widget.user_response = None + if replay_choice: choice = replay_choice execute_on_main_thread_and_wait(lambda: self.pate_widget.output_field.appendPlainText(f'PATE Command: {replay_choice} (replay)\n'))