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

ltlsynt: do a fixpoint around the polarity simplifications

Browse source 
* bin/ltlsynt.cc: Here.
* tests/core/ltlsynt.test: Adjust.
This commit is contained in:
Alexandre Duret-Lutz 2023-09-26 17:10:05 +02:00
parent 6dc11b4715
commit 70812046d2
2 changed files with 62 additions and 61 deletions
Download patch file Download diff file Expand all files Collapse all files

92
bin/ltlsynt.cc
View file

@ -408,46 +408,62 @@ namespace
// or always in negative form. // or always in negative form.
// In syntcomp, this occurs more frequently for input variables than // In syntcomp, this occurs more frequently for input variables than
// output variable. See issue #529 for some examples. // output variable. See issue #529 for some examples.
spot::relabeling_map rm; spot::relabeling_map rm;
bool first_dap = true;
auto display_ap = [&rm, &first_dap](spot::formula p)
{
if (SPOT_LIKELY(!gi->verbose_stream))
return;
if (first_dap)
{
*gi->verbose_stream << ("the following APs are polarized, "
"they can be replaced by constants:\n");
first_dap = false;
}
*gi->verbose_stream << " " << p << " := " << rm[p] <<'\n';
};
spot::formula oldf;
if (opt_polarity) if (opt_polarity)
{ do
std::set<spot::formula> lits = spot::collect_litterals(f); {
for (const std::string& ap: output_aps) bool rm_has_new_terms = false;
{ std::set<spot::formula> lits = spot::collect_litterals(f);
spot::formula pos = spot::formula::ap(ap); for (const std::string& ap: output_aps)
spot::formula neg = spot::formula::Not(pos); {
bool has_pos = lits.find(pos) != lits.end(); spot::formula pos = spot::formula::ap(ap);
bool has_neg = lits.find(neg) != lits.end(); spot::formula neg = spot::formula::Not(pos);
if (has_pos && !has_neg) bool has_pos = lits.find(pos) != lits.end();
rm[pos] = spot::formula::tt(); bool has_neg = lits.find(neg) != lits.end();
else if (has_neg && !has_pos) if (has_pos ^ has_neg)
rm[pos] = spot::formula::ff(); {
} rm[pos] = has_pos ? spot::formula::tt() : spot::formula::ff();
for (const std::string& ap: input_aps) rm_has_new_terms = true;
{ display_ap(pos);
spot::formula pos = spot::formula::ap(ap); }
spot::formula neg = spot::formula::Not(pos); }
bool has_pos = lits.find(pos) != lits.end(); for (const std::string& ap: input_aps)
bool has_neg = lits.find(neg) != lits.end(); {
if (has_pos && !has_neg) spot::formula pos = spot::formula::ap(ap);
rm[pos] = spot::formula::ff(); spot::formula neg = spot::formula::Not(pos);
else if (has_neg && !has_pos) bool has_pos = lits.find(pos) != lits.end();
rm[pos] = spot::formula::tt(); bool has_neg = lits.find(neg) != lits.end();
} if (has_pos ^ has_neg)
if (!rm.empty()) {
{ rm[pos] = has_neg ? spot::formula::tt() : spot::formula::ff();
if (gi->verbose_stream) rm_has_new_terms = true;
{ display_ap(pos);
*gi->verbose_stream << ("the following APs are polarized, " }
"they can be replaced by constants:\n"); }
for (auto [k, v]: rm) oldf = f;
*gi->verbose_stream << " " << k << " := " << v <<'\n'; if (rm_has_new_terms)
} {
f = spot::relabel_apply(f, &rm); f = spot::relabel_apply(f, &rm);
if (gi->verbose_stream) if (gi->verbose_stream)
*gi->verbose_stream << "new formula: " << f << '\n'; *gi->verbose_stream << "new formula: " << f << '\n';
} }
} }
while (oldf != f);
std::vector<spot::formula> sub_form; std::vector<spot::formula> sub_form;
std::vector<std::set<spot::formula>> sub_outs; std::vector<std::set<spot::formula>> sub_outs;

31
tests/core/ltlsynt.test
View file

@ -764,31 +764,16 @@ diff outx exp
cat >exp <<EOF cat >exp <<EOF
the following APs are polarized, they can be replaced by constants: the following APs are polarized, they can be replaced by constants:
a := 1
b := 1 b := 1
a := 1
new formula: x & y new formula: x & y
there are 2 subformulas x := 1
trying to create strategy directly for x y := 1
direct strategy might exist but was not found. new formula: 1
translating formula done in X seconds there are 1 subformulas
automaton has 2 states and 1 colors trying to create strategy directly for 1
LAR construction done in X seconds direct strategy was found.
DPA has 2 states, 0 colors direct strat has 1 states, 1 edges and 0 colors
split inputs and outputs done in X seconds
automaton has 4 states
solving game with acceptance: all
game solved in X seconds
simplification took X seconds
trying to create strategy directly for y
direct strategy might exist but was not found.
translating formula done in X seconds
automaton has 2 states and 1 colors
LAR construction done in X seconds
DPA has 2 states, 0 colors
split inputs and outputs done in X seconds
automaton has 4 states
solving game with acceptance: all
game solved in X seconds
simplification took X seconds simplification took X seconds
AIG circuit was created in X seconds and has 0 latches and 0 gates AIG circuit was created in X seconds and has 0 latches and 0 gates
EOF EOF