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

ltl2tgba: Set assume_sba for automata read from a neverclaim.

Browse source 
This cause double-circles for accepting states in dot output.

* src/tgbatest/ltl2tgba.cc: Set assume_sba for automata read from
neverclaims.  Reset assume_sba after scc_filter and simulation.
* src/tgbatest/neverclaimread.test: Expect a double circle.
This commit is contained in:
Alexandre Duret-Lutz 2012-05-19 22:58:55 +02:00
parent e5a86290cf
commit cb068599dc
2 changed files with 7 additions and 3 deletions
Download patch file Download diff file Expand all files Collapse all files

3
src/tgbatest/ltl2tgba.cc
View file

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

7
src/tgbatest/neverclaimread.test
View file

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