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

improve coverage of LaTeX/utf8 printers for SERE

Browse source 
* 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.
This commit is contained in:
Alexandre Duret-Lutz 2023-07-27 14:28:15 +02:00
parent 15857385a5
commit 44d9e34e32
7 changed files with 54 additions and 8 deletions
Download patch file Download diff file Expand all files Collapse all files

2
NEWS
View file

@ -11,6 +11,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)

16
bin/common_output.cc
View file

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

1
bin/common_output.hh
View file

@ -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 "; " \

1
bin/randltl.cc
View file

@ -180,6 +180,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;

7
tests/core/latex.test
View file

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

17
tests/core/utf8.test
View file

@ -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 <<EOF
0
b:{1 | [*0]}[:*1..3]
c̅
a | [*0]
b[*2..3]
1
{a∨b}[*][:*]
b
a
[*0]
EOF
diff formulae expected

18
tests/python/ltlparse.py
View file

@ -1,5 +1,5 @@
# -*- mode: python; coding: utf-8 -*-
# Copyright (C) 2009-2012, 2014-2017, 2019, 2021-2022 Laboratoire de
# Copyright (C) 2009-2012, 2014-2017, 2019, 2021-2023 Laboratoire de
# Recherche et Développement de l'Epita (LRDE).
# Copyright (C) 2003, 2004 Laboratoire d'Informatique de Paris 6 (LIP6),
# département Systèmes Répartis Coopératifs (SRC), Université Pierre
@ -219,3 +219,19 @@ f = spot.formula_G(2, spot.formula_unbounded(), spot.formula_ap("a"))
tc.assertEqual(f, spot.formula("XXG(a)"))
f = spot.formula_F(2, spot.formula_unbounded(), spot.formula_ap("a"))
tc.assertEqual(f, spot.formula("XXF(a)"))
pf = spot.parse_infix_sere('a[->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}')