diff --git a/NEWS b/NEWS index c540aec68..c405dca2f 100644 --- a/NEWS +++ b/NEWS @@ -13,6 +13,11 @@ New in spot 2.9.4.dev (not yet released) - ltlsynt learned --print-game-hoa to output its internal parity game in the HOA format (with an extension described below). + - ltlsynt --aiger option now takes an optional argument indicating + how the bdd and states are to be encoded in the aiger output. + Choices are "ITE" for the if-then-else normal form or "ISOP" for + relying on irreducible sums of products. + Library: - Historically, Spot labels automata by Boolean formulas over diff --git a/bin/ltlsynt.cc b/bin/ltlsynt.cc index b5fa67bac..4c5b10d7c 100644 --- a/bin/ltlsynt.cc +++ b/bin/ltlsynt.cc @@ -93,8 +93,10 @@ static const argp_option options[] = "print the parity game in the HOA format, do not solve it", 0}, { "realizability", OPT_REAL, nullptr, 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}, + { "aiger", OPT_PRINT_AIGER, "ITE|ISOP", OPTION_ARG_OPTIONAL, + "prints a winning strategy as an AIGER circuit. With argument \"ISOP\"" + " conditions are converted to DNF, while the default \"ITE\" uses the " + "if-the-else normal form.", 0}, { "verbose", OPT_VERBOSE, nullptr, 0, "verbose mode", -1 }, { "csv", OPT_CSV, "[>>]FILENAME", OPTION_ARG_OPTIONAL, @@ -132,7 +134,7 @@ static bool opt_print_pg = false; static bool opt_print_hoa = false; static const char* opt_print_hoa_args = nullptr; static bool opt_real = false; -static bool opt_print_aiger = false; +static const char* opt_print_aiger = nullptr; static spot::option_map extra_options; static double trans_time = 0.0; @@ -542,7 +544,7 @@ namespace // output the winning strategy if (opt_print_aiger) - spot::print_aiger(std::cout, strat_aut); + spot::print_aiger(std::cout, strat_aut, opt_print_aiger); else { automaton_printer printer; @@ -612,7 +614,7 @@ parse_opt(int key, char* arg, struct argp_state*) opt_print_hoa_args = arg; break; case OPT_PRINT_AIGER: - opt_print_aiger = true; + opt_print_aiger = arg ? arg : "INF"; break; case OPT_REAL: opt_real = true; diff --git a/spot/twaalgos/aiger.cc b/spot/twaalgos/aiger.cc index ea8f8ee6e..ff73e7a58 100644 --- a/spot/twaalgos/aiger.cc +++ b/spot/twaalgos/aiger.cc @@ -1,5 +1,5 @@ // -*- coding: utf-8 -*- -// Copyright (C) 2017-2019 Laboratoire de Recherche et Développement +// Copyright (C) 2017-2020 Laboratoire de Recherche et Développement // de l'Epita (LRDE). // // This file is part of Spot, a model checking library. @@ -21,10 +21,10 @@ #include #include -#include -#include #include #include +#include +#include #include #include @@ -47,13 +47,16 @@ namespace spot class aig { private: - unsigned num_inputs_; unsigned max_var_; - std::map> and_gates_; + unsigned num_inputs_; + unsigned num_latches_; + unsigned num_outputs_; + std::vector latches_; std::vector outputs_; std::vector input_names_; std::vector output_names_; + std::vector> and_gates_; // Cache the function computed by each variable as a bdd. std::unordered_map var2bdd_; std::unordered_map bdd2var_; @@ -62,8 +65,10 @@ namespace spot aig(const std::vector& inputs, const std::vector& outputs, unsigned num_latches) - : num_inputs_(inputs.size()), - max_var_((inputs.size() + num_latches)*2), + : max_var_((inputs.size() + num_latches)*2), + num_inputs_(inputs.size()), + num_latches_(num_latches), + num_outputs_(outputs.size()), latches_(num_latches), outputs_(outputs.size()), input_names_(inputs), @@ -73,38 +78,58 @@ namespace spot var2bdd_[1] = bddtrue; bdd2var_[bddfalse] = 0; var2bdd_[0] = bddfalse; + + bdd2var_.reserve(4 * (num_inputs_ + num_latches_)); + var2bdd_.reserve(4 * (num_inputs_ + num_latches_)); } 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) + // register the bdd corresponding the an + // aig literal + inline void register_new_lit(unsigned v, const bdd& b) + { + assert(!var2bdd_.count(v) || var2bdd_.at(v) == b); + assert(!bdd2var_.count(b) || bdd2var_.at(b) == v); + var2bdd_[v] = b; + bdd2var_[b] = v; + // Also store negation + // Do not use aig_not as tests will fail + var2bdd_[v ^ 1] = !b; + bdd2var_[!b] = v ^ 1; + } + + inline unsigned input_var(unsigned i) const + { + assert(i < num_inputs_); + return (1 + i) * 2; + } + + inline unsigned latch_var(unsigned i) { assert(i < latches_.size()); - unsigned v = (1 + num_inputs_ + i) * 2; - bdd2var_[b] = v; - var2bdd_[v] = b; - return v; + return (1 + num_inputs_ + i) * 2; + } + + inline unsigned gate_var(unsigned i)const + { + assert(i < and_gates_.size()); + return (1 + num_inputs_ + num_latches_ + i) * 2; } void set_output(unsigned i, unsigned v) { + assert(v <= max_var_+1); outputs_[i] = v; } void set_latch(unsigned i, unsigned v) { + assert(v <= max_var_+1); latches_[i] = v; } @@ -121,9 +146,8 @@ namespace spot unsigned aig_not(unsigned v) { unsigned not_v = v ^ 1; - assert(var2bdd_.count(v)); - var2bdd_[not_v] = !(var2bdd_[v]); - bdd2var_[var2bdd_[not_v]] = not_v; + assert(var2bdd_.count(v) + && var2bdd_.count(not_v)); return not_v; } @@ -136,9 +160,8 @@ namespace spot if (it != bdd2var_.end()) return it->second; max_var_ += 2; - and_gates_[max_var_] = {v1, v2}; - bdd2var_[b] = max_var_; - var2bdd_[max_var_] = b; + and_gates_.emplace_back(v1, v2); + register_new_lit(max_var_, b); return max_var_; } @@ -150,12 +173,20 @@ namespace spot return vs[0]; if (vs.size() == 2) return aig_and(vs[0], vs[1]); - unsigned m = vs.size() / 2; - unsigned left = - aig_and(std::vector(vs.begin(), vs.begin() + m)); - unsigned right = - aig_and(std::vector(vs.begin() + m, vs.end())); - return aig_and(left, right); + + do + { + if (vs.size()&1) + // Odd size -> make even + vs.push_back(aig_true()); + // Sort to increase reusage gates + std::sort(vs.begin(), vs.end()); + // Reduce two by two inplace + for (unsigned i = 0; i < vs.size()/2; ++i) + vs[i] = aig_and(vs[2*i], vs[2*i + 1]); + vs.resize(vs.size()/2); + }while (vs.size() > 1); + return vs[0]; } unsigned aig_or(unsigned v1, unsigned v2) @@ -174,121 +205,227 @@ namespace spot unsigned aig_pos(unsigned v) { - return v & ~1; } void remove_unused() { - // Run a DFS on the gates and latches to collect + // Run a DFS on the gates to collect // all nodes connected to the output. - std::deque todo; - std::vector used(max_var_ / 2 + 1, false); + std::vector todo; + std::vector used(and_gates_.size(), false); + + // The variables are numbered by first enumerating + // inputs, latches and finally the and-gates + // v_latch = (1+n_i+i)*2 if latch is in positive form + // if v/2 < 1+n_i -> v is an input + // v_gate = (1+n_i+n_l+i)*2 if gate is in positive form + // if v/2 < 1+n_i_nl -> v is a latch + auto v2idx = [&](unsigned v)->unsigned + { + assert(!(v & 1)); + const unsigned Nlatch_min = 1 + num_inputs_; + const unsigned Ngate_min = 1 + num_inputs_ + num_latches_; + + // Note: this will at most run twice + while (true) + { + unsigned i = v / 2; + if (i >= Ngate_min) + // v is a gate + return i - Ngate_min; + else if (i >= Nlatch_min) + // v is a latch -> get gate + v = aig_pos(latches_.at(i - Nlatch_min)); + else + // v is a input -> nothing to do + return -1U; + } + }; + auto mark = [&](unsigned v) - { - unsigned pos = aig_pos(v); - if (!used[pos/2]) - { - used[pos/2] = 1; - todo.push_back(pos); - } - }; + { + unsigned idx = v2idx(aig_pos(v)); + if ((idx == -1U) || used[idx]) + return; + used[idx] = true; + todo.push_back(idx); + }; + for (unsigned v : outputs_) mark(v); + while (!todo.empty()) { - unsigned v = todo.front(); - todo.pop_front(); - auto it_and = and_gates_.find(v); - if (it_and != and_gates_.end()) - { - mark(it_and->second.first); - mark(it_and->second.second); - } - else if (v <= (num_inputs_ + latches_.size()) * 2 - && v > num_inputs_ * 2) - { - mark(latches_[v / 2 - num_inputs_ - 1]); - } + unsigned idx = todo.back(); + todo.pop_back(); + + mark(and_gates_[idx].first); + mark(and_gates_[idx].second); } // Erase and_gates that were not seen in the above // exploration. - auto e = and_gates_.end(); - for (auto i = and_gates_.begin(); i != e;) + // To avoid renumbering all gates, erasure is done + // by setting both inputs to "false" + for (unsigned idx = 0; idx < used.size(); ++idx) + if (!used[idx]) + { + and_gates_[idx].first = 0; + and_gates_[idx].second = 0; + } + } + + // Takes a bdd, computes the corresponding literal + // using its DNF + unsigned bdd2DNFvar(const bdd& b, + const std::unordered_map& + bddvar_to_num) + { + std::vector plus_vars; + std::vector prod_vars(num_inputs_); + + minato_isop cond(b); + bdd prod; + + while ((prod = cond.next()) != bddfalse) { - if (!used[i->first/2]) - i = and_gates_.erase(i); + prod_vars.clear(); + // Check if existing + auto it = bdd2var_.find(prod); + if (it != bdd2var_.end()) + plus_vars.push_back(it->second); else - ++i; + { + // Create + while (prod != bddfalse && prod != bddtrue) + { + unsigned v = + input_var(bddvar_to_num.at(bdd_var(prod))); + if (bdd_high(prod) == bddfalse) + { + v = aig_not(v); + prod = bdd_low(prod); + } + else + prod = bdd_high(prod); + prod_vars.push_back(v); + } + plus_vars.push_back(aig_and(prod_vars)); + } } + + // Done building + return aig_or(plus_vars); + } + + // Takes a bdd, computes the corresponding literal + // using its INF + unsigned bdd2INFvar(bdd b) + { + // F = !v&low | v&high + // De-morgan + // !(!v&low | v&high) = !(!v&low) & !(v&high) + // !v&low | v&high = !(!(!v&low) & !(v&high)) + auto b_it = bdd2var_.find(b); + if (b_it != bdd2var_.end()) + return b_it->second; + + unsigned v_var = bdd2var_.at(bdd_ithvar(bdd_var(b))); + + bdd b_branch[2] = {bdd_low(b), bdd_high(b)}; + unsigned b_branch_var[2]; + + for (unsigned i: {0, 1}) + { + auto b_branch_it = bdd2var_.find(b_branch[i]); + if (b_branch_it == bdd2var_.end()) + b_branch_var[i] = bdd2INFvar(b_branch[i]); + else + b_branch_var[i] = b_branch_it->second; + } + + unsigned r = aig_not(aig_and(v_var, b_branch_var[1])); + unsigned l = aig_not(aig_and(aig_not(v_var), b_branch_var[0])); + return aig_not(aig_and(l, r)); } void print(std::ostream& os) const { + // Writing gates to formatted buffer speed-ups output + // as it avoids "<<" calls + // vars are unsigned -> 10 digits at most + char gate_buffer[3*10+5]; + auto write_gate = [&](unsigned o, unsigned i0, unsigned i1) + { + std::sprintf(gate_buffer, "%u %u %u\n", o, i0, i1); + os << gate_buffer; + }; + // Count active gates + unsigned n_gates=0; + for (auto& g : and_gates_) + if ((g.first != 0) && (g.second != 0)) + ++n_gates; + // Note max_var_ is now an upper bound os << "aag " << max_var_ / 2 << ' ' << num_inputs_ - << ' ' << latches_.size() - << ' ' << outputs_.size() - << ' ' << and_gates_.size() << '\n'; + << ' ' << num_latches_ + << ' ' << num_outputs_ + << ' ' << n_gates << '\n'; for (unsigned i = 0; i < num_inputs_; ++i) os << (1 + i) * 2 << '\n'; - for (unsigned i = 0; i < latches_.size(); ++i) + for (unsigned i = 0; i < num_latches_; ++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 - state_to_vec(unsigned s, unsigned size) + static void + state_to_vec(std::vector& v, unsigned s) { - std::vector v(size); - for (unsigned i = 0; i < size; ++i) + for (unsigned i = 0; i < v.size(); ++i) { v[i] = s & 1; s >>= 1; - } - return v; + }; } - static std::vector - output_to_vec(bdd b, - const std::unordered_map& bddvar_to_outputnum) + static void + output_to_vec(std::vector& v, bdd b, + const std::unordered_map& + bddvar_to_outputnum) { - std::vector v(bddvar_to_outputnum.size()); + std::fill(v.begin(), v.end(), false); 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); + unsigned i = bddvar_to_outputnum.at(bdd_var(b)); + v.at(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) + state_to_bdd(unsigned s, bdd all_latches) { bdd b = bddtrue; - unsigned size = bdd_nodecount(all); + unsigned size = bdd_nodecount(all_latches); if (size) { - unsigned st0 = bdd_var(all); + unsigned st0 = bdd_var(all_latches); for (unsigned i = 0; i < size; ++i) { - b &= (s & 1) ? bdd_ithvar(st0 + i) : bdd_nithvar(st0 + i); + b &= (s & 1) ? bdd_ithvar(st0 + i) : bdd_nithvar(st0 + i); s >>= 1; } } @@ -303,28 +440,84 @@ namespace spot return src == init ? 0 : src == 0 ? init : src; } + // Takes a product and returns the + // number of highs + inline unsigned count_high(bdd b) + { + unsigned high=0; + while (b != bddtrue) + { + if (bdd_low(b) == bddfalse) + { + ++high; + b = bdd_high(b); + } + else + { + assert(bdd_high(b) == bddfalse); + b = bdd_low(b); + } + } + return high; + } + + // Heuristic to minimize the number of gates + // in the resulting aiger + // the idea is to take the (valid) output with the + // least "highs" for each transition. + // Another idea is to chose conditions such that transitions + // can share output conditions. Problem this is a combinatorial + // problem and suboptimal solutions that can be computed in + // reasonable time have proven to be not as good + // Stores the outcondition to use in the used_outc vector + // for each transition in aut + std::vector maxlow_outc(const const_twa_graph_ptr& aut, + const bdd& all_inputs) + { + std::vector used_outc(aut->num_edges()+1, bddfalse); + + for (const auto &e : aut->edges()) + { + unsigned idx = aut->edge_number(e); + assert(e.cond != bddfalse); + bdd bout = bdd_exist(e.cond, all_inputs); + assert(((bout & bdd_existcomp(e.cond, all_inputs)) == e.cond) && + "Precondition (in) & (out) == cond violated"); + unsigned n_high=-1u; + while (bout != bddfalse) + { + bdd nextsat = bdd_satone(bout); + bout -= nextsat; + unsigned next_high = count_high(nextsat); + if (next_highacc().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); - + // get the propositions std::vector input_names; std::vector output_names; bdd all_inputs = bddtrue; - std::unordered_map bddvar_to_inputnum; - std::unordered_map bddvar_to_outputnum; + std::vector all_inputs_vec; + std::unordered_map bddvar_to_num; for (const auto& ap : aut->ap()) { int bddvar = aut->get_dict()->has_registered_proposition(ap, aut); @@ -332,92 +525,169 @@ namespace spot bdd b = bdd_ithvar(bddvar); if (bdd_implies(all_outputs, b)) // ap is an output AP { - bddvar_to_outputnum[bddvar] = output_names.size(); + bddvar_to_num[bddvar] = output_names.size(); output_names.emplace_back(ap.ap_name()); } else // ap is an input AP { - bddvar_to_inputnum[bddvar] = input_names.size(); + bddvar_to_num[bddvar] = input_names.size(); input_names.emplace_back(ap.ap_name()); all_inputs &= b; + all_inputs_vec.push_back(b); } } - unsigned num_outputs = bdd_nodecount(all_outputs); - unsigned num_latches = bdd_nodecount(all_states); + // Decide on which outcond to use + // The edges of the automaton all have the form in&out + // due to the unsplit + // however we need the edge to be deterministic in out too + // So we need determinism and we also want the resulting aiger + // to have as few gates as possible + std::vector used_outc = maxlow_outc(aut, all_inputs); + + // 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); + + unsigned num_outputs = output_names.size(); unsigned init = aut->get_init_state_number(); + assert(num_outputs == (unsigned) bdd_nodecount(all_outputs)); + aig circuit(input_names, output_names, log2n); - aig circuit(input_names, output_names, num_latches); - bdd b; - + // Register + // latches + for (unsigned i = 0; i < log2n; ++i) + circuit.register_new_lit(circuit.latch_var(i), bdd_ithvar(st0+i)); + // inputs + for (unsigned i = 0; i < all_inputs_vec.size(); ++i) + circuit.register_new_lit(circuit.input_var(i), all_inputs_vec[i]); // 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(); + std::vector out_vec(output_names.size()); + std::vector next_state_vec(log2n); + if (strcasecmp(mode, "ISOP") == 0) + { + std::vector> latch(log2n); + std::vector> out(num_outputs); + // Keep track of bdd that were already transformed into a gate + std::unordered_map incond_map; + std::vector prod_state(log2n); + for (unsigned s = 0; s < aut->num_states(); ++s) + { + unsigned src = encode_init_0(s, init); + prod_state.clear(); + unsigned src2 = src; + for (unsigned i = 0; i < log2n; ++i) + { + unsigned v = circuit.latch_var(i); + prod_state.push_back(src2 & 1 ? v : circuit.aig_not(v)); + src2 >>= 1; + } + assert(src2 <= 1); + unsigned state_var = circuit.aig_and(prod_state); + // Done state var + + for (auto &e: aut->out(s)) + { + unsigned e_idx = aut->edge_number(e); + // Same outcond for all ins + const bdd &letter_out = used_outc[e_idx]; + output_to_vec(out_vec, letter_out, bddvar_to_num); + + unsigned dst = encode_init_0(e.dst, init); + state_to_vec(next_state_vec, dst); + + // Get the isops over the input condition + // Each isop only contains variables from in + // -> directly compute the corresponding + // variable and and-gate + bdd incond = bdd_exist(e.cond, all_outputs); + auto incond_var_it = incond_map.find(incond); + if (incond_var_it == incond_map.end()) + // The incond and its isops have not yet been calculated + { + bool inserted; + unsigned var = circuit.bdd2DNFvar(incond, bddvar_to_num); + std::tie(incond_var_it, inserted) = + incond_map.insert(std::make_pair(incond, var)); + assert(inserted && incond_var_it->second == var); + } + + // AND with state + unsigned t = + circuit.aig_and(state_var, incond_var_it->second); + // Set in latches/outs having "high" + for (unsigned i = 0; i < log2n; ++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); + } // edge + } // state + + for (unsigned i = 0; i < log2n; ++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(); + } + else if (strcasecmp(mode, "ITE") == 0) + { + std::vector latch(log2n, bddfalse); + std::vector out(num_outputs, bddfalse); + bdd all_latches = bddtrue; + for (unsigned i = 0; i < log2n; ++i) + all_latches &= bdd_ithvar(st0 + i); + + for (unsigned s = 0; s < aut->num_states(); ++s) + { + // Convert state to bdd + unsigned src = encode_init_0(s, init); + bdd src_bdd = state_to_bdd(src, all_latches); + + for (const auto& e : aut->out(src)) + { + unsigned dst = encode_init_0(e.dst, init); + state_to_vec(next_state_vec, dst); + // edges have the form + // f(ins) & f(outs) + // one specific truth assignment has been selected above + // and stored in used_outc + output_to_vec(out_vec, used_outc[aut->edge_number(e)], + bddvar_to_num); + // The condition that joins in_cond and src + bdd tot_cond = src_bdd & bdd_exist(e.cond, all_outputs); + + // Add to existing cond + for (unsigned i = 0; i < log2n; ++i) + if (next_state_vec[i]) + latch[i] |= tot_cond; + for (unsigned i = 0; i < num_outputs; ++i) + if (out_vec[i]) + out[i] |= tot_cond; + } // e + } // src + // Create the vars + for (unsigned i = 0; i < num_outputs; ++i) + circuit.set_output(i, circuit.bdd2INFvar(out[i])); + for (unsigned i = 0; i < log2n; ++i) + circuit.set_latch(i, circuit.bdd2INFvar(latch[i])); + } + else + { + throw std::runtime_error + ("print_aiger(): mode must be \"ISOP\" or \"ITE\""); + } + return circuit; - } + } // aut_to_aiger_isop } std::ostream& - print_aiger(std::ostream& os, const const_twa_ptr& aut) + print_aiger(std::ostream& os, const const_twa_ptr& aut, const char* mode) { auto a = down_cast(aut); if (!a) @@ -425,7 +695,8 @@ namespace spot bdd* all_outputs = aut->get_named_prop("synthesis-outputs"); - aig circuit = aut_to_aiger(a, all_outputs ? *all_outputs : bdd(bddfalse)); + aig circuit = + aut_to_aiger(a, all_outputs ? *all_outputs : bdd(bddfalse), mode); circuit.print(os); return os; } diff --git a/spot/twaalgos/aiger.hh b/spot/twaalgos/aiger.hh index dcd0f5b2a..9c7270cbb 100644 --- a/spot/twaalgos/aiger.hh +++ b/spot/twaalgos/aiger.hh @@ -1,5 +1,5 @@ // -*- coding: utf-8 -*- -// Copyright (C) 2017 Laboratoire de Recherche et Développement +// Copyright (C) 2020 Laboratoire de Recherche et Développement // de l'Epita (LRDE). // // This file is part of Spot, a model checking library. @@ -39,8 +39,18 @@ namespace spot /// property is not set, all AP are encoded as inputs, and the circuit has no /// output. /// + /// \pre In order to ensure correctness, edge conditions have + /// to have the form (input cond) & (output cond). The output cond + /// does not need to be a minterm. + /// Correct graphs are generated by spot::unsplit_2step + /// + /// /// \param os The output stream to print on. /// \param aut The automaton to output. + /// \param mode Determines how the automaton is encoded. + /// "ISOP" Uses DNF. + /// "ITE" Uses the "if-then-else" normal-form SPOT_API std::ostream& - print_aiger(std::ostream& os, const const_twa_ptr& aut); + print_aiger(std::ostream& os, const const_twa_ptr& aut, + const char* mode); } diff --git a/tests/core/ltlsynt.test b/tests/core/ltlsynt.test index 663994c00..55a2751a3 100644 --- a/tests/core/ltlsynt.test +++ b/tests/core/ltlsynt.test @@ -47,42 +47,80 @@ diff out exp cat >exp < GFb' --aiger >out +ltlsynt --ins=a --outs=b -f 'GFa <-> GFb' --aiger=ISOP >out +diff out exp + +cat >exp < GFb' --aiger=ITE >out diff out exp cat >exp < (GFb & GFc)' --aiger >out +ltlsynt --ins=a --outs=b,c -f 'GFa <-> (GFb & GFc)' --aiger=Isop >out +diff out exp + +cat >exp < (GFb & GFc)' --aiger=ite >out diff out exp cat >exp <