ltlsynt: improve construction of turn-based games
Improve the way transitions are duplicated when preparing the turn-based game for synthesis. The resulting arena should now be deterministic on nodes owned by the environment. Also move the code to another file, so that it is easier to test (e.g. in Python). * bin/ltlsynt.cc: move the code * spot/twaalgos/split.cc, spot/twaalgos/split.hh: move the code and implement the improvements * tests/Makefile.am, tests/python/split.py: test it * tests/core/ltlsynt.test: update existing tests to reflect the changes
This commit is contained in:
Maximilien Colange
parent
4fbcdaca91
commit
1fdc32f9bb
6 changed files with 289 additions and 62 deletions
|
|
@ -34,17 +34,18 @@
|
|||
|
||||
#include <spot/misc/bddlt.hh>
|
||||
#include <spot/misc/game.hh>
|
||||
#include <spot/misc/minato.hh>
|
||||
#include <spot/tl/formula.hh>
|
||||
#include <spot/twa/twagraph.hh>
|
||||
#include <spot/twaalgos/aiger.hh>
|
||||
#include <spot/twaalgos/complete.hh>
|
||||
#include <spot/twaalgos/degen.hh>
|
||||
#include <spot/twaalgos/determinize.hh>
|
||||
#include <spot/twaalgos/parity.hh>
|
||||
#include <spot/twaalgos/sbacc.hh>
|
||||
#include <spot/twaalgos/totgba.hh>
|
||||
#include <spot/twaalgos/translate.hh>
|
||||
#include <spot/twa/twagraph.hh>
|
||||
#include <spot/twaalgos/simulation.hh>
|
||||
#include <spot/twaalgos/split.hh>
|
||||
|
||||
enum
|
||||
{
|
||||
|
|
@ -136,54 +137,6 @@ static bool verbose = false;
|
|||
|
||||
namespace
|
||||
{
|
||||
// Take an automaton and a set of atomic propositions I, and split each
|
||||
// transition
|
||||
//
|
||||
// p -- cond --> q cond in 2^2^AP
|
||||
//
|
||||
// into a set of transitions of the form
|
||||
//
|
||||
// p -- i1 --> r1 -- o1 --> q i1 in 2^I
|
||||
// o1 in 2^O
|
||||
//
|
||||
// p -- i2 --> r2 -- o2 --> q i2 in 2^I
|
||||
// o2 in 2^O
|
||||
// ...
|
||||
//
|
||||
// where O = AP\I, and such that cond = (i1 & o1) | (i2 & o2) | ...
|
||||
//
|
||||
// When determinized, this encodes a game automaton that has a winning
|
||||
// strategy iff aut has an accepting run for any valuation of atomic
|
||||
// propositions in I.
|
||||
|
||||
static spot::twa_graph_ptr
|
||||
split_automaton(const spot::twa_graph_ptr& aut,
|
||||
bdd input_bdd)
|
||||
{
|
||||
auto tgba = spot::to_generalized_buchi(aut);
|
||||
auto split = spot::make_twa_graph(tgba->get_dict());
|
||||
split->copy_ap_of(tgba);
|
||||
split->copy_acceptance_of(tgba);
|
||||
split->new_states(tgba->num_states());
|
||||
split->set_init_state(tgba->get_init_state_number());
|
||||
|
||||
for (unsigned src = 0; src < tgba->num_states(); ++src)
|
||||
for (const auto& e: tgba->out(src))
|
||||
{
|
||||
spot::minato_isop isop(e.cond);
|
||||
bdd cube;
|
||||
while ((cube = isop.next()) != bddfalse)
|
||||
{
|
||||
unsigned q = split->new_state();
|
||||
bdd in = bdd_existcomp(cube, input_bdd);
|
||||
bdd out = bdd_exist(cube, input_bdd);
|
||||
split->new_edge(src, q, in, {});
|
||||
split->new_edge(q, e.dst, out, e.acc);
|
||||
}
|
||||
}
|
||||
split->prop_universal(spot::trival::maybe());
|
||||
return split;
|
||||
}
|
||||
|
||||
// Ensures that the game is complete for player 0.
|
||||
// Also computes the owner of each state (false for player 0, i.e. env).
|
||||
|
|
@ -232,7 +185,9 @@ namespace
|
|||
static spot::twa_graph_ptr
|
||||
to_dpa(const spot::twa_graph_ptr& split)
|
||||
{
|
||||
auto dpa = spot::tgba_determinize(split);
|
||||
// if the input automaton is deterministic, degeneralize it to be sure to
|
||||
// end up with a parity automaton
|
||||
auto dpa = spot::tgba_determinize(spot::degeneralize_tba(split));
|
||||
dpa->merge_edges();
|
||||
if (opt_print_pg)
|
||||
dpa = spot::sbacc(dpa);
|
||||
|
|
@ -338,7 +293,7 @@ namespace
|
|||
all_outputs &= bdd_ithvar(v);
|
||||
}
|
||||
|
||||
auto split = split_automaton(aut, all_inputs);
|
||||
auto split = split_2step(aut, all_inputs);
|
||||
if (verbose)
|
||||
std::cerr << "split inputs and outputs done" << std::endl;
|
||||
auto dpa = to_dpa(split);
|
||||
|
|
|
|||
|
|
@ -19,9 +19,154 @@
|
|||
|
||||
#include "config.h"
|
||||
#include <spot/twaalgos/split.hh>
|
||||
#include <spot/misc/minato.hh>
|
||||
#include <spot/twaalgos/totgba.hh>
|
||||
#include <spot/misc/bddlt.hh>
|
||||
|
||||
namespace spot
|
||||
{
|
||||
twa_graph_ptr
|
||||
split_2step(const const_twa_graph_ptr& aut, bdd input_bdd)
|
||||
{
|
||||
if (!aut->acc().is_generalized_buchi())
|
||||
throw std::runtime_error("2step_split only works on TGBA");
|
||||
auto split = make_twa_graph(aut->get_dict());
|
||||
split->copy_ap_of(aut);
|
||||
split->copy_acceptance_of(aut);
|
||||
split->new_states(aut->num_states());
|
||||
split->set_init_state(aut->get_init_state_number());
|
||||
|
||||
std::unordered_map<bdd, unsigned, spot::bdd_hash> sig2state;
|
||||
|
||||
unsigned set_num = split->get_dict()
|
||||
->register_anonymous_variables(aut->num_states()+1, &sig2state);
|
||||
bdd all_states = bddtrue;
|
||||
for (unsigned i = 0; i <= aut->num_states(); ++i)
|
||||
all_states &= bdd_ithvar(set_num + i);
|
||||
|
||||
unsigned acc_vars = split->get_dict()
|
||||
->register_anonymous_variables(aut->num_sets(), &sig2state);
|
||||
bdd all_acc = bddtrue;
|
||||
for (unsigned i = 0; i < aut->num_sets(); ++i)
|
||||
all_acc &= bdd_ithvar(acc_vars + i);
|
||||
|
||||
for (unsigned src = 0; src < aut->num_states(); ++src)
|
||||
{
|
||||
std::unordered_map<bdd, bdd, spot::bdd_hash> input2sig;
|
||||
bdd support = bddtrue;
|
||||
for (const auto& e : aut->out(src))
|
||||
support &= bdd_support(e.cond);
|
||||
support = bdd_existcomp(support, input_bdd);
|
||||
|
||||
bdd all_letters = bddtrue;
|
||||
while (all_letters != bddfalse)
|
||||
{
|
||||
bdd one_letter = bdd_satoneset(all_letters, support, bddtrue);
|
||||
all_letters -= one_letter;
|
||||
auto it = input2sig.emplace(one_letter, bddfalse).first;
|
||||
|
||||
for (const auto& e : aut->out(src))
|
||||
{
|
||||
bdd sig = bddtrue;
|
||||
sig &= bdd_exist(e.cond & one_letter, input_bdd);
|
||||
|
||||
for (auto n : e.acc.sets())
|
||||
sig &= bdd_ithvar(acc_vars + n);
|
||||
sig &= bdd_ithvar(set_num + e.dst);
|
||||
|
||||
it->second |= sig;
|
||||
}
|
||||
}
|
||||
|
||||
for (const auto& in : input2sig)
|
||||
{
|
||||
bdd sig = in.second;
|
||||
auto it = sig2state.find(sig);
|
||||
if (it == sig2state.end())
|
||||
{
|
||||
unsigned ns = split->new_state();
|
||||
it = sig2state.emplace(sig, ns).first;
|
||||
}
|
||||
split->new_edge(src, it->second, in.first);
|
||||
}
|
||||
}
|
||||
|
||||
// Now add all states based on their signatures
|
||||
// This is very similar to the code of the simulation
|
||||
bdd nonapvars = all_acc & all_states;
|
||||
for (const auto& sig : sig2state)
|
||||
{
|
||||
// for each valuation, extract cond, acc and dst
|
||||
bdd sup_sig = bdd_support(sig.first);
|
||||
bdd sup_all_atomic_prop = bdd_exist(sup_sig, nonapvars);
|
||||
bdd all_atomic_prop = bdd_exist(sig.first, nonapvars);
|
||||
|
||||
// FIXME this is overkill, is not it?
|
||||
while (all_atomic_prop != bddfalse)
|
||||
{
|
||||
bdd one = bdd_satoneset(all_atomic_prop, sup_all_atomic_prop,
|
||||
bddtrue);
|
||||
all_atomic_prop -= one;
|
||||
|
||||
minato_isop isop(sig.first & one);
|
||||
bdd cond_acc_dest;
|
||||
while ((cond_acc_dest = isop.next()) != bddfalse)
|
||||
{
|
||||
|
||||
bdd cond = bdd_existcomp(cond_acc_dest, sup_all_atomic_prop);
|
||||
unsigned dst =
|
||||
bdd_var(bdd_existcomp(cond_acc_dest, all_states)) - set_num;
|
||||
|
||||
bdd acc = bdd_existcomp(cond_acc_dest, all_acc);
|
||||
spot::acc_cond::mark_t m({});
|
||||
while (acc != bddtrue)
|
||||
{
|
||||
m.set(bdd_var(acc) - acc_vars);
|
||||
acc = bdd_high(acc);
|
||||
}
|
||||
|
||||
split->new_edge(sig.second, dst, cond, m);
|
||||
}
|
||||
}
|
||||
}
|
||||
|
||||
split->get_dict()->unregister_all_my_variables(&sig2state);
|
||||
|
||||
split->merge_edges();
|
||||
|
||||
split->prop_universal(spot::trival::maybe());
|
||||
return split;
|
||||
}
|
||||
|
||||
twa_graph_ptr unsplit_2step(const const_twa_graph_ptr& aut)
|
||||
{
|
||||
twa_graph_ptr out = make_twa_graph(aut->get_dict());
|
||||
out->copy_acceptance_of(aut);
|
||||
out->copy_ap_of(aut);
|
||||
out->new_states(aut->num_states());
|
||||
out->set_init_state(aut->get_init_state_number());
|
||||
|
||||
std::vector<bool> seen(aut->num_states(), false);
|
||||
std::deque<unsigned> todo;
|
||||
todo.push_back(aut->get_init_state_number());
|
||||
seen[aut->get_init_state_number()] = true;
|
||||
while (!todo.empty())
|
||||
{
|
||||
unsigned cur = todo.front();
|
||||
todo.pop_front();
|
||||
seen[cur] = true;
|
||||
|
||||
for (const auto& i : aut->out(cur))
|
||||
for (const auto& o : aut->out(i.dst))
|
||||
{
|
||||
out->new_edge(cur, o.dst, i.cond & o.cond, i.acc | o.acc);
|
||||
if (!seen[o.dst])
|
||||
todo.push_back(o.dst);
|
||||
}
|
||||
}
|
||||
return out;
|
||||
}
|
||||
|
||||
twa_graph_ptr split_edges(const const_twa_graph_ptr& aut)
|
||||
{
|
||||
twa_graph_ptr out = make_twa_graph(aut->get_dict());
|
||||
|
|
|
|||
|
|
@ -31,4 +31,24 @@ namespace spot
|
|||
/// propositions. After this we can consider that each edge of the
|
||||
/// automate is a transition labeled by one letter.
|
||||
SPOT_API twa_graph_ptr split_edges(const const_twa_graph_ptr& aut);
|
||||
|
||||
/// \brief make each transition a 2-step transition
|
||||
///
|
||||
/// Given a set of atomic propositions I, split each transition
|
||||
/// p -- cond --> q cond in 2^2^AP
|
||||
/// into a set of transitions of the form
|
||||
/// p -- {a} --> (p,a) -- o --> q
|
||||
/// for each a in cond \cap 2^2^I
|
||||
/// and where o = (cond & a) \cap 2^2^(AP - I)
|
||||
///
|
||||
/// By definition, the states p are deterministic, only the states of the form
|
||||
/// (p,a) may be non-deterministic.
|
||||
/// This function is used to transform an automaton into a turn-based game in
|
||||
/// the context of LTL reactive synthesis.
|
||||
SPOT_API twa_graph_ptr
|
||||
split_2step(const const_twa_graph_ptr& aut, bdd input_bdd);
|
||||
|
||||
/// \brief the reverse of 2step_split
|
||||
SPOT_API twa_graph_ptr
|
||||
unsplit_2step(const const_twa_graph_ptr& aut);
|
||||
}
|
||||
|
|
|
|||
|
|
@ -393,6 +393,7 @@ TESTS_python = \
|
|||
python/setacc.py \
|
||||
python/setxor.py \
|
||||
python/simstate.py \
|
||||
python/split.py \
|
||||
python/streett_totgba.py \
|
||||
python/streett_totgba2.py \
|
||||
python/rs_like.py \
|
||||
|
|
|
|||
|
|
@ -23,22 +23,25 @@
|
|||
set -e
|
||||
|
||||
cat >exp <<EOF
|
||||
parity 16;
|
||||
parity 19;
|
||||
0 0 0 1,2 "INIT";
|
||||
2 0 1 3;
|
||||
3 2 0 4,5;
|
||||
5 0 1 3,6;
|
||||
6 3 0 4,5;
|
||||
4 0 1 7,8;
|
||||
8 2 0 9,10;
|
||||
10 3 1 3,11;
|
||||
11 0 0 4,5;
|
||||
9 0 1 8,12;
|
||||
12 1 0 9,10;
|
||||
7 1 0 4,13;
|
||||
13 2 1 3,6;
|
||||
1 3 1 3,14;
|
||||
14 3 0 1,2;
|
||||
8 0 0 9,10;
|
||||
10 0 1 11,12;
|
||||
12 0 0 9,13;
|
||||
13 1 1 11,12;
|
||||
11 2 0 9,10;
|
||||
9 3 1 3,6;
|
||||
7 0 0 14,15;
|
||||
15 1 1 7,11;
|
||||
14 2 1 3,6;
|
||||
1 0 1 3,16;
|
||||
16 3 0 2,17;
|
||||
17 3 1 3,16;
|
||||
EOF
|
||||
ltlsynt --ins='a' --outs='b' -f 'GFa <-> GFb' --print-pg > out
|
||||
diff out exp
|
||||
|
|
|
|||
103
tests/python/split.py
Normal file
103
tests/python/split.py
Normal file
|
|
@ -0,0 +1,103 @@
|
|||
# -*- mode: python; coding: utf-8 -*-
|
||||
# Copyright (C) 2018 Laboratoire de Recherche et
|
||||
# Développement de l'Epita
|
||||
#
|
||||
# This file is part of Spot, a model checking library.
|
||||
#
|
||||
# Spot is free software; you can redistribute it and/or modify it
|
||||
# under the terms of the GNU General Public License as published by
|
||||
# the Free Software Foundation; either version 3 of the License, or
|
||||
# (at your option) any later version.
|
||||
#
|
||||
# Spot is distributed in the hope that it will be useful, but WITHOUT
|
||||
# ANY WARRANTY; without even the implied warranty of MERCHANTABILITY
|
||||
# or FITNESS FOR A PARTICULAR PURPOSE. See the GNU General Public
|
||||
# License for more details.
|
||||
#
|
||||
# You should have received a copy of the GNU General Public License
|
||||
# along with this program. If not, see <http://www.gnu.org/licenses/>.
|
||||
|
||||
import spot
|
||||
|
||||
def incl(a,b):
|
||||
return not b.intersects(spot.dualize(spot.tgba_determinize(a)))
|
||||
def equiv(a,b):
|
||||
return incl(a,b) and incl(b,a)
|
||||
|
||||
def do_split(f, in_list):
|
||||
aut = spot.translate(f)
|
||||
inputs = spot.buddy.bddtrue
|
||||
for a in in_list:
|
||||
inputs &= spot.buddy.bdd_ithvar(aut.get_dict().varnum(spot.formula(a)))
|
||||
s = spot.split_2step(aut, inputs)
|
||||
return aut,s
|
||||
|
||||
aut, s = do_split('(FG !a) <-> (GF b)', ['a'])
|
||||
assert equiv(aut, spot.unsplit_2step(s))
|
||||
|
||||
aut, s = do_split('GFa && GFb', ['a'])
|
||||
assert equiv(aut, spot.unsplit_2step(s))
|
||||
assert s.to_str() == """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
|
||||
--BODY--
|
||||
State: 0
|
||||
[!0] 1
|
||||
[0] 2
|
||||
State: 1
|
||||
[!1] 0
|
||||
[1] 0 {1}
|
||||
State: 2
|
||||
[!1] 0 {0}
|
||||
[1] 0 {0 1}
|
||||
--END--"""
|
||||
|
||||
aut, s = do_split('! ((G (req -> (F ack))) && (G (go -> (F grant))))', ['go',
|
||||
'req'])
|
||||
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
|
||||
#assert s.to_str() == """HOA: v1
|
||||
#States: 9
|
||||
#Start: 0
|
||||
#AP: 4 "ack" "req" "go" "grant"
|
||||
#acc-name: Buchi
|
||||
#Acceptance: 1 Inf(0)
|
||||
#properties: trans-labels explicit-labels state-acc
|
||||
#--BODY--
|
||||
#State: 0
|
||||
#[1&!2] 3
|
||||
#[!1&!2] 4
|
||||
#[1&2] 5
|
||||
#[!1&2] 6
|
||||
#State: 1
|
||||
#[t] 7
|
||||
#State: 2
|
||||
#[t] 8
|
||||
#State: 3
|
||||
#[t] 0
|
||||
#[!0] 1
|
||||
#State: 4
|
||||
#[t] 0
|
||||
#State: 5
|
||||
#[t] 0
|
||||
#[!0] 1
|
||||
#[!3] 2
|
||||
#State: 6
|
||||
#[t] 0
|
||||
#[!3] 2
|
||||
#State: 7 {0}
|
||||
#[!0] 1
|
||||
#State: 8 {0}
|
||||
#[!3] 2
|
||||
#--END--"""
|
||||
|
||||
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'])
|
||||
assert equiv(aut, spot.unsplit_2step(s))
|
||||
|
||||
Loading…
Add table
Add a link
Reference in a new issue