From 29055c8109705a2d54dc35a93b56f0ef8468555e Mon Sep 17 00:00:00 2001 From: philipp Date: Thu, 24 Sep 2020 16:25:53 +0200 Subject: [PATCH] Improving split and reorganizing * 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. --- bin/ltlsynt.cc | 176 +++----------- python/spot/impl.i | 2 + spot/misc/game.cc | 6 +- spot/misc/game.hh | 2 +- spot/twaalgos/Makefile.am | 2 + spot/twaalgos/split.cc | 124 +--------- spot/twaalgos/split.hh | 22 +- spot/twaalgos/synthesis.cc | 480 +++++++++++++++++++++++++++++++++++++ spot/twaalgos/synthesis.hh | 77 ++++++ tests/core/ltlsynt.test | 26 +- tests/python/split.py | 32 ++- 11 files changed, 641 insertions(+), 308 deletions(-) create mode 100644 spot/twaalgos/synthesis.cc create mode 100644 spot/twaalgos/synthesis.hh diff --git a/bin/ltlsynt.cc b/bin/ltlsynt.cc index f9a02e951..1ab755e7f 100644 --- a/bin/ltlsynt.cc +++ b/bin/ltlsynt.cc @@ -47,7 +47,7 @@ #include #include #include -#include +#include #include #include @@ -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("state-winner"); - spot::strategy_t* s_ptr = - arena->get_named_prop("strategy"); - std::vector* sp_ptr = - arena->get_named_prop>("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::max(); - std::vector todo{arena->get_init_state_number()}; - std::vector 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& sp_pg = * sp_ptr; - std::vector 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(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; } diff --git a/python/spot/impl.i b/python/spot/impl.i index 3604014ab..a959310b2 100644 --- a/python/spot/impl.i +++ b/python/spot/impl.i @@ -153,6 +153,7 @@ #include #include #include +#include #include #include #include @@ -675,6 +676,7 @@ def state_is_accepting(self, src) -> "bool": %include %include %include +%include %include %include %include diff --git a/spot/misc/game.cc b/spot/misc/game.cc index eaa602b53..f2b6179d7 100644 --- a/spot/misc/game.cc +++ b/spot/misc/game.cc @@ -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) diff --git a/spot/misc/game.hh b/spot/misc/game.hh index 8d5760e86..96d563c05 100644 --- a/spot/misc/game.hh +++ b/spot/misc/game.hh @@ -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); diff --git a/spot/twaalgos/Makefile.am b/spot/twaalgos/Makefile.am index adbecbd82..fd9d96218 100644 --- a/spot/twaalgos/Makefile.am +++ b/spot/twaalgos/Makefile.am @@ -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 \ diff --git a/spot/twaalgos/split.cc b/spot/twaalgos/split.cc index 13f51c97f..f082e826f 100644 --- a/spot/twaalgos/split.cc +++ b/spot/twaalgos/split.cc @@ -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 #include +#include + 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> 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); - } - }; - - std::vector 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::init; - for (const auto& t: dests) - { - h ^= t.hash(); - h *= fnv::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 seen(aut->num_states(), false); - std::deque 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()); diff --git a/spot/twaalgos/split.hh b/spot/twaalgos/split.hh index a3d070d37..7bfe7b02c 100644 --- a/spot/twaalgos/split.hh +++ b/spot/twaalgos/split.hh @@ -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); } diff --git a/spot/twaalgos/synthesis.cc b/spot/twaalgos/synthesis.cc new file mode 100644 index 000000000..86cb97ab7 --- /dev/null +++ b/spot/twaalgos/synthesis.cc @@ -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 . +#include "config.h" + +#include +#include +#include +#include + +#include + +// 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, 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_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& 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()(acc)) + * spot::fnv::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 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 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> env_edge_hash; + typedef std::map>::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_cache; + + // Vector of destinations actually reachable for a given + // minterm in ins + // Automatically "almost" sorted due to the sorting of e_cache + std::vector 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::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* owner = + new std::vector(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>("state-player"); + if (!owner_ptr) + throw std::runtime_error("unsplit requires the named prop " + "state-player as set by split_2step"); + + std::vector seen(aut->num_states(), false); + std::deque 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* w_ptr = + arena->get_named_prop>("state-winner"); + std::vector* s_ptr = + arena->get_named_prop>("strategy"); + std::vector* sp_ptr = + arena->get_named_prop>("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& w = *w_ptr; + std::vector& 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::max(); + std::vector todo{arena->get_init_state_number()}; + std::vector 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& sp_pg = * sp_ptr; + std::vector sp_aut(aut->num_states()); + std::vector 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(std::move(sp_aut))); + aut->set_named_prop( + "state-winner", new std::vector(aut->num_states(), true)); + aut->set_named_prop( + "strategy", new std::vector(std::move(str_aut))); + } + return aut; + + } + +} // spot \ No newline at end of file diff --git a/spot/twaalgos/synthesis.hh b/spot/twaalgos/synthesis.hh new file mode 100644 index 000000000..7b77e1592 --- /dev/null +++ b/spot/twaalgos/synthesis.hh @@ -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 . + +#pragma once + +#include +#include + +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); +} \ No newline at end of file diff --git a/tests/core/ltlsynt.test b/tests/core/ltlsynt.test index 22627be88..60937204d 100644 --- a/tests/core/ltlsynt.test +++ b/tests/core/ltlsynt.test @@ -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 < 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 < 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))' diff --git a/tests/python/split.py b/tests/python/split.py index 51a7b40d9..2f7d8c756 100644 --- a/tests/python/split.py +++ b/tests/python/split.py @@ -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))