mirror of
https://github.com/AdaCore/spat.git
synced 2026-02-12 13:09:53 -08:00
919dd515c2
CODE:
* Minor optimizations:
When collecting files to parse we use a hashed set now instead of a vector.
In theory that is way more efficient, in practice it will probably only make a
difference with thousands of files.
Instead of storing the file name in the entity to establish the backward
reference, store the file names in a set and just store a cursor to the
appropriate position in the set. We will need that kind of cross reference
anyway.
* Read steps value for provers and take them into account when sorting. Some
items are now ordered differently, so templates have been updated.
Sidenote: I am not sure how ideal it is to compare steps between different
provers.
* Sorting stability improvement with assigning unique id to sorted items.
* Added steps to output information.
* Fixed inconsistency, the File component had a type Subject_Name instead of
File_Name.
* Moved Image function (instance for Duration) into SPAT package. The useful
types can now all output themselves in the expected format.
* Renamed File/Line/Column functions to Source_* to make intent clear.
DOCUMENTATION:
* Visualization of inheritance tree.
* Script for and final rendering of internal data format.
108 lines
3.9 KiB
Python
Executable File
108 lines
3.9 KiB
Python
Executable File
#!/usr/bin/env python3
|
|
|
|
"""
|
|
Creates a graphviz dotfile to show our internal data format
|
|
and renders it to a .png with the use of graphviz.
|
|
"""
|
|
|
|
from graphviz import Digraph
|
|
|
|
def repeat_anchors(up_to, name):
|
|
"""
|
|
Repeats given name given up_to times with gv specific separators and (according to
|
|
up_to) unique anchors. The resulting string is returned.
|
|
"""
|
|
result = ""
|
|
for i in up_to[:-1]:
|
|
result = "".join([result, "<", str(i), ">", name, "|"])
|
|
|
|
return "".join([result, "<", str(up_to[-1]), ">..."])
|
|
|
|
def main():
|
|
"""Main function"""
|
|
__anchors_range = range(4)
|
|
|
|
# Repeatedly used _attributes
|
|
__top_bottom = {"rankdir":"TB"}
|
|
__dashed = {"style":"dashed"}
|
|
|
|
# Main graph
|
|
graph = Digraph(name="Internal Data Format",
|
|
filename="internal-data-format",
|
|
format="png",
|
|
body=('\trankdir=LR',
|
|
'\tviewport="800,600,0.9"',
|
|
'\tordering=out',
|
|
'\tbgcolor="#EEEEEE"'),
|
|
node_attr={"shape":"record"})
|
|
graph.node(name="Analyzed_Entity",
|
|
label="Analyzed_Entity|{|{<t>The_Tree|<f>Flows|<p>Proofs}}")
|
|
|
|
# The "root" of the entity tree
|
|
with graph.subgraph(name="Tree_Root") as subgraph:
|
|
subgraph.node(name="Root",
|
|
label="<t>The_Tree|<f>Flows_Sentinel|"\
|
|
"{|flow-data}|<p>Proofs_Sentinel|{|{proof-data}}|...")
|
|
|
|
# The flow items. Subtree of Flows_Sentinel
|
|
with graph.subgraph(name="Flow_Tree", graph_attr=__top_bottom) as subgraph:
|
|
subgraph.node(name="Flow_Items",
|
|
label=repeat_anchors(up_to=__anchors_range, name="flow_item|{|{flow_data}}"))
|
|
|
|
# The proof items. Subtree of Proofs_Sentinel
|
|
with graph.subgraph(name="Proof_Tree", graph_attr=__top_bottom) as subgraph:
|
|
subgraph.node(name="Proof_Items",
|
|
label="".join([repeat_anchors(up_to=__anchors_range,
|
|
name="proof_item|{|{proof_data}}")]))
|
|
|
|
# Proof attempt subtrees, subtree of their respective Proof_Items
|
|
for i in __anchors_range[:-1]:
|
|
with graph.subgraph(name="".join(["Proof_Attempts_", str(i), "_N"]),
|
|
graph_attr=__top_bottom) as subgraph:
|
|
subgraph.node(name="".join(["Proof_Attempts_", str(i)]),
|
|
label=repeat_anchors(up_to=__anchors_range, name="proof_attempt"))
|
|
|
|
# Make the connections
|
|
|
|
# Analyzed entity connections to tree
|
|
graph.edge("Analyzed_Entity:t", "Root:t", _attributes={"arrowhead":"none"})
|
|
graph.edge("Analyzed_Entity:f", "Root:f", _attributes=__dashed)
|
|
graph.edge("Analyzed_Entity:p", "Root:p", _attributes=__dashed)
|
|
|
|
# Flow root to each flow item
|
|
for i in __anchors_range[:-1]:
|
|
graph.edge("Root:f",
|
|
"".join(["Flow_Items:", str(i)]))
|
|
|
|
# Last edge dashed
|
|
graph.edge("Root:f",
|
|
"".join(["Flow_Items:", str(__anchors_range[-1])]),
|
|
_attributes=__dashed)
|
|
|
|
# Proof root to each proof item.
|
|
for i in __anchors_range[:-1]:
|
|
graph.edge("Root:p",
|
|
"".join(["Proof_Items:", str(i)]))
|
|
|
|
# Last edge dashed
|
|
graph.edge("Root:p",
|
|
"".join(["Proof_Items:", str(__anchors_range[-1])]),
|
|
_attributes=__dashed)
|
|
|
|
# Each proof item to their respective proof attempts.
|
|
for i in __anchors_range[:-1]:
|
|
# Undashed edges
|
|
for j in __anchors_range[:-1]:
|
|
graph.edge("".join(["Proof_Items:", str(i)]),
|
|
"".join(["Proof_Attempts_", str(i), ":", str(j)]))
|
|
|
|
# Last edge dashed
|
|
graph.edge("".join(["Proof_Items:", str(i)]),
|
|
"".join(["Proof_Attempts_", str(i), ":", str(__anchors_range[-1])]),
|
|
_attributes=__dashed)
|
|
|
|
graph.render(view=False, cleanup=True)
|
|
|
|
if __name__ == "main":
|
|
main()
|