From 2c9f201c0d3a365b1c53b535987b457c84120200 Mon Sep 17 00:00:00 2001 From: Alexandre Duret-Lutz Date: Tue, 7 Mar 2017 13:36:49 +0100 Subject: [PATCH] twa_graph: fix set_univ_init_state() with initializer_list Reported by Thomas Medioni. * spot/twa/twagraph.hh (set_univ_init_state): Remove the bogus template parameter. * tests/core/twagraph.cc, tests/core/tgbagraph.test: Test the method. * NEWS: Mention the bug. --- NEWS | 3 +++ spot/twa/twagraph.hh | 1 - tests/core/tgbagraph.test | 20 ++++++++++++++++++-- tests/core/twagraph.cc | 22 ++++++++++++++++++++-- 4 files changed, 41 insertions(+), 5 deletions(-) diff --git a/NEWS b/NEWS index 0d9820355..6a4fc8736 100644 --- a/NEWS +++ b/NEWS @@ -35,6 +35,9 @@ New in spot 2.3.1.dev (not yet released) would always report 'weak' automata. Both variants now report the most precise between 'weak' or 'terminal'. + - spot::twa_graph::set_univ_init_state() could not be called with + an initializer list. + Deprecation notices: - Using --format=%a to print the number of atomic propositions in diff --git a/spot/twa/twagraph.hh b/spot/twa/twagraph.hh index 18732b7f0..24d4c8552 100644 --- a/spot/twa/twagraph.hh +++ b/spot/twa/twagraph.hh @@ -277,7 +277,6 @@ namespace spot init_number_ = g_.new_univ_dests(dst_begin, dst_end); } - template void set_univ_init_state(const std::initializer_list& il) { set_univ_init_state(il.begin(), il.end()); diff --git a/tests/core/tgbagraph.test b/tests/core/tgbagraph.test index 1b4afad69..37aa4e0f8 100755 --- a/tests/core/tgbagraph.test +++ b/tests/core/tgbagraph.test @@ -1,7 +1,7 @@ #!/bin/sh # -*- coding: utf-8 -*- -# Copyright (C) 2014, 2015, 2016 Laboratoire de Recherche et Développement -# de l'Epita (LRDE). +# Copyright (C) 2014-2017 Laboratoire de Recherche et Développement de +# l'Epita (LRDE). # # This file is part of Spot, a model checking library. # @@ -254,6 +254,22 @@ State: 1 State: 2 [t] 1 --END-- +HOA: v1.1 +States: 3 +Start: 2&0 +AP: 0 +acc-name: all +Acceptance: 0 t +properties: univ-branch trans-labels explicit-labels state-acc complete +properties: deterministic +--BODY-- +State: 0 +[t] 0 +State: 1 +[t] 0 +State: 2 +[t] 0&1 +--END-- EOF diff stdout expected diff --git a/tests/core/twagraph.cc b/tests/core/twagraph.cc index 5d066455a..c3cf98b20 100644 --- a/tests/core/twagraph.cc +++ b/tests/core/twagraph.cc @@ -1,6 +1,6 @@ // -*- coding: utf-8 -*- -// Copyright (C) 2014, 2015, 2016 Laboratoire de Recherche et Développement -// de l'Epita. +// Copyright (C) 2014-2017 Laboratoire de Recherche et Développement +// de l'Epita (LRDE). // // This file is part of Spot, a model checking library. // @@ -129,9 +129,27 @@ static void f3() spot::print_hoa(std::cout, tg, "1.1") << '\n'; } +// Test creation of universal edges via initializer-list +static void f4() +{ + auto d = spot::make_bdd_dict(); + auto tg = make_twa_graph(d); + + auto s1 = tg->new_state(); + auto s2 = tg->new_state(); + auto s3 = tg->new_state(); + tg->set_univ_init_state({s3, s1}); + tg->new_univ_edge(s3, {s1, s2}, bddtrue); + tg->new_univ_edge(s2, {s1}, bddtrue); + tg->new_edge(s1, s1, bddtrue); + + spot::print_hoa(std::cout, tg, "1.1") << '\n'; +} + int main() { f1(); f2(); f3(); + f4(); } -- GitLab