diff --git a/NEWS b/NEWS index f89546641..05af3081f 100644 --- a/NEWS +++ b/NEWS @@ -44,8 +44,8 @@ New in spot 2.4.2.dev (not yet released) also be used to detect unreliable measurements. See https://spot.lrde.epita.fr/oaut.html#timing - - ltlsynt is a new tool for synthesizing AIGER circuits from LTL/PSL - formulas. + - ltlsynt is a new tool for synthesizing a controller from LTL/PSL + specifications. - ltldo learned to limit the number of automata it outputs using -n. @@ -190,6 +190,15 @@ New in spot 2.4.2.dev (not yet released) - The new spot::formula::is_leaf() method can be used to detect formulas without children (atomic propositions, or constants). + - The new function spot::print_aiger() encodes an automaton as an + AIGER circuit and prints it. This is only possible for automata + whose acceptance condition is trivial. It relies on a new named + property "synthesis outputs" that describes which atomic + propositions are to be encoded as outputs of the circuits. + This function is used by ltlsynt to output the synthesized + controllers in the format required by the synthesis tools + competition SYNTCOMP. + Deprecation notices: (These functions still work but compilers emit warnings.) diff --git a/bin/ltlsynt.cc b/bin/ltlsynt.cc index a59bb20bc..7d10a74c7 100644 --- a/bin/ltlsynt.cc +++ b/bin/ltlsynt.cc @@ -19,8 +19,6 @@ #include -#include -#include #include #include #include @@ -39,6 +37,7 @@ #include #include #include +#include #include #include #include @@ -53,6 +52,7 @@ enum OPT_INPUT, OPT_OUTPUT, OPT_PRINT, + OPT_PRINT_AIGER, OPT_REAL }; @@ -60,10 +60,10 @@ static const argp_option options[] = { /**************************************************/ { nullptr, 0, nullptr, 0, "Input options:", 1 }, - { "input", OPT_INPUT, "PROPS", 0, + { "ins", OPT_INPUT, "PROPS", 0, "comma-separated list of uncontrollable (a.k.a. input) atomic" " propositions", 0}, - { "output", OPT_OUTPUT, "PROPS", 0, + { "outs", OPT_OUTPUT, "PROPS", 0, "comma-separated list of controllable (a.k.a. output) atomic" " propositions", 0}, /**************************************************/ @@ -77,30 +77,38 @@ static const argp_option options[] = { "print-pg", OPT_PRINT, nullptr, 0, "print the parity game in the pgsolver format, do not solve it", 0}, { "realizability", OPT_REAL, nullptr, 0, - "realizability only, do not synthesize the circuit", 0}, + "realizability only, do not compute a winning strategy", 0}, + { "aiger", OPT_PRINT_AIGER, nullptr, 0, + "prints the winning strategy as an AIGER circuit", 0}, /**************************************************/ { nullptr, 0, nullptr, 0, "Miscellaneous options:", -1 }, { nullptr, 0, nullptr, 0, nullptr, 0 }, }; -const struct argp_child children[] = +static const struct argp_child children[] = { { &finput_argp_headless, 0, nullptr, 0 }, + { &aoutput_argp, 0, nullptr, 0 }, + //{ &aoutput_o_format_argp, 0, nullptr, 0 }, { &misc_argp, 0, nullptr, 0 }, { nullptr, 0, nullptr, 0 } }; -const char argp_program_doc[] = -"Synthesize an AIGER circuit from its LTL specifications."; +const char argp_program_doc[] = "\ +Synthesize a controller from its LTL specification.\v\ +Exit status:\n\ + 0 if the input problem is realizable\n\ + 1 if the input problem is not realizable\n\ + 2 if any error has been reported"; -std::vector input_aps; -std::vector output_aps; -std::unordered_map bddvar_to_inputnum; -std::unordered_map bddvar_to_outputnum; +static std::vector input_aps; +static std::vector output_aps; bool opt_print_pg(false); bool opt_real(false); +bool opt_print_aiger(false); +// FIXME rename options to choose the algorithm enum solver { QP, @@ -120,7 +128,7 @@ static solver const solver_types[] = }; ARGMATCH_VERIFY(solver_args, solver_types); -solver opt_solver = REC; +static solver opt_solver = REC; namespace { @@ -144,7 +152,7 @@ namespace // strategy iff aut has an accepting run for any valuation of atomic // propositions in I. - spot::twa_graph_ptr + static spot::twa_graph_ptr split_automaton(const spot::twa_graph_ptr& aut, bdd input_bdd) { @@ -177,8 +185,9 @@ namespace // convention that false is player 0 (the environment) and true is player 1 // (the controller). Starting with player 0 on the initial state, the owner // is switched after each transition. - std::vector make_alternating_owner(const spot::twa_graph_ptr& dpa, - bool init_owner = false) + static std::vector + make_alternating_owner(const spot::twa_graph_ptr& dpa, + bool init_owner = false) { std::vector seen(dpa->num_states(), false); std::vector todo({dpa->get_init_state_number()}); @@ -201,7 +210,8 @@ namespace return owner; } - spot::twa_graph_ptr to_dpa(const spot::twa_graph_ptr& split) + static spot::twa_graph_ptr + to_dpa(const spot::twa_graph_ptr& split) { auto dpa = spot::tgba_determinize(split); dpa->merge_edges(); @@ -218,225 +228,10 @@ namespace return dpa; } - // Parity game strategy to AIGER - - class aig - { - private: - unsigned num_inputs_; - unsigned max_var_; - std::map> and_gates_; - std::vector latches_; - std::vector outputs_; - // Cache the function computed by each variable as a bdd. - std::unordered_map var2bdd_; - std::unordered_map bdd2var_; - - public: - aig(unsigned num_inputs, unsigned num_latches, unsigned num_outputs) - : num_inputs_(num_inputs), - max_var_((num_inputs + num_latches) * 2), - latches_(std::vector(num_latches)), - outputs_(std::vector(num_outputs)) - { - bdd2var_[bddtrue] = 1; - var2bdd_[1] = bddtrue; - bdd2var_[bddfalse] = 0; - var2bdd_[0] = bddfalse; - } - - unsigned input_var(unsigned i, bdd b) - { - assert(i < num_inputs_); - unsigned v = (1 + i) * 2; - bdd2var_[b] = v; - var2bdd_[v] = b; - return v; - } - - unsigned latch_var(unsigned i, bdd b) - { - assert(i < latches_.size()); - unsigned v = (1 + num_inputs_ + i) * 2; - bdd2var_[b] = v; - var2bdd_[v] = b; - return v; - } - - void set_output(unsigned i, unsigned v) - { - outputs_[i] = v; - } - - void set_latch(unsigned i, unsigned v) - { - latches_[i] = v; - } - - unsigned aig_true() const - { - return 1; - } - - unsigned aig_false() const - { - return 0; - } - - unsigned aig_not(unsigned v) - { - unsigned not_v = v + 1 - 2 * (v % 2); - assert(var2bdd_.count(v)); - var2bdd_[not_v] = !(var2bdd_[v]); - bdd2var_[var2bdd_[not_v]] = not_v; - return not_v; - } - - unsigned aig_and(unsigned v1, unsigned v2) - { - assert(var2bdd_.count(v1)); - assert(var2bdd_.count(v2)); - bdd b = var2bdd_[v1] & var2bdd_[v2]; - auto it = bdd2var_.find(b); - if (it != bdd2var_.end()) - return it->second; - max_var_ += 2; - and_gates_[max_var_] = {v1, v2}; - bdd v1v2 = var2bdd_[v1] & var2bdd_[v2]; - bdd2var_[v1v2] = max_var_; - var2bdd_[max_var_] = v1v2; - return max_var_; - } - - unsigned aig_and(std::vector vs) - { - if (vs.empty()) - return aig_true(); - if (vs.size() == 1) - return vs[0]; - if (vs.size() == 2) - return aig_and(vs[0], vs[1]); - unsigned m = vs.size() / 2; - std::vector left(vs.begin(), vs.begin() + m); - std::vector right(vs.begin() + m, vs.end()); - return aig_and(aig_and(left), aig_and(right)); - } - - unsigned aig_or(unsigned v1, unsigned v2) - { - return aig_not(aig_and(aig_not(v1), aig_not(v2))); - } - - unsigned aig_or(std::vector vs) - { - for (unsigned i = 0; i < vs.size(); ++i) - vs[i] = aig_not(vs[i]); - return aig_not(aig_and(vs)); - } - - unsigned aig_pos(unsigned v) - { - return v - v % 2; - } - - void remove_unused() - { - std::unordered_set todo; - for (unsigned v : outputs_) - todo.insert(aig_pos(v)); - std::unordered_set used; - while (!todo.empty()) - { - used.insert(todo.begin(), todo.end()); - std::unordered_set todo_next; - for (unsigned v : todo) - { - auto it_and = and_gates_.find(v); - if (it_and != and_gates_.end()) - { - if (!used.count(aig_pos(it_and->second.first))) - todo_next.insert(aig_pos(it_and->second.first)); - if (!used.count(aig_pos(it_and->second.second))) - todo_next.insert(aig_pos(it_and->second.second)); - } - else if (v <= (num_inputs_ + latches_.size()) * 2 - && v > num_inputs_ * 2) - { - unsigned l = v / 2 - num_inputs_ - 1; - if (!used.count(aig_pos(latches_[l]))) - todo_next.insert(aig_pos(latches_[l])); - } - } - todo = todo_next; - } - std::unordered_set unused; - for (auto& p : and_gates_) - if (!used.count(p.first)) - unused.insert(p.first); - for (unsigned v : unused) - and_gates_.erase(v); - } - - void print() - { - std::cout << "aag " << max_var_ / 2 - << ' ' << num_inputs_ - << ' ' << latches_.size() - << ' ' << outputs_.size() - << ' ' << and_gates_.size() << '\n'; - for (unsigned i = 0; i < num_inputs_; ++i) - std::cout << (1 + i) * 2 << '\n'; - for (unsigned i = 0; i < latches_.size(); ++i) - std::cout << (1 + num_inputs_ + i) * 2 - << ' ' << latches_[i] << '\n'; - for (unsigned i = 0; i < outputs_.size(); ++i) - std::cout << outputs_[i] << '\n'; - for (auto& p : and_gates_) - std::cout << p.first - << ' ' << p.second.first - << ' ' << p.second.second << '\n'; - for (unsigned i = 0; i < num_inputs_; ++i) - std::cout << 'i' << i << ' ' << input_aps[i] << '\n'; - for (unsigned i = 0; i < outputs_.size(); ++i) - std::cout << 'o' << i << ' ' << output_aps[i] << '\n'; - } - }; - - std::vector output_to_vec(bdd b) - { - std::vector v(bddvar_to_outputnum.size()); - while (b != bddtrue && b != bddfalse) - { - unsigned i = bddvar_to_outputnum[bdd_var(b)]; - v[i] = (bdd_low(b) == bddfalse); - if (v[i]) - b = bdd_high(b); - else - b = bdd_low(b); - } - return v; - } - - bdd state_to_bdd(unsigned s, bdd all) - { - bdd b = bddtrue; - unsigned size = bdd_nodecount(all); - if (size) - { - unsigned st0 = bdd_var(all); - for (unsigned i = 0; i < size; ++i) - { - b &= s % 2 ? bdd_ithvar(st0 + i) : bdd_nithvar(st0 + i); - s >>= 1; - } - } - return b; - } - // Construct a smaller automaton, filtering out states that are not // accessible. Also merge back pairs of p --(i)--> q --(o)--> r // transitions to p --(i&o)--> r. - spot::twa_graph_ptr + static spot::twa_graph_ptr strat_to_aut(const spot::parity_game& pg, const spot::parity_game::strategy_t& strat, const spot::twa_graph_ptr& dpa, @@ -477,110 +272,10 @@ namespace } } aut->purge_dead_states(); + aut->set_named_prop("synthesis-outputs", new bdd(all_outputs)); return aut; } - std::vector state_to_vec(unsigned s, unsigned size) - { - std::vector v(size); - for (unsigned i = 0; i < size; ++i) - { - v[i] = s % 2; - s >>= 1; - } - return v; - } - - // Switch initial state and 0 in the AIGER encoding, so that the - // 0-initialized latches correspond to the initial state. - unsigned encode_init_0(unsigned src, unsigned init) - { - return src == init ? 0 : src == 0 ? init : src; - } - - aig aut_to_aiger(const spot::twa_graph_ptr& aut, - bdd all_inputs, bdd all_outputs) - { - // Encode state in log2(num_states) latches. - unsigned log2n = std::ceil(std::log2(aut->num_states())); - unsigned st0 = aut->get_dict()->register_anonymous_variables(log2n, aut); - bdd all_states = bddtrue; - for (unsigned i = 0; i < log2n; ++i) - all_states &= bdd_ithvar(st0 + i); - - unsigned num_inputs = bdd_nodecount(all_inputs); - unsigned num_outputs = bdd_nodecount(all_outputs); - unsigned num_latches = bdd_nodecount(all_states); - unsigned init = aut->get_init_state_number(); - - aig circuit(num_inputs, num_latches, num_outputs); - bdd b; - - // Latches and outputs are expressed as a DNF in which each term represents - // a transition. - // latch[i] (resp. out[i]) represents the i-th latch's (resp. output's) - // DNF. - std::vector> latch(num_latches); - std::vector> out(num_outputs); - for (unsigned s = 0; s < aut->num_states(); ++s) - for (auto& e: aut->out(s)) - { - spot::minato_isop cond(e.cond); - while ((b = cond.next()) != bddfalse) - { - bdd input = bdd_existcomp(b, all_inputs); - bdd letter_out = bdd_existcomp(b, all_outputs); - auto out_vec = output_to_vec(letter_out); - unsigned dst = encode_init_0(e.dst, init); - auto next_state_vec = state_to_vec(dst, log2n); - unsigned src = encode_init_0(s, init); - bdd state_bdd = state_to_bdd(src, all_states); - std::vector prod; - while (input != bddfalse && input != bddtrue) - { - unsigned v = - circuit.input_var(bddvar_to_inputnum[bdd_var(input)], - bdd_ithvar(bdd_var(input))); - if (bdd_high(input) == bddfalse) - { - v = circuit.aig_not(v); - input = bdd_low(input); - } - else - input = bdd_high(input); - prod.push_back(v); - } - - while (state_bdd != bddfalse && state_bdd != bddtrue) - { - unsigned v = - circuit.latch_var(bdd_var(state_bdd) - st0, - bdd_ithvar(bdd_var(state_bdd))); - if (bdd_high(state_bdd) == bddfalse) - { - v = circuit.aig_not(v); - state_bdd = bdd_low(state_bdd); - } - else - state_bdd = bdd_high(state_bdd); - prod.push_back(v); - } - unsigned t = circuit.aig_and(prod); - for (unsigned i = 0; i < next_state_vec.size(); ++i) - if (next_state_vec[i]) - latch[i].push_back(t); - for (unsigned i = 0; i < num_outputs; ++i) - if (out_vec[i]) - out[i].push_back(t); - } - } - for (unsigned i = 0; i < num_latches; ++i) - circuit.set_latch(i, circuit.aig_or(latch[i])); - for (unsigned i = 0; i < num_outputs; ++i) - circuit.set_output(i, circuit.aig_or(out[i])); - circuit.remove_unused(); - return circuit; - } class ltl_processor final : public job_processor { @@ -601,6 +296,9 @@ namespace int process_formula(spot::formula f, const char*, int) override { + spot::process_timer timer; + timer.start(); + auto aut = trans_.run(&f); bdd all_inputs = bddtrue; bdd all_outputs = bddtrue; @@ -611,7 +309,6 @@ namespace lowercase << (char)std::tolower(c); unsigned v = aut->register_ap(spot::formula::ap(lowercase.str())); all_inputs &= bdd_ithvar(v); - bddvar_to_inputnum[v] = i; } for (unsigned i = 0; i < output_aps_.size(); ++i) { @@ -620,12 +317,13 @@ namespace lowercase << (char)std::tolower(c); unsigned v = aut->register_ap(spot::formula::ap(lowercase.str())); all_outputs &= bdd_ithvar(v); - bddvar_to_outputnum[v] = i; } auto split = split_automaton(aut, all_inputs); auto dpa = to_dpa(split); auto owner = make_alternating_owner(dpa); auto pg = spot::parity_game(dpa, owner); + timer.stop(); + if (opt_print_pg) { pg.print(std::cout); @@ -645,30 +343,44 @@ namespace { auto strat_aut = strat_to_aut(pg, strategy, dpa, all_outputs); - auto circuit = - aut_to_aiger(strat_aut, all_inputs, all_outputs); - circuit.print(); + + // output the winning strategy + if (opt_print_aiger) + spot::print_aiger(std::cout, strat_aut); + else + { + automaton_printer printer; + printer.print(strat_aut, timer); + } } + return 0; } else - std::cout << "UNREALIZABLE\n"; - return 0; + { + std::cout << "UNREALIZABLE\n"; + return 1; + } } case QP: if (!opt_real) { std::cout << "The quasi-polynomial time algorithm does not" " implement synthesis yet, use --realizability\n"; - return 1; + return 2; } else if (pg.solve_qp()) - std::cout << "REALIZABLE\n"; + { + std::cout << "REALIZABLE\n"; + return 0; + } else - std::cout << "UNREALIZABLE\n"; - return 0; + { + std::cout << "UNREALIZABLE\n"; + return 1; + } default: SPOT_UNREACHABLE(); - return 0; + return 2; } } }; @@ -710,11 +422,15 @@ parse_opt(int key, char* arg, struct argp_state*) case OPT_REAL: opt_real = true; break; + case OPT_PRINT_AIGER: + opt_print_aiger = true; + break; } return 0; } -int main(int argc, char **argv) +int +main(int argc, char **argv) { setup(argv); const argp ap = { options, parse_opt, nullptr, @@ -725,5 +441,5 @@ int main(int argc, char **argv) spot::translator trans; ltl_processor processor(trans, input_aps, output_aps); - processor.run(); + return processor.run(); } diff --git a/doc/org/concepts.org b/doc/org/concepts.org index 9f79718a8..45042a106 100644 --- a/doc/org/concepts.org +++ b/doc/org/concepts.org @@ -1130,7 +1130,7 @@ Here is a list of named properties currently used inside Spot: | ~incomplete-states~ | ~std::set~ | set of states numbers that should be displayed as incomplete (used internally by ~print_dot()~ when truncating large automata) | | ~degen-levels~ | ~std::vector~ | level associated to each state by the degeneralization algorithm | | ~simulated-states~ | ~std::vector~ | map states of the original automaton to states if the current automaton in the result of simulation-based reductions | - +| ~synthesis-outputs~ | ~bdd~ | conjunction of controllable atomic propositions (used by ~print_aiger()~ to determine which propositions should be encoded as outputs of the circuit) Objects referenced via named properties are automatically destroyed when the automaton is destroyed, but this can be altered by passing a custom destructor as a third parameter to =twa::set_named_prop()=. diff --git a/spot/twaalgos/Makefile.am b/spot/twaalgos/Makefile.am index e64bb9d11..78ae1720d 100644 --- a/spot/twaalgos/Makefile.am +++ b/spot/twaalgos/Makefile.am @@ -28,6 +28,7 @@ AM_CXXFLAGS = $(WARNING_CXXFLAGS) twaalgosdir = $(pkgincludedir)/twaalgos twaalgos_HEADERS = \ + aiger.hh \ alternation.hh \ are_isomorphic.hh \ bfssteps.hh \ @@ -93,6 +94,7 @@ twaalgos_HEADERS = \ noinst_LTLIBRARIES = libtwaalgos.la libtwaalgos_la_SOURCES = \ + aiger.cc \ alternation.cc \ are_isomorphic.cc \ bfssteps.cc \ diff --git a/spot/twaalgos/aiger.cc b/spot/twaalgos/aiger.cc new file mode 100644 index 000000000..26344ce68 --- /dev/null +++ b/spot/twaalgos/aiger.cc @@ -0,0 +1,420 @@ +// -*- coding: utf-8 -*- +// Copyright (C) 2017 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 + +#include +#include +#include +#include +#include + +#include +#include +#include + +namespace spot +{ + namespace + { + static std::vector + name_vector(unsigned n, const std::string& prefix) + { + std::vector res(n); + for (unsigned i = 0; i != n; ++i) + res[i] = prefix + std::to_string(i); + return res; + } + + // A class to represent an AIGER circuit + class aig + { + private: + unsigned num_inputs_; + unsigned max_var_; + std::map> and_gates_; + std::vector latches_; + std::vector outputs_; + std::vector input_names_; + std::vector output_names_; + // Cache the function computed by each variable as a bdd. + std::unordered_map var2bdd_; + std::unordered_map bdd2var_; + + public: + aig(const std::vector& inputs, + const std::vector& outputs, + unsigned num_latches) + : num_inputs_(inputs.size()), + max_var_((inputs.size() + num_latches)*2), + latches_(num_latches), + outputs_(outputs.size()), + input_names_(inputs), + output_names_(outputs) + { + bdd2var_[bddtrue] = 1; + var2bdd_[1] = bddtrue; + bdd2var_[bddfalse] = 0; + var2bdd_[0] = bddfalse; + } + + aig(unsigned num_inputs, unsigned num_latches, unsigned num_outputs) + : aig(name_vector(num_inputs, "in"), name_vector(num_outputs, "out"), + num_latches) + {} + + unsigned input_var(unsigned i, bdd b) + { + assert(i < num_inputs_); + unsigned v = (1 + i) * 2; + bdd2var_[b] = v; + var2bdd_[v] = b; + return v; + } + + unsigned latch_var(unsigned i, bdd b) + { + assert(i < latches_.size()); + unsigned v = (1 + num_inputs_ + i) * 2; + bdd2var_[b] = v; + var2bdd_[v] = b; + return v; + } + + void set_output(unsigned i, unsigned v) + { + outputs_[i] = v; + } + + void set_latch(unsigned i, unsigned v) + { + latches_[i] = v; + } + + unsigned aig_true() const + { + return 1; + } + + unsigned aig_false() const + { + return 0; + } + + unsigned aig_not(unsigned v) + { + unsigned not_v = v + 1 - 2 * (v % 2); + assert(var2bdd_.count(v)); + var2bdd_[not_v] = !(var2bdd_[v]); + bdd2var_[var2bdd_[not_v]] = not_v; + return not_v; + } + + unsigned aig_and(unsigned v1, unsigned v2) + { + assert(var2bdd_.count(v1)); + assert(var2bdd_.count(v2)); + bdd b = var2bdd_[v1] & var2bdd_[v2]; + auto it = bdd2var_.find(b); + if (it != bdd2var_.end()) + return it->second; + max_var_ += 2; + and_gates_[max_var_] = {v1, v2}; + bdd v1v2 = var2bdd_[v1] & var2bdd_[v2]; + bdd2var_[v1v2] = max_var_; + var2bdd_[max_var_] = v1v2; + return max_var_; + } + + unsigned aig_and(std::vector vs) + { + if (vs.empty()) + return aig_true(); + if (vs.size() == 1) + return vs[0]; + if (vs.size() == 2) + return aig_and(vs[0], vs[1]); + unsigned m = vs.size() / 2; + std::vector left(vs.begin(), vs.begin() + m); + std::vector right(vs.begin() + m, vs.end()); + return aig_and(aig_and(left), aig_and(right)); + } + + unsigned aig_or(unsigned v1, unsigned v2) + { + return aig_not(aig_and(aig_not(v1), aig_not(v2))); + } + + unsigned aig_or(std::vector vs) + { + for (unsigned i = 0; i < vs.size(); ++i) + vs[i] = aig_not(vs[i]); + return aig_not(aig_and(vs)); + } + + unsigned aig_pos(unsigned v) + { + return v - v % 2; + } + + void remove_unused() + { + std::unordered_set todo; + for (unsigned v : outputs_) + todo.insert(aig_pos(v)); + std::unordered_set used; + while (!todo.empty()) + { + used.insert(todo.begin(), todo.end()); + std::unordered_set todo_next; + for (unsigned v : todo) + { + auto it_and = and_gates_.find(v); + if (it_and != and_gates_.end()) + { + if (!used.count(aig_pos(it_and->second.first))) + todo_next.insert(aig_pos(it_and->second.first)); + if (!used.count(aig_pos(it_and->second.second))) + todo_next.insert(aig_pos(it_and->second.second)); + } + else if (v <= (num_inputs_ + latches_.size()) * 2 + && v > num_inputs_ * 2) + { + unsigned l = v / 2 - num_inputs_ - 1; + if (!used.count(aig_pos(latches_[l]))) + todo_next.insert(aig_pos(latches_[l])); + } + } + todo = todo_next; + } + std::unordered_set unused; + for (auto& p : and_gates_) + if (!used.count(p.first)) + unused.insert(p.first); + for (unsigned v : unused) + and_gates_.erase(v); + } + + void + print(std::ostream& os) const + { + os << "aag " << max_var_ / 2 + << ' ' << num_inputs_ + << ' ' << latches_.size() + << ' ' << outputs_.size() + << ' ' << and_gates_.size() << '\n'; + for (unsigned i = 0; i < num_inputs_; ++i) + os << (1 + i) * 2 << '\n'; + for (unsigned i = 0; i < latches_.size(); ++i) + os << (1 + num_inputs_ + i) * 2 << ' ' << latches_[i] << '\n'; + for (unsigned i = 0; i < outputs_.size(); ++i) + os << outputs_[i] << '\n'; + for (auto& p : and_gates_) + os << p.first + << ' ' << p.second.first + << ' ' << p.second.second << '\n'; + for (unsigned i = 0; i < num_inputs_; ++i) + os << 'i' << i << ' ' << input_names_[i] << '\n'; + for (unsigned i = 0; i < outputs_.size(); ++i) + os << 'o' << i << ' ' << output_names_[i] << '\n'; + } + + }; + + static std::vector + state_to_vec(unsigned s, unsigned size) + { + std::vector v(size); + for (unsigned i = 0; i < size; ++i) + { + v[i] = s % 2; + s >>= 1; + } + return v; + } + + static std::vector + output_to_vec(bdd b, + const std::unordered_map& bddvar_to_outputnum) + { + std::vector v(bddvar_to_outputnum.size()); + while (b != bddtrue && b != bddfalse) + { + unsigned i = bddvar_to_outputnum.at(bdd_var(b)); + v[i] = (bdd_low(b) == bddfalse); + if (v[i]) + b = bdd_high(b); + else + b = bdd_low(b); + } + return v; + } + + static bdd + state_to_bdd(unsigned s, bdd all) + { + bdd b = bddtrue; + unsigned size = bdd_nodecount(all); + if (size) + { + unsigned st0 = bdd_var(all); + for (unsigned i = 0; i < size; ++i) + { + b &= s % 2 ? bdd_ithvar(st0 + i) : bdd_nithvar(st0 + i); + s >>= 1; + } + } + return b; + } + + // Switch initial state and 0 in the AIGER encoding, so that the + // 0-initialized latches correspond to the initial state. + static unsigned + encode_init_0(unsigned src, unsigned init) + { + return src == init ? 0 : src == 0 ? init : src; + } + + // Transforms an automaton into an AIGER circuit + static aig + aut_to_aiger(const const_twa_graph_ptr& aut, const bdd& all_outputs) + { + // The aiger circuit cannot encode the acceptance condition + // Test that the acceptance condition is true + if (!aut->acc().is_t()) + throw std::runtime_error("Cannot turn automaton into aiger circuit"); + + // Encode state in log2(num_states) latches. + // TODO how hard is it to compute the binary log of a binary integer?? + unsigned log2n = std::ceil(std::log2(aut->num_states())); + unsigned st0 = aut->get_dict()->register_anonymous_variables(log2n, aut); + bdd all_states = bddtrue; + for (unsigned i = 0; i < log2n; ++i) + all_states &= bdd_ithvar(st0 + i); + + std::vector input_names; + std::vector output_names; + bdd all_inputs = bddtrue; + std::unordered_map bddvar_to_inputnum; + std::unordered_map bddvar_to_outputnum; + for (const auto& ap : aut->ap()) + { + int bddvar = aut->get_dict()->has_registered_proposition(ap, aut); + assert(bddvar >= 0); + bdd b = bdd_ithvar(bddvar); + if (bdd_implies(b, all_outputs)) // ap is an output AP + { + bddvar_to_outputnum[bddvar] = output_names.size(); + output_names.emplace_back(ap.ap_name()); + } + else // ap is an input AP + { + bddvar_to_inputnum[bddvar] = input_names.size(); + input_names.emplace_back(ap.ap_name()); + all_inputs &= b; + } + } + + unsigned num_outputs = bdd_nodecount(all_outputs); + unsigned num_latches = bdd_nodecount(all_states); + unsigned init = aut->get_init_state_number(); + + aig circuit(input_names, output_names, num_latches); + bdd b; + + // Latches and outputs are expressed as a DNF in which each term + // represents a transition. + // latch[i] (resp. out[i]) represents the i-th latch (resp. output) DNF. + std::vector> latch(num_latches); + std::vector> out(num_outputs); + for (unsigned s = 0; s < aut->num_states(); ++s) + for (auto& e: aut->out(s)) + { + minato_isop cond(e.cond); + while ((b = cond.next()) != bddfalse) + { + bdd input = bdd_existcomp(b, all_inputs); + bdd letter_out = bdd_existcomp(b, all_outputs); + auto out_vec = output_to_vec(letter_out, bddvar_to_outputnum); + unsigned dst = encode_init_0(e.dst, init); + auto next_state_vec = state_to_vec(dst, log2n); + unsigned src = encode_init_0(s, init); + bdd state_bdd = state_to_bdd(src, all_states); + std::vector prod; + while (input != bddfalse && input != bddtrue) + { + unsigned v = + circuit.input_var(bddvar_to_inputnum[bdd_var(input)], + bdd_ithvar(bdd_var(input))); + if (bdd_high(input) == bddfalse) + { + v = circuit.aig_not(v); + input = bdd_low(input); + } + else + input = bdd_high(input); + prod.push_back(v); + } + + while (state_bdd != bddfalse && state_bdd != bddtrue) + { + unsigned v = + circuit.latch_var(bdd_var(state_bdd) - st0, + bdd_ithvar(bdd_var(state_bdd))); + if (bdd_high(state_bdd) == bddfalse) + { + v = circuit.aig_not(v); + state_bdd = bdd_low(state_bdd); + } + else + state_bdd = bdd_high(state_bdd); + prod.push_back(v); + } + unsigned t = circuit.aig_and(prod); + for (unsigned i = 0; i < next_state_vec.size(); ++i) + if (next_state_vec[i]) + latch[i].push_back(t); + for (unsigned i = 0; i < num_outputs; ++i) + if (out_vec[i]) + out[i].push_back(t); + } + } + for (unsigned i = 0; i < num_latches; ++i) + circuit.set_latch(i, circuit.aig_or(latch[i])); + for (unsigned i = 0; i < num_outputs; ++i) + circuit.set_output(i, circuit.aig_or(out[i])); + circuit.remove_unused(); + return circuit; + } + } + + std::ostream& + print_aiger(std::ostream& os, const const_twa_ptr& aut) + { + auto a = down_cast(aut); + if (!a) + throw std::runtime_error("aiger output is only for twa_graph"); + + bdd* all_outputs = aut->get_named_prop("synthesis-outputs"); + + aig circuit = aut_to_aiger(a, all_outputs ? *all_outputs : bdd(bddfalse)); + circuit.print(os); + return os; + } +} diff --git a/spot/twaalgos/aiger.hh b/spot/twaalgos/aiger.hh new file mode 100644 index 000000000..dcd0f5b2a --- /dev/null +++ b/spot/twaalgos/aiger.hh @@ -0,0 +1,46 @@ +// -*- coding: utf-8 -*- +// Copyright (C) 2017 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 +#include + +namespace spot +{ + /// \ingroup twa_io + /// \brief Encode and print an automaton as an AIGER circuit. + /// + /// The circuit actually encodes the transition relation of the automaton, not + /// its acceptance condition. Therefore, this function will reject automata + /// whose acceptance condition is not trivial (i.e. true). + /// States are encoded by latches (or registers) in the circuit. Atomic + /// propositions are encoded as inputs and outputs of the circuit. To know + /// which AP should be encoded as outputs, print_aiger() relies on the named + /// property "synthesis-outputs", which is a bdd containing the conjunction of + /// such output propositions. All other AP are encoded as inputs. If the named + /// property is not set, all AP are encoded as inputs, and the circuit has no + /// output. + /// + /// \param os The output stream to print on. + /// \param aut The automaton to output. + SPOT_API std::ostream& + print_aiger(std::ostream& os, const const_twa_ptr& aut); +} diff --git a/tests/Makefile.am b/tests/Makefile.am index 8fe314b19..fd076c0df 100644 --- a/tests/Makefile.am +++ b/tests/Makefile.am @@ -309,7 +309,8 @@ TESTS_twa = \ core/acc_word.test \ core/dca.test \ core/dnfstreett.test \ - core/parity.test + core/parity.test \ + core/ltlsynt.test ############################## PYTHON ############################## diff --git a/tests/core/ltlsynt.test b/tests/core/ltlsynt.test index 0d9cfdd51..50874a47f 100644 --- a/tests/core/ltlsynt.test +++ b/tests/core/ltlsynt.test @@ -1,6 +1,6 @@ #! /bin/sh # -*- coding: utf-8 -*- -# Copyright (C) 2014, 2015 Laboratoire de Recherche et Développement +# Copyright (C) 2017 Laboratoire de Recherche et Développement # de l'Epita (LRDE). # # This file is part of Spot, a model checking library. @@ -80,1011 +80,33 @@ U (r0)) || (G (a0)))) && (((a1) U (r1)) || (G (a1)))) && (((a2) U (r2)) || (G IN9='r0, r1, r2' OUT9='a0, a1, a2' EXP9='UNREALIZABLE' - -cat <exp2 -REALIZABLE -aag 144 3 4 1 132 -2 -4 -6 -8 211 -10 245 -12 271 -14 289 -271 -16 13 15 -18 11 16 -20 3 9 -26 6 20 -28 26 18 -30 2 9 -32 7 30 -34 32 18 -36 6 30 -38 36 18 -40 3 8 -42 7 40 -44 42 18 -46 6 40 -48 46 18 -50 2 8 -52 7 50 -54 52 18 -56 6 50 -58 56 18 -60 9 10 -62 60 16 -64 3 4 -66 7 64 -70 6 64 -72 70 62 -74 2 4 -76 7 74 -78 76 62 -80 6 74 -82 80 62 -84 10 16 -86 5 9 -88 86 84 -90 8 10 -92 90 16 -94 66 92 -96 70 92 -98 76 92 -100 80 92 -102 5 8 -104 102 84 -106 12 15 -108 11 106 -112 26 108 -114 32 108 -116 36 108 -118 40 108 -120 50 108 -122 60 106 -126 70 122 -128 76 122 -130 80 122 -132 10 106 -134 86 132 -136 4 8 -138 3 136 -140 138 132 -142 2 136 -144 142 132 -146 102 132 -148 13 14 -150 9 11 -152 150 148 -154 11 148 -156 42 154 -158 46 154 -160 52 154 -162 56 154 -164 10 148 -166 86 164 -168 60 148 -170 66 168 -172 70 168 -174 76 168 -176 80 168 -178 173 177 -180 163 178 -182 141 159 -184 182 180 -186 127 131 -188 117 119 -190 188 186 -192 190 184 -194 101 113 -196 97 194 -198 73 83 -200 198 196 -202 49 59 -204 29 39 -206 204 202 -208 206 200 -210 208 192 -212 175 177 -214 163 212 -216 145 161 -218 216 214 -220 129 131 -222 117 121 -224 222 220 -226 224 218 -228 101 115 -230 99 228 -232 79 83 -234 232 230 -236 55 59 -238 35 39 -240 238 236 -242 240 234 -244 242 226 -246 171 173 -248 246 212 -250 161 163 -252 157 159 -254 252 250 -256 254 248 -258 99 101 -260 95 97 -262 260 258 -264 45 49 -266 264 236 -268 266 262 -270 268 256 -272 153 167 -274 147 272 -276 141 145 -278 276 274 -280 121 135 -282 119 280 -284 89 105 -286 284 282 -288 286 278 -i0 cancel -i1 go -i2 req -o0 grant -EOF - -cat <exp3 -REALIZABLE -aag 264 3 4 1 257 -2 -4 -6 -8 313 -10 377 -12 443 -14 483 -529 -16 13 15 -18 11 16 -20 3 9 -22 7 20 -24 22 18 -26 2 9 -28 7 26 -30 28 18 -32 6 26 -34 32 18 -36 6 20 -38 36 18 -40 3 8 -42 7 40 -44 42 18 -46 2 8 -48 7 46 -50 48 18 -52 6 46 -54 52 18 -56 6 40 -58 56 18 -60 9 10 -62 60 16 -64 3 4 -66 7 64 -68 66 62 -70 2 4 -72 7 70 -74 72 62 -76 6 70 -78 76 62 -80 6 64 -82 80 62 -84 10 16 -86 5 9 -88 7 86 -90 88 84 -92 6 86 -94 92 84 -96 5 8 -98 96 84 -100 8 10 -102 100 16 -104 66 102 -106 72 102 -108 76 102 -110 80 102 -112 12 15 -114 11 112 -116 22 114 -118 28 114 -120 32 114 -122 36 114 -124 42 114 -126 48 114 -128 52 114 -130 56 114 -132 60 112 -134 66 132 -136 72 132 -138 76 132 -140 80 132 -142 10 112 -144 88 142 -146 92 142 -148 96 142 -150 4 8 -152 3 150 -154 152 142 -156 2 150 -158 156 142 -160 13 14 -162 11 160 -164 20 162 -166 26 162 -168 42 162 -170 48 162 -172 52 162 -174 56 162 -176 60 160 -178 66 176 -180 72 176 -182 76 176 -184 80 176 -186 10 160 -188 86 186 -190 96 186 -192 100 160 -194 66 192 -196 72 192 -198 76 192 -200 80 192 -202 12 14 -204 9 11 -206 204 202 -208 11 202 -210 96 208 -212 8 11 -214 212 202 -216 66 214 -218 72 214 -220 76 214 -222 80 214 -224 60 202 -226 66 224 -228 72 224 -230 76 224 -232 80 224 -234 10 202 -236 86 234 -238 100 202 -240 66 238 -242 72 238 -244 76 238 -246 80 238 -248 96 234 -250 241 245 -252 231 250 -254 221 227 -256 254 252 -258 199 217 -260 189 195 -262 260 258 -264 262 256 -266 179 183 -268 169 173 -270 268 266 -272 155 165 -274 147 149 -276 274 272 -278 276 270 -280 278 264 -282 135 139 -284 125 129 -286 284 282 -288 117 121 -290 105 109 -292 290 288 -294 292 286 -296 95 99 -298 69 79 -300 298 296 -302 45 55 -304 25 35 -306 304 302 -308 306 300 -310 308 294 -312 310 280 -314 243 245 -316 231 314 -318 221 229 -320 318 316 -322 199 219 -324 189 197 -326 324 322 -328 326 320 -330 181 183 -332 171 173 -334 332 330 -336 159 167 -338 145 147 -340 338 336 -342 340 334 -344 342 328 -346 137 139 -348 127 129 -350 348 346 -352 119 121 -354 107 109 -356 354 352 -358 356 350 -360 91 95 -362 75 79 -364 362 360 -366 51 55 -368 31 35 -370 368 366 -372 370 364 -374 372 358 -376 374 344 -378 245 249 -380 243 378 -382 237 241 -384 382 380 -386 221 233 -388 219 386 -390 211 217 -392 390 388 -394 392 384 -396 199 207 -398 197 396 -400 191 195 -402 400 398 -404 173 179 -406 404 330 -408 406 402 -410 408 394 -412 169 171 -414 149 412 -416 338 414 -418 131 141 -420 121 418 -422 117 119 -424 422 420 -426 424 416 -428 105 354 -430 296 428 -432 83 91 -434 39 59 -436 434 432 -438 436 430 -440 438 426 -442 440 410 -444 247 249 -446 237 444 -448 211 223 -450 207 448 -452 450 446 -454 191 201 -456 189 454 -458 175 185 -460 167 458 -462 460 456 -464 462 452 -466 159 165 -468 155 466 -470 145 274 -472 470 468 -474 111 123 -476 99 474 -478 360 476 -480 478 472 -482 480 464 -484 245 247 -486 241 243 -488 486 484 -490 221 223 -492 219 490 -494 492 488 -496 201 217 -498 197 199 -500 498 496 -502 185 195 -504 183 502 -506 504 500 -508 506 494 -510 179 181 -512 173 175 -514 512 510 -516 123 412 -518 516 514 -520 111 117 -522 520 352 -524 428 522 -526 524 518 -528 526 508 -i0 cancel -i1 go -i2 req -o0 grant -EOF - -cat <exp4 -REALIZABLE -aag 174 3 4 1 163 -2 -4 -6 -8 251 -10 299 -12 325 -14 333 -349 -16 13 15 -18 11 16 -20 7 9 -22 3 20 -26 6 9 -28 3 26 -30 28 18 -32 2 20 -34 32 18 -36 2 26 -38 36 18 -40 7 8 -42 2 40 -44 42 18 -46 6 8 -48 2 46 -50 48 18 -52 3 40 -54 52 18 -56 3 46 -58 56 18 -60 9 10 -62 60 16 -64 7 4 -66 3 64 -70 6 4 -72 3 70 -74 72 62 -76 2 64 -78 76 62 -80 2 70 -82 80 62 -84 10 16 -86 5 9 -88 7 86 -90 88 84 -92 6 86 -94 92 84 -96 8 10 -98 96 16 -100 76 98 -102 80 98 -104 66 98 -106 72 98 -108 7 5 -110 2 108 -112 110 98 -114 6 5 -116 2 114 -118 116 98 -120 5 8 -122 3 120 -124 122 84 -126 12 15 -128 11 126 -132 28 128 -134 32 128 -136 36 128 -138 42 128 -140 48 128 -142 3 8 -144 142 128 -146 60 126 -150 72 146 -152 76 146 -154 80 146 -156 10 126 -158 86 156 -160 96 126 -162 76 160 -164 80 160 -166 66 160 -168 72 160 -170 120 156 -172 13 14 -174 9 11 -176 174 172 -178 76 176 -180 80 176 -182 66 176 -184 72 176 -186 11 172 -188 86 186 -190 8 11 -192 190 172 -194 10 172 -196 32 194 -198 36 194 -200 22 194 -202 28 194 -204 199 203 -206 189 193 -208 206 204 -210 181 185 -212 171 210 -214 212 208 -216 165 169 -218 159 216 -220 151 155 -222 141 220 -224 222 218 -226 224 214 -228 133 137 -230 119 228 -232 103 107 -234 95 232 -236 234 230 -238 75 83 -240 59 238 -242 39 51 -244 31 242 -246 244 240 -248 246 236 -250 248 226 -252 197 199 -254 179 181 -256 254 252 -258 163 165 -260 155 258 -262 260 256 -264 145 153 -266 141 264 -268 137 139 -270 135 268 -272 270 266 -274 272 262 -276 113 119 -278 103 276 -280 95 101 -282 91 280 -284 282 278 -286 79 83 -288 51 286 -290 39 45 -292 35 290 -294 292 288 -296 294 284 -298 296 274 -300 201 203 -302 183 185 -304 302 300 -306 167 169 -308 119 306 -310 308 304 -312 107 113 -314 95 105 -316 314 312 -318 59 91 -320 55 318 -322 320 316 -324 322 310 -326 171 206 -328 145 159 -330 125 328 -332 330 326 -334 185 300 -336 169 183 -338 336 334 -340 107 167 -342 105 340 -344 55 59 -346 344 342 -348 346 338 -i0 cancel -i1 go -i2 req -o0 grant -EOF - -cat <exp5 -REALIZABLE -aag 289 3 4 1 282 -2 -4 -6 -8 367 -10 455 -12 509 -14 547 -579 -16 13 15 -18 11 16 -20 7 9 -22 3 20 -24 22 18 -26 2 20 -28 26 18 -30 6 9 -32 2 30 -34 32 18 -36 3 30 -38 36 18 -40 7 8 -42 3 40 -44 42 18 -46 2 40 -48 46 18 -50 6 8 -52 2 50 -54 52 18 -56 3 50 -58 56 18 -60 9 10 -62 60 16 -64 7 4 -66 3 64 -68 66 62 -70 2 64 -72 70 62 -74 6 4 -76 2 74 -78 76 62 -80 3 74 -82 80 62 -84 10 16 -86 5 9 -88 7 86 -90 88 84 -92 6 86 -94 92 84 -96 8 10 -98 96 16 -100 70 98 -102 76 98 -104 7 5 -106 2 104 -108 106 98 -110 6 5 -112 2 110 -114 112 98 -116 5 8 -118 3 116 -120 118 84 -122 66 98 -124 80 98 -126 12 15 -128 11 126 -130 26 128 -132 32 128 -134 22 128 -136 36 128 -138 46 128 -140 52 128 -142 3 8 -144 142 128 -146 10 126 -148 26 146 -150 32 146 -152 22 146 -154 36 146 -156 96 126 -158 66 156 -160 70 156 -162 76 156 -164 80 156 -166 7 116 -168 166 146 -170 6 116 -172 170 146 -174 13 14 -176 9 11 -178 176 174 -180 70 178 -182 76 178 -184 66 178 -186 80 178 -188 106 178 -190 112 178 -192 11 174 -194 3 86 -196 194 192 -198 8 11 -200 198 174 -202 70 200 -204 76 200 -206 106 200 -208 112 200 -210 118 192 -212 66 200 -214 80 200 -216 60 174 -218 66 216 -220 70 216 -222 76 216 -224 80 216 -226 10 174 -228 86 226 -230 96 174 -232 70 230 -234 76 230 -236 66 230 -238 80 230 -240 116 226 -242 12 14 -244 176 242 -246 70 244 -248 76 244 -250 11 242 -252 86 250 -254 66 244 -256 80 244 -258 198 242 -260 10 242 -262 22 260 -264 26 260 -266 32 260 -268 36 260 -270 96 242 -272 70 270 -274 76 270 -276 66 270 -278 80 270 -280 116 260 -282 279 281 -284 277 282 -286 267 275 -288 259 286 -290 288 284 -292 255 257 -294 253 292 -296 241 249 -298 296 294 -300 298 290 -302 237 239 -304 235 302 -306 223 229 -308 215 306 -310 308 304 -312 209 213 -314 205 312 -316 191 197 -318 316 314 -320 318 310 -322 320 300 -324 185 187 -326 183 324 -328 163 173 -330 155 328 -332 330 326 -334 151 153 -336 141 334 -338 135 137 -340 338 336 -342 340 332 -344 125 133 -346 123 344 -348 109 121 -350 103 348 -352 350 346 -354 79 91 -356 55 354 -358 25 35 -360 358 356 -362 360 352 -364 362 342 -366 364 322 -368 273 275 -370 267 368 -372 263 265 -374 249 372 -376 374 370 -378 235 247 -380 233 378 -382 221 223 -384 219 382 -386 384 380 -388 386 376 -390 207 209 -392 205 390 -394 197 203 -396 191 394 -398 396 392 -400 183 189 -402 181 400 -404 169 173 -406 404 402 -408 406 398 -410 408 388 -412 161 163 -414 159 412 -416 149 151 -418 145 416 -420 418 414 -422 139 141 -424 133 422 -426 109 131 -428 426 424 -430 428 420 -432 101 103 -434 91 432 -436 73 79 -438 69 436 -440 438 434 -442 49 55 -444 45 442 -446 29 35 -448 446 444 -450 448 440 -452 450 430 -454 452 410 -456 263 269 -458 456 282 -460 257 259 -462 241 253 -464 462 460 -466 464 458 -468 229 239 -470 219 225 -472 470 468 -474 211 215 -476 197 474 -478 476 472 -480 478 466 -482 165 187 -484 155 159 -486 484 482 -488 137 145 -490 125 488 -492 490 486 -494 91 109 -496 69 83 -498 496 494 -500 45 59 -502 39 500 -504 502 498 -506 504 492 -508 506 480 -510 263 281 -512 259 510 -514 229 462 -516 514 512 -518 211 219 -520 209 518 -522 197 207 -524 522 520 -526 524 516 -528 189 191 -530 173 528 -532 159 169 -534 532 530 -536 115 121 -538 95 536 -540 45 69 -542 540 538 -544 542 534 -546 544 526 -548 277 279 -550 257 548 -552 239 255 -554 552 550 -556 215 237 -558 187 213 -560 558 556 -562 560 554 -564 155 185 -566 137 153 -568 566 564 -570 125 135 -572 25 123 -574 572 570 -576 574 568 -578 576 562 -i0 cancel -i1 go -i2 req -o0 grant -EOF - -cat <exp6 -REALIZABLE -aag 76 3 3 1 63 -2 -4 -6 -8 125 -10 141 -12 147 -153 -14 11 13 -16 2 9 -18 16 14 -20 9 14 -26 3 6 -28 26 20 -30 8 14 -32 2 4 -34 32 30 -42 6 4 -44 3 42 -46 44 30 -48 6 5 -50 3 48 -52 50 30 -54 2 5 -56 54 30 -58 7 5 -60 58 30 -62 10 13 -64 16 62 -66 9 62 -70 26 66 -72 2 8 -74 72 62 -76 3 8 -78 76 62 -80 11 12 -82 9 80 -84 32 82 -86 3 4 -88 86 82 -90 5 9 -92 90 80 -94 8 80 -96 32 94 -100 44 94 -102 5 8 -104 102 80 -106 10 12 -108 9 106 -110 85 97 -112 75 110 -114 65 71 -116 114 112 -118 57 61 -120 19 35 -122 120 118 -124 122 116 -126 105 109 -128 101 126 -130 89 93 -132 130 128 -134 71 79 -136 29 47 -138 136 134 -140 138 132 -142 93 126 -144 53 118 -146 144 142 -148 89 101 -150 79 148 -152 136 150 -i0 cancel -i1 go -i2 req -o0 grant -EOF +IN10='a, b, c' +OUT10='p0, p1, p2' +F10='G (p0 && ! p1 && ! p2 || (! p0 && p1 && ! p2) || (! p0 && ! p1 && p2)) && + (F (G a) || F (G b) || G (F c) <-> (G (F p0) || (G (F p1) && ! G (F p2))))' +EXP10='REALIZABLE' for i in 0 1 7 8 9; do F=$(eval echo \$F$i) IN=$(eval echo \$IN$i) OUT=$(eval echo \$OUT$i) EXP=$(eval echo \$EXP$i) - REAL_REC=$(ltlsynt -f "$F" --input="$IN" --output="$OUT" \ - --realizability --algo=rec) - test $REAL_REC = UNREALIZABLE - REAL_QP=$(ltlsynt -f "$F" --input="$IN" --output="$OUT" \ - --realizability --algo=qp) - test $REAL_QP = UNREALIZABLE - SYNT=$(ltlsynt -f "$F" --input="$IN" --output="$OUT") - test $SYNT = UNREALIZABLE - PG=$(mktemp) + test $EXP = `ltlsynt -f "$F" --ins="$IN" --outs="$OUT" --realizability + --algo=rec` + test $EXP = `ltlsynt -f "$F" --ins="$IN" --outs="$OUT" --realizability + --algo=qp` done -for i in 2 3 4 5 6; do +for i in 2 3 4 5 6 10; do F=$(eval echo \$F$i) IN=$(eval echo \$IN$i) OUT=$(eval echo \$OUT$i) EXP=$(eval echo \$EXP$i) - REAL=$(ltlsynt -f "$F" --input="$IN" --output="$OUT" --realizability) - test $REAL = REALIZABLE - ltlsynt -f "$F" --input="$IN" --output="$OUT" > out$i - diff out$i exp$i + ltlsynt -f "$F" --ins="$IN" --outs="$OUT" > out$i + REAL=`head -1 out$i` + test $REAL = $EXP + tail -n +2 out$i > res$i + ltl2tgba -f "!($F)" > negf_aut$i + # check that the L(strategy) is included in L(F) + autfilt -q -v --intersect=negf_aut$i res$i done