mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-04-27 10:55:50 +00:00
Code Activity

dgml output generation for regex state graphs (#4620)

Browse source 
* dgml output generation for regex state graphs

* fixed issue in header file
This commit is contained in:
Margus Veanes 2020-08-08 09:40:20 -07:00 • committed by GitHub
parent a51e40a6cd
commit 934f87a336
No known key found for this signature in database
GPG key ID: 4AEE18F83AFDEB23
2 changed files with 86 additions and 0 deletions
Download patch file Download diff file Expand all files Collapse all files

84
src/util/state_graph.cpp
View file

@ -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) {
@ -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) {
@ -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) {
@ -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;);
}
@ -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
src/util/state_graph.h
View file

@ -114,6 +114,8 @@ private:
bool check_invariant() const;
#endif
void write_dgml();
/*
'Core' functions that modify the plain graph, without
updating SCCs or propagating live/dead state information.