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

ltlsynt: add option --global-equivalence

Browse source 
Fixes issue #529.

* spot/tl/apcollect.hh,
spot/tl/apcollect.cc (collect_equivalent_literals): New function.
* python/spot/impl.i: Adjust.
* spot/tl/formula.hh,
spot/tl/formula.cc (formula_ptr_less_than_bool_first): New comparison
function.
* spot/twaalgos/aiger.hh, spot/twaalgos/aiger.cc: Adjust to deal
with equivalent assignments.
* bin/ltlsynt.cc: Implement the new option.
* tests/core/ltlsynt.test: Adjust test cases.
This commit is contained in:
Alexandre Duret-Lutz 2023-10-02 14:11:45 +02:00
parent c016f561fa
commit 9bf1edd80d
10 changed files with 515 additions and 70 deletions
Download patch file Download diff file Expand all files Collapse all files

152
spot/tl/apcollect.cc
View file

@ -21,9 +21,13 @@
// along with this program. If not, see <http://www.gnu.org/licenses/>.
#include "config.h"
#include <map>
#include <spot/tl/apcollect.hh>
#include <spot/twa/twa.hh>
#include <spot/twa/twagraph.hh>
#include <spot/twa/bdddict.hh>
#include <spot/twaalgos/hoa.hh>
#include <spot/twaalgos/sccinfo.hh>
namespace spot
{
@ -64,7 +68,7 @@ namespace spot
return res;
}
atomic_prop_set collect_litterals(formula f)
atomic_prop_set collect_literals(formula f)
{
atomic_prop_set res;
@ -131,4 +135,150 @@ namespace spot
return res;
}
std::vector<std::vector<spot::formula>>
collect_equivalent_literals(formula f)
{
std::map<spot::formula, unsigned> l2s;
// represent the implication graph as a twa_graph so we cab reuse
// scc_info. Literals can be converted to states using the l2s
// map.
twa_graph_ptr igraph = make_twa_graph(make_bdd_dict());
auto state_of = [&](formula a)
{
auto [it, b] = l2s.insert({a, 0});
if (b)
it->second = igraph->new_state();
return it->second;
};
auto implies = [&](formula a, formula b)
{
unsigned pos_a = state_of(a);
unsigned neg_a = state_of(formula::Not(a));
unsigned pos_b = state_of(b);
unsigned neg_b = state_of(formula::Not(b));
igraph->new_edge(pos_a, pos_b, bddtrue);
igraph->new_edge(neg_b, neg_a, bddtrue);
};
auto collect = [&](formula f, bool in_g, auto self)
{
switch (f.kind())
{
case op::ff:
case op::tt:
case op::eword:
case op::ap:
case op::UConcat:
case op::Not:
case op::NegClosure:
case op::NegClosureMarked:
case op::U:
case op::R:
case op::W:
case op::M:
case op::EConcat:
case op::EConcatMarked:
case op::X:
case op::F:
case op::Closure:
case op::OrRat:
case op::AndRat:
case op::AndNLM:
case op::Concat:
case op::Fusion:
case op::Star:
case op::FStar:
case op::first_match:
case op::strong_X:
return;
case op::Xor:
if (in_g && f[0].is_literal() && f[1].is_literal())
{
implies(f[0], formula::Not(f[1]));
implies(formula::Not(f[0]), f[1]);
}
return;
case op::Equiv:
if (in_g && f[0].is_literal() && f[1].is_literal())
{
implies(f[0], f[1]);
implies(formula::Not(f[0]), formula::Not(f[1]));
}
return;
case op::Implies:
if (in_g && f[0].is_literal() && f[1].is_literal())
implies(f[0], f[1]);
return;
case op::G:
self(f[0], true, self);
return;
case op::Or:
if (f.size() == 2 && f[0].is_literal() && f[1].is_literal())
implies(formula::Not(f[0]), f[1]);
return;
case op::And:
for (formula c: f)
self(c, in_g, self);
return;
}
};
collect(f, false, collect);
scc_info si(igraph, scc_info_options::PROCESS_UNREACHABLE_STATES);
// print_hoa(std::cerr, igraph);
// Build sets of equivalent literals.
unsigned nscc = si.scc_count();
std::vector<std::vector<spot::formula>> scc(nscc);
for (auto [f, i]: l2s)
scc[si.scc_of(i)].push_back(f);
// For each set, we will decide if we keep it or not.
std::vector<bool> keep(nscc, true);
for (unsigned i = 0; i < nscc; ++i)
{
if (keep[i] == false)
continue;
// We don't keep trivial SCCs
if (scc[i].size() <= 1)
{
keep[i] = false;
continue;
}
// Each SCC will appear twice. Because if {a,!b,c,!d,!e} are
// equivalent literals, then so are {!a,b,!c,d,e}. We will
// keep the SCC with the fewer negation if we can.
unsigned neg_count = 0;
for (formula f: scc[i])
{
SPOT_ASSUME(f != nullptr);
neg_count += f.is(op::Not);
}
if (neg_count > scc[i].size()/2)
{
keep[i] = false;
continue;
}
// We will keep the current SCC. Just
// mark the dual one for removal.
keep[si.scc_of(state_of(formula::Not(*scc[i].begin())))] = false;
}
// purge unwanted SCCs
unsigned j = 0;
for (unsigned i = 0; i < nscc; ++i)
{
if (keep[i] == false)
continue;
if (i > j)
scc[j] = std::move(scc[i]);
++j;
}
scc.resize(j);
return scc;
}
}

13
spot/tl/apcollect.hh
View file

@ -24,6 +24,7 @@
#include <spot/tl/formula.hh>
#include <set>
#include <vector>
#include <bddx.h>
#include <spot/twa/fwd.hh>
@ -60,14 +61,22 @@ namespace spot
atomic_prop_collect_as_bdd(formula f, const twa_ptr& a);
/// \brief Collect the litterals occuring in f
/// \brief Collect the literals occuring in f
///
/// This function records each atomic proposition occurring in f
/// along with the polarity of its occurrence. For instance if the
/// formula is `G(a -> b) & X(!b & c)`, then this will output `{!a,
/// b, !b, c}`.
SPOT_API
atomic_prop_set collect_litterals(formula f);
atomic_prop_set collect_literals(formula f);
/// \brief Collect equivalent APs
///
/// Looks for patterns like `...&G(...&(x->y)&...)&...` or
/// other forms of constant implications, then build a graph
/// of implications to compute equivalence classes of literals.
SPOT_API
std::vector<std::vector<spot::formula>>
collect_equivalent_literals(formula f);
/// @}
}

9
spot/tl/formula.cc
View file

@ -1,5 +1,5 @@
// -*- coding: utf-8 -*-
// Copyright (C) 2015-2019, 2021, 2022 Laboratoire de Recherche et
// Copyright (C) 2015-2019, 2021, 2022, 2023 Laboratoire de Recherche et
// Développement de l'Epita (LRDE).
//
// This file is part of Spot, a model checking library.
@ -2071,4 +2071,11 @@ namespace spot
{
return print_psl(os, f);
}
bool
formula_ptr_less_than_bool_first::operator()(const formula& left,
const formula& right) const
{
return operator()(left.ptr_, right.ptr_);
}
}

8
spot/tl/formula.hh
View file

@ -652,6 +652,8 @@ namespace spot
SPOT_API
int atomic_prop_cmp(const fnode* f, const fnode* g);
class SPOT_API formula;
struct formula_ptr_less_than_bool_first
{
bool
@ -718,7 +720,10 @@ namespace spot
right->dump(ord);
return old.str() < ord.str();
}
};
SPOT_API bool
operator()(const formula& left, const formula& right) const;
};
#endif // SWIG
@ -726,6 +731,7 @@ namespace spot
/// \brief Main class for temporal logic formula
class SPOT_API formula final
{
friend struct formula_ptr_less_than_bool_first;
const fnode* ptr_;
public:
/// \brief Create a formula from an fnode.

66
spot/twaalgos/aiger.cc
View file

@ -1986,6 +1986,21 @@ namespace
for (unsigned i = 0; i < n_outs; ++i)
circuit.set_output(i, bdd2var_min(out[i], out_dc[i]));
// Add the unused propositions
//
// RM contains assignments like
// out1 := 1
// out2 := 0
// out3 := in1
// out4 := !out3
// but it is possible that the rhs could refer to a variable
// that is not yet defined because of the ordering. For
// this reason, the first pass will store signals it could not
// complete in the POSTPONE vector.
//
// In that vector, (u,v,b) means that output u should be mapped to
// the same formula as output v, possibly negated (if b).
std::vector<std::tuple<int, int, bool>> postpone;
const unsigned n_outs_all = output_names_all.size();
for (unsigned i = n_outs; i < n_outs_all; ++i)
if (rm)
@ -2003,10 +2018,61 @@ namespace
circuit.set_output(i, circuit.aig_false());
continue;
}
else
{
formula repr = to->second;
bool neg_repr = false;
if (repr.is(op::Not))
{
neg_repr = true;
repr = repr[0];
}
// is repr an input?
if (auto it = std::find(input_names_all.begin(),
input_names_all.end(),
repr.ap_name());
it != input_names_all.end())
{
unsigned ivar =
circuit.input_var(it - input_names_all.begin(),
neg_repr);
circuit.set_output(i, ivar);
}
// is repr an output?
else if (auto it = std::find(output_names_all.begin(),
output_names_all.end(),
repr.ap_name());
it != output_names_all.end())
{
unsigned outnum = it - output_names_all.begin();
unsigned outvar = circuit.output(outnum);
if (outvar == -1u)
postpone.emplace_back(i, outnum, neg_repr);
else
circuit.set_output(i, outvar + neg_repr);
}
}
}
}
else
circuit.set_output(i, circuit.aig_false());
unsigned postponed = postpone.size();
while (postponed)
{
unsigned postponed_again = 0;
for (auto [u, v, b]: postpone)
{
unsigned outvar = circuit.output(v);
if (outvar == -1u)
++postponed_again;
else
circuit.set_output(u, outvar + b);
}
if (postponed_again >= postponed)
throw std::runtime_error("aiger encoding bug: "
"postponed output shunts not decreasing");
postponed = postponed_again;
}
for (unsigned i = 0; i < n_latches; ++i)
circuit.set_next_latch(i, bdd2var_min(latch[i], bddfalse));
return circuit_ptr;

9
spot/twaalgos/aiger.hh
View file

@ -174,6 +174,15 @@ namespace spot
[](unsigned o){return o == -1u; }));
return outputs_;
}
/// \brief return the variable associated to output \a num
///
/// This will be equal to -1U if aig::set_output() hasn't been called.
unsigned output(unsigned num) const
{
return outputs_[num];
}
/// \brief Get the set of output names
const std::vector<std::string>& output_names() const
{