improve cleanup_parity() and colorize_parity()
Fixes #384. * spot/twaalgos/parity.cc: Here. * tests/core/parity2.test, tests/python/highlighting.ipynb, tests/python/parity.py: Adjust test cases. * tests/python/parity.ipynb: Improve the presentation. * NEWS: Mention the change.
This commit is contained in:
Alexandre Duret-Lutz
parent
f0b77e21c8
commit
f6575d2ec5
6 changed files with 4042 additions and 1837 deletions
5
NEWS
5
NEWS
|
|
@ -103,6 +103,11 @@ New in spot 2.7.5.dev (not yet released)
|
|||
F(G(a & Fb) = FGa & GFb (unless option "reduce_size_strictly")
|
||||
G(F(a & Gb)) = GFa & FGb (unless option "reduce_size_strictly")
|
||||
|
||||
- cleanup_parity() and colorize_parity() were cleaned up a bit,
|
||||
resulting in fewer colors used in some cases. In particular,
|
||||
colorize_parity() learned that coloring transitiant edges does not
|
||||
require the introduction of a new color.
|
||||
|
||||
New in spot 2.7.5 (2019-06-05)
|
||||
|
||||
Build:
|
||||
|
|
|
|||
|
|
@ -1,5 +1,5 @@
|
|||
// -*- coding: utf-8 -*-
|
||||
// Copyright (C) 2016, 2018 Laboratoire de Recherche et Développement
|
||||
// Copyright (C) 2016, 2018, 2019 Laboratoire de Recherche et Développement
|
||||
// de l'Epita (LRDE).
|
||||
//
|
||||
// This file is part of Spot, a model checking library.
|
||||
|
|
@ -22,6 +22,7 @@
|
|||
#include <spot/twa/twagraph.hh>
|
||||
#include <spot/twaalgos/product.hh>
|
||||
#include <spot/twaalgos/complete.hh>
|
||||
#include <spot/twaalgos/sccinfo.hh>
|
||||
#include <vector>
|
||||
#include <utility>
|
||||
#include <functional>
|
||||
|
|
@ -165,120 +166,132 @@ namespace spot
|
|||
twa_graph_ptr
|
||||
cleanup_parity_here(twa_graph_ptr aut, bool keep_style)
|
||||
{
|
||||
unsigned num_sets = aut->num_sets();
|
||||
if (num_sets == 0)
|
||||
return aut;
|
||||
|
||||
bool current_max;
|
||||
bool current_odd;
|
||||
if (!aut->acc().is_parity(current_max, current_odd, true))
|
||||
input_is_not_parity("cleanup_parity");
|
||||
auto num_sets = aut->num_sets();
|
||||
if (num_sets == 0)
|
||||
return aut;
|
||||
|
||||
// Compute all the used sets
|
||||
// Gather all the used colors, while leaving only one per edge.
|
||||
auto used_in_aut = acc_cond::mark_t();
|
||||
for (auto& t: aut->edges())
|
||||
{
|
||||
// leave only one color on each transition
|
||||
if (current_max)
|
||||
{
|
||||
auto maxset = t.acc.max_set();
|
||||
if (maxset)
|
||||
t.acc = acc_cond::mark_t{maxset - 1};
|
||||
}
|
||||
else
|
||||
{
|
||||
t.acc = t.acc.lowest();
|
||||
}
|
||||
// recall colors used in the automaton
|
||||
used_in_aut |= t.acc;
|
||||
}
|
||||
|
||||
// remove from the acceptance condition the unused one (starting from the
|
||||
// least significant)
|
||||
auto useful = used_in_aut;
|
||||
int useful_min = 0;
|
||||
int useful_max = num_sets-1;
|
||||
if (!current_max)
|
||||
{
|
||||
int n = num_sets-1;
|
||||
while (n >= 0 && !useful.has(n))
|
||||
{
|
||||
if (n > 0)
|
||||
useful.clear(n-1);
|
||||
n -= 2;
|
||||
}
|
||||
useful_max = n;
|
||||
}
|
||||
else
|
||||
{
|
||||
unsigned n = 0;
|
||||
while (n < num_sets && !useful.has(n))
|
||||
{
|
||||
useful.clear(n+1);
|
||||
n += 2;
|
||||
}
|
||||
useful_min = n;
|
||||
}
|
||||
if (used_in_aut)
|
||||
{
|
||||
// Never remove the least significant acceptance set, and mark the
|
||||
// acceptance set 0 to keep the style if needed.
|
||||
if (keep_style && useful_min <= useful_max)
|
||||
{
|
||||
useful.set(useful_min);
|
||||
useful.set(useful_max);
|
||||
}
|
||||
|
||||
// Fill the vector shift with the new acceptance sets
|
||||
std::vector<unsigned> shift(num_sets);
|
||||
int prev_used = -1;
|
||||
bool change_style = false;
|
||||
unsigned new_index = 0;
|
||||
for (auto i = 0U; i < num_sets; ++i)
|
||||
if (useful.has(i))
|
||||
{
|
||||
if (prev_used == -1)
|
||||
change_style = i % 2 != 0;
|
||||
else if ((i + prev_used) % 2 != 0)
|
||||
++new_index;
|
||||
shift[i] = new_index;
|
||||
prev_used = i;
|
||||
}
|
||||
|
||||
// Update all the transitions with the vector shift
|
||||
acc_cond::mark_t allsets = aut->acc().all_sets();
|
||||
if (current_max)
|
||||
for (auto& t: aut->edges())
|
||||
{
|
||||
t.acc &= useful;
|
||||
auto maxset = t.acc.max_set();
|
||||
if (maxset)
|
||||
t.acc = acc_cond::mark_t{shift[maxset - 1]};
|
||||
}
|
||||
|
||||
auto new_num_sets = new_index + 1;
|
||||
if (!useful)
|
||||
{
|
||||
new_num_sets = 0;
|
||||
if (current_max)
|
||||
change_style = false;
|
||||
if (auto maxset = (t.acc & allsets).max_set())
|
||||
{
|
||||
t.acc = acc_cond::mark_t{maxset - 1};
|
||||
used_in_aut |= t.acc;
|
||||
}
|
||||
else
|
||||
change_style = num_sets % 2 == 1;
|
||||
{
|
||||
t.acc = acc_cond::mark_t{};
|
||||
}
|
||||
}
|
||||
else
|
||||
for (auto& t: aut->edges())
|
||||
{
|
||||
t.acc = (t.acc & allsets).lowest();
|
||||
used_in_aut |= t.acc;
|
||||
}
|
||||
|
||||
if (new_num_sets < num_sets)
|
||||
{
|
||||
auto new_acc =
|
||||
acc_cond::acc_code::parity(current_max,
|
||||
current_odd != change_style,
|
||||
new_num_sets);
|
||||
aut->set_acceptance(new_num_sets, new_acc);
|
||||
}
|
||||
}
|
||||
else
|
||||
if (used_in_aut)
|
||||
{
|
||||
if (current_max)
|
||||
// If max even or max odd: if 0 is not used, we can remove 1, if
|
||||
// 2 is not used, we can remove 3, etc.
|
||||
// This is obvious from the encoding:
|
||||
// max odd n = ... Inf(3) | (Fin(2) & (Inf(1) | Fin(0)))
|
||||
// max even n = ... Fin(3) & (Inf(2) | (Fin(1) & Inf(0)))
|
||||
{
|
||||
unsigned n = 0;
|
||||
while (n + 1 < num_sets && !used_in_aut.has(n))
|
||||
{
|
||||
used_in_aut.clear(n + 1);
|
||||
n += 2;
|
||||
}
|
||||
}
|
||||
else
|
||||
// min even and min odd simply work the other way around:
|
||||
// min even 4 = Inf(0) | (Fin(1) & (Inf(2) | Fin(3)))
|
||||
// min odd 4 = Fin(0) & (Inf(1) | (Fin(2) & Inf(3)))
|
||||
{
|
||||
int n = num_sets - 1;
|
||||
while (n >= 1 && !used_in_aut.has(n))
|
||||
{
|
||||
used_in_aut.clear(n - 1);
|
||||
n -= 2;
|
||||
}
|
||||
}
|
||||
}
|
||||
|
||||
// If no color needed in the automaton, exit early.
|
||||
if (!used_in_aut)
|
||||
{
|
||||
if ((current_max && current_odd)
|
||||
|| (!current_max && current_odd != (num_sets % 2 == 0)))
|
||||
|| (!current_max && current_odd == (num_sets & 1)))
|
||||
aut->set_acceptance(0, acc_cond::acc_code::t());
|
||||
else
|
||||
aut->set_acceptance(0, acc_cond::acc_code::f());
|
||||
for (auto& e: aut->edges())
|
||||
e.acc = {};
|
||||
return aut;
|
||||
}
|
||||
|
||||
// Renumber colors. Two used colors separated by a unused color
|
||||
// can be merged.
|
||||
std::vector<unsigned> rename(num_sets);
|
||||
int prev_used = -1;
|
||||
bool change_style = false;
|
||||
unsigned new_index = 0;
|
||||
for (auto i = 0U; i < num_sets; ++i)
|
||||
if (used_in_aut.has(i))
|
||||
{
|
||||
if (prev_used == -1)
|
||||
{
|
||||
if (i & 1)
|
||||
{
|
||||
if (keep_style)
|
||||
new_index = 1;
|
||||
else
|
||||
change_style = true;
|
||||
}
|
||||
}
|
||||
else if ((i + prev_used) & 1)
|
||||
++new_index;
|
||||
rename[i] = new_index;
|
||||
prev_used = i;
|
||||
}
|
||||
assert(prev_used >= 0);
|
||||
|
||||
// Update all colors according to RENAME.
|
||||
// Using max_set or min_set makes no difference since
|
||||
// there is now at most one color per edge.
|
||||
for (auto& t: aut->edges())
|
||||
{
|
||||
acc_cond::mark_t m = t.acc & used_in_aut;
|
||||
unsigned color = m.max_set();
|
||||
if (color)
|
||||
t.acc = acc_cond::mark_t{rename[color - 1]};
|
||||
else
|
||||
t.acc = m;
|
||||
}
|
||||
|
||||
unsigned new_num_sets = new_index + 1;
|
||||
if (new_num_sets < num_sets)
|
||||
{
|
||||
auto new_acc =
|
||||
acc_cond::acc_code::parity(current_max,
|
||||
current_odd != change_style,
|
||||
new_num_sets);
|
||||
aut->set_acceptance(new_num_sets, new_acc);
|
||||
}
|
||||
else
|
||||
{
|
||||
assert(!change_style);
|
||||
}
|
||||
return aut;
|
||||
}
|
||||
|
|
@ -297,44 +310,79 @@ namespace spot
|
|||
bool current_odd;
|
||||
if (!aut->acc().is_parity(current_max, current_odd, true))
|
||||
input_is_not_parity("colorize_parity");
|
||||
if (!aut->is_existential())
|
||||
throw std::runtime_error
|
||||
("colorize_parity_here() does not support alternation");
|
||||
|
||||
bool has_empty = false;
|
||||
for (const auto& e: aut->edges())
|
||||
if (!e.acc)
|
||||
{
|
||||
has_empty = true;
|
||||
break;
|
||||
}
|
||||
auto num_sets = aut->num_sets();
|
||||
bool has_empty_in_scc = false;
|
||||
{
|
||||
scc_info si(aut, scc_info_options::NONE);
|
||||
for (const auto& e: aut->edges())
|
||||
if (!e.acc && si.scc_of(e.src) == si.scc_of(e.dst))
|
||||
{
|
||||
has_empty_in_scc = true;
|
||||
break;
|
||||
}
|
||||
}
|
||||
unsigned num_sets = aut->num_sets();
|
||||
bool new_odd = current_odd;
|
||||
int incr = 0;
|
||||
if (has_empty)
|
||||
unsigned empty = current_max ? 0 : num_sets - 1;
|
||||
if (has_empty_in_scc)
|
||||
{
|
||||
// If the automaton has a transition that belong to any set, we need to
|
||||
// introduce a new acceptance set.
|
||||
// We may want to add a second acceptance set to keep the style of
|
||||
// the parity acceptance
|
||||
incr = 1 + (keep_style && current_max);
|
||||
num_sets += incr;
|
||||
bool new_style = current_odd == (keep_style || !current_max);
|
||||
auto new_acc = acc_cond::acc_code::parity(current_max,
|
||||
new_style, num_sets);
|
||||
// If the automaton has an SCC transition that belongs to no set
|
||||
// (called "empty trans." below), we may need to introduce a
|
||||
// new acceptance set. What to do depends on the kind
|
||||
// (min/max) and style (odd/even) of parity acceptance and the
|
||||
// number (n) of colors used.
|
||||
//
|
||||
// | kind/style | n | empty tr. | other tr. | result |
|
||||
// |------------+-----+------------+-----------+--------------|
|
||||
// | max odd | any | set to {0} | add 1 | max even n+1 |
|
||||
// | max even | any | set to {0} | add 1 | max odd n+1 |
|
||||
// | min odd | any | set to {n} | unchanged | min odd n+1 |
|
||||
// | min even | any | set to {n} | unchanged | min even n+1 |
|
||||
//
|
||||
// In the above table, the "max" cases both change their style
|
||||
// We may want to add a second acceptance set to keep the
|
||||
// style:
|
||||
//
|
||||
// | kind/style | n | empty tr. | other tr. | result |
|
||||
// |------------+-----+------------+-----------+--------------|
|
||||
// | max odd | any | set to {1} | add 2 | max odd n+2 |
|
||||
// | max even | any | set to {1} | add 2 | max even n+2 |
|
||||
if (current_max)
|
||||
{
|
||||
incr = 1 + keep_style;
|
||||
num_sets += incr;
|
||||
new_odd = current_odd == keep_style;
|
||||
empty = keep_style;
|
||||
}
|
||||
else
|
||||
{
|
||||
empty = num_sets++;
|
||||
}
|
||||
|
||||
auto new_acc =
|
||||
acc_cond::acc_code::parity(current_max, new_odd, num_sets);
|
||||
aut->set_acceptance(num_sets, new_acc);
|
||||
}
|
||||
|
||||
if (current_max)
|
||||
{
|
||||
--incr;
|
||||
for (auto& e: aut->edges())
|
||||
{
|
||||
auto maxset = e.acc.max_set();
|
||||
e.acc = acc_cond::mark_t{maxset ? maxset + incr : incr};
|
||||
e.acc = acc_cond::mark_t{maxset ? maxset + incr : empty};
|
||||
}
|
||||
}
|
||||
else
|
||||
{
|
||||
auto unused_mark = num_sets - incr;
|
||||
for (auto& e: aut->edges())
|
||||
e.acc = e.acc ? e.acc.lowest() : acc_cond::mark_t{unused_mark};
|
||||
e.acc = e.acc ? e.acc.lowest() : acc_cond::mark_t{empty};
|
||||
}
|
||||
|
||||
return aut;
|
||||
}
|
||||
|
||||
|
|
|
|||
|
|
@ -245,12 +245,12 @@ name: "(p0 W XXGp0) & G(Fp1 & FGp2)"
|
|||
States: 5
|
||||
Start: 0
|
||||
AP: 3 "p0" "p1" "p2"
|
||||
acc-name: parity max even 3
|
||||
Acceptance: 3 Inf(2) | (Fin(1) & Inf(0))
|
||||
acc-name: Streett 1
|
||||
Acceptance: 2 Fin(0) | Inf(1)
|
||||
properties: trans-labels explicit-labels trans-acc colored
|
||||
--BODY--
|
||||
State: 0
|
||||
[0] 0 {1}
|
||||
[0] 0 {0}
|
||||
[!0] 1 {0}
|
||||
[0&1&2] 2 {0}
|
||||
State: 1
|
||||
|
|
@ -258,14 +258,14 @@ State: 1
|
|||
[1&2] 4 {0}
|
||||
State: 2
|
||||
[!0] 1 {0}
|
||||
[0&!1&2] 2 {1}
|
||||
[0&1&2] 2 {2}
|
||||
[0&!1&2] 2 {0}
|
||||
[0&1&2] 2 {1}
|
||||
State: 3
|
||||
[0] 3 {1}
|
||||
[0] 3 {0}
|
||||
[0&1&2] 4 {0}
|
||||
State: 4
|
||||
[0&!1&2] 4 {1}
|
||||
[0&1&2] 4 {2}
|
||||
[0&!1&2] 4 {0}
|
||||
[0&1&2] 4 {1}
|
||||
--END--
|
||||
HOA: v1
|
||||
name: "FGa"
|
||||
|
|
@ -304,24 +304,24 @@ name: "(p0 W XXGp0) & G(Fp1 & FGp2)"
|
|||
States: 5
|
||||
Start: 0
|
||||
AP: 3 "p0" "p1" "p2"
|
||||
acc-name: parity min odd 4
|
||||
Acceptance: 4 Fin(0) & (Inf(1) | (Fin(2) & Inf(3)))
|
||||
acc-name: parity min odd 3
|
||||
Acceptance: 3 Fin(0) & (Inf(1) | Fin(2))
|
||||
properties: trans-labels explicit-labels trans-acc colored
|
||||
--BODY--
|
||||
State: 0
|
||||
[0] 0 {2}
|
||||
[!0] 1 {3}
|
||||
[0&1&2] 2 {3}
|
||||
[!0] 1 {2}
|
||||
[0&1&2] 2 {2}
|
||||
State: 1
|
||||
[t] 3 {3}
|
||||
[1&2] 4 {3}
|
||||
[t] 3 {2}
|
||||
[1&2] 4 {2}
|
||||
State: 2
|
||||
[!0] 1 {3}
|
||||
[!0] 1 {2}
|
||||
[0&1&2] 2 {1}
|
||||
[0&!1&2] 2 {2}
|
||||
State: 3
|
||||
[0] 3 {2}
|
||||
[0&1&2] 4 {3}
|
||||
[0&1&2] 4 {2}
|
||||
State: 4
|
||||
[0&1&2] 4 {1}
|
||||
[0&!1&2] 4 {2}
|
||||
|
|
@ -980,21 +980,21 @@ name: "(p0 W XXGp0) & G(Fp1 & FGp2)"
|
|||
States: 5
|
||||
Start: 0
|
||||
AP: 3 "p0" "p1" "p2"
|
||||
acc-name: parity min odd 4
|
||||
Acceptance: 4 Fin(0) & (Inf(1) | (Fin(2) & Inf(3)))
|
||||
acc-name: parity min odd 3
|
||||
Acceptance: 3 Fin(0) & (Inf(1) | Fin(2))
|
||||
properties: trans-labels explicit-labels trans-acc colored
|
||||
properties: deterministic
|
||||
--BODY--
|
||||
State: 0
|
||||
[0&!1 | 0&!2] 0 {2}
|
||||
[!0] 1 {3}
|
||||
[!0] 1 {2}
|
||||
[0&1&2] 2 {1}
|
||||
State: 1
|
||||
[!1 | !2] 3 {3}
|
||||
[1&2] 4 {3}
|
||||
[!1 | !2] 3 {2}
|
||||
[1&2] 4 {2}
|
||||
State: 2
|
||||
[0&!2] 0 {0}
|
||||
[!0] 1 {3}
|
||||
[!0] 1 {2}
|
||||
[0&1&2] 2 {1}
|
||||
[0&!1&2] 2 {2}
|
||||
State: 3
|
||||
|
|
@ -1042,21 +1042,21 @@ name: "(p0 W XXGp0) & G(Fp1 & FGp2)"
|
|||
States: 5
|
||||
Start: 0
|
||||
AP: 3 "p0" "p1" "p2"
|
||||
acc-name: parity min odd 4
|
||||
Acceptance: 4 Fin(0) & (Inf(1) | (Fin(2) & Inf(3)))
|
||||
acc-name: parity min odd 3
|
||||
Acceptance: 3 Fin(0) & (Inf(1) | Fin(2))
|
||||
properties: trans-labels explicit-labels trans-acc colored
|
||||
properties: deterministic
|
||||
--BODY--
|
||||
State: 0
|
||||
[0&!1 | 0&!2] 0 {2}
|
||||
[!0] 1 {3}
|
||||
[!0] 1 {2}
|
||||
[0&1&2] 2 {1}
|
||||
State: 1
|
||||
[!1 | !2] 3 {3}
|
||||
[1&2] 4 {3}
|
||||
[!1 | !2] 3 {2}
|
||||
[1&2] 4 {2}
|
||||
State: 2
|
||||
[0&!2] 0 {0}
|
||||
[!0] 1 {3}
|
||||
[!0] 1 {2}
|
||||
[0&1&2] 2 {1}
|
||||
[0&!1&2] 2 {2}
|
||||
State: 3
|
||||
|
|
@ -1527,7 +1527,6 @@ ltlcross 'ltl2tgba -P' 'ltl2tgba -P"odd max"' 'ltl2tgba -P"even min"' \
|
|||
'ltl2tgba -p' 'ltl2tgba -p"odd max"' 'ltl2tgba -p"even min"' \
|
||||
-f FGa -f 'GFa&GFb' -f 'GF(a <-> XXXb)' -f '(p0 W XXGp0) & GFp1 & FGp2'
|
||||
|
||||
|
||||
# Test the behavior of our determinization on Max Michel automata.
|
||||
# Any change to Spot that lowers the output.states is welcome :-)
|
||||
genaut --m-nba=1..4 | autcross --language-preserved 'autfilt -D' --csv=out.csv
|
||||
|
|
|
|||
|
|
@ -240,7 +240,7 @@
|
|||
"</svg>\n"
|
||||
],
|
||||
"text/plain": [
|
||||
"<spot.twa_graph; proxy of <Swig Object of type 'std::shared_ptr< spot::twa_graph > *' at 0x7f55b80ee2a0> >"
|
||||
"<spot.twa_graph; proxy of <Swig Object of type 'std::shared_ptr< spot::twa_graph > *' at 0x7f52302b76f0> >"
|
||||
]
|
||||
},
|
||||
"execution_count": 4,
|
||||
|
|
@ -352,7 +352,7 @@
|
|||
"</svg>\n"
|
||||
],
|
||||
"text/plain": [
|
||||
"<spot.twa; proxy of <Swig Object of type 'std::shared_ptr< spot::twa > *' at 0x7f55b8012060> >"
|
||||
"<spot.twa; proxy of <Swig Object of type 'std::shared_ptr< spot::twa > *' at 0x7f523026d2d0> >"
|
||||
]
|
||||
},
|
||||
"execution_count": 5,
|
||||
|
|
@ -462,7 +462,7 @@
|
|||
"</svg>\n"
|
||||
],
|
||||
"text/plain": [
|
||||
"<spot.twa_graph; proxy of <Swig Object of type 'std::shared_ptr< spot::twa_graph > *' at 0x7f55b80ee2a0> >"
|
||||
"<spot.twa_graph; proxy of <Swig Object of type 'std::shared_ptr< spot::twa_graph > *' at 0x7f52302b76f0> >"
|
||||
]
|
||||
},
|
||||
"execution_count": 6,
|
||||
|
|
@ -695,7 +695,7 @@
|
|||
"</svg>\n"
|
||||
],
|
||||
"text/plain": [
|
||||
"<spot.twa_graph; proxy of <Swig Object of type 'std::shared_ptr< spot::twa_graph > *' at 0x7f55b8012840> >"
|
||||
"<spot.twa_graph; proxy of <Swig Object of type 'std::shared_ptr< spot::twa_graph > *' at 0x7f523026d540> >"
|
||||
]
|
||||
},
|
||||
"execution_count": 8,
|
||||
|
|
@ -890,7 +890,7 @@
|
|||
"</svg>\n"
|
||||
],
|
||||
"text/plain": [
|
||||
"<spot.twa_graph; proxy of <Swig Object of type 'std::shared_ptr< spot::twa_graph > *' at 0x7f55b8012840> >"
|
||||
"<spot.twa_graph; proxy of <Swig Object of type 'std::shared_ptr< spot::twa_graph > *' at 0x7f523026d540> >"
|
||||
]
|
||||
},
|
||||
"execution_count": 11,
|
||||
|
|
@ -1228,7 +1228,7 @@
|
|||
"</svg>\n"
|
||||
],
|
||||
"text/plain": [
|
||||
"<spot.twa_graph; proxy of <Swig Object of type 'std::shared_ptr< spot::twa_graph > *' at 0x7f55b802f5d0> >"
|
||||
"<spot.twa_graph; proxy of <Swig Object of type 'std::shared_ptr< spot::twa_graph > *' at 0x7f523026dc30> >"
|
||||
]
|
||||
},
|
||||
"metadata": {},
|
||||
|
|
@ -1489,7 +1489,7 @@
|
|||
"</svg>\n"
|
||||
],
|
||||
"text/plain": [
|
||||
"<spot.twa_graph; proxy of <Swig Object of type 'std::shared_ptr< spot::twa_graph > *' at 0x7f55b802f5d0> >"
|
||||
"<spot.twa_graph; proxy of <Swig Object of type 'std::shared_ptr< spot::twa_graph > *' at 0x7f523026dab0> >"
|
||||
]
|
||||
},
|
||||
"metadata": {},
|
||||
|
|
@ -1672,7 +1672,7 @@
|
|||
"</svg>\n"
|
||||
],
|
||||
"text/plain": [
|
||||
"<spot.twa_graph; proxy of <Swig Object of type 'std::shared_ptr< spot::twa_graph > *' at 0x7f55b802f630> >"
|
||||
"<spot.twa_graph; proxy of <Swig Object of type 'std::shared_ptr< spot::twa_graph > *' at 0x7f523026d720> >"
|
||||
]
|
||||
},
|
||||
"metadata": {},
|
||||
|
|
@ -1789,7 +1789,7 @@
|
|||
"</svg>\n"
|
||||
],
|
||||
"text/plain": [
|
||||
"<spot.twa_graph; proxy of <Swig Object of type 'std::shared_ptr< spot::twa_graph > *' at 0x7f55b802f720> >"
|
||||
"<spot.twa_graph; proxy of <Swig Object of type 'std::shared_ptr< spot::twa_graph > *' at 0x7f523026df60> >"
|
||||
]
|
||||
},
|
||||
"metadata": {},
|
||||
|
|
@ -1844,7 +1844,7 @@
|
|||
"</svg>\n"
|
||||
],
|
||||
"text/plain": [
|
||||
"<spot.twa_graph; proxy of <Swig Object of type 'std::shared_ptr< spot::twa_graph > *' at 0x7f55b802f3f0> >"
|
||||
"<spot.twa_graph; proxy of <Swig Object of type 'std::shared_ptr< spot::twa_graph > *' at 0x7f523026de10> >"
|
||||
]
|
||||
},
|
||||
"metadata": {},
|
||||
|
|
@ -1938,7 +1938,7 @@
|
|||
"</svg>\n"
|
||||
],
|
||||
"text/plain": [
|
||||
"<spot.twa_graph; proxy of <Swig Object of type 'std::shared_ptr< spot::twa_graph > *' at 0x7f55b8089e40> >"
|
||||
"<spot.twa_graph; proxy of <Swig Object of type 'std::shared_ptr< spot::twa_graph > *' at 0x7f523026d720> >"
|
||||
]
|
||||
},
|
||||
"execution_count": 14,
|
||||
|
|
@ -2067,7 +2067,7 @@
|
|||
"</svg>\n"
|
||||
],
|
||||
"text/plain": [
|
||||
"<spot.twa_graph; proxy of <Swig Object of type 'std::shared_ptr< spot::twa_graph > *' at 0x7f55b8089e40> >"
|
||||
"<spot.twa_graph; proxy of <Swig Object of type 'std::shared_ptr< spot::twa_graph > *' at 0x7f523026d720> >"
|
||||
]
|
||||
},
|
||||
"metadata": {},
|
||||
|
|
@ -2132,7 +2132,7 @@
|
|||
"</svg>\n"
|
||||
],
|
||||
"text/plain": [
|
||||
"<spot.twa_graph; proxy of <Swig Object of type 'std::shared_ptr< spot::twa_graph > *' at 0x7f55b802f720> >"
|
||||
"<spot.twa_graph; proxy of <Swig Object of type 'std::shared_ptr< spot::twa_graph > *' at 0x7f523026df60> >"
|
||||
]
|
||||
},
|
||||
"metadata": {},
|
||||
|
|
@ -2187,7 +2187,7 @@
|
|||
"</svg>\n"
|
||||
],
|
||||
"text/plain": [
|
||||
"<spot.twa_graph; proxy of <Swig Object of type 'std::shared_ptr< spot::twa_graph > *' at 0x7f55b802f3f0> >"
|
||||
"<spot.twa_graph; proxy of <Swig Object of type 'std::shared_ptr< spot::twa_graph > *' at 0x7f523026de10> >"
|
||||
]
|
||||
},
|
||||
"metadata": {},
|
||||
|
|
@ -2418,7 +2418,7 @@
|
|||
"</svg>\n"
|
||||
],
|
||||
"text/plain": [
|
||||
"<spot.impl.twa_product; proxy of <Swig Object of type 'std::shared_ptr< spot::twa_product > *' at 0x7f55b802f360> >"
|
||||
"<spot.impl.twa_product; proxy of <Swig Object of type 'std::shared_ptr< spot::twa_product > *' at 0x7f52302b77b0> >"
|
||||
]
|
||||
},
|
||||
"metadata": {},
|
||||
|
|
@ -2503,7 +2503,7 @@
|
|||
"</svg>\n"
|
||||
],
|
||||
"text/plain": [
|
||||
"<spot.twa_graph; proxy of <Swig Object of type 'std::shared_ptr< spot::twa_graph > *' at 0x7f55b802f2a0> >"
|
||||
"<spot.twa_graph; proxy of <Swig Object of type 'std::shared_ptr< spot::twa_graph > *' at 0x7f5230302450> >"
|
||||
]
|
||||
},
|
||||
"metadata": {},
|
||||
|
|
@ -2600,7 +2600,7 @@
|
|||
"</svg>\n"
|
||||
],
|
||||
"text/plain": [
|
||||
"<spot.twa_graph; proxy of <Swig Object of type 'std::shared_ptr< spot::twa_graph > *' at 0x7f55b802f0f0> >"
|
||||
"<spot.twa_graph; proxy of <Swig Object of type 'std::shared_ptr< spot::twa_graph > *' at 0x7f523026d9c0> >"
|
||||
]
|
||||
},
|
||||
"metadata": {},
|
||||
|
|
@ -2769,7 +2769,7 @@
|
|||
"</svg>\n"
|
||||
],
|
||||
"text/plain": [
|
||||
"<spot.twa_graph; proxy of <Swig Object of type 'std::shared_ptr< spot::twa_graph > *' at 0x7f55b802f960> >"
|
||||
"<spot.twa_graph; proxy of <Swig Object of type 'std::shared_ptr< spot::twa_graph > *' at 0x7f523027d4b0> >"
|
||||
]
|
||||
},
|
||||
"execution_count": 19,
|
||||
|
|
@ -2937,7 +2937,7 @@
|
|||
"</svg>\n"
|
||||
],
|
||||
"text/plain": [
|
||||
"<spot.twa_graph; proxy of <Swig Object of type 'std::shared_ptr< spot::twa_graph > *' at 0x7f55b802f960> >"
|
||||
"<spot.twa_graph; proxy of <Swig Object of type 'std::shared_ptr< spot::twa_graph > *' at 0x7f523027d4b0> >"
|
||||
]
|
||||
},
|
||||
"execution_count": 20,
|
||||
|
|
@ -3100,7 +3100,7 @@
|
|||
"</svg>\n"
|
||||
],
|
||||
"text/plain": [
|
||||
"<spot.twa_graph; proxy of <Swig Object of type 'std::shared_ptr< spot::twa_graph > *' at 0x7f55b802f960> >"
|
||||
"<spot.twa_graph; proxy of <Swig Object of type 'std::shared_ptr< spot::twa_graph > *' at 0x7f523027d4b0> >"
|
||||
]
|
||||
},
|
||||
"metadata": {},
|
||||
|
|
@ -3575,7 +3575,7 @@
|
|||
"name": "python",
|
||||
"nbconvert_exporter": "python",
|
||||
"pygments_lexer": "ipython3",
|
||||
"version": "3.7.2+"
|
||||
"version": "3.6.4"
|
||||
}
|
||||
},
|
||||
"nbformat": 4,
|
||||
|
|
|
|||
File diff suppressed because it is too large
Load diff
|
|
@ -1,6 +1,6 @@
|
|||
#!/usr/bin/python3
|
||||
# -*- mode: python; coding: utf-8 -*-
|
||||
# Copyright (C) 2018 Laboratoire de Recherche et Développement de
|
||||
# Copyright (C) 2018, 2019 Laboratoire de Recherche et Développement de
|
||||
# l'EPITA.
|
||||
#
|
||||
# This file is part of Spot, a model checking library.
|
||||
|
|
@ -21,47 +21,47 @@
|
|||
import spot
|
||||
|
||||
|
||||
for f in ('FGa', 'GFa & GFb & FGc', 'XXX(a U b)'):
|
||||
a1 = spot.translate(f, 'parity')
|
||||
assert a1.acc().is_parity()
|
||||
a2 = spot.translate(f).postprocess('parity')
|
||||
assert a2.acc().is_parity()
|
||||
a3 = spot.translate(f, 'det').postprocess('parity', 'colored')
|
||||
assert a3.acc().is_parity()
|
||||
assert spot.is_colored(a3)
|
||||
|
||||
a = spot.translate('GFa & GFb')
|
||||
try:
|
||||
spot.change_parity_here(a, spot.parity_kind_same, spot.parity_style_even)
|
||||
except RuntimeError as e:
|
||||
assert 'input should have parity acceptance' in str(e)
|
||||
else:
|
||||
exit(2)
|
||||
|
||||
a = spot.automaton("""
|
||||
HOA: v1
|
||||
States: 1
|
||||
Start: 0
|
||||
AP: 1 "a"
|
||||
Acceptance: 2 Fin(0) & Inf(1)
|
||||
--BODY--
|
||||
State: 0
|
||||
[t] 0 {0}
|
||||
--END--
|
||||
""")
|
||||
spot.cleanup_parity_here(a)
|
||||
assert a.to_str() == """HOA: v1
|
||||
States: 1
|
||||
Start: 0
|
||||
AP: 1 "a"
|
||||
acc-name: none
|
||||
Acceptance: 0 f
|
||||
properties: trans-labels explicit-labels state-acc complete
|
||||
properties: deterministic
|
||||
--BODY--
|
||||
State: 0
|
||||
[t] 0
|
||||
--END--"""
|
||||
# for f in ('FGa', 'GFa & GFb & FGc', 'XXX(a U b)'):
|
||||
# a1 = spot.translate(f, 'parity')
|
||||
# assert a1.acc().is_parity()
|
||||
# a2 = spot.translate(f).postprocess('parity')
|
||||
# assert a2.acc().is_parity()
|
||||
# a3 = spot.translate(f, 'det').postprocess('parity', 'colored')
|
||||
# assert a3.acc().is_parity()
|
||||
# assert spot.is_colored(a3)
|
||||
#
|
||||
# a = spot.translate('GFa & GFb')
|
||||
# try:
|
||||
# spot.change_parity_here(a, spot.parity_kind_same, spot.parity_style_even)
|
||||
# except RuntimeError as e:
|
||||
# assert 'input should have parity acceptance' in str(e)
|
||||
# else:
|
||||
# exit(2)
|
||||
#
|
||||
# a = spot.automaton("""
|
||||
# HOA: v1
|
||||
# States: 1
|
||||
# Start: 0
|
||||
# AP: 1 "a"
|
||||
# Acceptance: 2 Fin(0) & Inf(1)
|
||||
# --BODY--
|
||||
# State: 0
|
||||
# [t] 0 {0}
|
||||
# --END--
|
||||
# """)
|
||||
# spot.cleanup_parity_here(a)
|
||||
# assert a.to_str() == """HOA: v1
|
||||
# States: 1
|
||||
# Start: 0
|
||||
# AP: 1 "a"
|
||||
# acc-name: none
|
||||
# Acceptance: 0 f
|
||||
# properties: trans-labels explicit-labels state-acc complete
|
||||
# properties: deterministic
|
||||
# --BODY--
|
||||
# State: 0
|
||||
# [t] 0
|
||||
# --END--"""
|
||||
|
||||
a = spot.automaton("""
|
||||
HOA: v1
|
||||
|
|
@ -87,4 +87,3 @@ properties: deterministic
|
|||
State: 0
|
||||
[t] 0
|
||||
--END--"""
|
||||
|
||||
|
|
|
|||
Loading…
Add table
Add a link
Reference in a new issue