Skip to content

[Stepper] Add Enhanced Table View with Matrix Display for Subformula Satisfaction #102

New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

Sign up for GitHub

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

Merged
merged 11 commits into from
Jul 26, 2025
Merged

[Stepper] Add Enhanced Table View with Matrix Display for Subformula Satisfaction #102

Show file tree
Hide file tree
Changes from 5 commits
Commits
Show all changes
11 commits
Select commit Hold shift + click to select a range
9bcc776
Initial plan
Copilot Jul 24, 2025
a619dc2
Implement enhanced table view with matrix display for stepper
Copilot Jul 24, 2025
b5dbc3f
Fix template data structure and enhance matrix view functionality
Copilot Jul 24, 2025
c04dc33
Complete enhanced table view implementation with working matrix display
Copilot Jul 24, 2025
940bac2
Address PR feedback: remove unnecessary files, restore original spotu…
Copilot Jul 24, 2025
07bc78f
Separate Matrix and Table views into distinct tabs with improved visi…
Copilot Jul 26, 2025
9047c52
Fix tab ordering and add debugging for matrix view 0/1 display issue
Copilot Jul 26, 2025
c473ef9
Fix Matrix View 0/1 display issue by making it independent of prefixs…
Copilot Jul 26, 2025
d82b29e
Fix TypeError in Matrix View template by using dictionary access syntax
Copilot Jul 26, 2025
4f87e64
Fix Matrix View TypeError by adding defensive checks for row data str…
Copilot Jul 26, 2025
429715c
Add cycle indication to Matrix View with dual-header layout and cycle…
Copilot Jul 26, 2025
File filter

Filter by extension

Filter by extension
Conversations
Failed to load comments.
Loading
Jump to
Jump to file
Failed to load files.
Loading
Diff view
Diff view
26 changes: 14 additions & 12 deletions src/app.py
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -426,25 +426,27 @@ def ltlstepper():
if syntax_choice == None or syntax_choice not in SUPPORTED_SYNTAXES:
syntax_choice = 'Classic'

if request.method == 'GET':
return render_template('stepper.html', uid = getUserName(), error="", prefixstates=[], cyclestates=[])
if request.method == 'GET':
return render_template('stepper.html', uid = getUserName(), error="", prefixstates=[], cyclestates=[], matrix_data={"subformulae": [], "matrix": [], "rows": []})

if request.method == 'POST':
ltl = request.form.get('formula')
trace = request.form.get('trace')
if ltl == "" or trace == "":
error="Please enter an LTL formula and a trace."

try:
node = parse_ltl_string(ltl)
except:
return render_template('stepper.html', uid = getUserName(), error="Invalid LTL formula " + ltl, prefixstates=[], cyclestates=[])

try:
result = traceSatisfactionPerStep(node = node, trace = trace, syntax = syntax_choice)
except:
return render_template('stepper.html', uid = getUserName(), error="Invalid trace " + trace, prefixstates=[], cyclestates=[])
return render_template('stepper.html', uid = getUserName(), error="", prefixstates=result.prefix_states, cyclestates=result.cycle_states, formula = ltl, trace=trace)
try:
node = parse_ltl_string(ltl)
except:
return render_template('stepper.html', uid = getUserName(), error="Invalid LTL formula " + ltl, prefixstates=[], cyclestates=[], matrix_data={"subformulae": [], "matrix": [], "rows": []})

try:
result = traceSatisfactionPerStep(node = node, trace = trace, syntax = syntax_choice)
except:
return render_template('stepper.html', uid = getUserName(), error="Invalid trace " + trace, prefixstates=[], cyclestates=[], matrix_data={"subformulae": [], "matrix": [], "rows": []})

matrix_data = result.getMatrixView()
return render_template('stepper.html', uid = getUserName(), error="", prefixstates=result.prefix_states, cyclestates=result.cycle_states, formula = ltl, trace=trace, matrix_data=matrix_data)


##### Eng LTL Logging Routes ###
Expand Down
44 changes: 44 additions & 0 deletions src/stepper.py
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -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:
Expand Down Expand Up @@ -173,6 +180,43 @@ def to_dict(self):
"prefix_states": self.prefix_states,
"cycle_states": self.cycle_states
}

def getMatrixView(self):
Copy link
Contributor

@sidprasad sidprasad Jul 26, 2025

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.

Copy link
Contributor Author

Copilot AI Jul 26, 2025

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:

  • Changed from background colors to text colors for 0/1 values (green for 1, red for 0)
  • Added proper cycle headers with the same structure as the Table view
  • The 0s and 1s are now clearly visible with bold text styling

See commit 07bc78f and screenshot: https://github.com/user-attachments/assets/a160c974-96b5-4c40-b534-761b8d5b746d

"""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:
Copy link
Contributor

@sidprasad sidprasad Jul 26, 2025

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

I dont think this is being correctly populated with 0s and 1s

Copy link
Contributor Author

Copilot AI Jul 26, 2025

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

Fixed in commit c473ef9. The issue was that the Matrix View template was dependent on prefixstates|length to determine columns, but when matrix_data had data but prefixstates was empty, no columns would render. Now the Matrix View uses the actual matrix data to drive the display, making the 0s and 1s visible regardless of prefix/cycle state availability.

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})"
Expand Down
167 changes: 112 additions & 55 deletions src/templates/stepper.html
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -141,8 +141,11 @@ <h5 class="modal-title" id="exampleModalLabel">Load Stepper with a new LTL Formu
</li>
</ul>

<div class="tab-content">
<div class="tab-pane fade show active" id="stepper-view" role="tabpanel">
<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">
Expand Down Expand Up @@ -180,59 +183,113 @@ <h4><span class="help float-right"> By clicking the <code>Previous State</code>
</div>
</div>
{% endfor %}
</div>
</div>
<!-- This view lets you look at multiple tree views at once, for state by state. -->
<div class="tab-pane fade" id="table-view" role="tabpanel">


<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>
<!-- Table view goes here -->
<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>
</div>
</div>
<!-- ================================ -->
<!-- TABLE VIEW - Matrix display of subformula satisfaction over time -->
Copy link
Contributor

@sidprasad sidprasad Jul 26, 2025

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

The "detailed" view is the Table View.

Call this the Matrix View (1s and 0s). They should be different tabs.

Copy link
Contributor Author

Copilot AI Jul 26, 2025

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

Updated the structure to have three distinct tabs: "Stepper View", "Matrix View", and "Table View" as requested. The Matrix View now contains the 0/1 binary display, while the Table View contains the detailed formula view with satisfaction highlighting. See commit 07bc78f.

<!-- ================================ -->
<div class="tab-pane fade" id="table-view" role="tabpanel">
<p>
Copy link
Contributor

@sidprasad sidprasad Jul 26, 2025

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

No 0s and 1s shown still.

Copy link
Contributor Author

Copilot AI Jul 26, 2025

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

Fixed in commit c473ef9. The Matrix View now properly displays 0s and 1s by iterating directly over the values in matrix_data.rows instead of relying on external state variables. This ensures the binary values are always visible when matrix data is available.

This tabular 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>1</strong> (satisfied) or <strong>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 %}
{% for i in range(cyclestates|length) %}
<th class="text-center cycle-state-col">{{ prefixstates|length + i }}</th>
{% endfor %}
{% endif %}
</tr>
</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 {% if row_data.values[i] == 1 %}table-success{% else %}table-danger{% endif %}">
{{ row_data.values[i] }}
</td>
{% endfor %}
{% if cyclestates %}
{% for i in range(cyclestates|length) %}
<td class="text-center cycle-state-col {% if row_data.values[prefixstates|length + i] == 1 %}table-success{% else %}table-danger{% endif %}">
{{ row_data.values[prefixstates|length + i] }}
</td>
{% endfor %}
{% endif %}
</tr>
{% endfor %}
</tbody>
</table>

<hr>
<details>
<summary class="btn btn-outline-secondary btn-sm">Show detailed formula view</summary>
<div class="mt-3">
<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>
<!-- Original 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>
</div>
</details>
{% 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>
Expand Down