acc: make &= and |= symmetrical
Operator &= used to always move Fin to the front, it does not anymore.
The only thing it does now is to merge Inf(x)&Inf(y) as Inf({x,y}).
Operator |= is now symmetrical and merges Fin()s.
Fixes #253.
* spot/twa/acc.cc, spot/twa/acc.hh: Simplify &= and make |= symmetrical.
* spot/twaalgos/cleanacc.cc: Fix conjunction order.
* tests/core/acc.test, tests/core/acc2.test, tests/core/parseaut.test,
tests/core/readsave.test, tests/core/satmin2.test,
tests/core/sccdot.test, tests/python/acc_cond.ipynb,
tests/python/accparse.ipynb, tests/python/automata.ipynb,
tests/python/product.ipynb, tests/python/randaut.ipynb: Adjust test
cases.
This commit is contained in:
Alexandre Duret-Lutz
parent
8e685e00c9
commit
abe2c08b78
15 changed files with 254 additions and 295 deletions
6
NEWS
6
NEWS
|
|
@ -156,6 +156,12 @@ New in spot 2.3.5.dev (not yet released)
|
|||
- If the SPOT_BDD_TRACE envorinment variable is set, statistics
|
||||
about BDD garbage collection and table resizing are shown.
|
||||
|
||||
- The & and | operators for acceptannce conditions have been changed
|
||||
slightly to be more symmetrical. In older version, operator &
|
||||
would move Fin() terms to the front, but that is not the case
|
||||
anymore. Also operator & was already grouping all Inf() terms
|
||||
(for efficiency reasons), in this version operator | is
|
||||
symmetrically grouping all Fin() terms.
|
||||
|
||||
Python:
|
||||
|
||||
|
|
|
|||
|
|
@ -914,7 +914,7 @@ namespace spot
|
|||
while ((cube = isop.next()) != bddfalse)
|
||||
{
|
||||
mark_t i = 0U;
|
||||
acc_code c;
|
||||
acc_code f;
|
||||
while (cube != bddtrue)
|
||||
{
|
||||
// The acceptance set associated to this BDD variable
|
||||
|
|
@ -928,8 +928,7 @@ namespace spot
|
|||
// The strange order here make sure we can smaller set
|
||||
// numbers at the end of the acceptance code, i.e., at
|
||||
// the front of the output.
|
||||
auto a = fin(s) & std::move(c);
|
||||
std::swap(a, c);
|
||||
f = fin(s) & f;
|
||||
}
|
||||
else // Positive variable? -> Inf
|
||||
{
|
||||
|
|
@ -937,10 +936,8 @@ namespace spot
|
|||
cube = h;
|
||||
}
|
||||
}
|
||||
c &= inf(i);
|
||||
// See comment above for the order.
|
||||
c |= std::move(rescode);
|
||||
std::swap(c, rescode);
|
||||
rescode = (inf(i) & f) | rescode;
|
||||
}
|
||||
|
||||
return rescode;
|
||||
|
|
@ -986,7 +983,7 @@ namespace spot
|
|||
while ((cube = isop.next()) != bddfalse)
|
||||
{
|
||||
mark_t m = 0U;
|
||||
acc_code c = f();
|
||||
acc_code i = f();
|
||||
while (cube != bddtrue)
|
||||
{
|
||||
// The acceptance set associated to this BDD variable
|
||||
|
|
@ -1000,8 +997,7 @@ namespace spot
|
|||
// The strange order here make sure we can smaller set
|
||||
// numbers at the end of the acceptance code, i.e., at
|
||||
// the front of the output.
|
||||
auto a = inf(s) | std::move(c);
|
||||
std::swap(a, c);
|
||||
i = inf(s) | i;
|
||||
}
|
||||
else // Positive variable? -> Fin
|
||||
{
|
||||
|
|
@ -1009,10 +1005,8 @@ namespace spot
|
|||
cube = h;
|
||||
}
|
||||
}
|
||||
c |= fin(m);
|
||||
// See comment above for the order.
|
||||
c &= std::move(rescode);
|
||||
std::swap(c, rescode);
|
||||
rescode = (fin(m) | i) & rescode;
|
||||
}
|
||||
return rescode;
|
||||
}
|
||||
|
|
|
|||
212
spot/twa/acc.hh
212
spot/twa/acc.hh
|
|
@ -578,11 +578,11 @@ namespace spot
|
|||
unsigned n = 0;
|
||||
for (Iterator i = begin; i != end; ++i)
|
||||
{
|
||||
acc_cond::acc_code pair = fin({n++});
|
||||
unsigned f = n++;
|
||||
acc_cond::mark_t m = 0U;
|
||||
for (unsigned ni = *i; ni > 0; --ni)
|
||||
m.set(n++);
|
||||
pair &= inf(m);
|
||||
auto pair = inf(m) & fin({f});
|
||||
std::swap(pair, res);
|
||||
res |= std::move(pair);
|
||||
}
|
||||
|
|
@ -596,100 +596,6 @@ namespace spot
|
|||
// acceptance formula.
|
||||
static acc_code random(unsigned n, double reuse = 0.0);
|
||||
|
||||
acc_code& operator&=(acc_code&& r)
|
||||
{
|
||||
if (is_t() || r.is_f())
|
||||
{
|
||||
*this = std::move(r);
|
||||
return *this;
|
||||
}
|
||||
if (is_f() || r.is_t())
|
||||
return *this;
|
||||
unsigned s = size() - 1;
|
||||
unsigned rs = r.size() - 1;
|
||||
// We want to group all Inf(x) operators:
|
||||
// Inf(a) & Inf(b) = Inf(a & b)
|
||||
if (((*this)[s].sub.op == acc_op::Inf
|
||||
&& r[rs].sub.op == acc_op::Inf)
|
||||
|| ((*this)[s].sub.op == acc_op::InfNeg
|
||||
&& r[rs].sub.op == acc_op::InfNeg))
|
||||
{
|
||||
(*this)[s - 1].mark |= r[rs - 1].mark;
|
||||
return *this;
|
||||
}
|
||||
|
||||
// In the more complex scenarios, left and right may both
|
||||
// be conjunctions, and Inf(x) might be a member of each
|
||||
// side. Find it if it exists.
|
||||
// left_inf points to the left Inf mark if any.
|
||||
// right_inf points to the right Inf mark if any.
|
||||
acc_word* left_inf = nullptr;
|
||||
if ((*this)[s].sub.op == acc_op::And)
|
||||
{
|
||||
auto start = &(*this)[s] - (*this)[s].sub.size;
|
||||
auto pos = &(*this)[s] - 1;
|
||||
pop_back();
|
||||
while (pos > start)
|
||||
{
|
||||
if (pos->sub.op == acc_op::Inf)
|
||||
{
|
||||
left_inf = pos - 1;
|
||||
break;
|
||||
}
|
||||
pos -= pos->sub.size + 1;
|
||||
}
|
||||
}
|
||||
else if ((*this)[s].sub.op == acc_op::Inf)
|
||||
{
|
||||
left_inf = &(*this)[s - 1];
|
||||
}
|
||||
|
||||
acc_word* right_inf = nullptr;
|
||||
auto right_end = &r.back();
|
||||
if (right_end->sub.op == acc_op::And)
|
||||
{
|
||||
auto start = &r[0];
|
||||
auto pos = --right_end;
|
||||
while (pos > start)
|
||||
{
|
||||
if (pos->sub.op == acc_op::Inf)
|
||||
{
|
||||
right_inf = pos - 1;
|
||||
break;
|
||||
}
|
||||
pos -= pos->sub.size + 1;
|
||||
}
|
||||
}
|
||||
else if (right_end->sub.op == acc_op::Inf)
|
||||
{
|
||||
right_inf = right_end - 1;
|
||||
}
|
||||
|
||||
if (left_inf && right_inf)
|
||||
{
|
||||
left_inf->mark |= right_inf->mark;
|
||||
insert(this->end(), &r[0], right_inf);
|
||||
insert(this->end(), right_inf + 2, right_end + 1);
|
||||
}
|
||||
else if (right_inf)
|
||||
{
|
||||
// Always insert Inf() at the very first entry.
|
||||
insert(this->begin(), right_inf, right_inf + 2);
|
||||
insert(this->end(), &r[0], right_inf);
|
||||
insert(this->end(), right_inf + 2, right_end + 1);
|
||||
}
|
||||
else
|
||||
{
|
||||
insert(this->end(), &r[0], right_end + 1);
|
||||
}
|
||||
|
||||
acc_word w;
|
||||
w.sub.op = acc_op::And;
|
||||
w.sub.size = size();
|
||||
emplace_back(w);
|
||||
return *this;
|
||||
}
|
||||
|
||||
acc_code& operator&=(const acc_code& r)
|
||||
{
|
||||
if (is_t() || r.is_f())
|
||||
|
|
@ -701,7 +607,8 @@ namespace spot
|
|||
return *this;
|
||||
unsigned s = size() - 1;
|
||||
unsigned rs = r.size() - 1;
|
||||
// Inf(a) & Inf(b) = Inf(a & b)
|
||||
// We want to group all Inf(x) operators:
|
||||
// Inf(a) & Inf(b) = Inf(a & b)
|
||||
if (((*this)[s].sub.op == acc_op::Inf
|
||||
&& r[rs].sub.op == acc_op::Inf)
|
||||
|| ((*this)[s].sub.op == acc_op::InfNeg
|
||||
|
|
@ -758,23 +665,17 @@ namespace spot
|
|||
right_inf = right_end - 1;
|
||||
}
|
||||
|
||||
acc_cond::mark_t carry = 0U;
|
||||
if (left_inf && right_inf)
|
||||
{
|
||||
left_inf->mark |= right_inf->mark;
|
||||
insert(this->end(), &r[0], right_inf);
|
||||
insert(this->end(), right_inf + 2, right_end + 1);
|
||||
}
|
||||
else if (right_inf)
|
||||
{
|
||||
// Always insert Inf() at the very first entry.
|
||||
insert(this->begin(), right_inf, right_inf + 2);
|
||||
insert(this->end(), &r[0], right_inf);
|
||||
insert(this->end(), right_inf + 2, right_end + 1);
|
||||
}
|
||||
else
|
||||
{
|
||||
insert(this->end(), &r[0], right_end + 1);
|
||||
carry = left_inf->mark;
|
||||
auto pos = left_inf - &(*this)[0];
|
||||
erase(begin() + pos, begin() + pos + 2);
|
||||
}
|
||||
auto sz = size();
|
||||
insert(end(), &r[0], right_end + 1);
|
||||
if (carry)
|
||||
(*this)[sz + (right_inf - &r[0])].mark |= carry;
|
||||
|
||||
acc_word w;
|
||||
w.sub.op = acc_op::And;
|
||||
|
|
@ -783,6 +684,11 @@ namespace spot
|
|||
return *this;
|
||||
}
|
||||
|
||||
acc_code operator&(const acc_code& r)
|
||||
{
|
||||
return *this &= r;
|
||||
}
|
||||
|
||||
acc_code operator&(acc_code&& r)
|
||||
{
|
||||
acc_code res = *this;
|
||||
|
|
@ -790,20 +696,13 @@ namespace spot
|
|||
return res;
|
||||
}
|
||||
|
||||
acc_code operator&(const acc_code& r)
|
||||
{
|
||||
acc_code res = *this;
|
||||
res &= r;
|
||||
return res;
|
||||
}
|
||||
|
||||
acc_code& operator|=(acc_code&& r)
|
||||
acc_code& operator|=(const acc_code& r)
|
||||
{
|
||||
if (is_t() || r.is_f())
|
||||
return *this;
|
||||
if (is_f() || r.is_t())
|
||||
{
|
||||
*this = std::move(r);
|
||||
*this = r;
|
||||
return *this;
|
||||
}
|
||||
unsigned s = size() - 1;
|
||||
|
|
@ -817,11 +716,65 @@ namespace spot
|
|||
(*this)[s - 1].mark |= r[rs - 1].mark;
|
||||
return *this;
|
||||
}
|
||||
|
||||
// In the more complex scenarios, left and right may both
|
||||
// be disjunctions, and Fin(x) might be a member of each
|
||||
// side. Find it if it exists.
|
||||
// left_inf points to the left Inf mark if any.
|
||||
// right_inf points to the right Inf mark if any.
|
||||
acc_word* left_fin = nullptr;
|
||||
if ((*this)[s].sub.op == acc_op::Or)
|
||||
pop_back();
|
||||
if (r.back().sub.op == acc_op::Or)
|
||||
r.pop_back();
|
||||
insert(this->end(), r.begin(), r.end());
|
||||
{
|
||||
auto start = &(*this)[s] - (*this)[s].sub.size;
|
||||
auto pos = &(*this)[s] - 1;
|
||||
pop_back();
|
||||
while (pos > start)
|
||||
{
|
||||
if (pos->sub.op == acc_op::Fin)
|
||||
{
|
||||
left_fin = pos - 1;
|
||||
break;
|
||||
}
|
||||
pos -= pos->sub.size + 1;
|
||||
}
|
||||
}
|
||||
else if ((*this)[s].sub.op == acc_op::Fin)
|
||||
{
|
||||
left_fin = &(*this)[s - 1];
|
||||
}
|
||||
|
||||
const acc_word* right_fin = nullptr;
|
||||
auto right_end = &r.back();
|
||||
if (right_end->sub.op == acc_op::Or)
|
||||
{
|
||||
auto start = &r[0];
|
||||
auto pos = --right_end;
|
||||
while (pos > start)
|
||||
{
|
||||
if (pos->sub.op == acc_op::Fin)
|
||||
{
|
||||
right_fin = pos - 1;
|
||||
break;
|
||||
}
|
||||
pos -= pos->sub.size + 1;
|
||||
}
|
||||
}
|
||||
else if (right_end->sub.op == acc_op::Fin)
|
||||
{
|
||||
right_fin = right_end - 1;
|
||||
}
|
||||
|
||||
acc_cond::mark_t carry = 0U;
|
||||
if (left_fin && right_fin)
|
||||
{
|
||||
carry = left_fin->mark;
|
||||
auto pos = (left_fin - &(*this)[0]);
|
||||
this->erase(begin() + pos, begin() + pos + 2);
|
||||
}
|
||||
auto sz = size();
|
||||
insert(end(), &r[0], right_end + 1);
|
||||
if (carry)
|
||||
(*this)[sz + (right_fin - &r[0])].mark |= carry;
|
||||
acc_word w;
|
||||
w.sub.op = acc_op::Or;
|
||||
w.sub.size = size();
|
||||
|
|
@ -829,11 +782,6 @@ namespace spot
|
|||
return *this;
|
||||
}
|
||||
|
||||
acc_code& operator|=(const acc_code& r)
|
||||
{
|
||||
return *this |= acc_code(r);
|
||||
}
|
||||
|
||||
acc_code operator|(acc_code&& r)
|
||||
{
|
||||
acc_code res = *this;
|
||||
|
|
@ -841,11 +789,9 @@ namespace spot
|
|||
return res;
|
||||
}
|
||||
|
||||
acc_code operator|(const acc_code& r)
|
||||
acc_code& operator|(const acc_code& r)
|
||||
{
|
||||
acc_code res = *this;
|
||||
res |= r;
|
||||
return res;
|
||||
return *this |= r;
|
||||
}
|
||||
|
||||
acc_code& operator<<=(unsigned sets)
|
||||
|
|
|
|||
|
|
@ -193,8 +193,7 @@ namespace spot
|
|||
for (auto m: seen_fin.sets())
|
||||
inf.front().mark -= complement[m];
|
||||
|
||||
res &= inf;
|
||||
return res;
|
||||
return inf & res;
|
||||
}
|
||||
case acc_cond::acc_op::Or:
|
||||
{
|
||||
|
|
@ -225,8 +224,7 @@ namespace spot
|
|||
for (auto m: seen_inf.sets())
|
||||
fin.front().mark -= complement[m];
|
||||
|
||||
res |= fin;
|
||||
return res;
|
||||
return res | fin;
|
||||
}
|
||||
case acc_cond::acc_op::Fin:
|
||||
return acc_cond::acc_code::fin(pos[-1].mark);
|
||||
|
|
|
|||
|
|
@ -64,12 +64,12 @@ stripping
|
|||
#1: {2}
|
||||
2 Inf(0)&Inf(1)&Inf(3) 1
|
||||
5 Fin(2) | (Inf(0)&Inf(1)&Inf(3)) 1
|
||||
7 Fin(0) | Fin(2) | (Inf(0)&Inf(1)&Inf(3)) 1
|
||||
7 Fin(0) | Fin(2) | (Inf(0)&Inf(1)&Inf(3)) 1
|
||||
7 Fin(0) | Fin(2) | (Inf(0)&Inf(1)&Inf(3)) 1
|
||||
10 (Fin(0)|Fin(1)) & (Fin(0) | Fin(2) | (Inf(0)&Inf(1)&Inf(3))) 0
|
||||
5 (Fin(0)|Fin(2)) | (Inf(0)&Inf(1)&Inf(3)) 1
|
||||
5 (Fin(0)|Fin(2)) | (Inf(0)&Inf(1)&Inf(3)) 1
|
||||
5 (Fin(0)|Fin(2)) | (Inf(0)&Inf(1)&Inf(3)) 1
|
||||
8 (Fin(0)|Fin(1)) & ((Fin(0)|Fin(2)) | (Inf(0)&Inf(1)&Inf(3))) 0
|
||||
2 f 1
|
||||
9 (Fin(0)|Fin(1)) | Fin(0) | Fin(2) | (Inf(0)&Inf(1)&Inf(3)) 1
|
||||
5 (Fin(0)|Fin(1)|Fin(2)) | (Inf(0)&Inf(1)&Inf(3)) 1
|
||||
5 (Fin(2)|Fin(3)) & (Inf(0)&Inf(1)) 0
|
||||
(Fin(2)|Fin(3)) & (Inf(0)&Inf(1)) {0} true
|
||||
{1}
|
||||
|
|
@ -82,9 +82,9 @@ f
|
|||
Fin(2)
|
||||
Inf(2)
|
||||
Fin(2) | Inf(2)
|
||||
Fin(2) & Inf(2)
|
||||
Fin(0) | (Fin(2) & Inf(1)) | Fin(3)
|
||||
Fin(0) | (Fin(2) & Inf(1)) | Fin(3)
|
||||
Inf(2) & Fin(2)
|
||||
(Fin(0)|Fin(3)) | (Inf(1) & Fin(2))
|
||||
(Fin(0)|Fin(3)) | (Inf(1) & Fin(2))
|
||||
EOF
|
||||
|
||||
run 0 ../acc | tee stdout
|
||||
|
|
|
|||
|
|
@ -1,6 +1,6 @@
|
|||
#!/bin/sh
|
||||
# -*- coding: utf-8 -*-
|
||||
# Copyright (C) 2015 Laboratoire de Recherche et Développement
|
||||
# Copyright (C) 2015, 2017 Laboratoire de Recherche et Développement
|
||||
# de l'Epita (LRDE).
|
||||
#
|
||||
# This file is part of Spot, a model checking library.
|
||||
|
|
@ -71,13 +71,13 @@ diff acceptances output
|
|||
|
||||
#------------- CNF -------------
|
||||
|
||||
res="(Fin(2) | Inf(1)) & (Fin(1) | Inf(3)) & Inf(0)"
|
||||
res="Inf(0) & (Inf(1) | Fin(2)) & (Inf(3) | Fin(1))"
|
||||
cat >acceptances<<EOF
|
||||
2 Inf(0)&Inf(1), 2 Inf(0)&Inf(1)
|
||||
2 Fin(0) & Inf(1), 2 Fin(0) & Inf(1)
|
||||
2 t, 2 t
|
||||
2 f, 2 f
|
||||
3 (Inf(1) | Fin(2)) & Inf(0), 3 (Fin(2) | Inf(1)) & Inf(0)
|
||||
3 (Inf(1) | Fin(2)) & Inf(0), 3 Inf(0) & (Inf(1) | Fin(2))
|
||||
4 (Fin(1) & Fin(2) & Inf(0)) | (Inf(0)&Inf(1)&Inf(3)), 4 $res
|
||||
4 $res, 4 $res
|
||||
3 (Fin(0) & Fin(2)) | (Fin(1) & Fin(2)), 3 (Fin(0)|Fin(1)) & Fin(2)
|
||||
|
|
@ -94,7 +94,7 @@ diff acceptances output
|
|||
#------------- COMP -------------
|
||||
|
||||
a="(Inf(1) | Fin(2)) & (Fin(1) | Inf(3)) & Inf(0)"
|
||||
b="(Fin(1) & Inf(2)) | (Fin(3) & Inf(1)) | Fin(0)"
|
||||
b="(Fin(1) & Inf(2)) | (Inf(1) & Fin(3)) | Fin(0)"
|
||||
cat >acceptances<<EOF
|
||||
2 Inf(0)&Inf(1), 2 Fin(0)|Fin(1)
|
||||
2 Fin(0) & Inf(1), 2 Inf(0) | Fin(1)
|
||||
|
|
@ -102,7 +102,7 @@ cat >acceptances<<EOF
|
|||
2 f, 2 t
|
||||
3 (Inf(1) | Fin(2)) & Inf(0), 3 (Fin(1) & Inf(2)) | Fin(0)
|
||||
4 $a, 4 $b
|
||||
4 $b, 4 (Inf(1) | Fin(2)) & (Inf(3) | Fin(1)) & Inf(0)
|
||||
4 $b, 4 (Inf(1) | Fin(2)) & (Fin(1) | Inf(3)) & Inf(0)
|
||||
3 (Fin(0)|Fin(1)) & Fin(2), 3 (Inf(0)&Inf(1)) | Inf(2)
|
||||
EOF
|
||||
|
||||
|
|
|
|||
|
|
@ -2508,7 +2508,7 @@ HOA: v1
|
|||
States: 1
|
||||
Start: 0
|
||||
AP: 2 "a" "b"
|
||||
Acceptance: 4 (Fin(1) & Inf(0)) | (Fin(3) & Inf(2))
|
||||
Acceptance: 4 (Inf(0) & Fin(1)) | (Inf(2) & Fin(3))
|
||||
properties: trans-labels explicit-labels trans-acc complete
|
||||
properties: deterministic
|
||||
--BODY--
|
||||
|
|
@ -2522,7 +2522,7 @@ HOA: v1
|
|||
States: 1
|
||||
Start: 0
|
||||
AP: 2 "a" "b"
|
||||
Acceptance: 4 (Fin(3) & Inf(2)) | (Fin(1) & Inf(0))
|
||||
Acceptance: 4 (Fin(3) & Inf(2)) | (Inf(0) & Fin(1))
|
||||
properties: trans-labels explicit-labels trans-acc complete
|
||||
properties: deterministic
|
||||
--BODY--
|
||||
|
|
@ -2536,7 +2536,7 @@ HOA: v1
|
|||
States: 1
|
||||
Start: 0
|
||||
AP: 2 "a" "b"
|
||||
Acceptance: 6 (Inf(1) | (Fin(2)|Fin(3))) & (Inf(4) | Fin(5)) & Inf(0)
|
||||
Acceptance: 6 Inf(0) & (Inf(1) | (Fin(2)|Fin(3))) & (Inf(4) | Fin(5))
|
||||
properties: trans-labels explicit-labels trans-acc complete
|
||||
properties: deterministic
|
||||
--BODY--
|
||||
|
|
@ -2550,7 +2550,7 @@ HOA: v1
|
|||
States: 1
|
||||
Start: 0
|
||||
AP: 2 "a" "b"
|
||||
Acceptance: 6 (Inf(4) | Fin(5)) & (Inf(1) | (Fin(2)|Fin(3))) & Inf(0)
|
||||
Acceptance: 6 (Fin(5) | Inf(4)) & Inf(0) & ((Fin(2)|Fin(3)) | Inf(1))
|
||||
properties: trans-labels explicit-labels trans-acc complete
|
||||
properties: deterministic
|
||||
--BODY--
|
||||
|
|
@ -2624,7 +2624,7 @@ HOA: v1
|
|||
States: 1
|
||||
Start: 0
|
||||
AP: 2 "a" "b"
|
||||
Acceptance: 4 Fin(0) & ((Fin(2) & Inf(3)) | Inf(1))
|
||||
Acceptance: 4 Fin(0) & ((Inf(3) & Fin(2)) | Inf(1))
|
||||
properties: trans-labels explicit-labels trans-acc complete
|
||||
properties: deterministic
|
||||
--BODY--
|
||||
|
|
|
|||
|
|
@ -470,7 +470,7 @@ EOF
|
|||
cat >expected <<EOF
|
||||
digraph G {
|
||||
rankdir=LR
|
||||
label="Fin(⓿) | (Fin(❶) & Inf(❷)) | Fin(❸)"
|
||||
label="(Fin(⓿)|Fin(❸)) | (Fin(❶) & Inf(❷))"
|
||||
labelloc="t"
|
||||
I [label="", style=invis, width=0]
|
||||
I -> 0
|
||||
|
|
@ -524,7 +524,7 @@ diff out expected
|
|||
cat >expected2 <<EOF
|
||||
digraph G {
|
||||
rankdir=LR
|
||||
label="Fin(⓿) | (Fin(❶) & Inf(❷)) | Fin(❸)"
|
||||
label="(Fin(⓿)|Fin(❸)) | (Fin(❶) & Inf(❷))"
|
||||
labelloc="t"
|
||||
node [shape="circle"]
|
||||
I [label="", style=invis, width=0]
|
||||
|
|
|
|||
|
|
@ -335,7 +335,7 @@ HOA: v1
|
|||
States: 1
|
||||
Start: 0
|
||||
AP: 1 "a"
|
||||
Acceptance: 2 (Fin(1) & Inf(0)) | (Fin(0) & Inf(1))
|
||||
Acceptance: 2 (Inf(0) & Fin(1)) | (Fin(0) & Inf(1))
|
||||
properties: trans-labels explicit-labels trans-acc colored complete
|
||||
properties: deterministic
|
||||
--BODY--
|
||||
|
|
|
|||
|
|
@ -74,7 +74,7 @@ run 0 autfilt --dot=as in.hoa > out.dot
|
|||
cat <<EOF >expected
|
||||
digraph G {
|
||||
rankdir=LR
|
||||
label="Fin(2) & (Inf(0)&Inf(1))"
|
||||
label="(Inf(0)&Inf(1)) & Fin(2)"
|
||||
labelloc="t"
|
||||
node [shape="circle"]
|
||||
I [label="", style=invis, width=0]
|
||||
|
|
@ -156,7 +156,7 @@ HOA: v1
|
|||
States: 8
|
||||
Start: 0
|
||||
AP: 2 "a" "b"
|
||||
Acceptance: 3 Fin(2) & (Inf(0)&Inf(1))
|
||||
Acceptance: 3 (Inf(0)&Inf(1)) & Fin(2)
|
||||
properties: trans-labels explicit-labels trans-acc
|
||||
--BODY--
|
||||
State: 0
|
||||
|
|
|
|||
|
|
@ -15,7 +15,7 @@
|
|||
"name": "python",
|
||||
"nbconvert_exporter": "python",
|
||||
"pygments_lexer": "ipython3",
|
||||
"version": "3.5.3"
|
||||
"version": "3.5.3+"
|
||||
},
|
||||
"name": ""
|
||||
},
|
||||
|
|
@ -489,7 +489,7 @@
|
|||
"output_type": "pyout",
|
||||
"prompt_number": 17,
|
||||
"text": [
|
||||
"(Fin(1) & Inf(0)) | Inf(2)"
|
||||
"(Inf(0) & Fin(1)) | Inf(2)"
|
||||
]
|
||||
}
|
||||
],
|
||||
|
|
@ -571,7 +571,7 @@
|
|||
"output_type": "pyout",
|
||||
"prompt_number": 20,
|
||||
"text": [
|
||||
"(Fin(3) | Inf(1)) & (Fin(0)|Fin(2)) & Inf(4)"
|
||||
"(Fin(3) | Inf(1)) & Inf(4) & (Fin(0)|Fin(2))"
|
||||
]
|
||||
}
|
||||
],
|
||||
|
|
@ -619,7 +619,7 @@
|
|||
"output_type": "pyout",
|
||||
"prompt_number": 22,
|
||||
"text": [
|
||||
"Fin(0) & (Fin(2) | Inf(1)) & (Fin(4) | Inf(1) | Inf(3))"
|
||||
"Fin(0) & (Inf(1) | Fin(2)) & (Inf(1) | Inf(3) | Fin(4))"
|
||||
]
|
||||
}
|
||||
],
|
||||
|
|
@ -720,8 +720,8 @@
|
|||
"output_type": "stream",
|
||||
"stream": "stdout",
|
||||
"text": [
|
||||
"(Fin(0) & Inf(1)) | (Fin(2) & Inf(3))\n",
|
||||
"(Inf(0) | Fin(1)) & (Inf(2) | Fin(3))\n"
|
||||
"((Fin(4) & Inf(5)) | (Fin(6) & Inf(7))) & ((Fin(0) & Inf(1)) | (Fin(2) & Inf(3)))\n",
|
||||
"((Inf(4) | Fin(5)) & (Inf(6) | Fin(7))) | ((Inf(0) | Fin(1)) & (Inf(2) | Fin(3)))\n"
|
||||
]
|
||||
}
|
||||
],
|
||||
|
|
|
|||
|
|
@ -15,10 +15,9 @@
|
|||
"name": "python",
|
||||
"nbconvert_exporter": "python",
|
||||
"pygments_lexer": "ipython3",
|
||||
"version": "3.4.3+"
|
||||
"version": "3.5.3+"
|
||||
},
|
||||
"name": "",
|
||||
"signature": "sha256:1ee7951bed30652ae110a14b210541829221552eb944ff01f25236179673dd5b"
|
||||
"name": ""
|
||||
},
|
||||
"nbformat": 3,
|
||||
"nbformat_minor": 0,
|
||||
|
|
@ -51,7 +50,7 @@
|
|||
"output_type": "pyout",
|
||||
"prompt_number": 2,
|
||||
"text": [
|
||||
"(Fin(1) & Inf(0)) | (Fin(3) & Inf(2))"
|
||||
"(Inf(0) & Fin(1)) | (Inf(2) & Fin(3))"
|
||||
]
|
||||
}
|
||||
],
|
||||
|
|
@ -91,7 +90,7 @@
|
|||
"output_type": "pyout",
|
||||
"prompt_number": 4,
|
||||
"text": [
|
||||
"(Inf(0) | Inf(2)) & (Fin(3) | Inf(0)) & (Fin(1) | Inf(2)) & (Fin(1)|Fin(3))"
|
||||
"(Inf(0) | Inf(2)) & (Inf(0) | Fin(3)) & (Inf(2) | Fin(1)) & (Fin(1)|Fin(3))"
|
||||
]
|
||||
}
|
||||
],
|
||||
|
|
|
|||
|
|
@ -15,7 +15,7 @@
|
|||
"name": "python",
|
||||
"nbconvert_exporter": "python",
|
||||
"pygments_lexer": "ipython3",
|
||||
"version": "3.5.3"
|
||||
"version": "3.5.3+"
|
||||
},
|
||||
"name": ""
|
||||
},
|
||||
|
|
@ -177,7 +177,7 @@
|
|||
"</svg>\n"
|
||||
],
|
||||
"text": [
|
||||
"<spot.impl.twa_graph; proxy of <Swig Object of type 'std::shared_ptr< spot::twa_graph > *' at 0x7f9ae817a8d0> >"
|
||||
"<spot.impl.twa_graph; proxy of <Swig Object of type 'std::shared_ptr< spot::twa_graph > *' at 0x7f364c1ff810> >"
|
||||
]
|
||||
}
|
||||
],
|
||||
|
|
@ -569,7 +569,7 @@
|
|||
"</svg>\n"
|
||||
],
|
||||
"text": [
|
||||
"<spot.impl.twa_graph; proxy of <Swig Object of type 'std::shared_ptr< spot::twa_graph > *' at 0x7f9ae816aa20> >"
|
||||
"<spot.impl.twa_graph; proxy of <Swig Object of type 'std::shared_ptr< spot::twa_graph > *' at 0x7f364c1ff720> >"
|
||||
]
|
||||
}
|
||||
],
|
||||
|
|
@ -639,7 +639,7 @@
|
|||
"</svg>\n"
|
||||
],
|
||||
"text": [
|
||||
"<spot.impl.twa_graph; proxy of <Swig Object of type 'std::shared_ptr< spot::twa_graph > *' at 0x7f9ae816a4b0> >"
|
||||
"<spot.impl.twa_graph; proxy of <Swig Object of type 'std::shared_ptr< spot::twa_graph > *' at 0x7f364c18dbd0> >"
|
||||
]
|
||||
}
|
||||
],
|
||||
|
|
@ -715,7 +715,7 @@
|
|||
"</svg>\n"
|
||||
],
|
||||
"text": [
|
||||
"<spot.impl.twa_graph; proxy of <Swig Object of type 'std::shared_ptr< spot::twa_graph > *' at 0x7f9ae816a300> >"
|
||||
"<spot.impl.twa_graph; proxy of <Swig Object of type 'std::shared_ptr< spot::twa_graph > *' at 0x7f364c18d150> >"
|
||||
]
|
||||
}
|
||||
],
|
||||
|
|
@ -1175,7 +1175,7 @@
|
|||
"</svg>\n"
|
||||
],
|
||||
"text": [
|
||||
"<spot.impl.twa_graph; proxy of <Swig Object of type 'std::shared_ptr< spot::twa_graph > *' at 0x7f9ae816a9f0> >"
|
||||
"<spot.impl.twa_graph; proxy of <Swig Object of type 'std::shared_ptr< spot::twa_graph > *' at 0x7f364c18df00> >"
|
||||
]
|
||||
}
|
||||
],
|
||||
|
|
@ -1276,7 +1276,7 @@
|
|||
"</svg>\n"
|
||||
],
|
||||
"text": [
|
||||
"<spot.impl.twa_graph; proxy of <Swig Object of type 'std::shared_ptr< spot::twa_graph > *' at 0x7f9ae816a870> >"
|
||||
"<spot.impl.twa_graph; proxy of <Swig Object of type 'std::shared_ptr< spot::twa_graph > *' at 0x7f364c18df30> >"
|
||||
]
|
||||
}
|
||||
],
|
||||
|
|
@ -1394,7 +1394,7 @@
|
|||
"</svg>\n"
|
||||
],
|
||||
"text": [
|
||||
"<spot.impl.twa_graph; proxy of <Swig Object of type 'std::shared_ptr< spot::twa_graph > *' at 0x7f9ae816a690> >"
|
||||
"<spot.impl.twa_graph; proxy of <Swig Object of type 'std::shared_ptr< spot::twa_graph > *' at 0x7f364c18d660> >"
|
||||
]
|
||||
}
|
||||
],
|
||||
|
|
@ -1493,7 +1493,7 @@
|
|||
"</svg>\n"
|
||||
],
|
||||
"text": [
|
||||
"<spot.impl.twa_graph; proxy of <Swig Object of type 'std::shared_ptr< spot::twa_graph > *' at 0x7f9ae816a6f0> >"
|
||||
"<spot.impl.twa_graph; proxy of <Swig Object of type 'std::shared_ptr< spot::twa_graph > *' at 0x7f364c18d870> >"
|
||||
]
|
||||
}
|
||||
],
|
||||
|
|
@ -1963,7 +1963,7 @@
|
|||
"</svg>\n"
|
||||
],
|
||||
"text": [
|
||||
"<spot.impl.twa_graph; proxy of <Swig Object of type 'std::shared_ptr< spot::twa_graph > *' at 0x7f9ae816a3f0> >"
|
||||
"<spot.impl.twa_graph; proxy of <Swig Object of type 'std::shared_ptr< spot::twa_graph > *' at 0x7f364c18ddb0> >"
|
||||
]
|
||||
}
|
||||
],
|
||||
|
|
@ -2056,12 +2056,12 @@
|
|||
"<g class=\"graph\" id=\"graph0\" transform=\"scale(1 1) rotate(0) translate(4 174.462)\">\n",
|
||||
"<title>G</title>\n",
|
||||
"<polygon fill=\"white\" points=\"-4,4 -4,-174.462 357,-174.462 357,4 -4,4\" stroke=\"none\"/>\n",
|
||||
"<text font-family=\"Lato\" font-size=\"14.00\" text-anchor=\"start\" x=\"8\" y=\"-156.262\">(Fin(</text>\n",
|
||||
"<text fill=\"#f17cb0\" font-family=\"Lato\" font-size=\"14.00\" text-anchor=\"start\" x=\"36\" y=\"-156.262\">\u2776</text>\n",
|
||||
"<text font-family=\"Lato\" font-size=\"14.00\" text-anchor=\"start\" x=\"52\" y=\"-156.262\">) & Fin(</text>\n",
|
||||
"<text fill=\"#b276b2\" font-family=\"Lato\" font-size=\"14.00\" text-anchor=\"start\" x=\"98\" y=\"-156.262\">\u2778</text>\n",
|
||||
"<text font-family=\"Lato\" font-size=\"14.00\" text-anchor=\"start\" x=\"114\" y=\"-156.262\">) & Inf(</text>\n",
|
||||
"<text fill=\"#5da5da\" font-family=\"Lato\" font-size=\"14.00\" text-anchor=\"start\" x=\"157\" y=\"-156.262\">\u24ff</text>\n",
|
||||
"<text font-family=\"Lato\" font-size=\"14.00\" text-anchor=\"start\" x=\"8\" y=\"-156.262\">(Inf(</text>\n",
|
||||
"<text fill=\"#5da5da\" font-family=\"Lato\" font-size=\"14.00\" text-anchor=\"start\" x=\"33\" y=\"-156.262\">\u24ff</text>\n",
|
||||
"<text font-family=\"Lato\" font-size=\"14.00\" text-anchor=\"start\" x=\"49\" y=\"-156.262\">) & Fin(</text>\n",
|
||||
"<text fill=\"#f17cb0\" font-family=\"Lato\" font-size=\"14.00\" text-anchor=\"start\" x=\"95\" y=\"-156.262\">\u2776</text>\n",
|
||||
"<text font-family=\"Lato\" font-size=\"14.00\" text-anchor=\"start\" x=\"111\" y=\"-156.262\">) & Fin(</text>\n",
|
||||
"<text fill=\"#b276b2\" font-family=\"Lato\" font-size=\"14.00\" text-anchor=\"start\" x=\"157\" y=\"-156.262\">\u2778</text>\n",
|
||||
"<text font-family=\"Lato\" font-size=\"14.00\" text-anchor=\"start\" x=\"173\" y=\"-156.262\">)) | (Inf(</text>\n",
|
||||
"<text fill=\"#faa43a\" font-family=\"Lato\" font-size=\"14.00\" text-anchor=\"start\" x=\"217\" y=\"-156.262\">\u2777</text>\n",
|
||||
"<text font-family=\"Lato\" font-size=\"14.00\" text-anchor=\"start\" x=\"233\" y=\"-156.262\">)&Inf(</text>\n",
|
||||
|
|
@ -2578,7 +2578,7 @@
|
|||
"</svg>\n"
|
||||
],
|
||||
"text": [
|
||||
"<spot.impl.twa_graph; proxy of <Swig Object of type 'std::shared_ptr< spot::twa_graph > *' at 0x7f9ae817a3f0> >"
|
||||
"<spot.impl.twa_graph; proxy of <Swig Object of type 'std::shared_ptr< spot::twa_graph > *' at 0x7f364c18de10> >"
|
||||
]
|
||||
}
|
||||
],
|
||||
|
|
@ -2734,7 +2734,7 @@
|
|||
"</svg>\n"
|
||||
],
|
||||
"text": [
|
||||
"<spot.impl.twa_graph; proxy of <Swig Object of type 'std::shared_ptr< spot::twa_graph > *' at 0x7f9ae816aab0> >"
|
||||
"<spot.impl.twa_graph; proxy of <Swig Object of type 'std::shared_ptr< spot::twa_graph > *' at 0x7f364c18d7b0> >"
|
||||
]
|
||||
}
|
||||
],
|
||||
|
|
@ -2804,7 +2804,7 @@
|
|||
"</svg>\n"
|
||||
],
|
||||
"text": [
|
||||
"<spot.impl.twa_graph; proxy of <Swig Object of type 'std::shared_ptr< spot::twa_graph > *' at 0x7f9ae816ae10> >"
|
||||
"<spot.impl.twa_graph; proxy of <Swig Object of type 'std::shared_ptr< spot::twa_graph > *' at 0x7f364c18de10> >"
|
||||
]
|
||||
}
|
||||
],
|
||||
|
|
@ -3231,7 +3231,7 @@
|
|||
"</svg>\n"
|
||||
],
|
||||
"text": [
|
||||
"<spot.impl.twa_graph; proxy of <Swig Object of type 'std::shared_ptr< spot::twa_graph > *' at 0x7f9ae816af60> >"
|
||||
"<spot.impl.twa_graph; proxy of <Swig Object of type 'std::shared_ptr< spot::twa_graph > *' at 0x7f364c1a9450> >"
|
||||
]
|
||||
},
|
||||
{
|
||||
|
|
@ -3399,7 +3399,7 @@
|
|||
"</svg>\n"
|
||||
],
|
||||
"text": [
|
||||
"<spot.impl.twa_graph; proxy of <Swig Object of type 'std::shared_ptr< spot::twa_graph > *' at 0x7f9ae81250f0> >"
|
||||
"<spot.impl.twa_graph; proxy of <Swig Object of type 'std::shared_ptr< spot::twa_graph > *' at 0x7f364c1a90c0> >"
|
||||
]
|
||||
}
|
||||
],
|
||||
|
|
@ -3488,7 +3488,7 @@
|
|||
"</svg>\n"
|
||||
],
|
||||
"text": [
|
||||
"<spot.impl.twa_graph; proxy of <Swig Object of type 'std::shared_ptr< spot::twa_graph > *' at 0x7f9ae81250f0> >"
|
||||
"<spot.impl.twa_graph; proxy of <Swig Object of type 'std::shared_ptr< spot::twa_graph > *' at 0x7f364c1a90c0> >"
|
||||
]
|
||||
}
|
||||
],
|
||||
|
|
@ -3577,7 +3577,7 @@
|
|||
"</svg>\n"
|
||||
],
|
||||
"text": [
|
||||
"<spot.impl.twa_graph; proxy of <Swig Object of type 'std::shared_ptr< spot::twa_graph > *' at 0x7f9ae81250f0> >"
|
||||
"<spot.impl.twa_graph; proxy of <Swig Object of type 'std::shared_ptr< spot::twa_graph > *' at 0x7f364c1a90c0> >"
|
||||
]
|
||||
}
|
||||
],
|
||||
|
|
|
|||
|
|
@ -15,7 +15,7 @@
|
|||
"name": "python",
|
||||
"nbconvert_exporter": "python",
|
||||
"pygments_lexer": "ipython3",
|
||||
"version": "3.5.3"
|
||||
"version": "3.5.3+"
|
||||
},
|
||||
"name": ""
|
||||
},
|
||||
|
|
@ -1191,60 +1191,64 @@
|
|||
"outputs": [
|
||||
{
|
||||
"html": [
|
||||
"<table><tr><td style=\"vertical-align: top;\"><svg height=\"294pt\" viewBox=\"0.00 0.00 99.00 294.00\" width=\"99pt\" xmlns=\"http://www.w3.org/2000/svg\" xmlns:xlink=\"http://www.w3.org/1999/xlink\">\n",
|
||||
"<table><tr><td style=\"vertical-align: top;\"><svg height=\"294pt\" viewBox=\"0.00 0.00 170.00 294.00\" width=\"170pt\" xmlns=\"http://www.w3.org/2000/svg\" xmlns:xlink=\"http://www.w3.org/1999/xlink\">\n",
|
||||
"<g class=\"graph\" id=\"graph0\" transform=\"scale(1 1) rotate(0) translate(4 290)\">\n",
|
||||
"<title>G</title>\n",
|
||||
"<polygon fill=\"white\" points=\"-4,4 -4,-290 95,-290 95,4 -4,4\" stroke=\"none\"/>\n",
|
||||
"<text font-family=\"Lato\" font-size=\"14.00\" text-anchor=\"start\" x=\"24.5\" y=\"-271.8\">Inf(</text>\n",
|
||||
"<text fill=\"#5da5da\" font-family=\"Lato\" font-size=\"14.00\" text-anchor=\"start\" x=\"46.5\" y=\"-271.8\">\u24ff</text>\n",
|
||||
"<text font-family=\"Lato\" font-size=\"14.00\" text-anchor=\"start\" x=\"62.5\" y=\"-271.8\">)</text>\n",
|
||||
"<polygon fill=\"white\" points=\"-4,4 -4,-290 166,-290 166,4 -4,4\" stroke=\"none\"/>\n",
|
||||
"<text font-family=\"Lato\" font-size=\"14.00\" text-anchor=\"start\" x=\"8\" y=\"-271.8\">Inf(</text>\n",
|
||||
"<text fill=\"#5da5da\" font-family=\"Lato\" font-size=\"14.00\" text-anchor=\"start\" x=\"30\" y=\"-271.8\">\u24ff</text>\n",
|
||||
"<text font-family=\"Lato\" font-size=\"14.00\" text-anchor=\"start\" x=\"46\" y=\"-271.8\">)&Inf(</text>\n",
|
||||
"<text fill=\"#f17cb0\" font-family=\"Lato\" font-size=\"14.00\" text-anchor=\"start\" x=\"82\" y=\"-271.8\">\u2776</text>\n",
|
||||
"<text font-family=\"Lato\" font-size=\"14.00\" text-anchor=\"start\" x=\"98\" y=\"-271.8\">)&Inf(</text>\n",
|
||||
"<text fill=\"#faa43a\" font-family=\"Lato\" font-size=\"14.00\" text-anchor=\"start\" x=\"134\" y=\"-271.8\">\u2777</text>\n",
|
||||
"<text font-family=\"Lato\" font-size=\"14.00\" text-anchor=\"start\" x=\"150\" y=\"-271.8\">)</text>\n",
|
||||
"<!-- I -->\n",
|
||||
"<!-- 1 -->\n",
|
||||
"<g class=\"node\" id=\"node2\"><title>1</title>\n",
|
||||
"<ellipse cx=\"18\" cy=\"-207\" fill=\"#ffffaa\" rx=\"18\" ry=\"18\" stroke=\"black\"/>\n",
|
||||
"<text font-family=\"Lato\" font-size=\"14.00\" text-anchor=\"middle\" x=\"18\" y=\"-203.3\">1</text>\n",
|
||||
"<ellipse cx=\"53.5\" cy=\"-207\" fill=\"#ffffaa\" rx=\"18\" ry=\"18\" stroke=\"black\"/>\n",
|
||||
"<text font-family=\"Lato\" font-size=\"14.00\" text-anchor=\"middle\" x=\"53.5\" y=\"-203.3\">1</text>\n",
|
||||
"</g>\n",
|
||||
"<!-- I->1 -->\n",
|
||||
"<g class=\"edge\" id=\"edge1\"><title>I->1</title>\n",
|
||||
"<path d=\"M18,-261.845C18,-260.206 18,-245.846 18,-232.368\" fill=\"none\" stroke=\"black\"/>\n",
|
||||
"<polygon fill=\"black\" points=\"18,-225.058 21.1501,-232.058 18,-228.558 18.0001,-232.058 18.0001,-232.058 18.0001,-232.058 18,-228.558 14.8501,-232.058 18,-225.058 18,-225.058\" stroke=\"black\"/>\n",
|
||||
"<path d=\"M53.5,-261.845C53.5,-260.206 53.5,-245.846 53.5,-232.368\" fill=\"none\" stroke=\"black\"/>\n",
|
||||
"<polygon fill=\"black\" points=\"53.5,-225.058 56.6501,-232.058 53.5,-228.558 53.5001,-232.058 53.5001,-232.058 53.5001,-232.058 53.5,-228.558 50.3501,-232.058 53.5,-225.058 53.5,-225.058\" stroke=\"black\"/>\n",
|
||||
"</g>\n",
|
||||
"<!-- 0 -->\n",
|
||||
"<g class=\"node\" id=\"node3\"><title>0</title>\n",
|
||||
"<ellipse cx=\"18\" cy=\"-120\" fill=\"#ffffaa\" rx=\"18\" ry=\"18\" stroke=\"black\"/>\n",
|
||||
"<text font-family=\"Lato\" font-size=\"14.00\" text-anchor=\"middle\" x=\"18\" y=\"-116.3\">0</text>\n",
|
||||
"<ellipse cx=\"53.5\" cy=\"-120\" fill=\"#ffffaa\" rx=\"18\" ry=\"18\" stroke=\"black\"/>\n",
|
||||
"<text font-family=\"Lato\" font-size=\"14.00\" text-anchor=\"middle\" x=\"53.5\" y=\"-116.3\">0</text>\n",
|
||||
"</g>\n",
|
||||
"<!-- 1->0 -->\n",
|
||||
"<g class=\"edge\" id=\"edge4\"><title>1->0</title>\n",
|
||||
"<path d=\"M18,-188.799C18,-176.356 18,-159.364 18,-145.504\" fill=\"none\" stroke=\"black\"/>\n",
|
||||
"<polygon fill=\"black\" points=\"18,-138.175 21.1501,-145.175 18,-141.675 18.0001,-145.175 18.0001,-145.175 18.0001,-145.175 18,-141.675 14.8501,-145.175 18,-138.175 18,-138.175\" stroke=\"black\"/>\n",
|
||||
"<text font-family=\"Lato\" font-size=\"14.00\" text-anchor=\"middle\" x=\"22.5\" y=\"-159.8\">1</text>\n",
|
||||
"<path d=\"M53.5,-188.799C53.5,-176.356 53.5,-159.364 53.5,-145.504\" fill=\"none\" stroke=\"black\"/>\n",
|
||||
"<polygon fill=\"black\" points=\"53.5,-138.175 56.6501,-145.175 53.5,-141.675 53.5001,-145.175 53.5001,-145.175 53.5001,-145.175 53.5,-141.675 50.3501,-145.175 53.5,-138.175 53.5,-138.175\" stroke=\"black\"/>\n",
|
||||
"<text font-family=\"Lato\" font-size=\"14.00\" text-anchor=\"middle\" x=\"58\" y=\"-159.8\">1</text>\n",
|
||||
"</g>\n",
|
||||
"<!-- 0->0 -->\n",
|
||||
"<g class=\"edge\" id=\"edge2\"><title>0->0</title>\n",
|
||||
"<path d=\"M34.6641,-127.383C44.625,-129.023 54,-126.562 54,-120 54,-115.078 48.7266,-112.463 41.8876,-112.156\" fill=\"none\" stroke=\"black\"/>\n",
|
||||
"<polygon fill=\"black\" points=\"34.6641,-112.617 41.449,-109.027 38.1569,-112.394 41.6498,-112.171 41.6498,-112.171 41.6498,-112.171 38.1569,-112.394 41.8507,-115.314 34.6641,-112.617 34.6641,-112.617\" stroke=\"black\"/>\n",
|
||||
"<text font-family=\"Lato\" font-size=\"14.00\" text-anchor=\"start\" x=\"54\" y=\"-123.8\">a & !b</text>\n",
|
||||
"<text fill=\"#5da5da\" font-family=\"Lato\" font-size=\"14.00\" text-anchor=\"start\" x=\"64.5\" y=\"-108.8\">\u24ff</text>\n",
|
||||
"<path d=\"M70.1641,-127.383C80.125,-129.023 89.5,-126.562 89.5,-120 89.5,-115.078 84.2266,-112.463 77.3876,-112.156\" fill=\"none\" stroke=\"black\"/>\n",
|
||||
"<polygon fill=\"black\" points=\"70.1641,-112.617 76.949,-109.027 73.6569,-112.394 77.1498,-112.171 77.1498,-112.171 77.1498,-112.171 73.6569,-112.394 77.3507,-115.314 70.1641,-112.617 70.1641,-112.617\" stroke=\"black\"/>\n",
|
||||
"<text font-family=\"Lato\" font-size=\"14.00\" text-anchor=\"start\" x=\"89.5\" y=\"-123.8\">a & !b</text>\n",
|
||||
"<text fill=\"#5da5da\" font-family=\"Lato\" font-size=\"14.00\" text-anchor=\"start\" x=\"100\" y=\"-108.8\">\u24ff</text>\n",
|
||||
"</g>\n",
|
||||
"<!-- 2 -->\n",
|
||||
"<g class=\"node\" id=\"node4\"><title>2</title>\n",
|
||||
"<ellipse cx=\"18\" cy=\"-18\" fill=\"#ffffaa\" rx=\"18\" ry=\"18\" stroke=\"black\"/>\n",
|
||||
"<text font-family=\"Lato\" font-size=\"14.00\" text-anchor=\"middle\" x=\"18\" y=\"-14.3\">2</text>\n",
|
||||
"<ellipse cx=\"53.5\" cy=\"-18\" fill=\"#ffffaa\" rx=\"18\" ry=\"18\" stroke=\"black\"/>\n",
|
||||
"<text font-family=\"Lato\" font-size=\"14.00\" text-anchor=\"middle\" x=\"53.5\" y=\"-14.3\">2</text>\n",
|
||||
"</g>\n",
|
||||
"<!-- 0->2 -->\n",
|
||||
"<g class=\"edge\" id=\"edge3\"><title>0->2</title>\n",
|
||||
"<path d=\"M18,-101.581C18,-85.5213 18,-61.5179 18,-43.5228\" fill=\"none\" stroke=\"black\"/>\n",
|
||||
"<polygon fill=\"black\" points=\"18,-36.2191 21.1501,-43.219 18,-39.7191 18.0001,-43.2191 18.0001,-43.2191 18.0001,-43.2191 18,-39.7191 14.8501,-43.2191 18,-36.2191 18,-36.2191\" stroke=\"black\"/>\n",
|
||||
"<text font-family=\"Lato\" font-size=\"14.00\" text-anchor=\"start\" x=\"21.5\" y=\"-72.8\">b</text>\n",
|
||||
"<text fill=\"#5da5da\" font-family=\"Lato\" font-size=\"14.00\" text-anchor=\"start\" x=\"18\" y=\"-57.8\">\u24ff</text>\n",
|
||||
"<path d=\"M53.5,-101.581C53.5,-85.5213 53.5,-61.5179 53.5,-43.5228\" fill=\"none\" stroke=\"black\"/>\n",
|
||||
"<polygon fill=\"black\" points=\"53.5,-36.2191 56.6501,-43.219 53.5,-39.7191 53.5001,-43.2191 53.5001,-43.2191 53.5001,-43.2191 53.5,-39.7191 50.3501,-43.2191 53.5,-36.2191 53.5,-36.2191\" stroke=\"black\"/>\n",
|
||||
"<text font-family=\"Lato\" font-size=\"14.00\" text-anchor=\"start\" x=\"57\" y=\"-72.8\">b</text>\n",
|
||||
"<text fill=\"#5da5da\" font-family=\"Lato\" font-size=\"14.00\" text-anchor=\"start\" x=\"53.5\" y=\"-57.8\">\u24ff</text>\n",
|
||||
"</g>\n",
|
||||
"<!-- 2->2 -->\n",
|
||||
"<g class=\"edge\" id=\"edge5\"><title>2->2</title>\n",
|
||||
"<path d=\"M33.916,-26.6334C44.1504,-28.8856 54,-26.0078 54,-18 54,-11.869 48.2263,-8.74515 40.9268,-8.6284\" fill=\"none\" stroke=\"black\"/>\n",
|
||||
"<polygon fill=\"black\" points=\"33.916,-9.36658 40.5477,-5.50081 37.3968,-9.00004 40.8775,-8.6335 40.8775,-8.6335 40.8775,-8.6335 37.3968,-9.00004 41.2074,-11.7662 33.916,-9.36658 33.916,-9.36658\" stroke=\"black\"/>\n",
|
||||
"<text font-family=\"Lato\" font-size=\"14.00\" text-anchor=\"start\" x=\"57.5\" y=\"-21.8\">1</text>\n",
|
||||
"<text fill=\"#5da5da\" font-family=\"Lato\" font-size=\"14.00\" text-anchor=\"start\" x=\"54\" y=\"-6.8\">\u24ff</text>\n",
|
||||
"<path d=\"M69.416,-26.6334C79.6504,-28.8856 89.5,-26.0078 89.5,-18 89.5,-11.869 83.7263,-8.74515 76.4268,-8.6284\" fill=\"none\" stroke=\"black\"/>\n",
|
||||
"<polygon fill=\"black\" points=\"69.416,-9.36658 76.0477,-5.50081 72.8968,-9.00004 76.3775,-8.6335 76.3775,-8.6335 76.3775,-8.6335 72.8968,-9.00004 76.7074,-11.7662 69.416,-9.36658 69.416,-9.36658\" stroke=\"black\"/>\n",
|
||||
"<text font-family=\"Lato\" font-size=\"14.00\" text-anchor=\"start\" x=\"93\" y=\"-21.8\">1</text>\n",
|
||||
"<text fill=\"#5da5da\" font-family=\"Lato\" font-size=\"14.00\" text-anchor=\"start\" x=\"89.5\" y=\"-6.8\">\u24ff</text>\n",
|
||||
"</g>\n",
|
||||
"</g>\n",
|
||||
"</svg></td><td style=\"vertical-align: top;\"><svg height=\"207pt\" viewBox=\"0.00 0.00 208.07 207.00\" width=\"208pt\" xmlns=\"http://www.w3.org/2000/svg\" xmlns:xlink=\"http://www.w3.org/1999/xlink\">\n",
|
||||
|
|
@ -1698,60 +1702,64 @@
|
|||
"outputs": [
|
||||
{
|
||||
"html": [
|
||||
"<table><tr><td style=\"vertical-align: top;\"><svg height=\"294pt\" viewBox=\"0.00 0.00 99.00 294.00\" width=\"99pt\" xmlns=\"http://www.w3.org/2000/svg\" xmlns:xlink=\"http://www.w3.org/1999/xlink\">\n",
|
||||
"<table><tr><td style=\"vertical-align: top;\"><svg height=\"294pt\" viewBox=\"0.00 0.00 170.00 294.00\" width=\"170pt\" xmlns=\"http://www.w3.org/2000/svg\" xmlns:xlink=\"http://www.w3.org/1999/xlink\">\n",
|
||||
"<g class=\"graph\" id=\"graph0\" transform=\"scale(1 1) rotate(0) translate(4 290)\">\n",
|
||||
"<title>G</title>\n",
|
||||
"<polygon fill=\"white\" points=\"-4,4 -4,-290 95,-290 95,4 -4,4\" stroke=\"none\"/>\n",
|
||||
"<text font-family=\"Lato\" font-size=\"14.00\" text-anchor=\"start\" x=\"24.5\" y=\"-271.8\">Inf(</text>\n",
|
||||
"<text fill=\"#5da5da\" font-family=\"Lato\" font-size=\"14.00\" text-anchor=\"start\" x=\"46.5\" y=\"-271.8\">\u24ff</text>\n",
|
||||
"<text font-family=\"Lato\" font-size=\"14.00\" text-anchor=\"start\" x=\"62.5\" y=\"-271.8\">)</text>\n",
|
||||
"<polygon fill=\"white\" points=\"-4,4 -4,-290 166,-290 166,4 -4,4\" stroke=\"none\"/>\n",
|
||||
"<text font-family=\"Lato\" font-size=\"14.00\" text-anchor=\"start\" x=\"8\" y=\"-271.8\">Inf(</text>\n",
|
||||
"<text fill=\"#5da5da\" font-family=\"Lato\" font-size=\"14.00\" text-anchor=\"start\" x=\"30\" y=\"-271.8\">\u24ff</text>\n",
|
||||
"<text font-family=\"Lato\" font-size=\"14.00\" text-anchor=\"start\" x=\"46\" y=\"-271.8\">)&Inf(</text>\n",
|
||||
"<text fill=\"#f17cb0\" font-family=\"Lato\" font-size=\"14.00\" text-anchor=\"start\" x=\"82\" y=\"-271.8\">\u2776</text>\n",
|
||||
"<text font-family=\"Lato\" font-size=\"14.00\" text-anchor=\"start\" x=\"98\" y=\"-271.8\">)&Inf(</text>\n",
|
||||
"<text fill=\"#faa43a\" font-family=\"Lato\" font-size=\"14.00\" text-anchor=\"start\" x=\"134\" y=\"-271.8\">\u2777</text>\n",
|
||||
"<text font-family=\"Lato\" font-size=\"14.00\" text-anchor=\"start\" x=\"150\" y=\"-271.8\">)</text>\n",
|
||||
"<!-- I -->\n",
|
||||
"<!-- 1 -->\n",
|
||||
"<g class=\"node\" id=\"node2\"><title>1</title>\n",
|
||||
"<ellipse cx=\"18\" cy=\"-207\" fill=\"#ffffaa\" rx=\"18\" ry=\"18\" stroke=\"black\"/>\n",
|
||||
"<text font-family=\"Lato\" font-size=\"14.00\" text-anchor=\"middle\" x=\"18\" y=\"-203.3\">1</text>\n",
|
||||
"<ellipse cx=\"53.5\" cy=\"-207\" fill=\"#ffffaa\" rx=\"18\" ry=\"18\" stroke=\"black\"/>\n",
|
||||
"<text font-family=\"Lato\" font-size=\"14.00\" text-anchor=\"middle\" x=\"53.5\" y=\"-203.3\">1</text>\n",
|
||||
"</g>\n",
|
||||
"<!-- I->1 -->\n",
|
||||
"<g class=\"edge\" id=\"edge1\"><title>I->1</title>\n",
|
||||
"<path d=\"M18,-261.845C18,-260.206 18,-245.846 18,-232.368\" fill=\"none\" stroke=\"black\"/>\n",
|
||||
"<polygon fill=\"black\" points=\"18,-225.058 21.1501,-232.058 18,-228.558 18.0001,-232.058 18.0001,-232.058 18.0001,-232.058 18,-228.558 14.8501,-232.058 18,-225.058 18,-225.058\" stroke=\"black\"/>\n",
|
||||
"<path d=\"M53.5,-261.845C53.5,-260.206 53.5,-245.846 53.5,-232.368\" fill=\"none\" stroke=\"black\"/>\n",
|
||||
"<polygon fill=\"black\" points=\"53.5,-225.058 56.6501,-232.058 53.5,-228.558 53.5001,-232.058 53.5001,-232.058 53.5001,-232.058 53.5,-228.558 50.3501,-232.058 53.5,-225.058 53.5,-225.058\" stroke=\"black\"/>\n",
|
||||
"</g>\n",
|
||||
"<!-- 0 -->\n",
|
||||
"<g class=\"node\" id=\"node3\"><title>0</title>\n",
|
||||
"<ellipse cx=\"18\" cy=\"-120\" fill=\"#ffffaa\" rx=\"18\" ry=\"18\" stroke=\"black\"/>\n",
|
||||
"<text font-family=\"Lato\" font-size=\"14.00\" text-anchor=\"middle\" x=\"18\" y=\"-116.3\">0</text>\n",
|
||||
"<ellipse cx=\"53.5\" cy=\"-120\" fill=\"#ffffaa\" rx=\"18\" ry=\"18\" stroke=\"black\"/>\n",
|
||||
"<text font-family=\"Lato\" font-size=\"14.00\" text-anchor=\"middle\" x=\"53.5\" y=\"-116.3\">0</text>\n",
|
||||
"</g>\n",
|
||||
"<!-- 1->0 -->\n",
|
||||
"<g class=\"edge\" id=\"edge4\"><title>1->0</title>\n",
|
||||
"<path d=\"M18,-188.799C18,-176.356 18,-159.364 18,-145.504\" fill=\"none\" stroke=\"black\"/>\n",
|
||||
"<polygon fill=\"black\" points=\"18,-138.175 21.1501,-145.175 18,-141.675 18.0001,-145.175 18.0001,-145.175 18.0001,-145.175 18,-141.675 14.8501,-145.175 18,-138.175 18,-138.175\" stroke=\"black\"/>\n",
|
||||
"<text font-family=\"Lato\" font-size=\"14.00\" text-anchor=\"middle\" x=\"22.5\" y=\"-159.8\">1</text>\n",
|
||||
"<path d=\"M53.5,-188.799C53.5,-176.356 53.5,-159.364 53.5,-145.504\" fill=\"none\" stroke=\"black\"/>\n",
|
||||
"<polygon fill=\"black\" points=\"53.5,-138.175 56.6501,-145.175 53.5,-141.675 53.5001,-145.175 53.5001,-145.175 53.5001,-145.175 53.5,-141.675 50.3501,-145.175 53.5,-138.175 53.5,-138.175\" stroke=\"black\"/>\n",
|
||||
"<text font-family=\"Lato\" font-size=\"14.00\" text-anchor=\"middle\" x=\"58\" y=\"-159.8\">1</text>\n",
|
||||
"</g>\n",
|
||||
"<!-- 0->0 -->\n",
|
||||
"<g class=\"edge\" id=\"edge2\"><title>0->0</title>\n",
|
||||
"<path d=\"M34.6641,-127.383C44.625,-129.023 54,-126.562 54,-120 54,-115.078 48.7266,-112.463 41.8876,-112.156\" fill=\"none\" stroke=\"black\"/>\n",
|
||||
"<polygon fill=\"black\" points=\"34.6641,-112.617 41.449,-109.027 38.1569,-112.394 41.6498,-112.171 41.6498,-112.171 41.6498,-112.171 38.1569,-112.394 41.8507,-115.314 34.6641,-112.617 34.6641,-112.617\" stroke=\"black\"/>\n",
|
||||
"<text font-family=\"Lato\" font-size=\"14.00\" text-anchor=\"start\" x=\"54\" y=\"-123.8\">a & !b</text>\n",
|
||||
"<text fill=\"#5da5da\" font-family=\"Lato\" font-size=\"14.00\" text-anchor=\"start\" x=\"64.5\" y=\"-108.8\">\u24ff</text>\n",
|
||||
"<path d=\"M70.1641,-127.383C80.125,-129.023 89.5,-126.562 89.5,-120 89.5,-115.078 84.2266,-112.463 77.3876,-112.156\" fill=\"none\" stroke=\"black\"/>\n",
|
||||
"<polygon fill=\"black\" points=\"70.1641,-112.617 76.949,-109.027 73.6569,-112.394 77.1498,-112.171 77.1498,-112.171 77.1498,-112.171 73.6569,-112.394 77.3507,-115.314 70.1641,-112.617 70.1641,-112.617\" stroke=\"black\"/>\n",
|
||||
"<text font-family=\"Lato\" font-size=\"14.00\" text-anchor=\"start\" x=\"89.5\" y=\"-123.8\">a & !b</text>\n",
|
||||
"<text fill=\"#5da5da\" font-family=\"Lato\" font-size=\"14.00\" text-anchor=\"start\" x=\"100\" y=\"-108.8\">\u24ff</text>\n",
|
||||
"</g>\n",
|
||||
"<!-- 2 -->\n",
|
||||
"<g class=\"node\" id=\"node4\"><title>2</title>\n",
|
||||
"<ellipse cx=\"18\" cy=\"-18\" fill=\"#ffffaa\" rx=\"18\" ry=\"18\" stroke=\"black\"/>\n",
|
||||
"<text font-family=\"Lato\" font-size=\"14.00\" text-anchor=\"middle\" x=\"18\" y=\"-14.3\">2</text>\n",
|
||||
"<ellipse cx=\"53.5\" cy=\"-18\" fill=\"#ffffaa\" rx=\"18\" ry=\"18\" stroke=\"black\"/>\n",
|
||||
"<text font-family=\"Lato\" font-size=\"14.00\" text-anchor=\"middle\" x=\"53.5\" y=\"-14.3\">2</text>\n",
|
||||
"</g>\n",
|
||||
"<!-- 0->2 -->\n",
|
||||
"<g class=\"edge\" id=\"edge3\"><title>0->2</title>\n",
|
||||
"<path d=\"M18,-101.581C18,-85.5213 18,-61.5179 18,-43.5228\" fill=\"none\" stroke=\"black\"/>\n",
|
||||
"<polygon fill=\"black\" points=\"18,-36.2191 21.1501,-43.219 18,-39.7191 18.0001,-43.2191 18.0001,-43.2191 18.0001,-43.2191 18,-39.7191 14.8501,-43.2191 18,-36.2191 18,-36.2191\" stroke=\"black\"/>\n",
|
||||
"<text font-family=\"Lato\" font-size=\"14.00\" text-anchor=\"start\" x=\"21.5\" y=\"-72.8\">b</text>\n",
|
||||
"<text fill=\"#5da5da\" font-family=\"Lato\" font-size=\"14.00\" text-anchor=\"start\" x=\"18\" y=\"-57.8\">\u24ff</text>\n",
|
||||
"<path d=\"M53.5,-101.581C53.5,-85.5213 53.5,-61.5179 53.5,-43.5228\" fill=\"none\" stroke=\"black\"/>\n",
|
||||
"<polygon fill=\"black\" points=\"53.5,-36.2191 56.6501,-43.219 53.5,-39.7191 53.5001,-43.2191 53.5001,-43.2191 53.5001,-43.2191 53.5,-39.7191 50.3501,-43.2191 53.5,-36.2191 53.5,-36.2191\" stroke=\"black\"/>\n",
|
||||
"<text font-family=\"Lato\" font-size=\"14.00\" text-anchor=\"start\" x=\"57\" y=\"-72.8\">b</text>\n",
|
||||
"<text fill=\"#5da5da\" font-family=\"Lato\" font-size=\"14.00\" text-anchor=\"start\" x=\"53.5\" y=\"-57.8\">\u24ff</text>\n",
|
||||
"</g>\n",
|
||||
"<!-- 2->2 -->\n",
|
||||
"<g class=\"edge\" id=\"edge5\"><title>2->2</title>\n",
|
||||
"<path d=\"M33.916,-26.6334C44.1504,-28.8856 54,-26.0078 54,-18 54,-11.869 48.2263,-8.74515 40.9268,-8.6284\" fill=\"none\" stroke=\"black\"/>\n",
|
||||
"<polygon fill=\"black\" points=\"33.916,-9.36658 40.5477,-5.50081 37.3968,-9.00004 40.8775,-8.6335 40.8775,-8.6335 40.8775,-8.6335 37.3968,-9.00004 41.2074,-11.7662 33.916,-9.36658 33.916,-9.36658\" stroke=\"black\"/>\n",
|
||||
"<text font-family=\"Lato\" font-size=\"14.00\" text-anchor=\"start\" x=\"57.5\" y=\"-21.8\">1</text>\n",
|
||||
"<text fill=\"#5da5da\" font-family=\"Lato\" font-size=\"14.00\" text-anchor=\"start\" x=\"54\" y=\"-6.8\">\u24ff</text>\n",
|
||||
"<path d=\"M69.416,-26.6334C79.6504,-28.8856 89.5,-26.0078 89.5,-18 89.5,-11.869 83.7263,-8.74515 76.4268,-8.6284\" fill=\"none\" stroke=\"black\"/>\n",
|
||||
"<polygon fill=\"black\" points=\"69.416,-9.36658 76.0477,-5.50081 72.8968,-9.00004 76.3775,-8.6335 76.3775,-8.6335 76.3775,-8.6335 72.8968,-9.00004 76.7074,-11.7662 69.416,-9.36658 69.416,-9.36658\" stroke=\"black\"/>\n",
|
||||
"<text font-family=\"Lato\" font-size=\"14.00\" text-anchor=\"start\" x=\"93\" y=\"-21.8\">1</text>\n",
|
||||
"<text fill=\"#5da5da\" font-family=\"Lato\" font-size=\"14.00\" text-anchor=\"start\" x=\"89.5\" y=\"-6.8\">\u24ff</text>\n",
|
||||
"</g>\n",
|
||||
"</g>\n",
|
||||
"</svg></td><td style=\"vertical-align: top;\"><svg height=\"207pt\" viewBox=\"0.00 0.00 208.07 207.00\" width=\"208pt\" xmlns=\"http://www.w3.org/2000/svg\" xmlns:xlink=\"http://www.w3.org/1999/xlink\">\n",
|
||||
|
|
@ -2021,7 +2029,7 @@
|
|||
]
|
||||
}
|
||||
],
|
||||
"prompt_number": 14
|
||||
"prompt_number": 9
|
||||
},
|
||||
{
|
||||
"cell_type": "markdown",
|
||||
|
|
@ -2045,7 +2053,7 @@
|
|||
"output_type": "stream",
|
||||
"stream": "stdout",
|
||||
"text": [
|
||||
"1000 loops, best of 3: 202 \u00b5s per loop\n"
|
||||
"1000 loops, best of 3: 209 \u00b5s per loop\n"
|
||||
]
|
||||
}
|
||||
],
|
||||
|
|
@ -2064,8 +2072,8 @@
|
|||
"output_type": "stream",
|
||||
"stream": "stdout",
|
||||
"text": [
|
||||
"The slowest run took 5.71 times longer than the fastest. This could mean that an intermediate result is being cached.\n",
|
||||
"100000 loops, best of 3: 4.39 \u00b5s per loop\n"
|
||||
"The slowest run took 5.67 times longer than the fastest. This could mean that an intermediate result is being cached.\n",
|
||||
"100000 loops, best of 3: 4.62 \u00b5s per loop\n"
|
||||
]
|
||||
}
|
||||
],
|
||||
|
|
|
|||
|
|
@ -15,10 +15,9 @@
|
|||
"name": "python",
|
||||
"nbconvert_exporter": "python",
|
||||
"pygments_lexer": "ipython3",
|
||||
"version": "3.4.3+"
|
||||
"version": "3.5.3+"
|
||||
},
|
||||
"name": "",
|
||||
"signature": "sha256:3e27359f7131b7b08ba2b01c8501a8f9c7c39c11a83133150d0a75de7bff2ef2"
|
||||
"name": ""
|
||||
},
|
||||
"nbformat": 3,
|
||||
"nbformat_minor": 0,
|
||||
|
|
@ -38,6 +37,13 @@
|
|||
"outputs": [],
|
||||
"prompt_number": 1
|
||||
},
|
||||
{
|
||||
"cell_type": "markdown",
|
||||
"metadata": {},
|
||||
"source": [
|
||||
"This shows the effect of running `cleanup_acceptance()` on 10 randomly generated automata."
|
||||
]
|
||||
},
|
||||
{
|
||||
"cell_type": "code",
|
||||
"collapsed": false,
|
||||
|
|
@ -49,7 +55,9 @@
|
|||
"HTML(txt)"
|
||||
],
|
||||
"language": "python",
|
||||
"metadata": {},
|
||||
"metadata": {
|
||||
"scrolled": false
|
||||
},
|
||||
"outputs": [
|
||||
{
|
||||
"html": [
|
||||
|
|
@ -462,10 +470,10 @@
|
|||
"<g class=\"graph\" id=\"graph0\" transform=\"scale(0.625905 0.625905) rotate(0) translate(4 172)\">\n",
|
||||
"<title>G</title>\n",
|
||||
"<polygon fill=\"white\" points=\"-4,4 -4,-172 617.5,-172 617.5,4 -4,4\" stroke=\"none\"/>\n",
|
||||
"<text font-family=\"Lato\" font-size=\"14.00\" text-anchor=\"start\" x=\"195.25\" y=\"-153.8\">(Fin(</text>\n",
|
||||
"<text fill=\"#f17cb0\" font-family=\"Lato\" font-size=\"14.00\" text-anchor=\"start\" x=\"223.25\" y=\"-153.8\">\u2776</text>\n",
|
||||
"<text font-family=\"Lato\" font-size=\"14.00\" text-anchor=\"start\" x=\"239.25\" y=\"-153.8\">) & Inf(</text>\n",
|
||||
"<text fill=\"#faa43a\" font-family=\"Lato\" font-size=\"14.00\" text-anchor=\"start\" x=\"282.25\" y=\"-153.8\">\u2777</text>\n",
|
||||
"<text font-family=\"Lato\" font-size=\"14.00\" text-anchor=\"start\" x=\"195.25\" y=\"-153.8\">(Inf(</text>\n",
|
||||
"<text fill=\"#faa43a\" font-family=\"Lato\" font-size=\"14.00\" text-anchor=\"start\" x=\"220.25\" y=\"-153.8\">\u2777</text>\n",
|
||||
"<text font-family=\"Lato\" font-size=\"14.00\" text-anchor=\"start\" x=\"236.25\" y=\"-153.8\">) & Fin(</text>\n",
|
||||
"<text fill=\"#f17cb0\" font-family=\"Lato\" font-size=\"14.00\" text-anchor=\"start\" x=\"282.25\" y=\"-153.8\">\u2776</text>\n",
|
||||
"<text font-family=\"Lato\" font-size=\"14.00\" text-anchor=\"start\" x=\"298.25\" y=\"-153.8\">)) | (Inf(</text>\n",
|
||||
"<text fill=\"#5da5da\" font-family=\"Lato\" font-size=\"14.00\" text-anchor=\"start\" x=\"342.25\" y=\"-153.8\">\u24ff</text>\n",
|
||||
"<text font-family=\"Lato\" font-size=\"14.00\" text-anchor=\"start\" x=\"358.25\" y=\"-153.8\">)&Inf(</text>\n",
|
||||
|
|
@ -952,15 +960,15 @@
|
|||
"<g class=\"graph\" id=\"graph0\" transform=\"scale(0.596626 0.596626) rotate(0) translate(4 295.049)\">\n",
|
||||
"<title>G</title>\n",
|
||||
"<polygon fill=\"white\" points=\"-4,4 -4,-295.049 648,-295.049 648,4 -4,4\" stroke=\"none\"/>\n",
|
||||
"<text font-family=\"Lato\" font-size=\"14.00\" text-anchor=\"start\" x=\"212\" y=\"-276.849\">(Fin(</text>\n",
|
||||
"<text fill=\"#faa43a\" font-family=\"Lato\" font-size=\"14.00\" text-anchor=\"start\" x=\"240\" y=\"-276.849\">\u2777</text>\n",
|
||||
"<text font-family=\"Lato\" font-size=\"14.00\" text-anchor=\"start\" x=\"256\" y=\"-276.849\">) | Inf(</text>\n",
|
||||
"<text fill=\"#b276b2\" font-family=\"Lato\" font-size=\"14.00\" text-anchor=\"start\" x=\"293\" y=\"-276.849\">\u2778</text>\n",
|
||||
"<text font-family=\"Lato\" font-size=\"14.00\" text-anchor=\"start\" x=\"309\" y=\"-276.849\">) | Fin(</text>\n",
|
||||
"<text fill=\"#f17cb0\" font-family=\"Lato\" font-size=\"14.00\" text-anchor=\"start\" x=\"349\" y=\"-276.849\">\u2776</text>\n",
|
||||
"<text font-family=\"Lato\" font-size=\"14.00\" text-anchor=\"start\" x=\"365\" y=\"-276.849\">)) & Inf(</text>\n",
|
||||
"<text fill=\"#5da5da\" font-family=\"Lato\" font-size=\"14.00\" text-anchor=\"start\" x=\"412\" y=\"-276.849\">\u24ff</text>\n",
|
||||
"<text font-family=\"Lato\" font-size=\"14.00\" text-anchor=\"start\" x=\"428\" y=\"-276.849\">)</text>\n",
|
||||
"<text font-family=\"Lato\" font-size=\"14.00\" text-anchor=\"start\" x=\"212.5\" y=\"-276.849\">((Fin(</text>\n",
|
||||
"<text fill=\"#f17cb0\" font-family=\"Lato\" font-size=\"14.00\" text-anchor=\"start\" x=\"244.5\" y=\"-276.849\">\u2776</text>\n",
|
||||
"<text font-family=\"Lato\" font-size=\"14.00\" text-anchor=\"start\" x=\"260.5\" y=\"-276.849\">)|Fin(</text>\n",
|
||||
"<text fill=\"#faa43a\" font-family=\"Lato\" font-size=\"14.00\" text-anchor=\"start\" x=\"292.5\" y=\"-276.849\">\u2777</text>\n",
|
||||
"<text font-family=\"Lato\" font-size=\"14.00\" text-anchor=\"start\" x=\"308.5\" y=\"-276.849\">)) | Inf(</text>\n",
|
||||
"<text fill=\"#b276b2\" font-family=\"Lato\" font-size=\"14.00\" text-anchor=\"start\" x=\"348.5\" y=\"-276.849\">\u2778</text>\n",
|
||||
"<text font-family=\"Lato\" font-size=\"14.00\" text-anchor=\"start\" x=\"364.5\" y=\"-276.849\">)) & Inf(</text>\n",
|
||||
"<text fill=\"#5da5da\" font-family=\"Lato\" font-size=\"14.00\" text-anchor=\"start\" x=\"411.5\" y=\"-276.849\">\u24ff</text>\n",
|
||||
"<text font-family=\"Lato\" font-size=\"14.00\" text-anchor=\"start\" x=\"427.5\" y=\"-276.849\">)</text>\n",
|
||||
"<!-- I -->\n",
|
||||
"<!-- 0 -->\n",
|
||||
"<g class=\"node\" id=\"node2\"><title>0</title>\n",
|
||||
|
|
@ -2081,10 +2089,10 @@
|
|||
"<text fill=\"#faa43a\" font-family=\"Lato\" font-size=\"14.00\" text-anchor=\"start\" x=\"218.5\" y=\"-137.8\">\u2777</text>\n",
|
||||
"<text font-family=\"Lato\" font-size=\"14.00\" text-anchor=\"start\" x=\"234.5\" y=\"-137.8\">)|Fin(</text>\n",
|
||||
"<text fill=\"#b276b2\" font-family=\"Lato\" font-size=\"14.00\" text-anchor=\"start\" x=\"266.5\" y=\"-137.8\">\u2778</text>\n",
|
||||
"<text font-family=\"Lato\" font-size=\"14.00\" text-anchor=\"start\" x=\"282.5\" y=\"-137.8\">)) | (Fin(</text>\n",
|
||||
"<text fill=\"#f17cb0\" font-family=\"Lato\" font-size=\"14.00\" text-anchor=\"start\" x=\"329.5\" y=\"-137.8\">\u2776</text>\n",
|
||||
"<text font-family=\"Lato\" font-size=\"14.00\" text-anchor=\"start\" x=\"345.5\" y=\"-137.8\">) & Inf(</text>\n",
|
||||
"<text fill=\"#5da5da\" font-family=\"Lato\" font-size=\"14.00\" text-anchor=\"start\" x=\"388.5\" y=\"-137.8\">\u24ff</text>\n",
|
||||
"<text font-family=\"Lato\" font-size=\"14.00\" text-anchor=\"start\" x=\"282.5\" y=\"-137.8\">)) | (Inf(</text>\n",
|
||||
"<text fill=\"#5da5da\" font-family=\"Lato\" font-size=\"14.00\" text-anchor=\"start\" x=\"326.5\" y=\"-137.8\">\u24ff</text>\n",
|
||||
"<text font-family=\"Lato\" font-size=\"14.00\" text-anchor=\"start\" x=\"342.5\" y=\"-137.8\">) & Fin(</text>\n",
|
||||
"<text fill=\"#f17cb0\" font-family=\"Lato\" font-size=\"14.00\" text-anchor=\"start\" x=\"388.5\" y=\"-137.8\">\u2776</text>\n",
|
||||
"<text font-family=\"Lato\" font-size=\"14.00\" text-anchor=\"start\" x=\"404.5\" y=\"-137.8\">))</text>\n",
|
||||
"<!-- I -->\n",
|
||||
"<!-- 0 -->\n",
|
||||
|
|
@ -2173,10 +2181,10 @@
|
|||
"<text fill=\"#faa43a\" font-family=\"Lato\" font-size=\"14.00\" text-anchor=\"start\" x=\"218.5\" y=\"-137.8\">\u2777</text>\n",
|
||||
"<text font-family=\"Lato\" font-size=\"14.00\" text-anchor=\"start\" x=\"234.5\" y=\"-137.8\">)|Fin(</text>\n",
|
||||
"<text fill=\"#b276b2\" font-family=\"Lato\" font-size=\"14.00\" text-anchor=\"start\" x=\"266.5\" y=\"-137.8\">\u2778</text>\n",
|
||||
"<text font-family=\"Lato\" font-size=\"14.00\" text-anchor=\"start\" x=\"282.5\" y=\"-137.8\">)) | (Fin(</text>\n",
|
||||
"<text fill=\"#f17cb0\" font-family=\"Lato\" font-size=\"14.00\" text-anchor=\"start\" x=\"329.5\" y=\"-137.8\">\u2776</text>\n",
|
||||
"<text font-family=\"Lato\" font-size=\"14.00\" text-anchor=\"start\" x=\"345.5\" y=\"-137.8\">) & Inf(</text>\n",
|
||||
"<text fill=\"#5da5da\" font-family=\"Lato\" font-size=\"14.00\" text-anchor=\"start\" x=\"388.5\" y=\"-137.8\">\u24ff</text>\n",
|
||||
"<text font-family=\"Lato\" font-size=\"14.00\" text-anchor=\"start\" x=\"282.5\" y=\"-137.8\">)) | (Inf(</text>\n",
|
||||
"<text fill=\"#5da5da\" font-family=\"Lato\" font-size=\"14.00\" text-anchor=\"start\" x=\"326.5\" y=\"-137.8\">\u24ff</text>\n",
|
||||
"<text font-family=\"Lato\" font-size=\"14.00\" text-anchor=\"start\" x=\"342.5\" y=\"-137.8\">) & Fin(</text>\n",
|
||||
"<text fill=\"#f17cb0\" font-family=\"Lato\" font-size=\"14.00\" text-anchor=\"start\" x=\"388.5\" y=\"-137.8\">\u2776</text>\n",
|
||||
"<text font-family=\"Lato\" font-size=\"14.00\" text-anchor=\"start\" x=\"404.5\" y=\"-137.8\">))</text>\n",
|
||||
"<!-- I -->\n",
|
||||
"<!-- 0 -->\n",
|
||||
|
|
@ -2263,7 +2271,7 @@
|
|||
"output_type": "pyout",
|
||||
"prompt_number": 2,
|
||||
"text": [
|
||||
"<IPython.core.display.HTML at 0x7f74a8298ac8>"
|
||||
"<IPython.core.display.HTML object>"
|
||||
]
|
||||
}
|
||||
],
|
||||
|
|
|
|||
Loading…
Add table
Add a link
Reference in a new issue