From 7358a264923065a33b2b0a561936c9e088a8df84 Mon Sep 17 00:00:00 2001 From: Alexandre Duret-Lutz Date: Thu, 27 Jul 2023 14:28:15 +0200 Subject: [PATCH] improve coverage of LaTeX/utf8 printers for SERE * bin/common_output.cc, bin/common_output.hh, bin/randltl.cc: Adjust so that running "randltl -S" use the SERE flavor of the spot/latex/utf8 formula printers. * tests/core/latex.test, tests/core/utf8.test, tests/python/ltlparse.py: Add more test cases. --- NEWS | 2 ++ bin/common_output.cc | 16 +++++++++++++--- bin/common_output.hh | 1 + bin/randltl.cc | 1 + tests/core/latex.test | 7 ++++--- tests/core/utf8.test | 17 ++++++++++++++++- tests/python/ltlparse.py | 18 +++++++++++++++++- 7 files changed, 54 insertions(+), 8 deletions(-) diff --git a/NEWS b/NEWS index 220947d3a..58cbcb28c 100644 --- a/NEWS +++ b/NEWS @@ -38,6 +38,8 @@ New in spot 2.11.5.dev (not yet released) - Using --format=... on a tool that output formulas would force the output on standard output, even when --output was given. + - Using "randltl -S" did not correctly go through the SERE printer + functions. New in spot 2.11.5 (2023-04-20) diff --git a/bin/common_output.cc b/bin/common_output.cc index 16beca34d..13988688a 100644 --- a/bin/common_output.cc +++ b/bin/common_output.cc @@ -45,6 +45,7 @@ output_format_t output_format = spot_output; bool full_parenth = false; bool escape_csv = false; char output_terminator = '\n'; +bool output_ratexp = false; static const argp_option options[] = { @@ -105,7 +106,10 @@ stream_formula(std::ostream& out, report_not_ltl(f, filename, linenum, "LBT"); break; case spot_output: - spot::print_psl(out, f, full_parenth); + if (output_ratexp) + spot::print_sere(out, f, full_parenth); + else + spot::print_psl(out, f, full_parenth); break; case spin_output: if (f.is_ltl_formula()) @@ -120,10 +124,16 @@ stream_formula(std::ostream& out, report_not_ltl(f, filename, linenum, "Wring"); break; case utf8_output: - spot::print_utf8_psl(out, f, full_parenth); + if (output_ratexp) + spot::print_utf8_sere(out, f, full_parenth); + else + spot::print_utf8_psl(out, f, full_parenth); break; case latex_output: - spot::print_latex_psl(out, f, full_parenth); + if (output_ratexp) + spot::print_latex_sere(out, f, full_parenth); + else + spot::print_latex_psl(out, f, full_parenth); break; case count_output: case quiet_output: diff --git a/bin/common_output.hh b/bin/common_output.hh index 3b08db27f..30fe9e7d1 100644 --- a/bin/common_output.hh +++ b/bin/common_output.hh @@ -36,6 +36,7 @@ enum output_format_t { spot_output, spin_output, utf8_output, extern output_format_t output_format; extern bool full_parenth; extern bool escape_csv; +extern bool output_ratexp; #define COMMON_X_OUTPUT_SPECS(where) \ "number of atomic propositions " #where "; " \ diff --git a/bin/randltl.cc b/bin/randltl.cc index 4dacf5264..2a95def20 100644 --- a/bin/randltl.cc +++ b/bin/randltl.cc @@ -182,6 +182,7 @@ parse_opt(int key, char* arg, struct argp_state* as) break; case 'S': output = spot::randltlgenerator::SERE; + output_ratexp = true; break; case OPT_BOOLEAN_PRIORITIES: opt_pB = arg; diff --git a/tests/core/latex.test b/tests/core/latex.test index 6e94e14d6..bd27964c5 100755 --- a/tests/core/latex.test +++ b/tests/core/latex.test @@ -1,7 +1,7 @@ #!/bin/sh # -*- coding: utf-8 -*- -# Copyright (C) 2013, 2015 Laboratoire de Recherche et Développement -# de l'Epita (LRDE). +# Copyright (C) 2013, 2015, 2023 Laboratoire de Recherche et +# Développement de l'Epita (LRDE). # # This file is part of Spot, a model checking library. # @@ -50,7 +50,8 @@ cat <<\EOF EOF ( ltlfilt --latex input --format='\texttt{%F:%L} & $%f$ \\'; genltl --go-theta=1..3 --latex \ - --format='\texttt{--%F:%L} & $%f$ \\') + --format='\texttt{--%F:%L} & $%f$ \\'; + randltl -S -n10 --latex 2 --format='\texttt{random %l} & $%f$ \\') cat <<\EOF \end{tabular} \end{document} diff --git a/tests/core/utf8.test b/tests/core/utf8.test index 45ba950f5..b0bfef043 100755 --- a/tests/core/utf8.test +++ b/tests/core/utf8.test @@ -1,6 +1,6 @@ #! /bin/sh # -*- coding: utf-8 -*- -# Copyright (C) 2012, 2013, 2015, 2016, 2019 Laboratoire de Recherche et +# Copyright (C) 2012, 2013, 2015, 2016, 2019, 2023 Laboratoire de Recherche et # Développement de l'Epita (LRDE). # # This file is part of Spot, a model checking library. @@ -70,3 +70,18 @@ ltlfilt -8 -f 'X[!]a' >out diff in out ltlfilt -8 -F in >out diff in out + +randltl --sere -8 --seed 0 --tree-size 8 a b c -n 10 > formulae +cat >expected <3]') +tc.assertEqual(spot.str_sere(pf.f), 'a[->3]') +tc.assertEqual(spot.str_latex_sere(pf.f), 'a\\SereGoto{3}') +pf = spot.parse_infix_sere('(!b)[*];b;(!b)[*]') +tc.assertEqual(spot.str_sere(pf.f), 'b[=1]') +pf = spot.parse_infix_sere('b[=1]') +tc.assertEqual(spot.str_sere(pf.f), 'b[=1]') +tc.assertEqual(spot.str_latex_sere(pf.f), 'b\\SereEqual{1}') +tc.assertEqual(spot.str_sclatex_sere(pf.f), 'b^{=1}') +pf = spot.parse_infix_sere('(!b)[*];b') +tc.assertEqual(spot.str_sere(pf.f), 'b[->]') +pf = spot.parse_infix_sere('b[->1]') +tc.assertEqual(spot.str_latex_sere(pf.f), 'b\\SereGoto{}') +tc.assertEqual(spot.str_sclatex_sere(pf.f), 'b^{\\to}')