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

declare all argp_program_doc as static

Browse source 
* bench/stutter/stutter_invariance_formulas.cc, bin/autcross.cc,
bin/autfilt.cc, bin/dstar2tgba.cc, bin/genaut.cc, bin/genltl.cc,
bin/ltl2tgba.cc, bin/ltl2tgta.cc, bin/ltlcross.cc, bin/ltldo.cc,
bin/ltlfilt.cc, bin/ltlsynt.cc, bin/randaut.cc, bin/randltl.cc,
bin/spot-x.cc, bin/spot.cc, tests/ltsmin/modelcheck.cc: Here.
This commit is contained in:
Alexandre Duret-Lutz 2022-10-25 16:31:35 +02:00
parent 65bc67f300
commit 0a710eb995
17 changed files with 34 additions and 32 deletions
Download patch file Download diff file Expand all files Collapse all files

6
bench/stutter/stutter_invariance_formulas.cc
View file

@ -1,6 +1,6 @@
// -*- coding: utf-8 -*-
// Copyright (C) 2014, 2015, 2016, 2017 Laboratoire de Recherche et
// Développement de l'Epita (LRDE).
// Copyright (C) 2014, 2015, 2016, 2017, 2022 Laboratoire de Recherche
// et Développement de l'Epita (LRDE).
//
// This file is part of Spot, a model checking library.
//
@ -28,7 +28,7 @@
#include <spot/misc/timer.hh>
#include <argp.h>
const char argp_program_doc[] ="";
static const char argp_program_doc[] = "";
const struct argp_child children[] =
{

6
bin/autcross.cc
View file

@ -1,6 +1,6 @@
// -*- coding: utf-8 -*-
// Copyright (C) 2017-2020, 2022 Laboratoire de Recherche et Développement de
// l'Epita (LRDE).
// Copyright (C) 2017-2020, 2022 Laboratoire de Recherche et
// Développement de l'Epita (LRDE).
//
// This file is part of Spot, a model checking library.
//
@ -51,7 +51,7 @@
#include <spot/misc/escape.hh>
#include <spot/misc/timer.hh>
const char argp_program_doc[] ="\
static const char argp_program_doc[] = "\
Call several tools that process automata and cross-compare their output \
to detect bugs, or to gather statistics. The list of automata to use \
should be supplied on standard input, or using the -F option.\v\

2
bin/autfilt.cc
View file

@ -75,7 +75,7 @@
#include <spot/twaalgos/sum.hh>
#include <spot/twaalgos/totgba.hh>
static const char argp_program_doc[] ="\
static const char argp_program_doc[] = "\
Convert, transform, and filter omega-automata.\v\
Exit status:\n\
0 if some automata were output\n\

2
bin/dstar2tgba.cc
View file

@ -48,7 +48,7 @@
#include <spot/parseaut/public.hh>
#include <spot/twaalgos/sccinfo.hh>
static const char argp_program_doc[] ="\
static const char argp_program_doc[] = "\
Convert automata with any acceptance condition into variants of \
Büchi automata.\n\nThis reads automata into any supported format \
(HOA, LBTT, ltl2dstar, never claim) and outputs a \

7
bin/genaut.cc
View file

@ -1,6 +1,6 @@
// -*- coding: utf-8 -*-
// Copyright (C) 2017-2019, 2022 Laboratoire de Recherche et Développement
// de l'Epita (LRDE).
// Copyright (C) 2017-2019, 2022 Laboratoire de Recherche et
// Développement de l'Epita (LRDE).
//
// This file is part of Spot, a model checking library.
//
@ -43,7 +43,8 @@
using namespace spot;
const char argp_program_doc[] ="Generate ω-automata from predefined patterns.";
static const char argp_program_doc[] =
"Generate ω-automata from predefined patterns.";
static const argp_option options[] =
{

2
bin/genltl.cc
View file

@ -45,7 +45,7 @@
using namespace spot;
const char argp_program_doc[] ="\
static const char argp_program_doc[] = "\
Generate temporal logic formulas from predefined patterns.";
// We reuse the values from gen::ltl_pattern_id as option keys.

2
bin/ltl2tgba.cc
View file

@ -39,7 +39,7 @@
#include <spot/misc/optionmap.hh>
#include <spot/misc/timer.hh>
static const char argp_program_doc[] ="\
static const char argp_program_doc[] = "\
Translate linear-time formulas (LTL/PSL) into various types of automata.\n\n\
By default it will apply all available optimizations to output \
the smallest Transition-based Generalized Büchi Automata, \

2
bin/ltl2tgta.cc
View file

@ -46,7 +46,7 @@
#include <spot/taalgos/minimize.hh>
#include <spot/misc/optionmap.hh>
const char argp_program_doc[] ="\
static const char argp_program_doc[] = "\
Translate linear-time formulas (LTL/PSL) into Testing Automata.\n\n\
By default it outputs a transition-based generalized Testing Automaton \
the smallest Transition-based Generalized Büchi Automata, \

6
bin/ltlcross.cc
View file

@ -1,6 +1,6 @@
// -*- coding: utf-8 -*-
// Copyright (C) 2012-2020, 2022 Laboratoire de Recherche et Développement
// de l'Epita (LRDE).
// Copyright (C) 2012-2020, 2022 Laboratoire de Recherche et
// Développement de l'Epita (LRDE).
//
// This file is part of Spot, a model checking library.
//
@ -69,7 +69,7 @@
#include <spot/misc/tmpfile.hh>
#include <spot/misc/timer.hh>
const char argp_program_doc[] ="\
static const char argp_program_doc[] = "\
Call several LTL/PSL translators and cross-compare their output to detect \
bugs, or to gather statistics. The list of formulas to use should be \
supplied on standard input, or using the -f or -F options.\v\

2
bin/ltldo.cc
View file

@ -47,7 +47,7 @@
#include <spot/twaalgos/totgba.hh>
#include <spot/parseaut/public.hh>
const char argp_program_doc[] ="\
static const char argp_program_doc[] = "\
Run LTL/PSL formulas through another program, performing conversion\n\
of input and output as required.";

2
bin/ltlfilt.cc
View file

@ -59,7 +59,7 @@
#include <spot/twaalgos/totgba.hh>
#include <spot/twaalgos/word.hh>
const char argp_program_doc[] ="\
static const char argp_program_doc[] = "\
Read a list of formulas and output them back after some optional processing.\v\
Exit status:\n\
0 if some formulas were output (skipped syntax errors do not count)\n\

2
bin/ltlsynt.cc
View file

@ -157,7 +157,7 @@ static const struct argp_child children[] =
{ nullptr, 0, nullptr, 0 }
};
const char argp_program_doc[] = "\
static const char argp_program_doc[] = "\
Synthesize a controller from its LTL specification.\v\
Exit status:\n\
0 if all input problems were realizable\n\

6
bin/randaut.cc
View file

@ -1,6 +1,6 @@
// -*- coding: utf-8 -*-
// Copyright (C) 2012-2016, 2018-2020 Laboratoire de Recherche et
// Développement de l'Epita (LRDE).
// Copyright (C) 2012-2016, 2018-2020, 2022 Laboratoire de Recherche
// et Développement de l'Epita (LRDE).
//
// This file is part of Spot, a model checking library.
//
@ -42,7 +42,7 @@
#include <spot/twaalgos/canonicalize.hh>
const char argp_program_doc[] = "\
static const char argp_program_doc[] = "\
Generate random connected automata.\n\n\
The automata are built over the atomic propositions named by PROPS...\n\
or, if N is a nonnegative number, using N arbitrary names.\n\

4
bin/randltl.cc
View file

@ -1,5 +1,5 @@
// -*- coding: utf-8 -*-
// Copyright (C) 2012-2016, 2018-2019 Laboratoire de Recherche
// Copyright (C) 2012-2016, 2018-2019, 2022 Laboratoire de Recherche
// et Développement de l'Epita (LRDE).
//
// This file is part of Spot, a model checking library.
@ -40,7 +40,7 @@
#include <spot/misc/random.hh>
#include <spot/misc/optionmap.hh>
const char argp_program_doc[] ="\
static const char argp_program_doc[] = "\
Generate random temporal logic formulas.\n\n\
The formulas are built over the atomic propositions named by PROPS...\n\
or, if N is a nonnegative number, using N arbitrary names.\v\

2
bin/spot-x.cc
View file

@ -24,7 +24,7 @@
#include <argp.h>
#include "common_setup.hh"
const char argp_program_doc[] ="\
static const char argp_program_doc[] = "\
Common fine-tuning options for programs installed with Spot.\n\
\n\
The argument of -x or --extra-options is a comma-separated list of KEY=INT \

7
bin/spot.cc
View file

@ -1,6 +1,6 @@
// -*- coding: utf-8 -*-
// Copyright (C) 2013-2018 Laboratoire de Recherche et Développement
// de l'Epita (LRDE).
// Copyright (C) 2013-2018, 2022 Laboratoire de Recherche et
// Développement de l'Epita (LRDE).
//
// This file is part of Spot, a model checking library.
//
@ -24,7 +24,8 @@
#include <argp.h>
#include "common_setup.hh"
const char argp_program_doc[] ="Command-line tools installed by Spot.";
static const char argp_program_doc[] =
"Command-line tools installed by Spot.";
#define DOC(NAME, TXT) NAME, 0, nullptr, OPTION_DOC | OPTION_NO_USAGE, TXT, 0

6
tests/ltsmin/modelcheck.cc
View file

@ -1,6 +1,6 @@
// -*- coding: utf-8 -*-
// Copyright (C) 2011-2020 Laboratoire de Recherche et Developpement
// de l'Epita (LRDE)
// Copyright (C) 2011-2020, 2022 Laboratoire de Recherche et
// Developpement de l'Epita (LRDE)
//
// This file is part of Spot, a model checking library.
//
@ -45,7 +45,7 @@
#include <spot/twacube/twacube.hh>
#include <spot/twacube_algos/convert.hh>
const char argp_program_doc[] =
static const char argp_program_doc[] =
"Process model and formula to check wether a "
"model meets a specification.\v\
Exit status:\n\