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

dtgba_complement: take a tgba_digraph_ptr as input

Browse source 
* src/tgbaalgos/dtgbacomp.cc, src/tgbaalgos/dtgbacomp.hh: Here.
* src/tgbatest/ltl2tgba.cc: Adjust.
This commit is contained in:
Alexandre Duret-Lutz 2015-02-10 16:58:08 +01:00
parent afc8773de1
commit 5d31094029
3 changed files with 8 additions and 8 deletions
Download patch file Download diff file Expand all files Collapse all files

10
src/tgbaalgos/dtgbacomp.cc
View file

@ -1,6 +1,6 @@
// -*- coding: utf-8 -*- // -*- coding: utf-8 -*-
// Copyright (C) 2013, 2014 Laboratoire de Recherche et Développement // Copyright (C) 2013, 2014, 2015 Laboratoire de Recherche et
// de l'Epita. // Développement de l'Epita.
// //
// This file is part of Spot, a model checking library. // This file is part of Spot, a model checking library.
// //
@ -22,7 +22,7 @@
namespace spot namespace spot
{ {
tgba_digraph_ptr dtgba_complement_nonweak(const const_tgba_ptr& aut) tgba_digraph_ptr dtgba_complement_nonweak(const const_tgba_digraph_ptr& aut)
{ {
// Clone the original automaton. // Clone the original automaton.
auto res = make_tgba_digraph(aut, auto res = make_tgba_digraph(aut,
@ -110,7 +110,7 @@ namespace spot
return res; return res;
} }
tgba_digraph_ptr dtgba_complement_weak(const const_tgba_ptr& aut) tgba_digraph_ptr dtgba_complement_weak(const const_tgba_digraph_ptr& aut)
{ {
// Clone the original automaton. // Clone the original automaton.
auto res = make_tgba_digraph(aut, auto res = make_tgba_digraph(aut,
@ -158,7 +158,7 @@ namespace spot
return res; return res;
} }
tgba_digraph_ptr dtgba_complement(const const_tgba_ptr& aut) tgba_digraph_ptr dtgba_complement(const const_tgba_digraph_ptr& aut)
{ {
if (aut->is_inherently_weak()) if (aut->is_inherently_weak())
return dtgba_complement_weak(aut); return dtgba_complement_weak(aut);

4
src/tgbaalgos/dtgbacomp.hh
View file

@ -1,5 +1,5 @@
// -*- coding: utf-8 -*- // -*- coding: utf-8 -*-
// Copyright (C) 2013, 2014 Laboratoire de Recherche et Développement // Copyright (C) 2013, 2014, 2015 Laboratoire de Recherche et Développement
// de l'Epita. // de l'Epita.
// //
// This file is part of Spot, a model checking library. // This file is part of Spot, a model checking library.
@ -32,7 +32,7 @@ namespace spot
/// which case the output will also be weak and deterministic) the /// which case the output will also be weak and deterministic) the
/// resulting automaton is very unlikely to be deterministic. /// resulting automaton is very unlikely to be deterministic.
SPOT_API tgba_digraph_ptr SPOT_API tgba_digraph_ptr
dtgba_complement(const const_tgba_ptr& aut); dtgba_complement(const const_tgba_digraph_ptr& aut);
} }
#endif // SPOT_TGBAALGOS_DTGBACOMP_HH #endif // SPOT_TGBAALGOS_DTGBACOMP_HH

2
src/tgbatest/ltl2tgba.cc
View file

@ -1279,7 +1279,7 @@ checked_main(int argc, char** argv)
if (opt_dtgbacomp) if (opt_dtgbacomp)
{ {
tm.start("DTGBA complement"); tm.start("DTGBA complement");
a = dtgba_complement(a); a = dtgba_complement(ensure_digraph(a));
tm.stop("DTGBA complement"); tm.stop("DTGBA complement");
} }