Commit acdaaac4 authored by Alexandre Duret-Lutz's avatar Alexandre Duret-Lutz
Browse files

bin: release all subformulas between runs

Fixes #262, reported by Maximilien Colange.

* bin/common_output.cc, bin/common_aoutput.cc, bin/common_aoutput.hh:
Clear the set of atomic propositions if --stats=%[...]x was used.
* spot/twa/bdddict.cc: Release any formula associated to a BDD when it
is unregistered, do not wait for the dictionary's destruction.  This
was the main culprit for #262.
* tests/core/ltl2tgba.test: Add test cases.
* NEWS: Mention the bug.
parent cdef3d69
......@@ -85,6 +85,12 @@ New in spot 2.3.4.dev (not yet released)
names from another automaton, honoring "original-states" if
present.
Bugs fixed:
- We have fixed new cases where translating multiple formula in a
single ltl2tgba run could produce automata different from those
produced by individual runs.
Backward-incompatible changes:
- spot::acc_cond::mark_t::operator bool() has been marked as
......
......@@ -518,6 +518,8 @@ hoa_stat_printer::print(const spot::const_parsed_aut_ptr& haut,
output_aut_ = nullptr;
input_aut_ = nullptr;
haut_scc_.reset();
aut_ap_.clear();
haut_ap_.clear();
return res;
}
......
......@@ -121,11 +121,15 @@ protected:
});
}
public:
void clear()
{
val_.clear();
}
template<class T>
void set(T begin, T end)
{
val_.clear();
clear();
val_.insert(val_.end(), begin, end);
sort();
}
......
......@@ -239,7 +239,13 @@ namespace
size_ = spot::length(f);
if (has('h'))
class_ = spot::mp_class(f);
return format(format_);
auto& res = format(format_);
// Make sure we do not store the formula until the next one is
// printed, as the order in which APs are registered may
// influence the automata output.
fl_ = nullptr;
ap_.clear();
return res;
}
private:
......
......@@ -235,7 +235,6 @@ namespace spot
// ME was the last user of this variable.
// Let's free it. First, we need to find
// if this is a Var or an Acc variable.
int n = 1;
formula f = nullptr;
switch (bdd_map[v].type)
{
......@@ -249,21 +248,19 @@ namespace spot
break;
case anon:
{
bdd_dict_priv::free_anonymous_list_of_type::iterator i;
// Nobody use this variable as an anonymous variable
// anymore, so remove it entirely from the anonymous
// free list so it can be used for something else.
for (i = priv_->free_anonymous_list_of.begin();
i != priv_->free_anonymous_list_of.end(); ++i)
i->second.remove(v, n);
for (auto& fal: priv_->free_anonymous_list_of)
fal.second.remove(v, 1);
break;
}
}
// Actually release the associated BDD variables, and the
// formula itself.
priv_->release_variables(v, n);
while (n--)
bdd_map[v + n].type = anon;
priv_->release_variables(v, 1);
bdd_map[v].type = anon;
bdd_map[v].f = nullptr;
}
void
......@@ -326,7 +323,6 @@ namespace spot
bdd_dict::assert_emptiness() const
{
bool fail = false;
bool var_seen = false;
bool acc_seen = false;
bool refs_seen = false;
......
......@@ -238,3 +238,20 @@ genltl --go-theta=18 | ltl2tgba --low --any -q
(ltl2tgba Fb ; ltl2tgba 'GFa & GFb') >out1
ltl2tgba Fb 'GFa & GFb' >out2
diff out1 out2
# Because atomic proposition were not released by bdd_dict, different
# order of transitions could be observed in automata output after a
# previous translation by the same process. (issue #262).
ltl2tgba --low --any 'Xp1 xor (Fp1 M (!p1 M (Fp0 W p1)))' \
'Fp0 -> XXG(1 U Gp1)' > res1
ltl2tgba --low --any 'Xp1 xor (Fp1 M (!p1 M (Fp0 W p1)))' >res2
ltl2tgba --low --any 'Fp0 -> XXG(1 U Gp1)' >>res2
diff res1 res2
# The same should work when printing SCCs or atomic propositions
s='--stats=%c,%[,]x'
ltl2tgba --low --any 'Xp1 xor (Fp1 M (!p1 M (Fp0 W p1)))' \
'Fp0 -> XXG(1 U Gp1)' "$s" >res1
ltl2tgba --low --any 'Xp1 xor (Fp1 M (!p1 M (Fp0 W p1)))' "$s" >res2
ltl2tgba --low --any 'Fp0 -> XXG(1 U Gp1)' "$s" >>res2
diff res1 res2
Markdown is supported
0% or .
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment