diff --git a/src/tgbatest/ltl2tgba.cc b/src/tgbatest/ltl2tgba.cc index 44f229705..c7c74fa36 100644 --- a/src/tgbatest/ltl2tgba.cc +++ b/src/tgbatest/ltl2tgba.cc @@ -826,6 +826,7 @@ main(int argc, char** argv) delete dict; return 2; } + assume_sba = true; } e->merge_transitions(); } @@ -947,6 +948,7 @@ main(int argc, char** argv) tm.start("reducing A_f w/ SCC"); aut_scc = a = spot::scc_filter(a, scc_filter_all); tm.stop("reducing A_f w/ SCC"); + assume_sba = false; } const spot::tgba* degeneralized = 0; @@ -988,6 +990,7 @@ main(int argc, char** argv) temp_dir_sim = spot::simulation(a); a = temp_dir_sim; tm.stop("Reduction w/ direct simulation"); + assume_sba = false; } diff --git a/src/tgbatest/neverclaimread.test b/src/tgbatest/neverclaimread.test index d652c2a02..d33f1d997 100755 --- a/src/tgbatest/neverclaimread.test +++ b/src/tgbatest/neverclaimread.test @@ -1,6 +1,7 @@ #!/bin/sh -# Copyright (C) 2010, 2011 Laboratoire de Recherche et Développement -# de l'Epita (LRDE). +# -*- coding: utf-8 -*- +# Copyright (C) 2010, 2011, 2012 Laboratoire de Recherche et +# DĂ©veloppement de l'Epita (LRDE). # # This file is part of Spot, a model checking library. # @@ -55,7 +56,7 @@ digraph G { 2 -> 3 [label="p1 & !p0\n"] 2 -> 2 [label="!p1\n"] 2 -> 1 [label="!p1\n"] - 3 [label="accept_all"] + 3 [label="accept_all", peripheries=2] 3 -> 3 [label="1\n{Acc[1]}"] } EOF