alarsyo/spot
1
0
Fork 0
Code Issues Pull requests Projects Releases Wiki Activity

twa_graph: fix set_univ_init_state() with initializer_list

Browse source 
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.
This commit is contained in:
Alexandre Duret-Lutz 2017-03-07 13:36:49 +01:00
parent 0621e0e9c5
commit 650bb7ed03
4 changed files with 41 additions and 5 deletions
Download patch file Download diff file Expand all files Collapse all files

3
NEWS
View file

@ -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

1
spot/twa/twagraph.hh
View file

@ -277,7 +277,6 @@ namespace spot
init_number_ = g_.new_univ_dests(dst_begin, dst_end);
}
template<class I>
void set_univ_init_state(const std::initializer_list<state_num>& il)
{
set_univ_init_state(il.begin(), il.end());

20
tests/core/tgbagraph.test
View file

@ -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

22
tests/core/twagraph.cc
View file

@ -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();
}