alarsyo/spot
1
0
Fork 0
Code Issues Pull requests Projects Releases Wiki Activity

Improving split and reorganizing

Browse source 
* spot/twaalgos/synthesis.cc, spot/twaalgos/synthesis.hh: New files
regrouping the functionnalities split and apply_strategy for synthesis
* python/spot/impl.i, spot/twaalgos/Makefile.am: Add them.
* spot/twaalgos/split.cc, spot/twaalgos/split.hh: No longer contains
the splits necessary for for synthesis, moved to
spot/twaalgos/synthesis.cc, spot/twaalgos/split.hh Split is now faster
and reduces the number of intermediate states, reducing the overall
size of the arena
* spot/misc/game.cc, spot/misc/game.hh: Renaming propagate_players to
alternate_players.
* tests/core/ltlsynt.test, tests/python/split.py: Update tests.
* bin/ltlsynt.cc: Adjust to new split. Swap order of split and
to_parity for lar.
This commit is contained in:
philipp 2020-09-24 16:25:53 +02:00 • committed by Alexandre Duret-Lutz
parent ca043bd62d
commit 29055c8109
11 changed files with 641 additions and 308 deletions
Download patch file Download diff file Expand all files Collapse all files

176
bin/ltlsynt.cc
View file

@ -47,7 +47,7 @@
#include <spot/twaalgos/translate.hh>
#include <spot/twa/twagraph.hh>
#include <spot/twaalgos/simulation.hh>
#include <spot/twaalgos/split.hh>
#include <spot/twaalgos/synthesis.hh>
#include <spot/twaalgos/toparity.hh>
#include <spot/twaalgos/hoa.hh>
@ -140,7 +140,6 @@ static spot::option_map extra_options;
static double trans_time = 0.0;
static double split_time = 0.0;
static double paritize_time = 0.0;
static double bgame_time = 0.0;
static double solve_time = 0.0;
static double strat2aut_time = 0.0;
static unsigned nb_states_dpa = 0;
@ -188,6 +187,14 @@ static bool verbose = false;
namespace
{
auto str_tolower = [] (std::string s)
{
std::transform(s.begin(), s.end(), s.begin(),
[](unsigned char c){ return std::tolower(c); });
return s;
};
static spot::twa_graph_ptr
to_dpa(const spot::twa_graph_ptr& split)
{
@ -212,104 +219,6 @@ namespace
return dpa;
}
spot::twa_graph_ptr
apply_strategy(const spot::twa_graph_ptr& arena,
bdd all_outputs,
bool unsplit, bool keep_acc, bool leave_choice)
{
spot::region_t* w_ptr =
arena->get_named_prop<spot::region_t>("state-winner");
spot::strategy_t* s_ptr =
arena->get_named_prop<spot::strategy_t>("strategy");
std::vector<bool>* sp_ptr =
arena->get_named_prop<std::vector<bool>>("state-player");
if (!w_ptr || !s_ptr || !sp_ptr)
throw std::runtime_error("Arena missing state-winner, strategy "
"or state-player");
if (!(w_ptr->at(arena->get_init_state_number())))
throw std::runtime_error("Player does not win initial state, strategy "
"is not applicable");
spot::region_t& w = *w_ptr;
spot::strategy_t& s = *s_ptr;
auto aut = spot::make_twa_graph(arena->get_dict());
aut->copy_ap_of(arena);
if (keep_acc)
aut->copy_acceptance_of(arena);
const unsigned unseen_mark = std::numeric_limits<unsigned>::max();
std::vector<unsigned> todo{arena->get_init_state_number()};
std::vector<unsigned> pg2aut(arena->num_states(), unseen_mark);
aut->set_init_state(aut->new_state());
pg2aut[arena->get_init_state_number()] = aut->get_init_state_number();
bdd out;
while (!todo.empty())
{
unsigned v = todo.back();
todo.pop_back();
// Env edge -> keep all
for (auto &e1: arena->out(v))
{
assert(w.at(e1.dst));
if (!unsplit)
{
if (pg2aut[e1.dst] == unseen_mark)
pg2aut[e1.dst] = aut->new_state();
aut->new_edge(pg2aut[v], pg2aut[e1.dst], e1.cond,
keep_acc ? e1.acc : spot::acc_cond::mark_t({}));
}
// Player strat
auto &e2 = arena->edge_storage(s[e1.dst]);
if (pg2aut[e2.dst] == unseen_mark)
{
pg2aut[e2.dst] = aut->new_state();
todo.push_back(e2.dst);
}
if (leave_choice)
// Leave the choice
out = e2.cond;
else
// Save only one letter
out = bdd_satoneset(e2.cond, all_outputs, bddfalse);
aut->new_edge(unsplit ? pg2aut[v] : pg2aut[e1.dst],
pg2aut[e2.dst],
unsplit ? (e1.cond & out):out,
keep_acc ? e2.acc : spot::acc_cond::mark_t({}));
}
}
aut->set_named_prop("synthesis-outputs", new bdd(all_outputs));
// If no unsplitting is demanded, it remains a two-player arena
// We do not need to track winner as this is a
// strategy automaton
if (!unsplit)
{
std::vector<bool>& sp_pg = * sp_ptr;
std::vector<bool> sp_aut(aut->num_states());
spot::strategy_t str_aut(aut->num_states());
for (unsigned i = 0; i < arena->num_states(); ++i)
{
if (pg2aut[i] == unseen_mark)
// Does not appear in strategy
continue;
sp_aut[pg2aut[i]] = sp_pg[i];
str_aut[pg2aut[i]] = s[i];
}
aut->set_named_prop("state-player",
new std::vector<bool>(std::move(sp_aut)));
aut->set_named_prop("state-winner",
new spot::region_t(aut->num_states(), true));
aut->set_named_prop("strategy",
new spot::strategy_t(std::move(str_aut)));
}
return aut;
}
static void
print_csv(spot::formula f, bool realizable)
{
@ -324,7 +233,7 @@ namespace
if (!outf.append())
{
out << ("\"formula\",\"algo\",\"trans_time\","
"\"split_time\",\"todpa_time\",\"build_game_time\"");
"\"split_time\",\"todpa_time\"");
if (!opt_print_pg && !opt_print_hoa)
{
out << ",\"solve_time\"";
@ -341,8 +250,7 @@ namespace
out << "\",\"" << solver_names[opt_solver]
<< "\"," << trans_time
<< ',' << split_time
<< ',' << paritize_time
<< ',' << bgame_time;
<< ',' << paritize_time;
if (!opt_print_pg && !opt_print_hoa)
{
out << ',' << solve_time;
@ -401,20 +309,14 @@ namespace
auto aut = trans_.run(&f);
bdd all_inputs = bddtrue;
bdd all_outputs = bddtrue;
for (unsigned i = 0; i < input_aps_.size(); ++i)
for (const auto& ap_i : input_aps_)
{
std::ostringstream lowercase;
for (char c: input_aps_[i])
lowercase << (char)std::tolower(c);
unsigned v = aut->register_ap(spot::formula::ap(lowercase.str()));
unsigned v = aut->register_ap(spot::formula::ap(ap_i));
all_inputs &= bdd_ithvar(v);
}
for (unsigned i = 0; i < output_aps_.size(); ++i)
for (const auto& ap_i : output_aps_)
{
std::ostringstream lowercase;
for (char c: output_aps_[i])
lowercase << (char)std::tolower(c);
unsigned v = aut->register_ap(spot::formula::ap(lowercase.str()));
unsigned v = aut->register_ap(spot::formula::ap(ap_i));
all_outputs &= bdd_ithvar(v);
}
if (want_time)
@ -449,7 +351,7 @@ namespace
<< paritize_time << " seconds\n";
if (want_time)
sw.start();
dpa = split_2step(tmp, all_inputs);
dpa = split_2step(tmp, all_inputs, all_outputs, true, true);
spot::colorize_parity_here(dpa, true);
if (want_time)
split_time = sw.stop();
@ -472,7 +374,7 @@ namespace
<< " states\n";
if (want_time)
sw.start();
dpa = split_2step(aut, all_inputs);
dpa = split_2step(aut, all_inputs, all_outputs, true, true);
spot::colorize_parity_here(dpa, true);
if (want_time)
split_time = sw.stop();
@ -486,7 +388,8 @@ namespace
{
if (want_time)
sw.start();
auto split = split_2step(aut, all_inputs);
auto split = split_2step(aut, all_inputs, all_outputs,
true, false);
if (want_time)
split_time = sw.stop();
if (verbose)
@ -508,33 +411,26 @@ namespace
<< paritize_time << " seconds\n";
if (want_time)
paritize_time = sw.stop();
// The named property "state-player" is set in split_2step
// but not propagated by to_dpa
alternate_players(dpa);
break;
}
case LAR:
case LAR_OLD:
{
if (want_time)
sw.start();
dpa = split_2step(aut, all_inputs);
dpa->merge_states();
if (want_time)
split_time = sw.stop();
if (verbose)
std::cerr << "split inputs and outputs done in " << split_time
<< " seconds\nautomaton has "
<< dpa->num_states() << " states\n";
if (want_time)
sw.start();
if (opt_solver == LAR)
{
dpa = spot::to_parity(dpa);
dpa = spot::to_parity(aut);
// reduce_parity is called by to_parity(),
// but with colorization turned off.
spot::colorize_parity_here(dpa, true);
}
else
{
dpa = spot::to_parity_old(dpa);
dpa = spot::to_parity_old(aut);
dpa = reduce_parity_here(dpa, true);
}
spot::change_parity_here(dpa, spot::parity_kind_max,
@ -546,17 +442,21 @@ namespace
<< " seconds\nDPA has "
<< dpa->num_states() << " states, "
<< dpa->num_sets() << " colors\n";
if (want_time)
sw.start();
dpa = split_2step(dpa, all_inputs, all_outputs, true, true);
spot::colorize_parity_here(dpa, true);
if (want_time)
split_time = sw.stop();
if (verbose)
std::cerr << "split inputs and outputs done in " << split_time
<< " seconds\nautomaton has "
<< dpa->num_states() << " states\n";
break;
}
}
nb_states_dpa = dpa->num_states();
if (want_time)
sw.start();
propagate_players(dpa, false, true);
if (want_time)
bgame_time = sw.stop();
if (verbose)
std::cerr << "parity game built in " << bgame_time << " seconds\n";
if (opt_print_pg)
{
@ -588,7 +488,7 @@ namespace
if (want_time)
sw.start();
auto strat_aut = apply_strategy(dpa, all_outputs,
true, false, true);
true, false);
if (want_time)
strat2aut_time = sw.stop();
@ -641,7 +541,7 @@ parse_opt(int key, char* arg, struct argp_state*)
while (std::getline(aps, ap, ','))
{
ap.erase(remove_if(ap.begin(), ap.end(), isspace), ap.end());
input_aps.push_back(ap);
input_aps.push_back(str_tolower(ap));
}
break;
}
@ -652,7 +552,7 @@ parse_opt(int key, char* arg, struct argp_state*)
while (std::getline(aps, ap, ','))
{
ap.erase(remove_if(ap.begin(), ap.end(), isspace), ap.end());
output_aps.push_back(ap);
output_aps.push_back(str_tolower(ap));
}
break;
}

2
python/spot/impl.i
View file

@ -153,6 +153,7 @@
#include <spot/twaalgos/powerset.hh>
#include <spot/twaalgos/product.hh>
#include <spot/twaalgos/stutter.hh>
#include <spot/twaalgos/synthesis.hh>
#include <spot/twaalgos/translate.hh>
#include <spot/twaalgos/toweak.hh>
#include <spot/twaalgos/hoa.hh>
@ -675,6 +676,7 @@ def state_is_accepting(self, src) -> "bool":
%include <spot/twaalgos/split.hh>
%include <spot/twaalgos/sum.hh>
%include <spot/twaalgos/stutter.hh>
%include <spot/twaalgos/synthesis.hh>
%include <spot/twaalgos/translate.hh>
%include <spot/twaalgos/toweak.hh>
%include <spot/twaalgos/hoa.hh>

6
spot/misc/game.cc
View file

@ -806,13 +806,13 @@ namespace spot
}
}
void propagate_players(spot::twa_graph_ptr& arena,
void alternate_players(spot::twa_graph_ptr& arena,
bool first_player, bool complete0)
{
auto um = arena->acc().unsat_mark();
if (!um.first)
throw std::runtime_error
("propagate_players(): game winning condition is a tautology");
("alternate_players(): game winning condition is a tautology");
unsigned sink_env = 0;
unsigned sink_con = 0;
@ -843,7 +843,7 @@ namespace spot
{
delete owner;
throw
std::runtime_error("propagate_players(): odd cycle detected");
std::runtime_error("alternate_players(): odd cycle detected");
}
}
if (complete0 && !(*owner)[src] && missing != bddfalse)

2
spot/misc/game.hh
View file

@ -42,7 +42,7 @@ namespace spot
/// If \a complete0 is set, ensure that states of player 0 are
/// complete.
SPOT_API
void propagate_players(spot::twa_graph_ptr& arena,
void alternate_players(spot::twa_graph_ptr& arena,
bool first_player = false,
bool complete0 = true);

2
spot/twaalgos/Makefile.am
View file

@ -89,6 +89,7 @@ twaalgos_HEADERS = \
stripacc.hh \
stutter.hh \
sum.hh \
synthesis.hh \
tau03.hh \
tau03opt.hh \
toparity.hh \
@ -157,6 +158,7 @@ libtwaalgos_la_SOURCES = \
stats.cc \
stripacc.cc \
stutter.cc \
synthesis.cc \
sum.cc \
tau03.cc \
tau03opt.cc \

124
spot/twaalgos/split.cc
View file

@ -1,5 +1,5 @@
// -*- coding: utf-8 -*-
// Copyright (C) 2017-2018 Laboratoire de Recherche et Développement
// Copyright (C) 2017-2020 Laboratoire de Recherche et Développement
// de l'Epita.
//
// This file is part of Spot, a model checking library.
@ -23,128 +23,10 @@
#include <spot/twaalgos/totgba.hh>
#include <spot/misc/bddlt.hh>
#include <algorithm>
namespace spot
{
twa_graph_ptr
split_2step(const const_twa_graph_ptr& aut, bdd input_bdd)
{
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());
// a sort of hash-map
std::map<size_t, std::set<unsigned>> env_hash;
struct trans_t
{
unsigned dst;
bdd cond;
acc_cond::mark_t acc;
size_t hash() const
{
return bdd_hash()(cond)
^ wang32_hash(dst) ^ std::hash<acc_cond::mark_t>()(acc);
}
};
std::vector<trans_t> dests;
for (unsigned src = 0; src < aut->num_states(); ++src)
{
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;
dests.clear();
for (const auto& e : aut->out(src))
{
bdd cond = bdd_exist(e.cond & one_letter, input_bdd);
if (cond != bddfalse)
dests.emplace_back(trans_t{e.dst, cond, e.acc});
}
bool to_add = true;
size_t h = fnv<size_t>::init;
for (const auto& t: dests)
{
h ^= t.hash();
h *= fnv<size_t>::prime;
}
for (unsigned i: env_hash[h])
{
auto out = split->out(i);
if (std::equal(out.begin(), out.end(),
dests.begin(), dests.end(),
[](const twa_graph::edge_storage_t& x,
const trans_t& y)
{
return x.dst == y.dst
&& x.cond.id() == y.cond.id()
&& x.acc == y.acc;
}))
{
to_add = false;
split->new_edge(src, i, one_letter);
break;
}
}
if (to_add)
{
unsigned d = split->new_state();
split->new_edge(src, d, one_letter);
env_hash[h].insert(d);
for (const auto& t: dests)
split->new_edge(d, t.dst, t.cond, t.acc);
}
}
}
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());

22
spot/twaalgos/split.hh
View file

@ -1,5 +1,5 @@
// -*- coding: utf-8 -*-
// Copyright (C) 2017, 2018 Laboratoire de Recherche et Développement
// Copyright (C) 2017, 2018, 2020 Laboratoire de Recherche et Développement
// de l'Epita.
//
// This file is part of Spot, a model checking library.
@ -31,24 +31,4 @@ 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 split_2step
SPOT_API twa_graph_ptr
unsplit_2step(const const_twa_graph_ptr& aut);
}

480
spot/twaalgos/synthesis.cc Normal file
View file

@ -0,0 +1,480 @@
// -*- coding: utf-8 -*-
// Copyright (C) 2020 Laboratoire de Recherche et
// Développement de l'Epita (LRDE).
//
// 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/>.
#include "config.h"
#include <spot/twaalgos/synthesis.hh>
#include <spot/misc/minato.hh>
#include <spot/twaalgos/totgba.hh>
#include <spot/misc/bddlt.hh>
#include <algorithm>
// Helper function/structures for split_2step
namespace{
// Computes and stores the restriction
// of each cond to the input domain and the support
// This is useful as it avoids recomputation
// and often many conditions are mapped to the same
// restriction
struct small_cacher_t
{
//e to e_in and support
std::unordered_map<bdd, std::pair<bdd, bdd>, spot::bdd_hash> cond_hash_;
void fill(const spot::const_twa_graph_ptr& aut, bdd output_bdd)
{
cond_hash_.reserve(aut->num_edges()/5+1);
// 20% is about lowest number of different edge conditions
// for benchmarks taken from syntcomp
for (const auto& e : aut->edges())
{
// Check if stored
if (cond_hash_.find(e.cond) != cond_hash_.end())
continue;
cond_hash_[e.cond] =
std::pair<bdd, bdd>(
bdd_exist(e.cond, output_bdd),
bdd_exist(bdd_support(e.cond), output_bdd));
}
}
// Get the condition restricted to input and support of a condition
const std::pair<bdd, bdd>& operator[](const bdd& econd) const
{
return cond_hash_.at(econd);
}
};
// Struct to locally store the information of all outgoing edges
// of the state.
struct e_info_t
{
e_info_t(const spot::twa_graph::edge_storage_t& e,
const small_cacher_t& sm)
: dst(e.dst),
econd(e.cond),
einsup(sm[e.cond]),
acc(e.acc)
{
pre_hash = (spot::wang32_hash(dst)
^ std::hash<spot::acc_cond::mark_t>()(acc))
* spot::fnv<size_t>::prime;
}
inline size_t hash() const
{
return spot::wang32_hash(spot::bdd_hash()(econdout)) ^ pre_hash;
}
unsigned dst;
bdd econd;
mutable bdd econdout;
std::pair<bdd, bdd> einsup;
spot::acc_cond::mark_t acc;
size_t pre_hash;
};
// We define a order between the edges to avoid creating multiple
// states that in fact correspond to permutations of the order of the
// outgoing edges
struct less_info_t
{
// Note: orders via !econd!
inline bool operator()(const e_info_t &lhs, const e_info_t &rhs) const
{
const int l_id = lhs.econd.id();
const int r_id = rhs.econd.id();
return std::tie(lhs.dst, lhs.acc, l_id)
< std::tie(rhs.dst, rhs.acc, r_id);
}
}less_info;
struct less_info_ptr_t
{
// Note: orders via !econdout!
inline bool operator()(const e_info_t* lhs, const e_info_t* rhs)const
{
const int l_id = lhs->econdout.id();
const int r_id = rhs->econdout.id();
return std::tie(lhs->dst, lhs->acc, l_id)
< std::tie(rhs->dst, rhs->acc, r_id);
}
}less_info_ptr;
}
namespace spot
{
twa_graph_ptr
split_2step(const const_twa_graph_ptr& aut, const bdd& input_bdd,
const bdd& output_bdd, bool complete_env,
bool do_simplify)
{
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());
// The environment has all states
// with num <= aut->num_states();
// So we can first loop over the aut
// and then deduce the owner
// 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());
// 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
// and map has shown to be faster than unordered_map for
// syntcomp examples
std::map<unsigned, std::pair<unsigned, bdd>> env_edge_hash;
typedef std::map<unsigned, std::pair<unsigned, bdd>>::mapped_type eeh_t;
small_cacher_t small_cacher;
small_cacher.fill(aut, output_bdd);
// Cache vector for all outgoing edges of this states
std::vector<e_info_t> e_cache;
// Vector of destinations actually reachable for a given
// minterm in ins
// Automatically "almost" sorted due to the sorting of e_cache
std::vector<const e_info_t*> dests;
// If a completion is demanded we might have to create sinks
// Sink controlled by player
auto get_sink_con_state = [&split]()
{
static unsigned sink_con=0;
if (SPOT_UNLIKELY(sink_con == 0))
sink_con = split->new_state();
return sink_con;
};
// Loop over all states
for (unsigned src = 0; src < aut->num_states(); ++src)
{
env_edge_hash.clear();
e_cache.clear();
auto out_cont = aut->out(src);
// Short-cut if we do not want to
// split the edges of nodes that have
// a single outgoing edge
if (do_simplify
&& (++out_cont.begin()) == out_cont.end())
{
// "copy" the edge
const auto& e = *out_cont.begin();
split->new_edge(src, e.dst, e.cond, e.acc);
// Check if it needs to be completed
if (complete_env)
{
bdd missing = bddtrue - bdd_exist(e.cond, output_bdd);
if (missing != bddfalse)
split->new_edge(src, get_sink_con_state(), missing);
}
// We are done for this state
continue;
}
// Avoid looping over all minterms
// we only loop over the minterms that actually exist
bdd all_letters = bddfalse;
bdd support = bddtrue;
for (const auto& e : out_cont)
{
e_cache.emplace_back(e, small_cacher);
all_letters |= e_cache.back().einsup.first;
support &= e_cache.back().einsup.second;
}
// Complete for env
if (complete_env && (all_letters != bddtrue))
split->new_edge(src, get_sink_con_state(), bddtrue - all_letters);
// Sort to avoid that permutations of the same edges
// get different intermediate states
std::sort(e_cache.begin(), e_cache.end(), less_info);
while (all_letters != bddfalse)
{
bdd one_letter = bdd_satoneset(all_letters, support, bddtrue);
all_letters -= one_letter;
dests.clear();
for (const auto& e_info : e_cache)
// implies is faster than and
if (bdd_implies(one_letter, e_info.einsup.first))
{
e_info.econdout =
bdd_appex(e_info.econd, one_letter,
bddop_and, input_bdd);
dests.push_back(&e_info);
assert(e_info.econdout != bddfalse);
}
// By construction this should not be empty
assert(!dests.empty());
// # dests is almost sorted -> insertion sort
if (dests.size()>1)
for (auto it = dests.begin(); it != dests.end(); ++it)
std::rotate(std::upper_bound(dests.begin(), it, *it,
less_info_ptr),
it, it + 1);
bool to_add = true;
size_t h = fnv<size_t>::init;
for (const auto& t: dests)
h ^= t->hash();
auto range_h = env_hash.equal_range(h);
for (auto it_h = range_h.first; it_h != range_h.second; ++it_h)
{
unsigned i = it_h->second;
auto out = split->out(i);
if (std::equal(out.begin(), out.end(),
dests.begin(), dests.end(),
[](const twa_graph::edge_storage_t& x,
const e_info_t* y)
{
return x.dst == y->dst
&& x.acc == y->acc
&& x.cond.id() == y->econdout.id();
}))
{
to_add = false;
auto it = env_edge_hash.find(i);
if (it != env_edge_hash.end())
it->second.second |= one_letter;
else
env_edge_hash.emplace(i,
eeh_t(split->new_edge(src, i, bddtrue), one_letter));
break;
}
}
if (to_add)
{
unsigned d = split->new_state();
unsigned n_e = split->new_edge(src, d, bddtrue);
env_hash.emplace(h, d);
env_edge_hash.emplace(d, eeh_t(n_e, one_letter));
for (const auto &t: dests)
split->new_edge(d, t->dst, t->econdout, t->acc);
}
} // letters
// save locally stored condition
for (const auto& elem : env_edge_hash)
split->edge_data(elem.second.first).cond = elem.second.second;
} // v-src
split->merge_edges();
split->prop_universal(spot::trival::maybe());
// The named property
// compute the owners
// env is equal to 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);
split->set_named_prop("state-player", owner);
// Done
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());
// split_2step is not guaranteed to produce
// states that alternate between env and player do to do_simplify
auto owner_ptr = aut->get_named_prop<std::vector<bool>>("state-player");
if (!owner_ptr)
throw std::runtime_error("unsplit requires the named prop "
"state-player as set by split_2step");
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))
{
// if the dst is also owned env
if (!(*owner_ptr)[i.dst])
{
// This can only happen if there is only
// one outgoing edges for cur
assert(([&aut, cur]()->bool
{
auto out_cont = aut->out(cur);
return (++(out_cont.begin()) == out_cont.end());
})());
out->new_edge(cur, i.dst, i.cond, i.acc);
if (!seen[i.dst])
todo.push_back(i.dst);
continue; // Done with 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);
}
}
}
out->merge_edges();
out->merge_states();
return out;
}
spot::twa_graph_ptr
apply_strategy(const spot::twa_graph_ptr& arena,
bdd all_outputs,
bool unsplit, bool keep_acc)
{
std::vector<bool>* w_ptr =
arena->get_named_prop<std::vector<bool>>("state-winner");
std::vector<unsigned>* s_ptr =
arena->get_named_prop<std::vector<unsigned>>("strategy");
std::vector<bool>* sp_ptr =
arena->get_named_prop<std::vector<bool>>("state-player");
if (!w_ptr || !s_ptr || !sp_ptr)
throw std::runtime_error("Arena missing state-winner, strategy "
"or state-player");
if (!(w_ptr->at(arena->get_init_state_number())))
throw std::runtime_error("Player does not win initial state, strategy "
"is not applicable");
std::vector<bool>& w = *w_ptr;
std::vector<unsigned>& s = *s_ptr;
auto aut = spot::make_twa_graph(arena->get_dict());
aut->copy_ap_of(arena);
if (keep_acc)
aut->copy_acceptance_of(arena);
constexpr unsigned unseen_mark = std::numeric_limits<unsigned>::max();
std::vector<unsigned> todo{arena->get_init_state_number()};
std::vector<unsigned> pg2aut(arena->num_states(), unseen_mark);
aut->set_init_state(aut->new_state());
pg2aut[arena->get_init_state_number()] = aut->get_init_state_number();
while (!todo.empty())
{
unsigned v = todo.back();
todo.pop_back();
// Check if a simplification occurred
// in the aut and we have env -> env
// Env edge -> keep all
for (auto &e1: arena->out(v))
{
assert(w.at(e1.dst));
// Check if a simplification occurred
// in the aut and we have env -> env
if (!(*sp_ptr)[e1.dst])
{
assert(([&arena, v]()
{
auto out_cont = arena->out(v);
return (++(out_cont.begin()) == out_cont.end());
})());
// If so we do not need to unsplit
if (pg2aut[e1.dst] == unseen_mark)
{
pg2aut[e1.dst] = aut->new_state();
todo.push_back(e1.dst);
}
// Create the edge
aut->new_edge(pg2aut[v],
pg2aut[e1.dst],
e1.cond,
keep_acc ? e1.acc : spot::acc_cond::mark_t({}));
// Done
continue;
}
if (!unsplit)
{
if (pg2aut[e1.dst] == unseen_mark)
pg2aut[e1.dst] = aut->new_state();
aut->new_edge(pg2aut[v], pg2aut[e1.dst], e1.cond,
keep_acc ? e1.acc : spot::acc_cond::mark_t({}));
}
// Player strat
auto &e2 = arena->edge_storage(s[e1.dst]);
if (pg2aut[e2.dst] == unseen_mark)
{
pg2aut[e2.dst] = aut->new_state();
todo.push_back(e2.dst);
}
aut->new_edge(unsplit ? pg2aut[v] : pg2aut[e1.dst],
pg2aut[e2.dst],
unsplit ? (e1.cond & e2.cond) : e2.cond,
keep_acc ? e2.acc : spot::acc_cond::mark_t({}));
}
}
aut->set_named_prop("synthesis-outputs", new bdd(all_outputs));
// If no unsplitting is demanded, it remains a two-player arena
// We do not need to track winner as this is a
// strategy automaton
if (!unsplit)
{
const std::vector<bool>& sp_pg = * sp_ptr;
std::vector<bool> sp_aut(aut->num_states());
std::vector<unsigned> str_aut(aut->num_states());
for (unsigned i = 0; i < arena->num_states(); ++i)
{
if (pg2aut[i] == unseen_mark)
// Does not appear in strategy
continue;
sp_aut[pg2aut[i]] = sp_pg[i];
str_aut[pg2aut[i]] = s[i];
}
aut->set_named_prop(
"state-player", new std::vector<bool>(std::move(sp_aut)));
aut->set_named_prop(
"state-winner", new std::vector<bool>(aut->num_states(), true));
aut->set_named_prop(
"strategy", new std::vector<unsigned>(std::move(str_aut)));
}
return aut;
}
} // spot

77
spot/twaalgos/synthesis.hh Normal file
View file

@ -0,0 +1,77 @@
// -*- coding: utf-8 -*-
// Copyright (C) 2020 Laboratoire de Recherche et
// Développement de l'Epita (LRDE).
//
// 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/>.
#pragma once
#include <spot/twa/twagraph.hh>
#include <bddx.h>
namespace spot
{
/// \brief make each transition (conditionally, see do__simpify)
/// 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^(O)
///
/// 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.
/// \param aut automaton to be transformed
/// \param input_bdd conjunction of all input AP
/// \param output_bdd conjunction of all output AP
/// \param complete_env Whether the automaton should be complete for the
/// environment, i.e. the player of I
/// \param do_simplify If a state has a single outgoing transition
/// we do not necessarily have to split it
/// to solve the game
/// \note: This function also computes the state players
/// \note: If the automaton is to be completed for both env and player
/// then egdes between the sinks will be added
/// (assuming that the environnement/player of I) plays first
SPOT_API twa_graph_ptr
split_2step(const const_twa_graph_ptr& aut, const bdd& input_bdd,
const bdd& output_bdd, bool complete_env, bool do_simplify);
/// \brief the reverse of split_2step
///
/// \note: This function relies on the named property "state-player"
SPOT_API twa_graph_ptr
unsplit_2step(const const_twa_graph_ptr& aut);
/// \brief Takes a solved game and restricts the automat to the
/// winning strategy of the player
///
/// \param arena twa_graph with named properties "state-player",
/// "strategy" and "state-winner"
/// \param all_outputs bdd of all output signals
/// \param unsplit Whether or not to unsplit the automaton
/// \param keep_acc Whether or not keep the acceptance condition
/// \return the resulting twa_graph
SPOT_API spot::twa_graph_ptr
apply_strategy(const spot::twa_graph_ptr& arena,
bdd all_outputs, bool unsplit, bool keep_acc);
}

26
tests/core/ltlsynt.test
View file

@ -62,12 +62,13 @@ parity 16;
14 1 1 10,16;
16 1 0 14,15;
1 1 1 3,6;
parity 4;
3 2 0 1,4 "INIT";
4 3 1 0,3;
0 1 0 1,2;
2 1 1 0,0;
1 2 1 3,3;
parity 5;
1 1 0 4,5 "INIT";
5 5 1 0,1;
0 1 0 2,3;
3 3 1 0,0;
2 5 1 1;
4 4 1 1,1;
EOF
: > out
@ -214,7 +215,6 @@ DPA has 12 states, 4 colors
simplification done
DPA has 11 states
determinization and simplification took X seconds
parity game built in X seconds
parity game solved in X seconds
EOF
ltlsynt --ins='a' --outs='b' -f 'GFa <-> GFb' --verbose --realizability 2> out
@ -228,7 +228,6 @@ simplification done in X seconds
DPA has 3 states
split inputs and outputs done in X seconds
automaton has 8 states
parity game built in X seconds
parity game solved in X seconds
EOF
ltlsynt --ins=a --outs=b -f 'GFa <-> GFb' --verbose --algo=ps 2> out
@ -238,11 +237,10 @@ diff outx exp
cat >exp <<EOF
translating formula done in X seconds
automaton has 16 states and 2 colors
LAR construction done in X seconds
DPA has 16 states, 4 colors
split inputs and outputs done in X seconds
automaton has 47 states
LAR construction done in X seconds
DPA has 47 states, 4 colors
parity game built in X seconds
parity game solved in X seconds
EOF
ltlsynt --ins='a,b,c,d' --outs='e' -f '(Fa & Fb & Fc & Fd) <-> GFe' \
@ -390,7 +388,7 @@ State: 2
[!0] 2
--END--
EOF
ltlsynt -x tls-impl=0 -f '!XXF(p0 & (p0 M Gp0))' > out
ltlsynt --outs=p0 -x tls-impl=0 -f '!XXF(p0 & (p0 M Gp0))' > out
diff out exp
cat >exp <<EOF
@ -407,10 +405,10 @@ State: 0
[!0] 0
--END--
EOF
ltlsynt -x tls-impl=1 -f '!XXF(p0 & (p0 M Gp0))' > out
ltlsynt --outs=p0 -x tls-impl=1 -f '!XXF(p0 & (p0 M Gp0))' > out
diff out exp
ltlsynt -f '!XXF(p0 & (p0 M Gp0))' > out
ltlsynt --outs=p0 -f '!XXF(p0 & (p0 M Gp0))' > out
diff out exp
f='Fp0 U XX((p0 & F!p1) | (!p0 & Gp1))'

32
tests/python/split.py
View file

@ -1,5 +1,5 @@
# -*- mode: python; coding: utf-8 -*-
# Copyright (C) 2018 Laboratoire de Recherche et
# Copyright (C) 2018-2020 Laboratoire de Recherche et
# Développement de l'Epita
#
# This file is part of Spot, a model checking library.
@ -28,21 +28,31 @@ def equiv(a, b):
return incl(a, b) and incl(b, a)
def do_split(f, in_list):
def do_split(f, in_list, out_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)
outputs = spot.buddy.bddtrue
for a in out_list:
outputs &= spot.buddy.bdd_ithvar(aut.get_dict().varnum(spot.formula(a)))
s = spot.split_2step(aut, inputs, 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'])
aut, s = do_split('(FG !a) <-> (GF b)', ['a'], ['b'])
assert equiv(aut, spot.unsplit_2step(s))
aut, s = do_split('GFa && GFb', ['a'])
aut, s = do_split('GFa && GFb', ['a'], ['b'])
assert equiv(aut, spot.unsplit_2step(s))
assert s.to_str() == """HOA: v1
assert str_diff("""HOA: v1
States: 3
Start: 0
AP: 2 "a" "b"
@ -50,6 +60,7 @@ 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
@ -60,10 +71,10 @@ State: 1
State: 2
[!1] 0
[1] 0 {1}
--END--"""
--END--""", s.to_str() )
aut, s = do_split('! ((G (req -> (F ack))) && (G (go -> (F grant))))', ['go',
'req'])
aut, s = do_split('! ((G (req -> (F ack))) && (G (go -> (F grant))))',
['go', 'req'], ['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
@ -103,5 +114,6 @@ assert equiv(aut, spot.unsplit_2step(s))
# --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'])
&& g_1))))) && (G (r_0 -> F g_0))) && (G (r_1 -> F g_1))',
['r_0', 'r_1'], ['g_0', 'g_1'])
assert equiv(aut, spot.unsplit_2step(s))