From e5693b8a981456ed77d5e539aae62327bdbaad3b Mon Sep 17 00:00:00 2001
From: Margus Veanes <veanes@users.noreply.github.com>
Date: Sun, 9 Aug 2020 14:53:29 -0700
Subject: [PATCH] added support for saving state graph in dot format (#4621)
* added support for saving state graph in dot format
* moved write_dgml and write_dot under CASSERT
* updated dgml and dot generation a bit so that a state that is both and alive state is detected as having green background but red border when the invariant is vioalted
---
src/util/state_graph.cpp | 64 +++++++++++++++++++++++++++++++++++-----
src/util/state_graph.h | 10 +++++--
2 files changed, 65 insertions(+), 9 deletions(-)
diff --git a/src/util/state_graph.cpp b/src/util/state_graph.cpp
index 1a59dc4af..b5f621a00 100644
--- a/src/util/state_graph.cpp
+++ b/src/util/state_graph.cpp
@@ -263,8 +263,9 @@ void state_graph::add_state(state s) {
if (m_seen.contains(s)) return;
STRACE("state_graph", tout << "[state_graph] adding state " << s << ": ";);
add_state_core(s);
+ CASSERT("state_graph", write_dgml());
+ CASSERT("state_graph", write_dot());
CASSERT("state_graph", check_invariant());
- STRACE("state_graph", write_dgml(););
STRACE("state_graph", tout << std::endl;);
}
void state_graph::mark_live(state s) {
@@ -273,8 +274,9 @@ void state_graph::mark_live(state s) {
SASSERT(m_state_ufind.is_root(s));
if (m_unexplored.contains(s)) mark_unknown_core(s);
mark_live_recursive(s);
+ CASSERT("state_graph", write_dgml());
+ CASSERT("state_graph", write_dot());
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) {
@@ -286,8 +288,9 @@ void state_graph::add_edge(state s1, state s2, bool maybecycle) {
s2 = m_state_ufind.find(s2);
add_edge_core(s1, s2, maybecycle);
if (m_live.contains(s2)) mark_live(s1);
+ CASSERT("state_graph", write_dgml());
+ CASSERT("state_graph", write_dot());
CASSERT("state_graph", check_invariant());
- STRACE("state_graph", write_dgml(););
STRACE("state_graph", tout << std::endl;);
}
void state_graph::mark_done(state s) {
@@ -298,8 +301,9 @@ void state_graph::mark_done(state s) {
if (m_unexplored.contains(s)) mark_unknown_core(s);
s = merge_all_cycles(s);
mark_dead_recursive(s); // check if dead
+ CASSERT("state_graph", write_dgml());
+ CASSERT("state_graph", write_dot());
CASSERT("state_graph", check_invariant());
- STRACE("state_graph", write_dgml(););
STRACE("state_graph", tout << std::endl;);
}
@@ -413,10 +417,11 @@ std::ostream& state_graph::display(std::ostream& o) const {
return o;
}
+#ifdef Z3DEBUG
/*
Output the whole state graph in dgml format into the file '.z3-state-graph.dgml'
*/
-void state_graph::write_dgml() {
+bool 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
@@ -432,10 +437,10 @@ void state_graph::write_dgml() {
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_live.contains(s))
+ dgml << "<Category Ref=\"Alive\"/>" << std::endl;
if (m_unexplored.contains(s))
dgml << "<Category Ref=\"Unexplored\"/>" << std::endl;
dgml << "</Node>" << std::endl;
@@ -469,6 +474,7 @@ void state_graph::write_dgml() {
<< "<Style TargetType=\"Node\" GroupLabel=\"Dead\" ValueLabel=\"True\">" << std::endl
<< "<Condition Expression=\"HasCategory('Dead')\"/>" << std::endl
<< "<Setter Property=\"Background\" Value=\"tomato\"/>" << std::endl
+ << "<Setter Property=\"Stroke\" Value=\"tomato\"/>" << std::endl
<< "</Style>" << std::endl
<< "<Style TargetType=\"Node\" GroupLabel=\"Unexplored\" ValueLabel=\"True\">" << std::endl
<< "<Condition Expression=\"HasCategory('Unexplored')\"/>" << std::endl
@@ -491,4 +497,48 @@ void state_graph::write_dgml() {
<< "</Styles>" << std::endl
<< "</DirectedGraph>" << std::endl;
dgml.close();
+ return true;
}
+
+/*
+ Output the whole state graph in dot format into the file '.z3-state-graph.dot'
+ */
+bool state_graph::write_dot() {
+ std::ofstream dot(".z3-state-graph.dot");
+ dot << "digraph \"state_graph\" {" << std::endl
+ << "rankdir=TB" << std::endl
+ << "node [peripheries=1,style=filled,fillcolor=white,fontsize=24]" << std::endl;
+ for (auto s : m_seen) {
+ if (m_state_ufind.is_root(s)) {
+ dot << s << " [label=\"";
+ auto r = s;
+ dot << r;
+ do {
+ if (r != s)
+ dot << "," << r;
+ r = m_state_ufind.next(r);
+ } while (r != s);
+ dot << "\"";
+ if (m_unexplored.contains(s))
+ dot << ",style=\"dashed,filled\"";
+ if (m_dead.contains(s))
+ dot << ",color=tomato,fillcolor=tomato";
+ if (m_live.contains(s))
+ dot << ",fillcolor=green";
+ dot << "]" << std::endl;
+ }
+ }
+ for (auto s : m_seen) {
+ if (m_state_ufind.is_root(s))
+ for (auto t : m_targets[s]) {
+ dot << s << " -> " << t;
+ if (!m_sources_maybecycle[t].contains(s))
+ dot << "[style=bold]";
+ dot << std::endl;
+ }
+ }
+ dot << "}" << std::endl;
+ dot.close();
+ return true;
+}
+#endif
diff --git a/src/util/state_graph.h b/src/util/state_graph.h
index 9e754048e..61e19946a 100644
--- a/src/util/state_graph.h
+++ b/src/util/state_graph.h
@@ -112,10 +112,16 @@ private:
bool is_subset(state_set set1, state_set set2) const;
bool is_disjoint(state_set set1, state_set set2) const;
bool check_invariant() const;
+ /*
+ Output the whole state graph in dgml format into the file '.z3-state-graph.dgml'
+ */
+ bool write_dgml();
+ /*
+ Output the whole state graph in dot format into the file '.z3-state-graph.dot'
+ */
+ bool write_dot();
#endif
- void write_dgml();
-
/*
'Core' functions that modify the plain graph, without
updating SCCs or propagating live/dead state information.