1 // -*- coding: utf-8 -*-
2 // Copyright (C) 2017-2019 Laboratoire de Recherche et Développement
3 // de l'Epita (LRDE).
4 //
5 // This file is part of Spot, a model checking library.
6 //
7 // Spot is free software; you can redistribute it and/or modify it
8 // under the terms of the GNU General Public License as published by
9 // the Free Software Foundation; either version 3 of the License, or
10 // (at your option) any later version.
11 //
12 // Spot is distributed in the hope that it will be useful, but WITHOUT
13 // ANY WARRANTY; without even the implied warranty of MERCHANTABILITY
14 // or FITNESS FOR A PARTICULAR PURPOSE. See the GNU General Public
15 // License for more details.
16 //
17 // You should have received a copy of the GNU General Public License
18 // along with this program. If not, see <http://www.gnu.org/licenses/>.
19
20 #include "common_sys.hh"
21
22 #include <iostream>
23 #include <fstream>
24 #include <argp.h>
25 #include <cstdlib>
26 #include "error.h"
27 #include <vector>
28
29 #include "common_setup.hh"
30 #include "common_aoutput.hh"
31 #include "common_range.hh"
32 #include "common_cout.hh"
33
34 #include <cassert>
35 #include <iostream>
36 #include <sstream>
37 #include <set>
38 #include <string>
39 #include <cmath>
40 #include <cstdlib>
41 #include <cstring>
42 #include <spot/gen/automata.hh>
43
44 using namespace spot;
45
46 const char argp_program_doc[] ="Generate ω-automata from predefined patterns.";
47
48 static const argp_option options[] =
49 {
50 /**************************************************/
51 // Keep this alphabetically sorted (expect for aliases).
52 { nullptr, 0, nullptr, 0, "Pattern selection:", 1},
53 { "ks-nca", gen::AUT_KS_NCA, "RANGE", 0,
54 "A co-Büchi automaton with 2N+1 states for which any equivalent "
55 "deterministic co-Büchi automaton has at least 2^N/(2N+1) states.", 0},
56 { "l-nba", gen::AUT_L_NBA, "RANGE", 0,
57 "A Büchi automaton with 3N+1 states whose complementary Streett "
58 "automaton needs at least N! states.", 0},
59 { "l-dsa", gen::AUT_L_DSA, "RANGE", 0,
60 "A deterministic Streett automaton with 4N states with no "
61 "equivalent deterministic Rabin automaton of less than N! states.", 0},
62 { "m-nba", gen::AUT_M_NBA, "RANGE", 0,
63 "An NBA with N+1 states whose determinization needs at least "
64 "N! states", 0},
65 RANGE_DOC,
66 /**************************************************/
67 { nullptr, 0, nullptr, 0, "Miscellaneous options:", -1 },
68 { nullptr, 0, nullptr, 0, nullptr, 0 }
69 };
70
71 struct job
72 {
73 gen::aut_pattern_id pattern;
74 struct range range;
75 };
76
77 typedef std::vector<job> jobs_t;
78 static jobs_t jobs;
79
80 const struct argp_child children[] =
81 {
82 { &aoutput_argp, 0, nullptr, 3 },
83 { &aoutput_o_format_argp, 0, nullptr, 4 },
84 { &misc_argp, 0, nullptr, -1 },
85 { nullptr, 0, nullptr, 0 }
86 };
87
88 static void
enqueue_job(int pattern,const char * range_str)89 enqueue_job(int pattern, const char* range_str)
90 {
91 job j;
92 j.pattern = static_cast<gen::aut_pattern_id>(pattern);
93 j.range = parse_range(range_str);
94 jobs.push_back(j);
95 }
96
97 static int
parse_opt(int key,char * arg,struct argp_state *)98 parse_opt(int key, char* arg, struct argp_state*)
99 {
100 // Called from C code, so should not raise any exception.
101 BEGIN_EXCEPTION_PROTECT;
102 if (key >= gen::AUT_BEGIN && key < gen::AUT_END)
103 {
104 enqueue_job(key, arg);
105 return 0;
106 }
107 END_EXCEPTION_PROTECT;
108 return ARGP_ERR_UNKNOWN;
109 }
110
111 static void
output_pattern(gen::aut_pattern_id pattern,int n)112 output_pattern(gen::aut_pattern_id pattern, int n)
113 {
114 process_timer timer;
115 timer.start();
116 twa_graph_ptr aut = spot::gen::aut_pattern(pattern, n);
117 timer.stop();
118 automaton_printer printer;
119 printer.print(aut, timer, nullptr, aut_pattern_name(pattern), n);
120 }
121
122 static void
run_jobs()123 run_jobs()
124 {
125 for (auto& j: jobs)
126 {
127 int inc = (j.range.max < j.range.min) ? -1 : 1;
128 int n = j.range.min;
129 for (;;)
130 {
131 output_pattern(j.pattern, n);
132 if (n == j.range.max)
133 break;
134 n += inc;
135 }
136 }
137 }
138
139
140 int
main(int argc,char ** argv)141 main(int argc, char** argv)
142 {
143 return protected_main(argv, [&] {
144 strcpy(F_doc, "the name of the pattern");
145 strcpy(L_doc, "the argument of the pattern");
146
147 const argp ap = { options, parse_opt, nullptr, argp_program_doc,
148 children, nullptr, nullptr };
149
150 if (int err = argp_parse(&ap, argc, argv, ARGP_NO_HELP, nullptr, nullptr))
151 exit(err);
152
153 if (jobs.empty())
154 error(1, 0, "Nothing to do. Try '%s --help' for more information.",
155 program_name);
156
157 run_jobs();
158 flush_cout();
159 return 0;
160 });
161 }
162