alarsyo/spot
1
0
Fork 0
Code Issues Pull requests Projects Releases Wiki Activity

Adding dot suppport for aiger class

Browse source 
* spot/twaalgos/aiger.cc: Useless assert
* spot/twaalgos/dot.hh,
spot/twaalgos/dot.cc: aig to dot
* python/spot/__init__.py: Adapting
* tests/python/games.ipynb: Additional tests
This commit is contained in:
philipp 2021-08-10 23:58:26 +02:00 • committed by Florian Renkin
parent 17db582341
commit 2c267dd894
5 changed files with 583 additions and 17 deletions
Download patch file Download diff file Expand all files Collapse all files

53
python/spot/__init__.py
View file

@ -136,6 +136,28 @@ def __om_init_new(self, str=None):
option_map.__init__ = __om_init_new
@_extend(aig)
class aig:
def _repr_svg_(self, opt=None):
ostr = ostringstream()
print_dot(ostr, self, opt)
return _ostream_to_svg(ostr)
def show(self, opt=None):
from spot.jupyter import SVG
return SVG(self._repr_svg_(opt))
def to_str(self, format='circuit', opt=None):
format = format.lower()
if format == 'circuit':
ostr = ostringstream()
print_aiger(ostr, self)
return ostr.str()
if format == 'dot':
ostr = ostringstream()
print_dot(ostr, self, opt)
return ostr.str()
raise ValueError("unknown string format: " + format)
__twa__acc1 = twa.acc
__twa__acc2 = twa.get_acceptance
@ -683,6 +705,37 @@ def automaton(filename, **kwargs):
except StopIteration:
raise RuntimeError("Failed to read automaton from {}".format(filename))
def aiger_circuits(*sources, bdd_dict = None):
"""Read aiger circuits from a list of sources.
Parameters
----------
*sources : list of str
These sources can be either commands (end with `|`),
textual representations of the circuit in restricted aag format
(start with aag and contain '\n'), or filenames (else).
bdd_dict : If not supplied, a fresh bdd_dict will be created, common for
all of the circuits.
"""
bdd_dict = bdd_dict if bdd_dict is not None else make_bdd_dict()
for source in sources:
if (source.startswith("aag") and '\n' in source):
yield aig.parse_aag(source, "<string>", bdd_dict)
else:
yield aig.parse_aag(source, bdd_dict)
def aiger_circuit(source, bdd_dict = None):
"""Read a single aiger circuit from file or textual representation.
See `spot.aiger_circuits` for a list of supported formats."""
try:
return next(aiger_circuits(source, bdd_dict = bdd_dict))
except StopIteration:
raise RuntimeError("Failed to read an aiger circuit "
"from {}".format(source))
def _postproc_translate_options(obj, default_type, *args):
type_name_ = None

2
spot/twaalgos/aiger.cc
View file

@ -1086,8 +1086,6 @@ namespace spot
std::function<bdd(unsigned)> get_gate_bdd;
get_gate_bdd = [&](unsigned g)->bdd
{
assert(v2g(circ.gate_var(g) == g));
unsigned v = circ.gate_var(g);
auto it = var2bdd.find(v);
if (it != var2bdd.end())

197
spot/twaalgos/dot.cc
View file

@ -1065,5 +1065,202 @@ namespace spot
return os;
}
namespace
{
class dotty_aig final
{
public:
bool vertical = true;
bool latex = false;
std::ostream& os_;
void
parse_opts(const char *options)
{
while (char c = *options++)
switch (c)
{
case 'h':
{
vertical = false;
break;
}
case 'v':
{
vertical = true;
break;
}
default:
throw std::runtime_error("unknown option for print_dot(): "s + c);
}
}
dotty_aig(std::ostream &os, const char *options)
: os_(os)
{
parse_opts(options ? options : "");
}
void print(const aig_ptr &circuit)
{
if (!circuit)
return;
auto is_input = [nb_in = circuit->num_inputs()](unsigned val)
{
return (val & ~1) <= (2 * nb_in);
};
const auto& in_names = circuit->input_names();
const auto& out_names = circuit->output_names();
auto num_latches = circuit->num_latches();
auto latches = circuit->next_latches();
auto num_inputs = circuit->num_inputs();
auto num_outputs = circuit->num_outputs();
auto outputs = circuit->outputs();
auto num_gates = circuit->num_gates();
auto gates = circuit->gates();
// If a circuit doesn't use an input, we need a special placement
bool uses_in = false;
auto add_edge = [](std::ostream &stream, const unsigned src,
const unsigned dst) {
auto src_gate = src & ~1;
stream << src_gate;
stream << " -> " << dst;
if (src & 1)
stream << " [arrowhead=dot]";
stream << '\n';
};
if (vertical)
os_ << "digraph \"\" {\nrankdir = BT;\n";
else
os_ << "digraph \"\" {\nrankdir = LR;\n";
os_ << "# latches left\n";
for (unsigned i = 0; i < num_latches; ++i)
{
auto first = circuit->latch_var(i);
auto first_m_mod = first & ~1;
os_ << "node[shape=box, label=\"L" << i << "_out\"] "
<< first_m_mod << ";\n";
}
//Predefine all nodes
os_ << "# input nodes\n";
for (unsigned i = 0; i < num_inputs; ++i)
os_ << "node [shape=triangle, label=\""
<< in_names[i] << "\"] "
<< circuit->input_var(i) << ";\n";
os_ << "# latch nodes\n";
for (unsigned i = 0; i < num_latches; ++i)
os_ << "node[shape=box, label=\"L" << i << "\"] L" << i << ";\n";
os_ << "# gate nodes\n";
for (unsigned i = 0; i < num_gates; ++i)
if ((gates[i].first != 0) && (gates[i].second != 0))
{
uses_in |= is_input(gates[i].first) | is_input(gates[i].second);
auto gate_var = circuit->gate_var(i);
os_ << "node [shape=circle, label=\"" << gate_var
<< "\"] " << gate_var << ";\n";
}
os_ << "# and ins\n";
for (unsigned i = 0; i < num_gates; ++i)
if ((gates[i].first != 0) && (gates[i].second != 0))
{
auto gate_var = circuit->gate_var(i);
add_edge(os_, gates[i].first, gate_var);
add_edge(os_, gates[i].second, gate_var);
}
bool has_alone_gate = false;
os_ << "# Latches\n";
for (unsigned i = 0; i < num_latches; ++i)
{
auto second = latches[i];
os_ << "node[shape=box, label=\"L" << i << "_in\"] L" << i << ";\n";
if (second <= 1 && !has_alone_gate)
{
os_ << "node[shape=box, label=\"Const\"] 0" << std::endl;
has_alone_gate = true;
}
os_ << (second & ~1) << " -> L" << i;
if (i & 1)
os_ << "[arrowhead=dot]";
os_ << '\n';
}
// Outs can be defined after everything else
os_ << "# Outs\n";
const char* out_pos = vertical ? ":s" : ":w";
for (unsigned i = 0; i < num_outputs; ++i)
{
os_ << "node [shape=triangle, orientation=180, label=\""
<< out_names[i] << "\"] o" << i
<< out_names[i] << ";\n";
auto z = outputs[i];
uses_in |= is_input(z);
if (z <= 1 && !has_alone_gate)
{
os_ << "node[shape=box, label=\"Const\"] 0" << std::endl;
has_alone_gate = true;
}
os_ << (z & ~1) << "->" << 'o' << i << out_names[i] << out_pos;
if (outputs[i] & 1)
os_ << " [arrowhead=dot]";
os_ << '\n';
}
if (has_alone_gate || num_inputs > 0)
{
os_ << (uses_in ? "{rank = source; " : "{rank = same; ");
for (unsigned i = 0; i < num_inputs; ++i)
os_ << circuit->input_var(i) << "; ";
if (has_alone_gate)
os_ << "0; ";
os_ << "}\n";
}
if (num_outputs > 0)
{
os_ << "{rank = sink; ";
for (unsigned i = 0; i < num_outputs; ++i)
os_ << 'o' << i << out_names[i] << "; ";
os_ << "}\n";
}
if (num_latches > 0)
{
os_ << "{rank = same; ";
for (unsigned i = 0; i < num_latches; ++i)
os_ << 'L' << i << "; ";
os_ << "}\n{rank = same; ";
for (unsigned i = 0; i < num_latches; ++i)
{
auto first = circuit->latch_var(i);
auto first_m_mod = first & ~1;
os_ << first_m_mod << "; ";
}
os_ << "}\n";
}
os_ << "}\n";
}
};
}
std::ostream &
print_dot(std::ostream &os, aig_ptr circuit, const char* options)
{
dotty_aig d(os, options);
if (!circuit)
return os;
d.print(circuit);
return os;
}
}

5
spot/twaalgos/dot.hh
View file

@ -25,6 +25,7 @@
#include <iosfwd>
#include <spot/twa/fwd.hh>
#include <spot/misc/common.hh>
#include <spot/twaalgos/aiger.hh>
namespace spot
{
@ -44,4 +45,8 @@ namespace spot
print_dot(std::ostream& os,
const const_twa_ptr& g,
const char* options = nullptr);
SPOT_API std::ostream &
print_dot(std::ostream &os, aig_ptr circuit, const char * = nullptr);
}

343
tests/python/games.ipynb
View file

@ -769,7 +769,7 @@
"<text text-anchor=\"start\" x=\"189.96\" y=\"-158.56\" font-family=\"Lato\" font-size=\"14.00\" fill=\"#ff4da0\">❶</text>\n",
"</g>\n",
"<!-- 2&#45;&gt;4 -->\n",
"<g id=\"edge6\" class=\"edge\">\n",
"<g id=\"edge7\" class=\"edge\">\n",
"<title>2&#45;&gt;4</title>\n",
"<path fill=\"none\" stroke=\"black\" d=\"M167.95,-196.4C181.93,-193.79 201.45,-190.14 216.79,-187.27\"/>\n",
"<polygon fill=\"black\" stroke=\"black\" points=\"223.94,-185.94 217.64,-190.32 220.5,-186.58 217.06,-187.22 217.06,-187.22 217.06,-187.22 220.5,-186.58 216.48,-184.13 223.94,-185.94 223.94,-185.94\"/>\n",
@ -783,7 +783,7 @@
"<text text-anchor=\"middle\" x=\"427.92\" y=\"-137.06\" font-family=\"Lato\" font-size=\"14.00\">5</text>\n",
"</g>\n",
"<!-- 2&#45;&gt;5 -->\n",
"<g id=\"edge7\" class=\"edge\">\n",
"<g id=\"edge6\" class=\"edge\">\n",
"<title>2&#45;&gt;5</title>\n",
"<path fill=\"none\" stroke=\"black\" d=\"M160.75,-208.85C168.39,-214.75 179.16,-222.01 189.96,-225.76 275.06,-255.28 319.26,-296.01 391.92,-242.76 413.34,-227.05 401.22,-210.86 409.92,-185.76 412.38,-178.66 415.21,-170.99 417.85,-164.03\"/>\n",
"<polygon fill=\"black\" stroke=\"black\" points=\"420.4,-157.35 420.84,-165.01 419.15,-160.62 417.9,-163.89 417.9,-163.89 417.9,-163.89 419.15,-160.62 414.96,-162.76 420.4,-157.35 420.4,-157.35\"/>\n",
@ -833,7 +833,7 @@
"<text text-anchor=\"start\" x=\"277.96\" y=\"-198.56\" font-family=\"Lato\" font-size=\"14.00\" fill=\"#ff7f00\">❷</text>\n",
"</g>\n",
"<!-- 5&#45;&gt;6 -->\n",
"<g id=\"edge12\" class=\"edge\">\n",
"<g id=\"edge11\" class=\"edge\">\n",
"<title>5&#45;&gt;6</title>\n",
"<path fill=\"none\" stroke=\"black\" d=\"M442.18,-129.03C460.14,-113.14 492.15,-84.82 511.36,-67.81\"/>\n",
"<polygon fill=\"black\" stroke=\"black\" points=\"516.89,-62.92 513.73,-69.92 514.27,-65.24 511.65,-67.56 511.65,-67.56 511.65,-67.56 514.27,-65.24 509.56,-65.2 516.89,-62.92 516.89,-62.92\"/>\n",
@ -841,7 +841,7 @@
"<text text-anchor=\"start\" x=\"463.92\" y=\"-110.56\" font-family=\"Lato\" font-size=\"14.00\" fill=\"#ff4da0\">❶</text>\n",
"</g>\n",
"<!-- 5&#45;&gt;7 -->\n",
"<g id=\"edge11\" class=\"edge\">\n",
"<g id=\"edge12\" class=\"edge\">\n",
"<title>5&#45;&gt;7</title>\n",
"<path fill=\"none\" stroke=\"black\" d=\"M409.86,-142.24C399.69,-142.52 386.71,-141.81 375.92,-137.76 366.67,-134.29 357.82,-127.88 350.82,-121.79\"/>\n",
"<polygon fill=\"black\" stroke=\"black\" points=\"345.4,-116.81 352.69,-119.22 347.98,-119.18 350.56,-121.55 350.56,-121.55 350.56,-121.55 347.98,-119.18 348.43,-123.87 345.4,-116.81 345.4,-116.81\"/>\n",
@ -865,7 +865,7 @@
"<text text-anchor=\"start\" x=\"375.92\" y=\"-107.56\" font-family=\"Lato\" font-size=\"14.00\" fill=\"#ff7f00\">❷</text>\n",
"</g>\n",
"<!-- 8&#45;&gt;4 -->\n",
"<g id=\"edge15\" class=\"edge\">\n",
"<g id=\"edge16\" class=\"edge\">\n",
"<title>8&#45;&gt;4</title>\n",
"<path fill=\"none\" stroke=\"black\" d=\"M327.6,-192.49C320.95,-181.1 309.32,-164.86 293.96,-157.76 282.73,-152.57 270.27,-158.46 260.47,-165.83\"/>\n",
"<polygon fill=\"black\" stroke=\"black\" points=\"255.04,-170.26 258.47,-163.39 257.75,-168.04 260.47,-165.83 260.47,-165.83 260.47,-165.83 257.75,-168.04 262.46,-168.27 255.04,-170.26 255.04,-170.26\"/>\n",
@ -879,7 +879,7 @@
"<text text-anchor=\"middle\" x=\"427.92\" y=\"-209.06\" font-family=\"Lato\" font-size=\"14.00\">9</text>\n",
"</g>\n",
"<!-- 8&#45;&gt;9 -->\n",
"<g id=\"edge16\" class=\"edge\">\n",
"<g id=\"edge15\" class=\"edge\">\n",
"<title>8&#45;&gt;9</title>\n",
"<path fill=\"none\" stroke=\"black\" d=\"M356.13,-206.53C369.86,-207.74 388.1,-209.35 402.62,-210.62\"/>\n",
"<polygon fill=\"black\" stroke=\"black\" points=\"409.84,-211.26 402.59,-213.78 406.35,-210.95 402.86,-210.64 402.86,-210.64 402.86,-210.64 406.35,-210.95 403.14,-207.51 409.84,-211.26 409.84,-211.26\"/>\n",
@ -912,7 +912,7 @@
"</svg>\n"
],
"text/plain": [
"<spot.twa_graph; proxy of <Swig Object of type 'std::shared_ptr< spot::twa_graph > *' at 0x7fa3979355d0> >"
"<spot.twa_graph; proxy of <Swig Object of type 'std::shared_ptr< spot::twa_graph > *' at 0x7fbc7c65c660> >"
]
},
"execution_count": 8,
@ -1112,7 +1112,7 @@
"<text text-anchor=\"start\" x=\"189.96\" y=\"-158.56\" font-family=\"Lato\" font-size=\"14.00\" fill=\"#ff4da0\">❶</text>\n",
"</g>\n",
"<!-- 2&#45;&gt;4 -->\n",
"<g id=\"edge6\" class=\"edge\">\n",
"<g id=\"edge7\" class=\"edge\">\n",
"<title>2&#45;&gt;4</title>\n",
"<path fill=\"none\" stroke=\"#33a02c\" stroke-width=\"2\" d=\"M167.95,-196.4C181.93,-193.79 201.45,-190.14 216.79,-187.27\"/>\n",
"<polygon fill=\"#33a02c\" stroke=\"#33a02c\" stroke-width=\"2\" points=\"223.94,-185.94 217.64,-190.32 220.6,-187.07 217.15,-187.72 217.06,-187.22 216.97,-186.73 220.41,-186.09 216.48,-184.13 223.94,-185.94 223.94,-185.94\"/>\n",
@ -1126,7 +1126,7 @@
"<text text-anchor=\"middle\" x=\"427.92\" y=\"-137.06\" font-family=\"Lato\" font-size=\"14.00\">5</text>\n",
"</g>\n",
"<!-- 2&#45;&gt;5 -->\n",
"<g id=\"edge7\" class=\"edge\">\n",
"<g id=\"edge6\" class=\"edge\">\n",
"<title>2&#45;&gt;5</title>\n",
"<path fill=\"none\" stroke=\"black\" d=\"M160.75,-208.85C168.39,-214.75 179.16,-222.01 189.96,-225.76 275.06,-255.28 319.26,-296.01 391.92,-242.76 413.34,-227.05 401.22,-210.86 409.92,-185.76 412.38,-178.66 415.21,-170.99 417.85,-164.03\"/>\n",
"<polygon fill=\"black\" stroke=\"black\" points=\"420.4,-157.35 420.84,-165.01 419.15,-160.62 417.9,-163.89 417.9,-163.89 417.9,-163.89 419.15,-160.62 414.96,-162.76 420.4,-157.35 420.4,-157.35\"/>\n",
@ -1176,7 +1176,7 @@
"<text text-anchor=\"start\" x=\"277.96\" y=\"-198.56\" font-family=\"Lato\" font-size=\"14.00\" fill=\"#ff7f00\">❷</text>\n",
"</g>\n",
"<!-- 5&#45;&gt;6 -->\n",
"<g id=\"edge12\" class=\"edge\">\n",
"<g id=\"edge11\" class=\"edge\">\n",
"<title>5&#45;&gt;6</title>\n",
"<path fill=\"none\" stroke=\"black\" d=\"M442.18,-129.03C460.14,-113.14 492.15,-84.82 511.36,-67.81\"/>\n",
"<polygon fill=\"black\" stroke=\"black\" points=\"516.89,-62.92 513.73,-69.92 514.27,-65.24 511.65,-67.56 511.65,-67.56 511.65,-67.56 514.27,-65.24 509.56,-65.2 516.89,-62.92 516.89,-62.92\"/>\n",
@ -1184,7 +1184,7 @@
"<text text-anchor=\"start\" x=\"463.92\" y=\"-110.56\" font-family=\"Lato\" font-size=\"14.00\" fill=\"#ff4da0\">❶</text>\n",
"</g>\n",
"<!-- 5&#45;&gt;7 -->\n",
"<g id=\"edge11\" class=\"edge\">\n",
"<g id=\"edge12\" class=\"edge\">\n",
"<title>5&#45;&gt;7</title>\n",
"<path fill=\"none\" stroke=\"#e31a1c\" stroke-width=\"2\" d=\"M409.86,-142.24C399.69,-142.52 386.71,-141.81 375.92,-137.76 366.67,-134.29 357.82,-127.88 350.82,-121.79\"/>\n",
"<polygon fill=\"#e31a1c\" stroke=\"#e31a1c\" stroke-width=\"2\" points=\"345.4,-116.81 352.69,-119.22 348.32,-118.81 350.9,-121.18 350.56,-121.55 350.22,-121.91 347.64,-119.55 348.43,-123.87 345.4,-116.81 345.4,-116.81\"/>\n",
@ -1208,7 +1208,7 @@
"<text text-anchor=\"start\" x=\"375.92\" y=\"-107.56\" font-family=\"Lato\" font-size=\"14.00\" fill=\"#ff7f00\">❷</text>\n",
"</g>\n",
"<!-- 8&#45;&gt;4 -->\n",
"<g id=\"edge15\" class=\"edge\">\n",
"<g id=\"edge16\" class=\"edge\">\n",
"<title>8&#45;&gt;4</title>\n",
"<path fill=\"none\" stroke=\"black\" d=\"M327.6,-192.49C320.95,-181.1 309.32,-164.86 293.96,-157.76 282.73,-152.57 270.27,-158.46 260.47,-165.83\"/>\n",
"<polygon fill=\"black\" stroke=\"black\" points=\"255.04,-170.26 258.47,-163.39 257.75,-168.04 260.47,-165.83 260.47,-165.83 260.47,-165.83 257.75,-168.04 262.46,-168.27 255.04,-170.26 255.04,-170.26\"/>\n",
@ -1222,7 +1222,7 @@
"<text text-anchor=\"middle\" x=\"427.92\" y=\"-209.06\" font-family=\"Lato\" font-size=\"14.00\">9</text>\n",
"</g>\n",
"<!-- 8&#45;&gt;9 -->\n",
"<g id=\"edge16\" class=\"edge\">\n",
"<g id=\"edge15\" class=\"edge\">\n",
"<title>8&#45;&gt;9</title>\n",
"<path fill=\"none\" stroke=\"#33a02c\" stroke-width=\"2\" d=\"M356.13,-206.53C369.86,-207.74 388.1,-209.35 402.62,-210.62\"/>\n",
"<polygon fill=\"#33a02c\" stroke=\"#33a02c\" stroke-width=\"2\" points=\"409.84,-211.26 402.59,-213.78 406.31,-211.45 402.82,-211.14 402.86,-210.64 402.91,-210.15 406.39,-210.45 403.14,-207.51 409.84,-211.26 409.84,-211.26\"/>\n",
@ -1255,7 +1255,7 @@
"</svg>\n"
],
"text/plain": [
"<spot.twa_graph; proxy of <Swig Object of type 'std::shared_ptr< spot::twa_graph > *' at 0x7fa37f087db0> >"
"<spot.twa_graph; proxy of <Swig Object of type 'std::shared_ptr< spot::twa_graph > *' at 0x7fbc7c250240> >"
]
},
"execution_count": 11,
@ -1267,6 +1267,319 @@
"spot.highlight_strategy(game)"
]
},
{
"cell_type": "code",
"execution_count": null,
"metadata": {},
"outputs": [],
"source": []
},
{
"cell_type": "markdown",
"metadata": {},
"source": [
"<h2>Reading an aiger-file</h2>\n",
"\n",
"<p>Read an aiger file. Note that we do not support the full \n",
" <a href=\"http://fmv.jku.at/aiger/FORMAT.aiger\">syntax</a>, but are restricted to:\n",
" <ul>\n",
" <li>Input variables start at index 2 and are consecutively numbered.</li>\n",
" <li>Latch variables start at index (1 + #inputs) * 2 and are consecutively numbered.</li>\n",
" <li>If inputs or outputs are named in the comments, all of them have to be named.</li>\n",
" <li>Gate number $n$ can only have latches, inputs or previously defined gates ($<n$). </li>\n",
" </ul>\n",
"</p>"
]
},
{
"cell_type": "code",
"execution_count": 12,
"metadata": {},
"outputs": [
{
"name": "stdout",
"output_type": "stream",
"text": [
"aag 5 2 0 2 3\n",
"2\n",
"4\n",
"10\n",
"6\n",
"6 2 4\n",
"8 3 5\n",
"10 7 9\n",
"i0 a\n",
"i1 b\n",
"o0 c\n",
"o1 d\n",
"\n"
]
}
],
"source": [
"#aiger file \n",
"aag_txt = \"\"\"aag 5 2 0 2 3\n",
"2\n",
"4\n",
"10\n",
"6\n",
"6 2 4\n",
"8 3 5\n",
"10 7 9\n",
"i0 a\n",
"i1 b\n",
"o0 c\n",
"o1 d\n",
"\"\"\"\n",
"print(aag_txt)"
]
},
{
"cell_type": "code",
"execution_count": 13,
"metadata": {},
"outputs": [],
"source": [
"this_aig = spot.aiger_circuit(aag_txt)"
]
},
{
"cell_type": "code",
"execution_count": 14,
"metadata": {},
"outputs": [
{
"data": {
"image/svg+xml": [
"<?xml version=\"1.0\" encoding=\"UTF-8\" standalone=\"no\"?>\n",
"<!DOCTYPE svg PUBLIC \"-//W3C//DTD SVG 1.1//EN\"\n",
" \"http://www.w3.org/Graphics/SVG/1.1/DTD/svg11.dtd\">\n",
"<!-- Generated by graphviz version 2.43.0 (0)\n",
" -->\n",
"<!-- Title: %3 Pages: 1 -->\n",
"<svg width=\"202pt\" height=\"289pt\"\n",
" viewBox=\"0.00 0.00 202.39 289.50\" xmlns=\"http://www.w3.org/2000/svg\" xmlns:xlink=\"http://www.w3.org/1999/xlink\">\n",
"<g id=\"graph0\" class=\"graph\" transform=\"scale(1.0 1.0) rotate(0) translate(4 285.5)\">\n",
"<title>%3</title>\n",
"<polygon fill=\"white\" stroke=\"transparent\" points=\"-4,4 -4,-285.5 198.39,-285.5 198.39,4 -4,4\"/>\n",
"<!-- 2 -->\n",
"<g id=\"node1\" class=\"node\">\n",
"<title>2</title>\n",
"<polygon fill=\"none\" stroke=\"black\" points=\"44.2,-46 5.2,-11.5 83.19,-11.5 44.2,-46\"/>\n",
"<text text-anchor=\"middle\" x=\"44.2\" y=\"-19.3\" font-family=\"Times,serif\" font-size=\"14.00\">i0</text>\n",
"</g>\n",
"<!-- 6 -->\n",
"<g id=\"node3\" class=\"node\">\n",
"<title>6</title>\n",
"<ellipse fill=\"none\" stroke=\"black\" cx=\"129.2\" cy=\"-100\" rx=\"18\" ry=\"18\"/>\n",
"<text text-anchor=\"middle\" x=\"129.2\" y=\"-96.3\" font-family=\"Times,serif\" font-size=\"14.00\">6</text>\n",
"</g>\n",
"<!-- 2&#45;&gt;6 -->\n",
"<g id=\"edge1\" class=\"edge\">\n",
"<title>2&#45;&gt;6</title>\n",
"<path fill=\"none\" stroke=\"black\" d=\"M56.74,-35.07C70.27,-47 92.03,-66.21 108.18,-80.46\"/>\n",
"<polygon fill=\"black\" stroke=\"black\" points=\"106.23,-83.4 116.04,-87.39 110.86,-78.15 106.23,-83.4\"/>\n",
"</g>\n",
"<!-- 8 -->\n",
"<g id=\"node4\" class=\"node\">\n",
"<title>8</title>\n",
"<ellipse fill=\"none\" stroke=\"black\" cx=\"65.2\" cy=\"-100\" rx=\"18\" ry=\"18\"/>\n",
"<text text-anchor=\"middle\" x=\"65.2\" y=\"-96.3\" font-family=\"Times,serif\" font-size=\"14.00\">8</text>\n",
"</g>\n",
"<!-- 2&#45;&gt;8 -->\n",
"<g id=\"edge3\" class=\"edge\">\n",
"<title>2&#45;&gt;8</title>\n",
"<path fill=\"none\" stroke=\"black\" d=\"M49.17,-41.77C51.92,-51.58 55.37,-63.89 58.36,-74.59\"/>\n",
"<ellipse fill=\"black\" stroke=\"black\" cx=\"59.46\" cy=\"-78.53\" rx=\"4\" ry=\"4\"/>\n",
"</g>\n",
"<!-- 4 -->\n",
"<g id=\"node2\" class=\"node\">\n",
"<title>4</title>\n",
"<polygon fill=\"none\" stroke=\"black\" points=\"140.2,-46 101.2,-11.5 179.19,-11.5 140.2,-46\"/>\n",
"<text text-anchor=\"middle\" x=\"140.2\" y=\"-19.3\" font-family=\"Times,serif\" font-size=\"14.00\">i1</text>\n",
"</g>\n",
"<!-- 4&#45;&gt;6 -->\n",
"<g id=\"edge2\" class=\"edge\">\n",
"<title>4&#45;&gt;6</title>\n",
"<path fill=\"none\" stroke=\"black\" d=\"M137.31,-43.71C136.05,-52.28 134.55,-62.48 133.19,-71.76\"/>\n",
"<polygon fill=\"black\" stroke=\"black\" points=\"129.72,-71.32 131.73,-81.72 136.64,-72.34 129.72,-71.32\"/>\n",
"</g>\n",
"<!-- 4&#45;&gt;8 -->\n",
"<g id=\"edge4\" class=\"edge\">\n",
"<title>4&#45;&gt;8</title>\n",
"<path fill=\"none\" stroke=\"black\" d=\"M128.48,-35.72C116.36,-47.83 97.3,-66.9 83.26,-80.94\"/>\n",
"<ellipse fill=\"black\" stroke=\"black\" cx=\"80.41\" cy=\"-83.79\" rx=\"4\" ry=\"4\"/>\n",
"</g>\n",
"<!-- 10 -->\n",
"<g id=\"node5\" class=\"node\">\n",
"<title>10</title>\n",
"<ellipse fill=\"none\" stroke=\"black\" cx=\"65.2\" cy=\"-176.75\" rx=\"23\" ry=\"23\"/>\n",
"<text text-anchor=\"middle\" x=\"65.2\" y=\"-173.05\" font-family=\"Times,serif\" font-size=\"14.00\">10</text>\n",
"</g>\n",
"<!-- 6&#45;&gt;10 -->\n",
"<g id=\"edge5\" class=\"edge\">\n",
"<title>6&#45;&gt;10</title>\n",
"<path fill=\"none\" stroke=\"black\" d=\"M117.75,-114.36C108.69,-124.95 95.81,-139.99 85.07,-152.53\"/>\n",
"<ellipse fill=\"black\" stroke=\"black\" cx=\"82.29\" cy=\"-155.79\" rx=\"4\" ry=\"4\"/>\n",
"</g>\n",
"<!-- o1o1 -->\n",
"<g id=\"node7\" class=\"node\">\n",
"<title>o1o1</title>\n",
"<polygon fill=\"none\" stroke=\"black\" points=\"150.2,-235.5 194.59,-270 105.8,-270 150.2,-235.5\"/>\n",
"<text text-anchor=\"middle\" x=\"150.2\" y=\"-254.8\" font-family=\"Times,serif\" font-size=\"14.00\">o1</text>\n",
"</g>\n",
"<!-- 6&#45;&gt;o1o1 -->\n",
"<g id=\"edge8\" class=\"edge\">\n",
"<title>6&#45;&gt;o1o1:s</title>\n",
"<path fill=\"none\" stroke=\"black\" d=\"M133.55,-117.85C139.22,-141.22 148.58,-185.13 150.01,-225.36\"/>\n",
"<polygon fill=\"black\" stroke=\"black\" points=\"146.51,-225.56 150.2,-235.5 153.51,-225.43 146.51,-225.56\"/>\n",
"</g>\n",
"<!-- 8&#45;&gt;10 -->\n",
"<g id=\"edge6\" class=\"edge\">\n",
"<title>8&#45;&gt;10</title>\n",
"<path fill=\"none\" stroke=\"black\" d=\"M65.2,-118.34C65.2,-126.54 65.2,-136.58 65.2,-145.95\"/>\n",
"<ellipse fill=\"black\" stroke=\"black\" cx=\"65.2\" cy=\"-149.95\" rx=\"4\" ry=\"4\"/>\n",
"</g>\n",
"<!-- o0o0 -->\n",
"<g id=\"node6\" class=\"node\">\n",
"<title>o0o0</title>\n",
"<polygon fill=\"none\" stroke=\"black\" points=\"44.2,-235.5 88.59,-270 -0.2,-270 44.2,-235.5\"/>\n",
"<text text-anchor=\"middle\" x=\"44.2\" y=\"-254.8\" font-family=\"Times,serif\" font-size=\"14.00\">o0</text>\n",
"</g>\n",
"<!-- 10&#45;&gt;o0o0 -->\n",
"<g id=\"edge7\" class=\"edge\">\n",
"<title>10&#45;&gt;o0o0:s</title>\n",
"<path fill=\"none\" stroke=\"black\" d=\"M54.45,-196.9C50.57,-205.12 46.74,-215.16 45.07,-225.34\"/>\n",
"<polygon fill=\"black\" stroke=\"black\" points=\"41.57,-225.23 44.2,-235.5 48.54,-225.83 41.57,-225.23\"/>\n",
"</g>\n",
"</g>\n",
"</svg>\n"
],
"text/plain": [
"<spot.jupyter.SVG object>"
]
},
"metadata": {},
"output_type": "display_data"
}
],
"source": [
"display(this_aig.show())"
]
},
{
"cell_type": "code",
"execution_count": 15,
"metadata": {},
"outputs": [
{
"name": "stdout",
"output_type": "stream",
"text": [
"aag 5 2 0 2 3\n",
"2\n",
"4\n",
"10\n",
"6\n",
"6 2 4\n",
"8 3 5\n",
"10 7 9\n",
"i0 i0\n",
"i1 i1\n",
"o0 o0\n",
"o1 o1\n",
"\n"
]
}
],
"source": [
"print(this_aig.to_str())"
]
},
{
"cell_type": "code",
"execution_count": 16,
"metadata": {},
"outputs": [
{
"name": "stdout",
"output_type": "stream",
"text": [
"((2, 4), (3, 5), (7, 9))\n"
]
}
],
"source": [
"print(this_aig.gates())"
]
},
{
"cell_type": "markdown",
"metadata": {},
"source": [
"<h2>Verifying an implementation</h2>\n",
"\n",
"<p>\n",
" An aiger circuit can be transformed into a monitor. If the aiger represents the implementation of a strategy in the context of active control, it can be check for correctness. This is done by computing the intersecting of the monitor and the negation of the specification.\n",
"</p>"
]
},
{
"cell_type": "code",
"execution_count": 17,
"metadata": {},
"outputs": [
{
"data": {
"image/svg+xml": [
"<?xml version=\"1.0\" encoding=\"UTF-8\" standalone=\"no\"?>\n",
"<!DOCTYPE svg PUBLIC \"-//W3C//DTD SVG 1.1//EN\"\n",
" \"http://www.w3.org/Graphics/SVG/1.1/DTD/svg11.dtd\">\n",
"<!-- Generated by graphviz version 2.43.0 (0)\n",
" -->\n",
"<!-- Pages: 1 -->\n",
"<svg width=\"535pt\" height=\"115pt\"\n",
" viewBox=\"0.00 0.00 535.00 115.00\" xmlns=\"http://www.w3.org/2000/svg\" xmlns:xlink=\"http://www.w3.org/1999/xlink\">\n",
"<g id=\"graph0\" class=\"graph\" transform=\"scale(1.0 1.0) rotate(0) translate(4 111)\">\n",
"<polygon fill=\"white\" stroke=\"transparent\" points=\"-4,4 -4,-111 531,-111 531,4 -4,4\"/>\n",
"<text text-anchor=\"start\" x=\"260.5\" y=\"-91.8\" font-family=\"Lato\" font-size=\"14.00\">t</text>\n",
"<text text-anchor=\"start\" x=\"252.5\" y=\"-76.8\" font-family=\"Lato\" font-size=\"14.00\">[all]</text>\n",
"<!-- I -->\n",
"<!-- 0 -->\n",
"<g id=\"node2\" class=\"node\">\n",
"<title>0</title>\n",
"<ellipse fill=\"#ffffaa\" stroke=\"black\" cx=\"263.5\" cy=\"-18\" rx=\"18\" ry=\"18\"/>\n",
"<text text-anchor=\"middle\" x=\"263.5\" y=\"-14.3\" font-family=\"Lato\" font-size=\"14.00\">0</text>\n",
"</g>\n",
"<!-- I&#45;&gt;0 -->\n",
"<g id=\"edge1\" class=\"edge\">\n",
"<title>I&#45;&gt;0</title>\n",
"<path fill=\"none\" stroke=\"black\" d=\"M208.65,-18C210.29,-18 224.65,-18 238.13,-18\"/>\n",
"<polygon fill=\"black\" stroke=\"black\" points=\"245.44,-18 238.44,-21.15 241.94,-18 238.44,-18 238.44,-18 238.44,-18 241.94,-18 238.44,-14.85 245.44,-18 245.44,-18\"/>\n",
"</g>\n",
"<!-- 0&#45;&gt;0 -->\n",
"<g id=\"edge2\" class=\"edge\">\n",
"<title>0&#45;&gt;0</title>\n",
"<path fill=\"none\" stroke=\"black\" d=\"M257.12,-35.04C255.82,-44.86 257.95,-54 263.5,-54 267.67,-54 269.9,-48.86 270.21,-42.14\"/>\n",
"<polygon fill=\"black\" stroke=\"black\" points=\"269.88,-35.04 273.35,-41.88 270.04,-38.53 270.21,-42.03 270.21,-42.03 270.21,-42.03 270.04,-38.53 267.06,-42.18 269.88,-35.04 269.88,-35.04\"/>\n",
"<text text-anchor=\"start\" x=\"0\" y=\"-57.8\" font-family=\"Lato\" font-size=\"14.00\">(!i0 &amp; !i1 &amp; !o0 &amp; !o1) | (!i0 &amp; i1 &amp; o0 &amp; !o1) | (i0 &amp; !i1 &amp; o0 &amp; !o1) | (i0 &amp; i1 &amp; !o0 &amp; o1)</text>\n",
"</g>\n",
"</g>\n",
"</svg>\n"
],
"text/plain": [
"<spot.twa_graph; proxy of <Swig Object of type 'std::shared_ptr< spot::twa_graph > *' at 0x7fbc7c1f07b0> >"
]
},
"metadata": {},
"output_type": "display_data"
}
],
"source": [
"aigasmon = this_aig.as_automaton()\n",
"display(aigasmon)"
]
},
{
"cell_type": "code",
"execution_count": null,
@ -1291,7 +1604,7 @@
"name": "python",
"nbconvert_exporter": "python",
"pygments_lexer": "ipython3",
"version": "3.9.1rc1"
"version": "3.8.10"
}
},
"nbformat": 4,