game: reimplement print_aiger
* spot/twaalgos/aiger.cc, spot/twaalgos/aiger.hh: Reimplement print_aiger for speed gain, also heuristics to minimize the number of gates as well as different encoding types have been added. * bin/ltlsynt.cc: Make the new options for print-aiger available. * tests/core/ltlsynt.test: Adjust tests.
This commit is contained in:
philipp
Alexandre Duret-Lutz
parent
f5965966e9
commit
0d43bedacb
5 changed files with 562 additions and 214 deletions
5
NEWS
5
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
|
||||
|
|
|
|||
|
|
@ -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;
|
||||
|
|
|
|||
|
|
@ -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 <spot/twaalgos/aiger.hh>
|
||||
|
||||
#include <cmath>
|
||||
#include <deque>
|
||||
#include <map>
|
||||
#include <unordered_map>
|
||||
#include <vector>
|
||||
#include <algorithm>
|
||||
#include <cstring>
|
||||
|
||||
#include <spot/twa/twagraph.hh>
|
||||
#include <spot/misc/bddlt.hh>
|
||||
|
|
@ -47,13 +47,16 @@ namespace spot
|
|||
class aig
|
||||
{
|
||||
private:
|
||||
unsigned num_inputs_;
|
||||
unsigned max_var_;
|
||||
std::map<unsigned, std::pair<unsigned, unsigned>> and_gates_;
|
||||
unsigned num_inputs_;
|
||||
unsigned num_latches_;
|
||||
unsigned num_outputs_;
|
||||
|
||||
std::vector<unsigned> latches_;
|
||||
std::vector<unsigned> outputs_;
|
||||
std::vector<std::string> input_names_;
|
||||
std::vector<std::string> output_names_;
|
||||
std::vector<std::pair<unsigned, unsigned>> and_gates_;
|
||||
// Cache the function computed by each variable as a bdd.
|
||||
std::unordered_map<unsigned, bdd> var2bdd_;
|
||||
std::unordered_map<bdd, unsigned, bdd_hash> bdd2var_;
|
||||
|
|
@ -62,8 +65,10 @@ namespace spot
|
|||
aig(const std::vector<std::string>& inputs,
|
||||
const std::vector<std::string>& 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<unsigned>(vs.begin(), vs.begin() + m));
|
||||
unsigned right =
|
||||
aig_and(std::vector<unsigned>(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<unsigned> todo;
|
||||
std::vector<bool> used(max_var_ / 2 + 1, false);
|
||||
std::vector<unsigned> todo;
|
||||
std::vector<bool> 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<unsigned, unsigned>&
|
||||
bddvar_to_num)
|
||||
{
|
||||
std::vector<unsigned> plus_vars;
|
||||
std::vector<unsigned> 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<and_gates_.size(); ++i)
|
||||
if ((and_gates_[i].first != 0) && (and_gates_[i].second != 0))
|
||||
write_gate(gate_var(i), and_gates_[i].first, and_gates_[i].second);
|
||||
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<bool>
|
||||
state_to_vec(unsigned s, unsigned size)
|
||||
static void
|
||||
state_to_vec(std::vector<bool>& v, unsigned s)
|
||||
{
|
||||
std::vector<bool> 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<bool>
|
||||
output_to_vec(bdd b,
|
||||
const std::unordered_map<unsigned, unsigned>& bddvar_to_outputnum)
|
||||
static void
|
||||
output_to_vec(std::vector<bool>& v, bdd b,
|
||||
const std::unordered_map<unsigned, unsigned>&
|
||||
bddvar_to_outputnum)
|
||||
{
|
||||
std::vector<bool> 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<bdd> maxlow_outc(const const_twa_graph_ptr& aut,
|
||||
const bdd& all_inputs)
|
||||
{
|
||||
std::vector<bdd> 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_high<n_high)
|
||||
{
|
||||
n_high = next_high;
|
||||
used_outc[idx] = nextsat;
|
||||
}
|
||||
}
|
||||
assert(used_outc[idx] != bddfalse);
|
||||
}
|
||||
//Done
|
||||
return used_outc;
|
||||
}
|
||||
|
||||
// Transforms an automaton into an AIGER circuit
|
||||
// using irreducible sums-of-products
|
||||
static aig
|
||||
aut_to_aiger(const const_twa_graph_ptr& aut, const bdd& all_outputs)
|
||||
aut_to_aiger(const const_twa_graph_ptr& aut, const bdd& all_outputs,
|
||||
const char* mode)
|
||||
{
|
||||
// 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);
|
||||
|
||||
// get the propositions
|
||||
std::vector<std::string> input_names;
|
||||
std::vector<std::string> output_names;
|
||||
bdd all_inputs = bddtrue;
|
||||
std::unordered_map<unsigned, unsigned> bddvar_to_inputnum;
|
||||
std::unordered_map<unsigned, unsigned> bddvar_to_outputnum;
|
||||
std::vector<bdd> all_inputs_vec;
|
||||
std::unordered_map<unsigned, unsigned> 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<bdd> 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<std::vector<unsigned>> latch(num_latches);
|
||||
std::vector<std::vector<unsigned>> 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<unsigned> 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<bool> out_vec(output_names.size());
|
||||
std::vector<bool> next_state_vec(log2n);
|
||||
if (strcasecmp(mode, "ISOP") == 0)
|
||||
{
|
||||
std::vector<std::vector<unsigned>> latch(log2n);
|
||||
std::vector<std::vector<unsigned>> out(num_outputs);
|
||||
// Keep track of bdd that were already transformed into a gate
|
||||
std::unordered_map<bdd, unsigned, bdd_hash> incond_map;
|
||||
std::vector<unsigned> 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<bdd> latch(log2n, bddfalse);
|
||||
std::vector<bdd> 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<const_twa_graph_ptr>(aut);
|
||||
if (!a)
|
||||
|
|
@ -425,7 +695,8 @@ namespace spot
|
|||
|
||||
bdd* all_outputs = aut->get_named_prop<bdd>("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;
|
||||
}
|
||||
|
|
|
|||
|
|
@ -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);
|
||||
}
|
||||
|
|
|
|||
|
|
@ -47,42 +47,80 @@ diff out exp
|
|||
|
||||
cat >exp <<EOF
|
||||
REALIZABLE
|
||||
aag 30 1 3 1 26
|
||||
aag 31 1 3 1 26
|
||||
2
|
||||
4 47
|
||||
4 49
|
||||
6 57
|
||||
8 59
|
||||
61
|
||||
10 3 5
|
||||
12 7 9
|
||||
14 10 12
|
||||
16 2 5
|
||||
18 16 12
|
||||
20 3 4
|
||||
22 20 12
|
||||
24 2 4
|
||||
26 24 12
|
||||
28 6 9
|
||||
30 16 28
|
||||
32 10 28
|
||||
34 24 28
|
||||
36 20 28
|
||||
63
|
||||
10 7 9
|
||||
12 5 10
|
||||
14 12 3
|
||||
16 12 2
|
||||
18 4 10
|
||||
20 18 3
|
||||
22 18 2
|
||||
24 6 9
|
||||
26 5 24
|
||||
30 26 3
|
||||
32 4 24
|
||||
34 32 2
|
||||
36 32 3
|
||||
38 7 8
|
||||
40 16 38
|
||||
42 10 38
|
||||
44 23 33
|
||||
46 15 44
|
||||
48 27 31
|
||||
50 19 48
|
||||
52 35 41
|
||||
54 33 52
|
||||
56 50 54
|
||||
58 37 43
|
||||
60 48 54
|
||||
40 5 38
|
||||
42 40 2
|
||||
44 40 3
|
||||
46 21 31
|
||||
48 15 46
|
||||
50 17 23
|
||||
52 35 43
|
||||
54 50 52
|
||||
56 27 54
|
||||
58 37 45
|
||||
60 27 52
|
||||
62 23 60
|
||||
i0 a
|
||||
o0 b
|
||||
EOF
|
||||
ltlsynt --ins=a --outs=b -f 'GFa <-> GFb' --aiger >out
|
||||
ltlsynt --ins=a --outs=b -f 'GFa <-> GFb' --aiger=ISOP >out
|
||||
diff out exp
|
||||
|
||||
cat >exp <<EOF
|
||||
REALIZABLE
|
||||
aag 28 1 3 1 24
|
||||
2
|
||||
4 38
|
||||
6 49
|
||||
8 56
|
||||
29
|
||||
10 6 9
|
||||
12 5 10
|
||||
14 7 8
|
||||
16 15 11
|
||||
18 4 9
|
||||
20 5 17
|
||||
22 21 19
|
||||
24 2 23
|
||||
26 3 12
|
||||
28 27 25
|
||||
30 7 9
|
||||
32 4 30
|
||||
34 5 9
|
||||
36 35 33
|
||||
38 3 37
|
||||
40 6 11
|
||||
42 5 41
|
||||
44 43 19
|
||||
46 2 45
|
||||
48 27 47
|
||||
50 4 10
|
||||
52 5 14
|
||||
54 53 51
|
||||
56 3 55
|
||||
i0 a
|
||||
o0 b
|
||||
EOF
|
||||
ltlsynt --ins=a --outs=b -f 'GFa <-> GFb' --aiger=ITE >out
|
||||
diff out exp
|
||||
|
||||
cat >exp <<EOF
|
||||
|
|
@ -94,14 +132,14 @@ aag 16 1 2 2 13
|
|||
31
|
||||
31
|
||||
8 5 7
|
||||
10 3 8
|
||||
12 2 8
|
||||
10 8 3
|
||||
12 8 2
|
||||
14 4 7
|
||||
16 3 14
|
||||
18 2 14
|
||||
16 14 3
|
||||
18 14 2
|
||||
20 5 6
|
||||
22 2 20
|
||||
24 3 20
|
||||
22 20 2
|
||||
24 20 3
|
||||
26 17 25
|
||||
28 11 26
|
||||
30 19 23
|
||||
|
|
@ -110,7 +148,29 @@ i0 a
|
|||
o0 b
|
||||
o1 c
|
||||
EOF
|
||||
ltlsynt --ins=a --outs=b,c -f 'GFa <-> (GFb & GFc)' --aiger >out
|
||||
ltlsynt --ins=a --outs=b,c -f 'GFa <-> (GFb & GFc)' --aiger=Isop >out
|
||||
diff out exp
|
||||
|
||||
cat >exp <<EOF
|
||||
REALIZABLE
|
||||
aag 10 1 2 2 7
|
||||
2
|
||||
4 18
|
||||
6 20
|
||||
14
|
||||
14
|
||||
8 4 7
|
||||
10 5 6
|
||||
12 11 9
|
||||
14 2 13
|
||||
16 4 9
|
||||
18 3 17
|
||||
20 2 17
|
||||
i0 a
|
||||
o0 b
|
||||
o1 c
|
||||
EOF
|
||||
ltlsynt --ins=a --outs=b,c -f 'GFa <-> (GFb & GFc)' --aiger=ite >out
|
||||
diff out exp
|
||||
|
||||
cat >exp <<EOF
|
||||
|
|
|
|||
Loading…
Add table
Add a link
Reference in a new issue