[Stepper] Add Enhanced Table View with Matrix Display for Subformula Satisfaction #102
There are no files selected for viewing
This file contains hidden or bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
This file contains hidden or bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
| Original file line number | Diff line number | Diff line change |
|---|---|---|
|
|
@@ -71,6 +71,13 @@ def formattedTraceAssignment(self): | |
| asStr = asStr.replace('!', '¬') | ||
| return asStr | ||
|
|
||
| def getAllSubformulae(self): | ||
| """Extract all subformulae from this node and its children recursively.""" | ||
| result = [(self.formula, self.satisfied)] | ||
| for child in self.children: | ||
| result.extend(child.getAllSubformulae()) | ||
| return result | ||
|
|
||
| def __formula_to__mermaid_inner__(self): | ||
| edges = [] | ||
| if self.satisfied: | ||
|
|
@@ -173,6 +180,43 @@ def to_dict(self): | |
| "prefix_states": self.prefix_states, | ||
| "cycle_states": self.cycle_states | ||
| } | ||
|
|
||
| def getMatrixView(self): | ||
| """Generate matrix view data for table display.""" | ||
| all_states = self.prefix_states + self.cycle_states | ||
|
|
||
| if not all_states: | ||
| return {"subformulae": [], "matrix": [], "rows": []} | ||
|
|
||
| # Collect all unique subformulae across all states | ||
| all_subformulae_set = set() | ||
| for state in all_states: | ||
| subformulae = state.getAllSubformulae() | ||
| for formula, _ in subformulae: | ||
| all_subformulae_set.add(formula) | ||
|
|
||
| # Sort subformulae for consistent ordering (simple ones first, complex ones last) | ||
| all_subformulae = sorted(list(all_subformulae_set), key=lambda x: (len(x), x)) | ||
|
|
||
| # Build matrix: rows are subformulae, columns are time steps | ||
| matrix = [] | ||
| rows = [] # Combined data for easier template iteration | ||
| for subformula in all_subformulae: | ||
|
There was a problem hiding this comment. I dont think this is being correctly populated with 0s and 1s There was a problem hiding this comment. Fixed in commit c473ef9. The issue was that the Matrix View template was dependent on |
||
| row = [] | ||
| for state in all_states: | ||
| # Find this subformula in the current state | ||
| subformulae = state.getAllSubformulae() | ||
| subformula_dict = {f: s for f, s in subformulae} | ||
| satisfaction = subformula_dict.get(subformula, False) | ||
| row.append(1 if satisfaction else 0) | ||
| matrix.append(row) | ||
| rows.append({"subformula": subformula, "values": row}) | ||
|
|
||
| return { | ||
| "subformulae": all_subformulae, | ||
| "matrix": matrix, | ||
| "rows": rows | ||
| } | ||
|
|
||
| def __repr__(self): | ||
| return f"TraceSatisfactionResult(prefix_states={self.prefix_states}, cycle_states={self.cycle_states})" | ||
|
|
||
This file contains hidden or bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
| Original file line number | Diff line number | Diff line change |
|---|---|---|
|
|
@@ -68,14 +68,25 @@ | |
| display: inline-block; | ||
| } | ||
|
|
||
| .unsatformula { | ||
|
|
||
| border: 2px solid #dc3545; | ||
| /* red solid border */ | ||
| border-radius: 6px; | ||
| padding: 4px 8px; | ||
|
|
||
| display: inline-block; | ||
| } | ||
|
|
||
| /* Matrix view text colors */ | ||
| .matrix-satisfied { | ||
| color: #28a745 !important; | ||
| font-weight: bold; | ||
| } | ||
|
|
||
| .matrix-unsatisfied { | ||
| color: #dc3545 !important; | ||
| font-weight: bold; | ||
| } | ||
| </style> | ||
|
|
||
|
|
@@ -131,18 +142,24 @@ <h5 class="modal-title" id="exampleModalLabel">Load Stepper with a new LTL Formu | |
| </div> | ||
|
|
||
|
|
||
| <ul class="nav nav-tabs mb-3 mt-4" id="stepperTabs" role="tablist"> | ||
| <li class="nav-item"> | ||
| <a class="nav-link active" id="stepper-tab" data-toggle="tab" href="#stepper-view" role="tab">Stepper | ||
| View</a> | ||
| </li> | ||
| <li class="nav-item"> | ||
| <a class="nav-link" id="matrix-tab" data-toggle="tab" href="#matrix-view" role="tab">Matrix View<sup>Beta</sup></a> | ||
| </li> | ||
| <li class="nav-item"> | ||
| <a class="nav-link" id="table-tab" data-toggle="tab" href="#table-view" role="tab">Table View<sup>Beta</sup></a> | ||
| </li> | ||
| </ul> | ||
|
|
||
| <div class="tab-content"> | ||
| <!-- ================================ --> | ||
| <!-- STEPPER VIEW - Interactive stepping through formula satisfaction --> | ||
| <!-- ================================ --> | ||
| <div class="tab-pane fade show active" id="stepper-view" role="tabpanel"> | ||
| <!-- Stepper view lets you see the entire trace at once, and each tree state one by one. --> | ||
|
|
||
| <div id="statecontainer"> | ||
|
|
@@ -180,59 +197,127 @@ <h4><span class="help float-right"> By clicking the <code>Previous State</code> | |
| </div> | ||
| </div> | ||
| {% endfor %} | ||
| </div> | ||
| </div> | ||
| <!-- ================================ --> | ||
| <!-- MATRIX VIEW - Binary matrix display of subformula satisfaction over time --> | ||
|
||
| <!-- ================================ --> | ||
| <div class="tab-pane fade" id="matrix-view" role="tabpanel"> | ||
| <p> | ||
|
||
| This matrix view shows how each subformula's satisfaction evolves over time. | ||
| Each row represents a subformula, and each column represents a time step. | ||
| Values are shown as <strong class="matrix-satisfied">1</strong> (satisfied) or <strong class="matrix-unsatisfied">0</strong> (unsatisfied). | ||
| </p> | ||
|
|
||
| {% if matrix_data.subformulae %} | ||
| <!-- Matrix view table --> | ||
| <table class="table table-bordered table-sm" id="matrixTable"> | ||
| <thead> | ||
| <tr> | ||
| <th class="w-auto">Subformula</th> | ||
| {% for i in range(prefixstates|length) %} | ||
| <th class="text-center">{{ i }}</th> | ||
| {% endfor %} | ||
| {% if cyclestates %} | ||
| <th class="text-center cycle-state-col" colspan="{{ cyclestates|length }}">Cycle</th> | ||
| {% endif %} | ||
| </tr> | ||
| {% if cyclestates %} | ||
| <tr> | ||
| <th class="w-auto"></th> | ||
| {% for i in range(prefixstates|length) %} | ||
| <th class="text-center">{{ i }}</th> | ||
| {% endfor %} | ||
| {% for i in range(cyclestates|length) %} | ||
| <th class="text-center cycle-state-col">{{ prefixstates|length + i }}</th> | ||
| {% endfor %} | ||
| </tr> | ||
| {% endif %} | ||
| </thead> | ||
| <tbody> | ||
| {% for row_data in matrix_data.rows %} | ||
| <tr> | ||
| <td class="font-monospace"><code>{{ row_data.subformula }}</code></td> | ||
| {% for i in range(prefixstates|length) %} | ||
| <td class="text-center"> | ||
| <span class="{% if row_data.values[i] == 1 %}matrix-satisfied{% else %}matrix-unsatisfied{% endif %}">{{ row_data.values[i] }}</span> | ||
| </td> | ||
| {% endfor %} | ||
| {% if cyclestates %} | ||
| {% for i in range(cyclestates|length) %} | ||
| <td class="text-center cycle-state-col"> | ||
| <span class="{% if row_data.values[prefixstates|length + i] == 1 %}matrix-satisfied{% else %}matrix-unsatisfied{% endif %}">{{ row_data.values[prefixstates|length + i] }}</span> | ||
| </td> | ||
| {% endfor %} | ||
| {% endif %} | ||
| </tr> | ||
| {% endfor %} | ||
| </tbody> | ||
| </table> | ||
| {% else %} | ||
| <div class="alert alert-info"> | ||
| <p><strong>No formula loaded.</strong></p> | ||
| <p>Please enter an LTL formula and trace to see the matrix view.</p> | ||
| </div> | ||
| {% endif %} | ||
| </div> | ||
| <!-- ================================ --> | ||
| <!-- TABLE VIEW - Detailed formula view with satisfaction highlighting --> | ||
| <!-- ================================ --> | ||
| <div class="tab-pane fade" id="table-view" role="tabpanel"> | ||
| {% if matrix_data.subformulae %} | ||
| <p> | ||
| Sub-formulae are demarcated by their bounding boxes, which | ||
| indicate whether they are <span class="satformula">satisfied</span> or | ||
| <span class="unsatformula">unsatisfied</span>. | ||
| </p> | ||
| <!-- Detailed table view --> | ||
| <table class="table table-bordered" id="stateTable"> | ||
| <thead> | ||
| <tr> | ||
| <th class="w-auto"></th> | ||
| {% for ps in prefixstates %} | ||
| <th></th> | ||
| {% endfor %} | ||
| {% if cyclestates %} | ||
| <th class="cycle-state-col" colspan="{{ cyclestates|length }}">Cycle</th> | ||
| {% endif %} | ||
| </tr> | ||
| </thead> | ||
| <tbody> | ||
| <tr> | ||
| <th class="w-auto">Trace State</th> | ||
| {% for ps in prefixstates %} | ||
| <td><pre>{{ ps.formattedTraceAssignment }}</pre></td> | ||
| {% endfor %} | ||
| {% for ps in cyclestates %} | ||
| <td class="cycle-state-col"><pre>{{ ps.formattedTraceAssignment }}</pre></td> | ||
| {% endfor %} | ||
| </tr> | ||
| <tr> | ||
| <th class="w-auto"> | ||
| Formula | ||
| </span> | ||
| </th> | ||
| {% for ps in prefixstates %} | ||
| <td> | ||
| {{ ps.formulaAsHTML | safe }} | ||
| </td> | ||
| {% endfor %} | ||
| {% for ps in cyclestates %} | ||
| <td class="cycle-state-col"> | ||
| {{ ps.formulaAsHTML | safe }} | ||
| </td> | ||
| {% endfor %} | ||
| </tr> | ||
| </tbody> | ||
| </table> | ||
| {% else %} | ||
| <div class="alert alert-info"> | ||
| <p><strong>No formula loaded.</strong></p> | ||
| <p>Please enter an LTL formula and trace to see the table view.</p> | ||
| </div> | ||
| {% endif %} | ||
| </div> | ||
| </div> | ||
| </div> | ||
|
|
||
Add this suggestion to a batch that can be applied as a single commit.
This suggestion is invalid because no changes were made to the code.
Suggestions cannot be applied while the pull request is closed.
Suggestions cannot be applied while viewing a subset of changes.
Only one suggestion per line can be applied in a batch.
Add this suggestion to a batch that can be applied as a single commit.
Applying suggestions on deleted lines is not supported.
You must change the existing code in this line in order to create a valid suggestion.
Outdated suggestions cannot be applied.
This suggestion has been applied or marked resolved.
Suggestions cannot be applied from pending reviews.
Suggestions cannot be applied on multi-line comments.
Suggestions cannot be applied while the pull request is queued to merge.
Suggestion cannot be applied right now. Please check back later.
There was a problem hiding this comment.
Choose a reason for hiding this comment
The reason will be displayed to describe this comment to others. Learn more.
The 0s and 1s are not visible in the matrix view. We should also make the cycle obvious with a header like we do in the Table view.
Don't worry about highlighting cells red or green, make the actual TEXT color for 0 or 1 these colors.
There was a problem hiding this comment.
Choose a reason for hiding this comment
The reason will be displayed to describe this comment to others. Learn more.
Fixed the Matrix View visibility issues:
See commit 07bc78f and screenshot: https://github.com/user-attachments/assets/a160c974-96b5-4c40-b534-761b8d5b746d