Commit 52660108 authored by Alexandre Duret-Lutz's avatar Alexandre Duret-Lutz

gfguarantee: fix a typo in the code

* spot/twaalgos/gfguarantee.cc: Call is_terminal_automaton() on
the reduced automaton.
* tests/core/ltl2tgba.test: Add a test case.
parent 7a65bdf6
......@@ -99,7 +99,9 @@ namespace spot
for (auto& e: aut->out(init))
aut->new_edge(accstate, e.dst, e.cond, {0});
// This is not mandatory, but starting on the accepting
// state helps getting shorter accepting words.
// state helps getting shorter accepting words and may
// reader the original initial state unreachable, saving one
// state.
aut->set_init_state(accstate);
}
......@@ -137,7 +139,7 @@ namespace spot
twa_graph_ptr reduced = minimize_obligation(aut, f, nullptr,
!deterministic);
scc_info si(reduced);
if (!is_terminal_automaton(aut, &si, true))
if (!is_terminal_automaton(reduced, &si, true))
return nullptr;
do_g_f_terminal_inplace(si, state_based);
return reduced;
......@@ -148,7 +150,7 @@ namespace spot
bool deterministic, bool state_based)
{
twa_graph_ptr res = gf_guarantee_to_ba_maybe(gf, dict,
deterministic, state_based);
deterministic, state_based);
if (!res)
throw std::runtime_error
("gf_guarantee_to_ba(): expects a formula of the form GF(guarantee)");
......
#!/bin/sh
# -*- coding: utf-8 -*-
# Copyright (C) 2009-2017 Laboratoire de Recherche et Développement de
# Copyright (C) 2009-2018 Laboratoire de Recherche et Développement de
# l'Epita (LRDE).
# Copyright (C) 2003-2004 Laboratoire d'Informatique de Paris 6
# (LIP6), département Systèmes Répartis Coopératifs (SRC), Université
......@@ -278,3 +278,6 @@ test 4 = `ltl2tgba -f "$f" --low -x tls-impl=0 --stats=%s`
test 3 = `ltl2tgba -f "$f" --low -x tls-impl=1 --stats=%s`
test 2 = `ltl2tgba -f "$f" --low -x tls-impl=2 --stats=%s`
test 2 = `ltl2tgba -f "$f" --low -x tls-impl=3 --stats=%s`
# This is not optimal, the smallest DBA for this formula has 2 states.
test 3 = `ltl2tgba -BD -f 'GF((p0 & GF!p0) | (!p0 & FGp0))' --stats=%s`
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