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

Trim DFAs used when translating PSL's closure operators.

This fixes a bug where {(a&!a)[=2]} was translated either into an
universal automaton (with simplification turned off) or in an
empty automaton (with simplification turned on).

* src/tgbaalgos/ltl2tgba_fm.cc (ratexp_to_dfa::translate): Trim
the automaton.
(ratexp_to_dfa::succ, ratexp_to_dfa::get_label): Deal with trimed
states.
(ltl_trad_visitor::visit(unop::Closure)): Likewise.
* src/tgbatest/ltl2tgba.test, src/ltltest/reduccmp.test: New test
cases.
parent d1530de1
......@@ -196,6 +196,12 @@ for x in ../reduccmp ../reductaustr; do
# Because reduccmp will translate the formula,
# this also check for an old bug in ltl2tgba_fm.
run 0 $x '{(c&!c)[->0..1]}!' '0'
# Tricky case that used to break the translator,
# because it was translating closer on-the-fly
# without pruning the rational automaton.
run 0 $x '{(c&!c)[=2]}' '0'
;;
esac
......
......@@ -37,6 +37,7 @@
#include <memory>
#include "ltl2tgba_fm.hh"
#include "tgba/bddprint.hh"
#include "tgbaalgos/scc.hh"
//#include "tgbaalgos/dotty.hh"
namespace spot
......@@ -891,11 +892,6 @@ namespace spot
const formula* now = *formulae_to_translate.begin();
formulae_to_translate.erase(formulae_to_translate.begin());
// Add it to the set of translated formulae.
// FIXME: That's incorrect: we need to (minimize&)trim the
// automaton first.
f2a_[now] = a;
// Translate it
bdd res = translate_ratexp(now, dict_);
......@@ -921,8 +917,68 @@ namespace spot
}
}
//dotty_reachable(std::cerr, a);
automata_.push_back(a);
return a;
// The following code trims the automaton in a crude way by
// eliminating SCCs that are not coaccessible. It does not
// actually remove the states, it simply marks the corresponding
// formulae as associated to the null pointer in the f2a_ map.
// The method succ() and get_label() interpret this as False.
scc_map* sm = new scc_map(a);
sm->build_map();
unsigned scc_count = sm->scc_count();
// Remember whether each SCC is coaccessible.
std::vector<bool> coaccessible(scc_count);
// SCC are numbered in topological order
for (unsigned n = 0; n < scc_count; ++n)
{
bool coacc = false;
const std::list<const state*>& st = sm->states_of(n);
// The SCC is coaccessible if any of its states
// is final (i.e., it accepts [*0])...
std::list<const state*>::const_iterator it;
for (it = st.begin(); it != st.end(); ++it)
if (a->get_label(*it)->accepts_eword())
{
coacc = true;
break;
}
if (!coacc)
{
// ... or if any of its successors is coaccessible.
const scc_map::succ_type& succ = sm->succ(n);
for (scc_map::succ_type::const_iterator i = succ.begin();
i != succ.end(); ++i)
if (coaccessible[i->first])
{
coacc = true;
break;
}
}
if (!coacc)
{
// Mark all formulas of this SCC as useless.
for (it = st.begin(); it != st.end(); ++it)
f2a_[a->get_label(*it)] = 0;
}
else
{
for (it = st.begin(); it != st.end(); ++it)
f2a_[a->get_label(*it)] = a;
}
coaccessible[n] = coacc;
}
delete sm;
if (coaccessible[scc_count - 1])
{
automata_.push_back(a);
return a;
}
else
{
delete a;
return 0;
}
}
tgba_succ_iterator*
......@@ -935,6 +991,10 @@ namespace spot
else
a = translate(f);
// If a is nul, f has an empty language.
if (!a)
return 0;
assert(a->has_state(f));
// This won't create a new state.
const state* s = a->add_state(f);
......@@ -948,7 +1008,15 @@ namespace spot
f2a_t::const_iterator it = f2a_.find(f);
assert(it != f2a_.end());
tgba_explicit_formula* a = it->second;
return a->get_label(s)->clone();
assert(a != 0);
const formula* f2 = a->get_label(s);
f2a_t::const_iterator it2 = f2a_.find(f2);
assert(it2 != f2a_.end());
if (it2->second == 0)
return constant::false_instance();
return f2->clone();
}
......@@ -1089,6 +1157,8 @@ namespace spot
tgba_succ_iterator* i = dict_.transdfa.succ(f);
res_ = bddfalse;
if (!i)
break;
for (i->first(); !i->done(); i->next())
{
bdd label = i->current_condition();
......
......@@ -99,6 +99,10 @@ check_psl '{[*]; {read[=3]} && {write[=2]}} |=>
check_psl '{[*]; start && comp_data_en; !comp_data_en && good_comp;
{status_valid[->]} && {stop[=0]; true}} |-> {!data_out}' # 2.33
# Some tricky cases that require the rational automaton to be pruned
# before it is used in the translation.
check_psl '{{b[*];c} | {{a && !a}}[=2]}'
check_psl '{((a&!b);((!a&!b)*))&&(!b*;(!a&b))}'
# Make sure 'a U (b U c)' has 3 states and 6 transitions,
# before and after degeneralization.
......
Supports Markdown
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