From a9b4560f3d65533453c4f3876515f49a3197f192 Mon Sep 17 00:00:00 2001 From: Alexandre Duret-Lutz Date: Mon, 1 Feb 2016 08:36:59 +0100 Subject: [PATCH] dot: add option "k" Fixes #134. * spot/twaalgos/dot.cc: Implement it. * bin/common_aoutput.cc, spot/twaalgos/dot.hh, NEWS: Document it. * tests/core/readsave.test, tests/python/ltsmin.ipynb: Test it. --- NEWS | 4 + bin/common_aoutput.cc | 6 +- spot/twaalgos/dot.cc | 61 ++- spot/twaalgos/dot.hh | 4 +- tests/core/readsave.test | 46 +- tests/python/ltsmin.ipynb | 858 ++++++++++++++++++-------------------- 6 files changed, 528 insertions(+), 451 deletions(-) diff --git a/NEWS b/NEWS index e1ed299a7..fb9e30850 100644 --- a/NEWS +++ b/NEWS @@ -19,6 +19,10 @@ New in spot 1.99.7a (not yet released) with ltl2tgba -D 'Ga | Gb | Gc' -d + * print_dot() now has option "k" to use state-based labels when + possible. This is similar to the "k" option already supported + by print_hoa(), and is useful when printing Kripke structures. + Python: * The ltsmin interface has been binded in Python. See diff --git a/bin/common_aoutput.cc b/bin/common_aoutput.cc index ccca94d21..6af324fd8 100644 --- a/bin/common_aoutput.cc +++ b/bin/common_aoutput.cc @@ -80,7 +80,7 @@ static const argp_option options[] = { /**************************************************/ { nullptr, 0, nullptr, 0, "Output format:", 3 }, - { "dot", 'd', "1|a|b|B|c|e|f(FONT)|h|n|N|o|r|R|s|t|v|+INT|* sn_ = nullptr; std::vector>* sprod_ = nullptr; @@ -192,6 +193,9 @@ namespace spot case 'h': opt_horizontal_ = true; break; + case 'k': + opt_state_labels_ = true; + break; case 'n': opt_name_ = true; break; @@ -319,6 +323,21 @@ namespace spot os_ << '}'; } + std::string + state_label(unsigned s) const + { + bdd label = bddfalse; + for (auto& t: aut_->out(s)) + { + label = t.cond; + break; + } + if (label == bddfalse + && incomplete_ && incomplete_->find(s) != incomplete_->end()) + return "..."; + return bdd_format_formula(aut_->get_dict(), label); + } + void start() { @@ -440,6 +459,8 @@ namespace spot os_ << "\\n"; output_set(acc); } + if (opt_state_labels_) + escape_str(os_ << "\\n", state_label(s)); os_ << '"'; } else @@ -456,6 +477,8 @@ namespace spot os_ << "
"; output_html_set(acc); } + if (opt_state_labels_) + escape_html(os_ << "
", state_label(s)); os_ << '>'; } os_ << "]\n"; @@ -470,6 +493,8 @@ namespace spot os_ << (*sprod_)[s].first << ',' << (*sprod_)[s].second; else os_ << s; + if (opt_state_labels_) + escape_str(os_ << "\\n", state_label(s)); os_ << '"'; // Use state_acc_sets(), not state_is_accepting() because // on co-Büchi automata we want to mark the rejecting @@ -486,8 +511,10 @@ namespace spot void process_link(const twa_graph::edge_storage_t& t, int number) { - std::string label = bdd_format_formula(aut_->get_dict(), t.cond); os_ << " " << t.src << " -> " << t.dst; + std::string label; + if (!opt_state_labels_) + label = bdd_format_formula(aut_->get_dict(), t.cond); if (!opt_html_labels_) { os_ << " [label=\""; @@ -495,7 +522,8 @@ namespace spot if (!mark_states_) if (auto a = t.acc) { - os_ << "\\n"; + if (!opt_state_labels_) + os_ << "\\n"; output_set(a); } os_ << '"'; @@ -507,7 +535,8 @@ namespace spot if (!mark_states_) if (auto a = t.acc) { - os_ << "
"; + if (!opt_state_labels_) + os_ << "
"; output_html_set(a); } os_ << '>'; @@ -533,6 +562,27 @@ namespace spot sprod_ = nullptr; } } + if (opt_state_labels_) + { + // Verify that we can use state labels for this automaton. + unsigned n = aut->num_states(); + for (unsigned s = 0; s < n; ++s) + { + bool first = true; + bdd cond = bddfalse; + for (auto& t: aut->out(s)) + if (first) + { + cond = t.cond; + first = false; + } + else if (t.cond != cond) + { + opt_state_labels_ = false; + break; + } + } + } incomplete_ = aut->get_named_prop>("incomplete-states"); if (opt_name_) @@ -541,11 +591,12 @@ namespace spot && aut_->prop_state_acc().is_true()); if (opt_shape_ == ShapeAuto) { - if (sn_ || sprod_ || aut->num_states() > 100) + if (sn_ || sprod_ || aut->num_states() > 100 || opt_state_labels_) { opt_shape_ = ShapeEllipse; // If all state names are short, prefer circles. - if (sn_ && std::all_of(sn_->begin(), sn_->end(), + if (!opt_state_labels_ && + sn_ && std::all_of(sn_->begin(), sn_->end(), [](const std::string& s) { return s.size() <= 2; })) opt_shape_ = ShapeCircle; diff --git a/spot/twaalgos/dot.hh b/spot/twaalgos/dot.hh index 0a64ca483..53e56cc23 100644 --- a/spot/twaalgos/dot.hh +++ b/spot/twaalgos/dot.hh @@ -1,5 +1,5 @@ // -*- coding: utf-8 -*- -// Copyright (C) 2011, 2012, 2013, 2014, 2015 Laboratoire de Recherche +// Copyright (C) 2011, 2012, 2013, 2014, 2015, 2016 Laboratoire de Recherche // et Developpement de l'Epita (LRDE). // Copyright (C) 2003, 2004 Laboratoire d'Informatique de Paris 6 (LIP6), // département Systèmes Répartis Coopératifs (SRC), Université Pierre @@ -39,7 +39,7 @@ namespace spot /// supported: 'v' for vertical output, 'h' for horizontal output, /// 't' force transition-based acceptance, 'N' hide the name of the /// automaton, 'n' shows the name, 'c' uses circle-shaped states, - /// 'a' shows the acceptance. + /// 'a' shows the acceptance, 'k' uses state-based labels if possible. SPOT_API std::ostream& print_dot(std::ostream& os, const const_twa_ptr& g, diff --git a/tests/core/readsave.test b/tests/core/readsave.test index e120aabd6..45bff75b8 100755 --- a/tests/core/readsave.test +++ b/tests/core/readsave.test @@ -344,7 +344,8 @@ test 1 = `autfilt -H input --complete | autfilt --is-complete --count` # The SPOT_DEFAULT_FORMAT envvar should be ignored if --dot is given. -SPOT_DEFAULT_FORMAT=hoa ltl2tgba --dot=a 'GFa & GFb' >output +# --dot=k should be ignored when not applicable. +SPOT_DEFAULT_FORMAT=hoa ltl2tgba --dot=ak 'GFa & GFb' >output cat output cat >expected <output6d +cat >expect6d < 1 + 0 [label="0\nb"] + 0 -> 2 [label=""] + 0 -> 1 [label=""] + 0 -> 1 [label=""] + 1 [label="1\na"] + 1 -> 0 [label=""] + 1 -> 1 [label=""] + 2 [label="2\na", peripheries=2] + 2 -> 2 [label=""] + 2 -> 0 [label=""] + 2 -> 1 [label=""] +} +EOF +diff output6d expect6d + +run 0 autfilt -dbark input6 >output6d2 +cat >expect6d2 <⓿)> + labelloc="t" + I [label="", style=invis, width=0] + I -> 1 + 0 [label=<0
b>] + 0 -> 2 [label=<>] + 0 -> 1 [label=<>] + 0 -> 1 [label=<>] + 1 [label=<1
a>] + 1 -> 0 [label=<>] + 1 -> 1 [label=<>] + 2 [label=<2
⓿
a>] + 2 -> 2 [label=<>] + 2 -> 0 [label=<>] + 2 -> 1 [label=<>] +} +EOF +diff output6d2 expect6d2 cat >input7 <2\"])\n", - "k" + "k.show('.k')" ], "language": "python", "metadata": {}, @@ -172,196 +172,186 @@ "output_type": "pyout", "prompt_number": 6, "svg": [ - "\n", - "\n", - "\n", - "\n", - "\n", - "\n", + "\n", + "\n", "G\n", - "\n", + "\n", "\n", "\n", - "0\n", - "\n", - "a=0, b=0, Q=0\n", + "0\n", + "\n", + "a=0, b=0, Q=0\n", + ""a<1" & !"b>2" & !dead\n", "\n", "\n", - "I->0\n", - "\n", - "\n", + "I->0\n", + "\n", + "\n", "\n", "\n", - "1\n", - "\n", - "a=1, b=0, Q=0\n", + "1\n", + "\n", + "a=1, b=0, Q=0\n", + "!"a<1" & !"b>2" & !dead\n", "\n", "\n", - "0->1\n", - "\n", - "\n", - ""a<1" & !"b>2" & !dead\n", + "0->1\n", + "\n", + "\n", "\n", "\n", - "2\n", - "\n", - "a=0, b=1, Q=0\n", + "2\n", + "\n", + "a=0, b=1, Q=0\n", + ""a<1" & !"b>2" & !dead\n", "\n", "\n", - "0->2\n", - "\n", - "\n", - ""a<1" & !"b>2" & !dead\n", + "0->2\n", + "\n", + "\n", "\n", "\n", - "3\n", - "\n", - "a=2, b=0, Q=0\n", + "3\n", + "\n", + "a=2, b=0, Q=0\n", + "!"a<1" & !"b>2" & !dead\n", "\n", "\n", - "1->3\n", - "\n", - "\n", - "!"a<1" & !"b>2" & !dead\n", + "1->3\n", + "\n", + "\n", "\n", "\n", - "4\n", - "\n", - "a=1, b=1, Q=0\n", + "4\n", + "\n", + "a=1, b=1, Q=0\n", + "!"a<1" & !"b>2" & !dead\n", "\n", "\n", - "1->4\n", - "\n", - "\n", - "!"a<1" & !"b>2" & !dead\n", + "1->4\n", + "\n", + "\n", "\n", "\n", - "2->4\n", - "\n", - "\n", - ""a<1" & !"b>2" & !dead\n", + "2->4\n", + "\n", + "\n", "\n", "\n", - "5\n", - "\n", - "a=0, b=2, Q=0\n", + "5\n", + "\n", + "a=0, b=2, Q=0\n", + ""a<1" & !"b>2" & !dead\n", "\n", "\n", - "2->5\n", - "\n", - "\n", - ""a<1" & !"b>2" & !dead\n", + "2->5\n", + "\n", + "\n", "\n", "\n", - "6\n", - "\n", - "a=3, b=0, Q=0\n", + "6\n", + "\n", + "a=3, b=0, Q=0\n", + "!"a<1" & !"b>2" & dead\n", "\n", "\n", - "3->6\n", - "\n", - "\n", - "!"a<1" & !"b>2" & !dead\n", + "3->6\n", + "\n", + "\n", "\n", "\n", - "7\n", - "\n", - "a=2, b=1, Q=0\n", + "7\n", + "\n", + "a=2, b=1, Q=0\n", + "...\n", "\n", "\n", - "3->7\n", - "\n", - "\n", - "!"a<1" & !"b>2" & !dead\n", + "3->7\n", + "\n", + "\n", "\n", "\n", - "4->7\n", - "\n", - "\n", - "!"a<1" & !"b>2" & !dead\n", + "4->7\n", + "\n", + "\n", "\n", "\n", - "8\n", - "\n", - "a=1, b=2, Q=0\n", + "8\n", + "\n", + "a=1, b=2, Q=0\n", + "...\n", "\n", "\n", - "4->8\n", - "\n", - "\n", - "!"a<1" & !"b>2" & !dead\n", + "4->8\n", + "\n", + "\n", "\n", "\n", - "5->8\n", - "\n", - "\n", - ""a<1" & !"b>2" & !dead\n", + "5->8\n", + "\n", + "\n", "\n", "\n", - "u5\n", - "\n", - "...\n", + "u5\n", + "\n", + "...\n", "\n", "\n", - "5->u5\n", - "\n", - "\n", + "5->u5\n", + "\n", + "\n", "\n", "\n", - "9\n", - "\n", - "a=0, b=3, Q=0\n", + "9\n", + "\n", + "a=0, b=3, Q=0\n", + "...\n", "\n", "\n", - "5->9\n", - "\n", - "\n", - ""a<1" & !"b>2" & !dead\n", + "5->9\n", + "\n", + "\n", "\n", "\n", - "6->6\n", - "\n", - "\n", - "!"a<1" & !"b>2" & dead\n", + "6->6\n", + "\n", + "\n", "\n", "\n", - "u7\n", - "\n", - "...\n", + "u7\n", + "\n", + "...\n", "\n", "\n", - "7->u7\n", - "\n", - "\n", + "7->u7\n", + "\n", + "\n", "\n", "\n", - "u8\n", - "\n", - "...\n", + "u8\n", + "\n", + "...\n", "\n", "\n", - "8->u8\n", - "\n", - "\n", + "8->u8\n", + "\n", + "\n", "\n", "\n", - "u9\n", - "\n", - "...\n", + "u9\n", + "\n", + "...\n", "\n", "\n", - "9->u9\n", - "\n", - "\n", + "9->u9\n", + "\n", + "\n", "\n", "\n", - "\n" + "" ], "text": [ - " *' at 0x7f7f00239600> >" + "" ] } ], @@ -371,7 +361,7 @@ "cell_type": "code", "collapsed": false, "input": [ - "k.show('.<15')" + "k.show('.k<15')" ], "language": "python", "metadata": {}, @@ -381,272 +371,266 @@ "output_type": "pyout", "prompt_number": 7, "svg": [ - "\n", - "\n", + "\n", + "\n", "G\n", - "\n", + "\n", "\n", "\n", "0\n", - "\n", - "a=0, b=0, Q=0\n", + "\n", + "a=0, b=0, Q=0\n", + ""a<1" & !"b>2" & !dead\n", "\n", "\n", "I->0\n", - "\n", - "\n", + "\n", + "\n", "\n", "\n", "1\n", - "\n", - "a=1, b=0, Q=0\n", + "\n", + "a=1, b=0, Q=0\n", + "!"a<1" & !"b>2" & !dead\n", "\n", "\n", "0->1\n", - "\n", - "\n", - ""a<1" & !"b>2" & !dead\n", + "\n", + "\n", "\n", "\n", "2\n", - "\n", - "a=0, b=1, Q=0\n", + "\n", + "a=0, b=1, Q=0\n", + ""a<1" & !"b>2" & !dead\n", "\n", "\n", "0->2\n", - "\n", - "\n", - ""a<1" & !"b>2" & !dead\n", + "\n", + "\n", "\n", "\n", "3\n", - "\n", - "a=2, b=0, Q=0\n", + "\n", + "a=2, b=0, Q=0\n", + "!"a<1" & !"b>2" & !dead\n", "\n", "\n", "1->3\n", - "\n", - "\n", - "!"a<1" & !"b>2" & !dead\n", + "\n", + "\n", "\n", "\n", "4\n", - "\n", - "a=1, b=1, Q=0\n", + "\n", + "a=1, b=1, Q=0\n", + "!"a<1" & !"b>2" & !dead\n", "\n", "\n", "1->4\n", - "\n", - "\n", - "!"a<1" & !"b>2" & !dead\n", + "\n", + "\n", "\n", "\n", "2->4\n", - "\n", - "\n", - ""a<1" & !"b>2" & !dead\n", + "\n", + "\n", "\n", "\n", "5\n", - "\n", - "a=0, b=2, Q=0\n", + "\n", + "a=0, b=2, Q=0\n", + ""a<1" & !"b>2" & !dead\n", "\n", "\n", "2->5\n", - "\n", - "\n", - ""a<1" & !"b>2" & !dead\n", + "\n", + "\n", "\n", "\n", "6\n", - "\n", - "a=3, b=0, Q=0\n", + "\n", + "a=3, b=0, Q=0\n", + "!"a<1" & !"b>2" & dead\n", "\n", "\n", "3->6\n", - "\n", - "\n", - "!"a<1" & !"b>2" & !dead\n", + "\n", + "\n", "\n", "\n", "7\n", - "\n", - "a=2, b=1, Q=0\n", + "\n", + "a=2, b=1, Q=0\n", + "!"a<1" & !"b>2" & !dead\n", "\n", "\n", "3->7\n", - "\n", - "\n", - "!"a<1" & !"b>2" & !dead\n", + "\n", + "\n", "\n", "\n", "4->7\n", - "\n", - "\n", - "!"a<1" & !"b>2" & !dead\n", + "\n", + "\n", "\n", "\n", "8\n", - "\n", - "a=1, b=2, Q=0\n", + "\n", + "a=1, b=2, Q=0\n", + "!"a<1" & !"b>2" & !dead\n", "\n", "\n", "4->8\n", - "\n", - "\n", - "!"a<1" & !"b>2" & !dead\n", + "\n", + "\n", "\n", "\n", "5->8\n", - "\n", - "\n", - ""a<1" & !"b>2" & !dead\n", + "\n", + "\n", "\n", "\n", "9\n", - "\n", - "a=0, b=3, Q=0\n", + "\n", + "a=0, b=3, Q=0\n", + "...\n", "\n", "\n", "5->9\n", - "\n", - "\n", - ""a<1" & !"b>2" & !dead\n", + "\n", + "\n", "\n", "\n", "10\n", - "\n", - "a=0, b=2, Q=1\n", + "\n", + "a=0, b=2, Q=1\n", + ""a<1" & !"b>2" & !dead\n", "\n", "\n", "5->10\n", - "\n", - "\n", - ""a<1" & !"b>2" & !dead\n", + "\n", + "\n", "\n", "\n", "6->6\n", - "\n", - "\n", - "!"a<1" & !"b>2" & dead\n", + "\n", + "\n", "\n", "\n", "11\n", - "\n", - "a=3, b=1, Q=0\n", + "\n", + "a=3, b=1, Q=0\n", + "!"a<1" & !"b>2" & dead\n", "\n", "\n", "7->11\n", - "\n", - "\n", - "!"a<1" & !"b>2" & !dead\n", + "\n", + "\n", "\n", "\n", "12\n", - "\n", - "a=2, b=2, Q=0\n", + "\n", + "a=2, b=2, Q=0\n", + "...\n", "\n", "\n", "7->12\n", - "\n", - "\n", - "!"a<1" & !"b>2" & !dead\n", + "\n", + "\n", "\n", "\n", "8->12\n", - "\n", - "\n", - "!"a<1" & !"b>2" & !dead\n", + "\n", + "\n", "\n", "\n", "13\n", - "\n", - "a=1, b=3, Q=0\n", + "\n", + "a=1, b=3, Q=0\n", + "...\n", "\n", "\n", "8->13\n", - "\n", - "\n", - "!"a<1" & !"b>2" & !dead\n", + "\n", + "\n", "\n", "\n", "14\n", - "\n", - "a=1, b=2, Q=1\n", + "\n", + "a=1, b=2, Q=1\n", + "...\n", "\n", "\n", "8->14\n", - "\n", - "\n", - "!"a<1" & !"b>2" & !dead\n", + "\n", + "\n", "\n", "\n", "u9\n", - "\n", - "...\n", + "\n", + "...\n", "\n", "\n", "9->u9\n", - "\n", - "\n", + "\n", + "\n", "\n", "\n", "10->14\n", - "\n", - "\n", - ""a<1" & !"b>2" & !dead\n", + "\n", + "\n", "\n", "\n", "u10\n", - "\n", - "...\n", + "\n", + "...\n", "\n", "\n", "10->u10\n", - "\n", - "\n", + "\n", + "\n", "\n", "\n", "11->11\n", - "\n", - "\n", - "!"a<1" & !"b>2" & dead\n", + "\n", + "\n", "\n", "\n", "u12\n", - "\n", - "...\n", + "\n", + "...\n", "\n", "\n", "12->u12\n", - "\n", - "\n", + "\n", + "\n", "\n", "\n", "u13\n", - "\n", - "...\n", + "\n", + "...\n", "\n", "\n", "13->u13\n", - "\n", - "\n", + "\n", + "\n", "\n", "\n", "u14\n", - "\n", - "...\n", + "\n", + "...\n", "\n", "\n", "14->u14\n", - "\n", - "\n", + "\n", + "\n", "\n", "\n", "" ], "text": [ - "" + "" ] } ], @@ -656,7 +640,7 @@ "cell_type": "code", "collapsed": false, "input": [ - "k.show('.<0') # unlimited output" + "k.show('.k<0') # unlimited output" ], "language": "python", "metadata": {}, @@ -666,359 +650,343 @@ "output_type": "pyout", "prompt_number": 8, "svg": [ - "\n", - "\n", + "\n", + "\n", "G\n", - "\n", + "\n", "\n", "\n", "0\n", - "\n", - "a=0, b=0, Q=0\n", + "\n", + "a=0, b=0, Q=0\n", + ""a<1" & !"b>2" & !dead\n", "\n", "\n", "I->0\n", - "\n", - "\n", + "\n", + "\n", "\n", "\n", "1\n", - "\n", - "a=1, b=0, Q=0\n", + "\n", + "a=1, b=0, Q=0\n", + "!"a<1" & !"b>2" & !dead\n", "\n", "\n", "0->1\n", - "\n", - "\n", - ""a<1" & !"b>2" & !dead\n", + "\n", + "\n", "\n", "\n", "2\n", - "\n", - "a=0, b=1, Q=0\n", + "\n", + "a=0, b=1, Q=0\n", + ""a<1" & !"b>2" & !dead\n", "\n", "\n", "0->2\n", - "\n", - "\n", - ""a<1" & !"b>2" & !dead\n", + "\n", + "\n", "\n", "\n", "3\n", - "\n", - "a=2, b=0, Q=0\n", + "\n", + "a=2, b=0, Q=0\n", + "!"a<1" & !"b>2" & !dead\n", "\n", "\n", "1->3\n", - "\n", - "\n", - "!"a<1" & !"b>2" & !dead\n", + "\n", + "\n", "\n", "\n", "4\n", - "\n", - "a=1, b=1, Q=0\n", + "\n", + "a=1, b=1, Q=0\n", + "!"a<1" & !"b>2" & !dead\n", "\n", "\n", "1->4\n", - "\n", - "\n", - "!"a<1" & !"b>2" & !dead\n", + "\n", + "\n", "\n", "\n", "2->4\n", - "\n", - "\n", - ""a<1" & !"b>2" & !dead\n", + "\n", + "\n", "\n", "\n", "5\n", - "\n", - "a=0, b=2, Q=0\n", + "\n", + "a=0, b=2, Q=0\n", + ""a<1" & !"b>2" & !dead\n", "\n", "\n", "2->5\n", - "\n", - "\n", - ""a<1" & !"b>2" & !dead\n", + "\n", + "\n", "\n", "\n", "6\n", - "\n", - "a=3, b=0, Q=0\n", + "\n", + "a=3, b=0, Q=0\n", + "!"a<1" & !"b>2" & dead\n", "\n", "\n", "3->6\n", - "\n", - "\n", - "!"a<1" & !"b>2" & !dead\n", + "\n", + "\n", "\n", "\n", "7\n", - "\n", - "a=2, b=1, Q=0\n", + "\n", + "a=2, b=1, Q=0\n", + "!"a<1" & !"b>2" & !dead\n", "\n", "\n", "3->7\n", - "\n", - "\n", - "!"a<1" & !"b>2" & !dead\n", + "\n", + "\n", "\n", "\n", "4->7\n", - "\n", - "\n", - "!"a<1" & !"b>2" & !dead\n", + "\n", + "\n", "\n", "\n", "8\n", - "\n", - "a=1, b=2, Q=0\n", + "\n", + "a=1, b=2, Q=0\n", + "!"a<1" & !"b>2" & !dead\n", "\n", "\n", "4->8\n", - "\n", - "\n", - "!"a<1" & !"b>2" & !dead\n", + "\n", + "\n", "\n", "\n", "5->8\n", - "\n", - "\n", - ""a<1" & !"b>2" & !dead\n", + "\n", + "\n", "\n", "\n", "9\n", - "\n", - "a=0, b=3, Q=0\n", + "\n", + "a=0, b=3, Q=0\n", + ""a<1" & "b>2" & !dead\n", "\n", "\n", "5->9\n", - "\n", - "\n", - ""a<1" & !"b>2" & !dead\n", + "\n", + "\n", "\n", "\n", "10\n", - "\n", - "a=0, b=2, Q=1\n", + "\n", + "a=0, b=2, Q=1\n", + ""a<1" & !"b>2" & !dead\n", "\n", "\n", "5->10\n", - "\n", - "\n", - ""a<1" & !"b>2" & !dead\n", + "\n", + "\n", "\n", "\n", "6->6\n", - "\n", - "\n", - "!"a<1" & !"b>2" & dead\n", + "\n", + "\n", "\n", "\n", "11\n", - "\n", - "a=3, b=1, Q=0\n", + "\n", + "a=3, b=1, Q=0\n", + "!"a<1" & !"b>2" & dead\n", "\n", "\n", "7->11\n", - "\n", - "\n", - "!"a<1" & !"b>2" & !dead\n", + "\n", + "\n", "\n", "\n", "12\n", - "\n", - "a=2, b=2, Q=0\n", + "\n", + "a=2, b=2, Q=0\n", + "!"a<1" & !"b>2" & !dead\n", "\n", "\n", "7->12\n", - "\n", - "\n", - "!"a<1" & !"b>2" & !dead\n", + "\n", + "\n", "\n", "\n", "8->12\n", - "\n", - "\n", - "!"a<1" & !"b>2" & !dead\n", + "\n", + "\n", "\n", "\n", "13\n", - "\n", - "a=1, b=3, Q=0\n", + "\n", + "a=1, b=3, Q=0\n", + "!"a<1" & "b>2" & !dead\n", "\n", "\n", "8->13\n", - "\n", - "\n", - "!"a<1" & !"b>2" & !dead\n", + "\n", + "\n", "\n", "\n", "14\n", - "\n", - "a=1, b=2, Q=1\n", + "\n", + "a=1, b=2, Q=1\n", + "!"a<1" & !"b>2" & !dead\n", "\n", "\n", "8->14\n", - "\n", - "\n", - "!"a<1" & !"b>2" & !dead\n", + "\n", + "\n", "\n", "\n", "15\n", - "\n", - "a=0, b=3, Q=1\n", + "\n", + "a=0, b=3, Q=1\n", + ""a<1" & "b>2" & dead\n", "\n", "\n", "9->15\n", - "\n", - "\n", - ""a<1" & "b>2" & !dead\n", + "\n", + "\n", "\n", "\n", "10->14\n", - "\n", - "\n", - ""a<1" & !"b>2" & !dead\n", + "\n", + "\n", "\n", "\n", "10->15\n", - "\n", - "\n", - ""a<1" & !"b>2" & !dead\n", + "\n", + "\n", "\n", "\n", "11->11\n", - "\n", - "\n", - "!"a<1" & !"b>2" & dead\n", + "\n", + "\n", "\n", "\n", "16\n", - "\n", - "a=3, b=2, Q=0\n", + "\n", + "a=3, b=2, Q=0\n", + "!"a<1" & !"b>2" & !dead\n", "\n", "\n", "12->16\n", - "\n", - "\n", - "!"a<1" & !"b>2" & !dead\n", + "\n", + "\n", "\n", "\n", "17\n", - "\n", - "a=2, b=3, Q=0\n", + "\n", + "a=2, b=3, Q=0\n", + "!"a<1" & "b>2" & !dead\n", "\n", "\n", "12->17\n", - "\n", - "\n", - "!"a<1" & !"b>2" & !dead\n", + "\n", + "\n", "\n", "\n", "18\n", - "\n", - "a=2, b=2, Q=1\n", + "\n", + "a=2, b=2, Q=1\n", + "!"a<1" & !"b>2" & !dead\n", "\n", "\n", "12->18\n", - "\n", - "\n", - "!"a<1" & !"b>2" & !dead\n", + "\n", + "\n", "\n", "\n", "19\n", - "\n", - "a=1, b=3, Q=1\n", + "\n", + "a=1, b=3, Q=1\n", + "!"a<1" & "b>2" & dead\n", "\n", "\n", "13->19\n", - "\n", - "\n", - "!"a<1" & "b>2" & !dead\n", + "\n", + "\n", "\n", "\n", "14->18\n", - "\n", - "\n", - "!"a<1" & !"b>2" & !dead\n", + "\n", + "\n", "\n", "\n", "14->19\n", - "\n", - "\n", - "!"a<1" & !"b>2" & !dead\n", + "\n", + "\n", "\n", "\n", "15->15\n", - "\n", - "\n", - ""a<1" & "b>2" & dead\n", + "\n", + "\n", "\n", "\n", "20\n", - "\n", - "a=3, b=2, Q=1\n", + "\n", + "a=3, b=2, Q=1\n", + "!"a<1" & !"b>2" & !dead\n", "\n", "\n", "16->20\n", - "\n", - "\n", - "!"a<1" & !"b>2" & !dead\n", + "\n", + "\n", "\n", "\n", "21\n", - "\n", - "a=2, b=3, Q=1\n", + "\n", + "a=2, b=3, Q=1\n", + "!"a<1" & "b>2" & !dead\n", "\n", "\n", "17->21\n", - "\n", - "\n", - "!"a<1" & "b>2" & !dead\n", + "\n", + "\n", "\n", "\n", "18->12\n", - "\n", - "\n", - "!"a<1" & !"b>2" & !dead\n", + "\n", + "\n", "\n", "\n", "18->20\n", - "\n", - "\n", - "!"a<1" & !"b>2" & !dead\n", + "\n", + "\n", "\n", "\n", "18->21\n", - "\n", - "\n", - "!"a<1" & !"b>2" & !dead\n", + "\n", + "\n", "\n", "\n", "19->19\n", - "\n", - "\n", - "!"a<1" & "b>2" & dead\n", + "\n", + "\n", "\n", "\n", "20->16\n", - "\n", - "\n", - "!"a<1" & !"b>2" & !dead\n", + "\n", + "\n", "\n", "\n", "21->17\n", - "\n", - "\n", - "!"a<1" & "b>2" & !dead\n", + "\n", + "\n", "\n", "\n", "" ], "text": [ - "" + "" ] } ], @@ -1044,51 +1012,51 @@ "\n", "\n", - "\n", + "\n", "\n", "G\n", - "\n", + "\n", "\n", - "\n", - "0\n", - "\n", - "1\n", - "\n", - "\n", - "I->0\n", - "\n", - "\n", - "\n", - "\n", - "0->0\n", - "\n", - "\n", - ""a<1" & !"b>2"\n", - "\n", "\n", - "1\n", - "\n", - "\n", - "0\n", + "1\n", + "\n", + "1\n", "\n", - "\n", - "0->1\n", - "\n", - "\n", - ""b>2"\n", + "\n", + "I->1\n", + "\n", + "\n", "\n", "\n", "1->1\n", - "\n", - "\n", - "1\n", + "\n", + "\n", + ""a<1" & !"b>2"\n", + "\n", + "\n", + "0\n", + "\n", + "\n", + "0\n", + "\n", + "\n", + "1->0\n", + "\n", + "\n", + ""b>2"\n", + "\n", + "\n", + "0->0\n", + "\n", + "\n", + "1\n", "\n", "\n", "\n" ], "text": [ - " *' at 0x7f7f00198690> >" + " *' at 0x7f9e12e0b060> >" ] } ], @@ -1250,11 +1218,19 @@ "\n" ], "text": [ - " *' at 0x7f7f00239cc0> >" + " *' at 0x7f9dfed0bf30> >" ] } ], "prompt_number": 10 + }, + { + "cell_type": "code", + "collapsed": false, + "input": [], + "language": "python", + "metadata": {}, + "outputs": [] } ], "metadata": {}