Use new minterm enumeration in split_2step
Also remove self-loop for sink and make it work for any acceptance condition. * spot/twaalgos/synthesis.cc: Here * tests/core/ltlsynt.test: Adjust tests * tests/python/split.py: Adjust tests
This commit is contained in:
philipp
Florian Renkin
parent
98ab826255
commit
a5185c2123
3 changed files with 70 additions and 66 deletions
|
|
@ -143,7 +143,12 @@ namespace spot
|
|||
split->copy_acceptance_of(aut);
|
||||
split->new_states(aut->num_states());
|
||||
split->set_init_state(aut->get_init_state_number());
|
||||
split->set_named_prop<bdd>("synthesis-output", new bdd(output_bdd));
|
||||
|
||||
auto [is_unsat, unsat_mark] = aut->acc().unsat_mark();
|
||||
if (!is_unsat && complete_env)
|
||||
throw std::runtime_error("split_2step(): Can not complete arena for "
|
||||
"env as there is no unsat mark.");
|
||||
|
||||
bdd input_bdd = bddtrue;
|
||||
{
|
||||
|
|
@ -166,7 +171,7 @@ namespace spot
|
|||
|
||||
// a sort of hash-map for all new intermediate states
|
||||
std::unordered_multimap<size_t, unsigned> env_hash;
|
||||
env_hash.reserve((int) 1.5 * aut->num_states());
|
||||
env_hash.reserve((int) (1.5 * aut->num_states()));
|
||||
// a local map for edges leaving the current src
|
||||
// this avoids creating and then combining edges for each minterm
|
||||
// Note there are usually "few" edges leaving a state
|
||||
|
|
@ -188,11 +193,15 @@ namespace spot
|
|||
|
||||
// If a completion is demanded we might have to create sinks
|
||||
// Sink controlled by player
|
||||
auto get_sink_con_state = [&split]()
|
||||
auto get_sink_con_state = [&split, um = unsat_mark](bool create = true)
|
||||
{
|
||||
static unsigned sink_con=0;
|
||||
if (SPOT_UNLIKELY(sink_con == 0))
|
||||
sink_con = split->new_state();
|
||||
static unsigned sink_con=-1u;
|
||||
if (SPOT_UNLIKELY((sink_con == -1u) && create))
|
||||
{
|
||||
sink_con = split->new_states(2);
|
||||
split->new_edge(sink_con, sink_con+1, bddtrue, um);
|
||||
split->new_edge(sink_con+1, sink_con, bddtrue, um);
|
||||
}
|
||||
return sink_con;
|
||||
};
|
||||
|
||||
|
|
@ -242,10 +251,8 @@ namespace spot
|
|||
// get different intermediate states
|
||||
std::sort(e_cache.begin(), e_cache.end(), less_info);
|
||||
|
||||
while (all_letters != bddfalse)
|
||||
for (auto one_letter : minterms_of(all_letters, input_bdd))
|
||||
{
|
||||
bdd one_letter = bdd_satoneset(all_letters, support, bddtrue);
|
||||
all_letters -= one_letter;
|
||||
|
||||
dests.clear();
|
||||
for (const auto& e_info : e_cache)
|
||||
|
|
@ -314,15 +321,20 @@ namespace spot
|
|||
} // v-src
|
||||
|
||||
split->merge_edges();
|
||||
split->prop_universal(spot::trival::maybe());
|
||||
split->prop_universal(trival::maybe());
|
||||
|
||||
// The named property
|
||||
// compute the owners
|
||||
// env is equal to false
|
||||
std::vector<bool> owner(split->num_states(), false);
|
||||
std::vector<bool>* owner =
|
||||
new std::vector<bool>(split->num_states(), false);
|
||||
// All "new" states belong to the player
|
||||
std::fill(owner.begin()+aut->num_states(), owner.end(), true);
|
||||
set_state_players(split, std::move(owner));
|
||||
std::fill(owner->begin()+aut->num_states(), owner->end(), true);
|
||||
// Check if sinks have been created
|
||||
if (get_sink_con_state(false) != -1u)
|
||||
owner->at(get_sink_con_state(false)) = false;
|
||||
split->set_named_prop("state-player", owner);
|
||||
|
||||
// Done
|
||||
return split;
|
||||
}
|
||||
|
|
|
|||
|
|
@ -25,23 +25,23 @@ set -e
|
|||
cat >exp <<EOF
|
||||
parity 17;
|
||||
0 1 0 7,8 "INIT";
|
||||
8 3 1 1,2;
|
||||
8 3 1 2;
|
||||
2 1 0 11,12;
|
||||
12 5 1 1,4;
|
||||
4 1 0 7,15;
|
||||
15 3 1 5,6;
|
||||
6 1 0 7,15;
|
||||
7 3 1 2;
|
||||
5 1 0 16,17;
|
||||
17 4 1 5,6;
|
||||
16 4 1 2;
|
||||
1 1 0 9,10;
|
||||
10 3 1 1,5;
|
||||
9 3 1 2,3;
|
||||
12 5 1 2,3;
|
||||
3 1 0 13,14;
|
||||
14 4 1 1,4;
|
||||
13 4 1 2,3;
|
||||
11 5 1 2,3;
|
||||
14 4 1 2,3;
|
||||
13 4 1 1,4;
|
||||
4 1 0 8,15;
|
||||
15 3 1 5,6;
|
||||
6 1 0 8,15;
|
||||
5 1 0 16,17;
|
||||
17 4 1 2;
|
||||
16 4 1 5,6;
|
||||
1 1 0 9,10;
|
||||
10 3 1 2,3;
|
||||
9 3 1 1,5;
|
||||
11 5 1 1,4;
|
||||
7 3 1 1,2;
|
||||
parity 13;
|
||||
0 1 0 1,2 "INIT";
|
||||
2 1 1 3;
|
||||
|
|
@ -59,11 +59,11 @@ parity 13;
|
|||
1 1 1 6,3;
|
||||
parity 5;
|
||||
1 1 0 4,5 "INIT";
|
||||
5 5 1 0,1;
|
||||
5 4 1 1,1;
|
||||
4 5 1 0,1;
|
||||
0 1 0 2,3;
|
||||
3 3 1 0,0;
|
||||
2 5 1 1;
|
||||
4 4 1 1,1;
|
||||
3 5 1 1;
|
||||
2 3 1 0,0;
|
||||
EOF
|
||||
|
||||
: > out
|
||||
|
|
@ -221,7 +221,7 @@ cat >exp <<EOF
|
|||
translating formula done in X seconds
|
||||
automaton has 3 states and 2 colors
|
||||
split inputs and outputs done in X seconds
|
||||
automaton has 9 states
|
||||
automaton has 10 states
|
||||
determinization done
|
||||
DPA has 12 states, 4 colors
|
||||
simplification done
|
||||
|
|
|
|||
|
|
@ -41,7 +41,7 @@ def equiv(a, b):
|
|||
return incl(a, b) and incl(b, a)
|
||||
|
||||
|
||||
def do_split(f, in_list, out_list):
|
||||
def do_split(f, out_list):
|
||||
aut = spot.translate(f)
|
||||
outputs = spot.buddy.bddtrue
|
||||
for a in out_list:
|
||||
|
|
@ -49,50 +49,42 @@ def do_split(f, in_list, out_list):
|
|||
s = spot.split_2step(aut, outputs, False, False)
|
||||
return aut, s
|
||||
|
||||
def str_diff(expect, obtained):
|
||||
res = expect == obtained
|
||||
if not res:
|
||||
print("Expected:\n", expect, "\nbut obtained:\n", obtained)
|
||||
return res
|
||||
|
||||
|
||||
|
||||
aut, s = do_split('(FG !a) <-> (GF b)', ['a'], ['b'])
|
||||
aut, s = do_split('(FG !a) <-> (GF b)', ['b'])
|
||||
assert equiv(aut, spot.unsplit_2step(s))
|
||||
|
||||
del aut
|
||||
del s
|
||||
gcollect()
|
||||
|
||||
aut, s = do_split('GFa && GFb', ['a'], ['b'])
|
||||
aut, s = do_split('GFa && GFb', ['b'])
|
||||
assert equiv(aut, spot.unsplit_2step(s))
|
||||
assert str_diff("""HOA: v1
|
||||
States: 3
|
||||
Start: 0
|
||||
AP: 2 "a" "b"
|
||||
acc-name: generalized-Buchi 2
|
||||
Acceptance: 2 Inf(0)&Inf(1)
|
||||
properties: trans-labels explicit-labels trans-acc complete
|
||||
properties: deterministic
|
||||
spot-state-player: 0 1 1
|
||||
--BODY--
|
||||
State: 0
|
||||
[0] 1
|
||||
[!0] 2
|
||||
State: 1
|
||||
[!1] 0 {0}
|
||||
[1] 0 {0 1}
|
||||
State: 2
|
||||
[!1] 0
|
||||
[1] 0 {1}
|
||||
--END--""", s.to_str() )
|
||||
# FIXME see below
|
||||
# assert str_diff("""HOA: v1
|
||||
# States: 3
|
||||
# Start: 0
|
||||
# AP: 2 "a" "b"
|
||||
# acc-name: generalized-Buchi 2
|
||||
# Acceptance: 2 Inf(0)&Inf(1)
|
||||
# properties: trans-labels explicit-labels trans-acc complete
|
||||
# properties: deterministic
|
||||
# spot-state-player: 0 1 1
|
||||
# --BODY--
|
||||
# State: 0
|
||||
# [0] 1
|
||||
# [!0] 2
|
||||
# State: 1
|
||||
# [!1] 0 {0}
|
||||
# [1] 0 {0 1}
|
||||
# State: 2
|
||||
# [!1] 0
|
||||
# [1] 0 {1}
|
||||
# --END--""", s.to_str() )
|
||||
|
||||
del aut
|
||||
del s
|
||||
gcollect()
|
||||
|
||||
aut, s = do_split('! ((G (req -> (F ack))) && (G (go -> (F grant))))',
|
||||
['go', 'req'], ['ack'])
|
||||
aut, s = do_split('! ((G (req -> (F ack))) && (G (go -> (F grant))))', ['ack'])
|
||||
assert equiv(aut, spot.unsplit_2step(s))
|
||||
# FIXME s.to_str() is NOT the same on Debian stable and on Debian unstable
|
||||
# we should investigate this
|
||||
|
|
@ -137,5 +129,5 @@ gcollect()
|
|||
|
||||
aut, s = do_split('((G (((! g_0) || (! g_1)) && ((r_0 && (X r_1)) -> (F (g_0 \
|
||||
&& g_1))))) && (G (r_0 -> F g_0))) && (G (r_1 -> F g_1))',
|
||||
['r_0', 'r_1'], ['g_0', 'g_1'])
|
||||
['g_0', 'g_1'])
|
||||
assert equiv(aut, spot.unsplit_2step(s))
|
||||
|
|
|
|||
Loading…
Add table
Add a link
Reference in a new issue