From b4963a7a6ce1d83207d84f603f8296dc30b555e1 Mon Sep 17 00:00:00 2001 From: Alexandre Duret-Lutz Date: Wed, 11 Oct 2017 14:35:23 +0200 Subject: [PATCH] genaut: fix ks_nca * spot/gen/automata.cc (ks_nca): The output is complete. * tests/core/genaut.test: Add test. * NEWS: Mention the bug. --- NEWS | 5 +++++ spot/gen/automata.cc | 2 +- tests/core/genaut.test | 2 ++ 3 files changed, 8 insertions(+), 1 deletion(-) diff --git a/NEWS b/NEWS index a7871fc65..c6b1e22eb 100644 --- a/NEWS +++ b/NEWS @@ -122,6 +122,11 @@ New in spot 2.4.1.dev (not yet released) spot::scc_info::marks(), spot::scc_info::marks_of() and spot::scc_info::acc_sets_of() respectively. + Bugs fixed: + + - Automata produced by "genaut --ks-nca=N" were incorrectly marked + as not complete. + New in spot 2.4.1 (2017-10-05) Bugs fixed: diff --git a/spot/gen/automata.cc b/spot/gen/automata.cc index f543d4682..e634d4e8a 100644 --- a/spot/gen/automata.cc +++ b/spot/gen/automata.cc @@ -87,7 +87,7 @@ namespace spot aut->merge_edges(); aut->prop_state_acc(true); aut->prop_universal(false); - aut->prop_complete(false); + aut->prop_complete(true); aut->prop_inherently_weak(false); aut->prop_stutter_invariant(false); aut->prop_semi_deterministic(false); diff --git a/tests/core/genaut.test b/tests/core/genaut.test index ec93c0b42..cddbe0c3f 100644 --- a/tests/core/genaut.test +++ b/tests/core/genaut.test @@ -43,6 +43,8 @@ cat >expected <err && exit 1 grep positive err genaut --l-nba=0 2>err && exit 1