Skip to content

Commit

Permalink
dgml output generation for regex state graphs (#4620)
Browse files Browse the repository at this point in the history 
* dgml output generation for regex state graphs

* fixed issue in header file
  • Loading branch information
@veanes
veanes authored Aug 8, 2020
1 parent a51e40a commit 934f87a
Show file tree
Hide file tree
Showing 2 changed files with 86 additions and 0 deletions.
84 changes: 84 additions & 0 deletions src/util/state_graph.cpp
View file
Original file line number Diff line number Diff line change
Expand Up @@ -264,6 +264,7 @@ void state_graph::add_state(state s) {
STRACE("state_graph", tout << "[state_graph] adding state " << s << ": ";);
add_state_core(s);
CASSERT("state_graph", check_invariant());
STRACE("state_graph", write_dgml(););
STRACE("state_graph", tout << std::endl;);
}
void state_graph::mark_live(state s) {
Expand All @@ -273,6 +274,7 @@ void state_graph::mark_live(state s) {
if (m_unexplored.contains(s)) mark_unknown_core(s);
mark_live_recursive(s);
CASSERT("state_graph", check_invariant());
STRACE("state_graph", write_dgml(););
STRACE("state_graph", tout << std::endl;);
}
void state_graph::add_edge(state s1, state s2, bool maybecycle) {
Expand All @@ -285,6 +287,7 @@ void state_graph::add_edge(state s1, state s2, bool maybecycle) {
add_edge_core(s1, s2, maybecycle);
if (m_live.contains(s2)) mark_live(s1);
CASSERT("state_graph", check_invariant());
STRACE("state_graph", write_dgml(););
STRACE("state_graph", tout << std::endl;);
}
void state_graph::mark_done(state s) {
Expand All @@ -296,6 +299,7 @@ void state_graph::mark_done(state s) {
s = merge_all_cycles(s);
mark_dead_recursive(s); // check if dead
CASSERT("state_graph", check_invariant());
STRACE("state_graph", write_dgml(););
STRACE("state_graph", tout << std::endl;);
}

Expand Down Expand Up @@ -408,3 +412,83 @@ std::ostream& state_graph::display(std::ostream& o) const {

return o;
}

/*
Output the whole state graph in dgml format into the file '.z3-state-graph.dgml'
*/
void state_graph::write_dgml() {
std::ofstream dgml(".z3-state-graph.dgml");
dgml << "<?xml version=\"1.0\" encoding=\"utf-8\"?>" << std::endl
<< "<DirectedGraph xmlns=\"http://schemas.microsoft.com/vs/2009/dgml\" GraphDirection=\"TopToBottom\">" << std::endl
<< "<Nodes>" << std::endl;
for (auto s : m_seen) {
if (m_state_ufind.is_root(s)) {
dgml << "<Node Id=\"" << s << "\" Label=\"";
auto r = s;
dgml << r;
do {
if (r != s)
dgml << "," << r;
r = m_state_ufind.next(r);
} while (r != s);
dgml << "\" Category=\"State\">" << std::endl;
if (m_live.contains(s))
dgml << "<Category Ref=\"Alive\"/>" << std::endl;
if (m_dead.contains(s))
dgml << "<Category Ref=\"Dead\"/>" << std::endl;
if (m_unexplored.contains(s))
dgml << "<Category Ref=\"Unexplored\"/>" << std::endl;
dgml << "</Node>" << std::endl;
}
}
dgml << "</Nodes>" << std::endl;
dgml << "<Links>" << std::endl;
for (auto s : m_seen) {
if (m_state_ufind.is_root(s))
for (auto t : m_targets[s]) {
dgml << "<Link Source=\"" << s << "\" Target=\"" << t << "\" Category=\"Transition\">" << std::endl;
if (!m_sources_maybecycle[t].contains(s))
dgml << "<Category Ref=\"Noncycle\"/>" << std::endl;
dgml << "</Link>" << std::endl;
}
}
dgml << "</Links>" << std::endl;
dgml << "<Categories>" << std::endl
<< "<Category Id=\"Alive\" Label=\"Alive\" IsTag=\"True\"/>" << std::endl
<< "<Category Id=\"Dead\" Label=\"Dead\" IsTag=\"True\"/>" << std::endl
<< "<Category Id=\"Unexplored\" Label=\"Unexplored\" IsTag=\"True\"/>" << std::endl
<< "<Category Id=\"Transition\" Label=\"Transition\" IsTag=\"True\"/>" << std::endl
<< "<Category Id=\"State\" Label=\"State\" IsTag=\"True\"/>" << std::endl
<< "<Category Id=\"Noncycle\" Label=\"Noncycle Transition\" IsTag=\"True\"/>" << std::endl
<< "</Categories>" << std::endl
<< "<Styles>" << std::endl
<< "<Style TargetType=\"Node\" GroupLabel=\"Alive\" ValueLabel=\"True\">" << std::endl
<< "<Condition Expression=\"HasCategory('Alive')\"/>" << std::endl
<< "<Setter Property=\"Background\" Value=\"lightgreen\"/>" << std::endl
<< "</Style>" << std::endl
<< "<Style TargetType=\"Node\" GroupLabel=\"Dead\" ValueLabel=\"True\">" << std::endl
<< "<Condition Expression=\"HasCategory('Dead')\"/>" << std::endl
<< "<Setter Property=\"Background\" Value=\"tomato\"/>" << std::endl
<< "</Style>" << std::endl
<< "<Style TargetType=\"Node\" GroupLabel=\"Unexplored\" ValueLabel=\"True\">" << std::endl
<< "<Condition Expression=\"HasCategory('Unexplored')\"/>" << std::endl
<< "<Setter Property=\"StrokeDashArray\" Value=\"8 8\"/>" << std::endl
<< "</Style>" << std::endl
<< "<Style TargetType=\"Node\" GroupLabel=\"State\" ValueLabel=\"True\">" << std::endl
<< "<Condition Expression=\"HasCategory('State')\"/>" << std::endl
<< "<Setter Property=\"Stroke\" Value=\"black\"/>" << std::endl
<< "<Setter Property=\"Background\" Value=\"white\"/>" << std::endl
<< "<Setter Property=\"MinWidth\" Value=\"0\"/>" << std::endl
<< "</Style>" << std::endl
<< "<Style TargetType=\"Link\" GroupLabel=\"Transition\" ValueLabel=\"True\">" << std::endl
<< "<Condition Expression=\"HasCategory('Transition')\"/>" << std::endl
<< "<Setter Property=\"Stroke\" Value=\"black\"/>" << std::endl
<< "</Style>" << std::endl
<< "<Style TargetType=\"Link\" GroupLabel=\"Noncycle\" ValueLabel=\"True\">" << std::endl
<< "<Condition Expression=\"HasCategory('Noncycle')\"/>" << std::endl
<< "<Setter Property=\"StrokeThickness\" Value=\"4\"/>" << std::endl
<< "</Style>" << std::endl
<< "</Styles>" << std::endl
<< "</DirectedGraph>" << std::endl;
dgml.close();
}
2 changes: 2 additions & 0 deletions src/util/state_graph.h
View file
Original file line number Diff line number Diff line change
Expand Up @@ -114,6 +114,8 @@ class state_graph {
bool check_invariant() const;
#endif

void write_dgml();

/*
'Core' functions that modify the plain graph, without
updating SCCs or propagating live/dead state information.
Expand Down

0 comments on commit 934f87a

Please sign in to comment.