diff --git a/ChangeLog b/ChangeLog index 5fe2a7322..959125bd0 100644 --- a/ChangeLog +++ b/ChangeLog @@ -1,3 +1,12 @@ +2009-10-16 Alexandre Duret-Lutz + + Escape labels in -KV output. + + * src/tgbaalgos/scc.cc (dump_scc_dot): Escape labels and other + strings output between quote in dot. + * src/tgbatest/kv.test: New file. + * src/tgbatest/Makefile.am (TESTS): Add it. + 2009-10-16 Alexandre Duret-Lutz * src/tgbaalgos/ltl2tgba_fm.cc: Typos. diff --git a/src/tgbaalgos/scc.cc b/src/tgbaalgos/scc.cc index ffd37a0d2..048525ffa 100644 --- a/src/tgbaalgos/scc.cc +++ b/src/tgbaalgos/scc.cc @@ -24,6 +24,7 @@ #include #include "scc.hh" #include "tgba/bddprint.hh" +#include "misc/escape.hh" namespace spot { @@ -455,22 +456,24 @@ namespace spot if (n > 1) ostr << "s"; ostr << ")\\naccs="; - bdd_print_accset(ostr, m.get_aut()->get_dict(), - m.acc_set_of(state)); + escape_str(ostr, bdd_format_accset(m.get_aut()->get_dict(), + m.acc_set_of(state))); ostr << "\\nconds=["; for (scc_map::cond_set::const_iterator i = cs.begin(); i != cs.end(); ++i) { if (i != cs.begin()) ostr << ", "; - bdd_print_formula(ostr, m.get_aut()->get_dict(), *i); + escape_str(ostr, + bdd_format_formula(m.get_aut()->get_dict(), *i)); } ostr << "]\\n AP=["; - bdd_print_sat(ostr, m.get_aut()->get_dict(), - m.ap_set_of(state)); + escape_str(ostr, + bdd_format_sat(m.get_aut()->get_dict(), + m.ap_set_of(state))); ostr << "]\\n APrec=["; - bdd_print_sat(ostr, m.get_aut()->get_dict(), - m.aprec_set_of(state)) << "]"; + escape_str(ostr, bdd_format_sat(m.get_aut()->get_dict(), + m.aprec_set_of(state))) << "]"; } std::cout << " " << state << " [shape=box," @@ -487,7 +490,7 @@ namespace spot out << " " << state << " -> " << dest << " [label=\""; - bdd_print_formula(out, m.get_aut()->get_dict(), label); + escape_str(out, bdd_format_formula(m.get_aut()->get_dict(), label)); out << "\"]" << std::endl; if (seen[dest]) diff --git a/src/tgbatest/Makefile.am b/src/tgbatest/Makefile.am index 9f3ad5cb2..735c75df3 100644 --- a/src/tgbatest/Makefile.am +++ b/src/tgbatest/Makefile.am @@ -86,6 +86,7 @@ TESTS = \ tripprod.test \ mixprod.test \ dupexp.test \ + kv.test \ reduccmp.test \ reductgba.test \ scc.test \ diff --git a/src/tgbatest/kv.test b/src/tgbatest/kv.test new file mode 100755 index 000000000..1cee58cdf --- /dev/null +++ b/src/tgbatest/kv.test @@ -0,0 +1,41 @@ +#!/bin/sh +# Copyright (C) 2009 Laboratoire de Recherche et Development de l'EPITA. +# +# This file is part of Spot, a model checking library. +# +# Spot is free software; you can redistribute it and/or modify it +# under the terms of the GNU General Public License as published by +# the Free Software Foundation; either version 2 of the License, or +# (at your option) any later version. +# +# Spot is distributed in the hope that it will be useful, but WITHOUT +# ANY WARRANTY; without even the implied warranty of MERCHANTABILITY +# or FITNESS FOR A PARTICULAR PURPOSE. See the GNU General Public +# License for more details. +# +# You should have received a copy of the GNU General Public License +# along with Spot; see the file COPYING. If not, write to the Free +# Software Foundation, Inc., 59 Temple Place - Suite 330, Boston, MA +# 02111-1307, USA. + + +. ./defs + +set -e + +check () +{ + run 0 ../ltl2tgba -f -KV "$1" > out.dot + run 0 $DOT out.dot > /dev/null + rm -f out.dot +} + +# We don't check the output, but running these might be +# enough to trigger assertions in the code, or raise valgrind concerns. + +check 'a R (b R c)' +check '(a U b) U (c U d)' +check '((Xp2)U(X(1)))*(p1 R(p2 R p0))' + +# Make sure escaped variables print OK. +check '"G1"U"GG" && "FF"'