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

lbtt_parse: add support for state-based acceptance

* src/tgbaalgos/lbtt.cc (lbtt_read_gba): New function.
(lbtt_parse): Call lbtt_read_gba.
* src/tgbatest/lbttparse.test: Add a test.
parent 37b0809c
......@@ -227,6 +227,80 @@ namespace spot
return 0;
}
const tgba*
lbtt_read_gba(unsigned num_states, unsigned num_acc,
std::istream& is, std::string& error,
bdd_dict* dict,
ltl::environment& env, ltl::environment& envacc)
{
tgba_explicit_number* aut = new tgba_explicit_number(dict);
std::vector<const ltl::formula*> acc_f(num_acc);
for (unsigned n = 0; n < num_acc; ++n)
{
std::ostringstream s;
s << n;
const ltl::formula* af = acc_f[n] = envacc.require(s.str());
aut->declare_acceptance_condition(af->clone());
}
std::vector<bdd> acc_b(num_acc);
for (unsigned n = 0; n < num_acc; ++n)
acc_b[n] = aut->get_acceptance_condition(acc_f[n]);
for (unsigned n = 0; n < num_states; ++n)
{
int src_state = 0;
int initial = 0;
is >> src_state >> initial;
if (initial)
aut->set_init_state(src_state);
// Read the acceptance conditions.
bdd acc = bddfalse;
for (;;)
{
int acc_n = 0;
is >> acc_n;
if (acc_n == -1)
break;
if (acc_n < 0 || (unsigned)acc_n >= num_acc)
{
error += "invalid acceptance set";
goto fail;
}
acc |= acc_b[acc_n];
}
// Read the transitions.
for (;;)
{
int dst_state = 0;
is >> dst_state;
if (dst_state == -1)
break;
std::string guard;
std::getline(is, guard);
ltl::parse_error_list pel;
const ltl::formula* f = parse_lbt(guard, pel, env);
if (!f || pel.size() > 0)
{
error += "failed to parse guard: " + guard;
if (f)
f->destroy();
goto fail;
}
state_explicit_number::transition* t
= aut->create_transition(src_state, dst_state);
aut->add_condition(t, f);
t->acceptance_conditions |= acc;
}
}
return aut;
fail:
delete aut;
return 0;
}
const tgba*
lbtt_parse(std::istream& is, std::string& error, bdd_dict* dict,
ltl::environment& env, ltl::environment& envacc)
......@@ -257,7 +331,8 @@ namespace spot
return lbtt_read_tgba(num_states, num_acc, is, error, dict,
env, envacc);
else
assert(!"unsupported format");
return lbtt_read_gba(num_states, num_acc, is, error, dict,
env, envacc);
return 0;
}
}
......@@ -39,3 +39,29 @@ do
l=`expr $st \* 2 + $tr + 1`
test "$s" -eq "$l"
done
# This is the output of 'lbt' on the formula 'U p0 p1'.
cat >Up0p1 <<EOF
4 1
0 1 -1
1 p0
2 p1
-1
1 0 -1
1 p0
2 p1
-1
2 0 0 -1
3 t
-1
3 0 0 -1
3 t
-1
EOF
run 0 ../ltl2tgba -ks -XL Up0p1 > size
test "`cat size | sed -n 's/states: //p'`" = 4
test "`cat size | sed -n 's/transitions: //p'`" = 6
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