Skip to content
GitLab
Projects
Groups
Snippets
Help
Loading...
Help
Help
Support
Community forum
Keyboard shortcuts
?
Submit feedback
Contribute to GitLab
Sign in / Register
Toggle navigation
Spot
Project overview
Project overview
Details
Activity
Releases
Repository
Repository
Files
Commits
Branches
Tags
Contributors
Graph
Compare
Issues
117
Issues
117
List
Boards
Labels
Service Desk
Milestones
Merge Requests
1
Merge Requests
1
CI / CD
CI / CD
Pipelines
Jobs
Schedules
Operations
Operations
Incidents
Environments
Analytics
Analytics
CI / CD
Repository
Value Stream
Wiki
Wiki
Members
Members
Collapse sidebar
Close sidebar
Activity
Graph
Create a new issue
Jobs
Commits
Issue Boards
Open sidebar
Spot
Spot
Commits
7615a57d
Commit
7615a57d
authored
Aug 20, 2015
by
Alexandre Duret-Lutz
Browse files
Options
Browse Files
Download
Email Patches
Plain Diff
dstar2tgba: rewrite using common_aoutput
Fixes
#8
. * src/bin/dstar2tgba.cc: Here.
parent
f831f729
Changes
1
Hide whitespace changes
Inline
Side-by-side
Showing
1 changed file
with
9 additions
and
247 deletions
+9
-247
src/bin/dstar2tgba.cc
src/bin/dstar2tgba.cc
+9
-247
No files found.
src/bin/dstar2tgba.cc
View file @
7615a57d
...
...
@@ -29,6 +29,7 @@
#include "common_setup.hh"
#include "common_finput.hh"
#include "common_cout.hh"
#include "common_aoutput.hh"
#include "common_post.hh"
#include "common_file.hh"
...
...
@@ -46,17 +47,13 @@
static
const
char
argp_program_doc
[]
=
"\
Convert Rabin and Streett automata into Büchi automata.
\n\n
\
This reads the output format of ltl2dstar and will output a
\n
\
This reads the output format of ltl2dstar and will output a
\n
\
Transition-based Generalized Büchi Automata in GraphViz's format by default.
\n
\
If multiple files are supplied (one automaton per file), several automata
\n
\
will be output."
;
enum
{
OPT_DOT
=
1
,
OPT_LBTT
,
OPT_NAME
,
OPT_STATS
,
OPT_TGBA
,
OPT_TGBA
=
1
,
};
static
const
argp_option
options
[]
=
...
...
@@ -73,71 +70,6 @@ static const argp_option options[] =
{
"monitor"
,
'M'
,
0
,
0
,
"Monitor (accepts all finite prefixes "
"of the given property)"
,
0
},
/**************************************************/
{
0
,
0
,
0
,
0
,
"Output format:"
,
3
},
{
"dot"
,
OPT_DOT
,
"1|a|b|B|c|e|f(FONT)|h|n|N|o|r|R|s|t|v"
,
OPTION_ARG_OPTIONAL
,
"GraphViz's format (default). Add letters for "
"(1) force numbered states, "
"(a) acceptance display, (b) acceptance sets as bullets, "
"(B) bullets except for Büchi/co-Büchi automata, "
"(c) force circular nodes, (e) force elliptic nodes, "
"(f(FONT)) use FONT, (h) horizontal layout, "
"(v) vertical layout, (n) with name, (N) without name, "
"(o) ordered transitions, "
"(r) rainbow colors for acceptance sets, "
"(R) color acceptance sets by Inf/Fin, (s) with SCCs, "
"(t) force transition-based acceptance."
,
0
},
{
"hoaf"
,
'H'
,
"i|s|t|m|l"
,
OPTION_ARG_OPTIONAL
,
"Output the automaton in HOA format. Add letters to select "
"(i) use implicit labels for complete deterministic automata, "
"(s) prefer state-based acceptance when possible [default], "
"(t) force transition-based acceptance, "
"(m) mix state and transition-based acceptance, "
"(l) single-line output"
,
0
},
{
"lbtt"
,
OPT_LBTT
,
"t"
,
OPTION_ARG_OPTIONAL
,
"LBTT's format (add =t to force transition-based acceptance even"
" on Büchi automata)"
,
0
},
{
"name"
,
OPT_NAME
,
"FORMAT"
,
0
,
"set the name of the output automaton"
,
0
},
{
"output"
,
'o'
,
"FORMAT"
,
0
,
"send output to a file named FORMAT instead of standard output. The"
" first automaton sent to a file truncates it unless FORMAT starts"
" with '>>'."
,
0
},
{
"spin"
,
's'
,
"6|c"
,
OPTION_ARG_OPTIONAL
,
"Spin neverclaim (implies --ba)."
" Add letters to select (6) Spin's 6.2.4 style, (c) comments on states"
,
0
},
{
"utf8"
,
'8'
,
0
,
0
,
"enable UTF-8 characters in output "
"(ignored with --lbtt or --spin)"
,
0
},
{
"stats"
,
OPT_STATS
,
"FORMAT"
,
0
,
"output statistics about the automaton"
,
0
},
/**************************************************/
{
0
,
0
,
0
,
0
,
"The FORMAT string passed to --stats may use "
\
"the following interpreted sequences (capitals for input,"
" minuscules for output):"
,
4
},
{
"%F"
,
0
,
0
,
OPTION_DOC
|
OPTION_NO_USAGE
,
"name of the input file"
,
0
},
{
"%S, %s"
,
0
,
0
,
OPTION_DOC
|
OPTION_NO_USAGE
,
"number of states"
,
0
},
{
"%E, %e"
,
0
,
0
,
OPTION_DOC
|
OPTION_NO_USAGE
,
"number of edges"
,
0
},
{
"%T, %t"
,
0
,
0
,
OPTION_DOC
|
OPTION_NO_USAGE
,
"number of transitions"
,
0
},
{
"%A, %a"
,
0
,
0
,
OPTION_DOC
|
OPTION_NO_USAGE
,
"number of acceptance pairs or sets"
,
0
},
{
"%C, %c"
,
0
,
0
,
OPTION_DOC
|
OPTION_NO_USAGE
,
"number of SCCs"
,
0
},
{
"%n"
,
0
,
0
,
OPTION_DOC
|
OPTION_NO_USAGE
,
"number of nondeterministic states in output"
,
0
},
{
"%d"
,
0
,
0
,
OPTION_DOC
|
OPTION_NO_USAGE
,
"1 if the output is deterministic, 0 otherwise"
,
0
},
{
"%p"
,
0
,
0
,
OPTION_DOC
|
OPTION_NO_USAGE
,
"1 if the output is complete, 0 otherwise"
,
0
},
{
"%r"
,
0
,
0
,
OPTION_DOC
|
OPTION_NO_USAGE
,
"conversion time (including post-processings, but not parsing)"
" in seconds"
,
0
},
{
"%%"
,
0
,
0
,
OPTION_DOC
|
OPTION_NO_USAGE
,
"a single %"
,
0
},
/**************************************************/
{
0
,
0
,
0
,
0
,
"Miscellaneous options:"
,
-
1
},
{
"extra-options"
,
'x'
,
"OPTS"
,
0
,
"fine-tuning options (see spot-x (7))"
,
0
},
...
...
@@ -146,20 +78,13 @@ static const argp_option options[] =
static
const
struct
argp_child
children
[]
=
{
{
&
aoutput_argp
,
0
,
0
,
0
},
{
&
aoutput_io_format_argp
,
0
,
0
,
4
},
{
&
post_argp
,
0
,
0
,
20
},
{
&
misc_argp
,
0
,
0
,
-
1
},
{
0
,
0
,
0
,
0
}
};
enum
output_format
{
Dot
,
Lbtt
,
Spin
,
Stats
,
Hoa
};
static
output_format
format
=
Dot
;
static
const
char
*
opt_dot
=
nullptr
;
static
const
char
*
stats
=
""
;
static
const
char
*
hoa_opt
=
nullptr
;
static
const
char
*
opt_never
=
nullptr
;
static
const
char
*
opt_lbtt
=
nullptr
;
static
const
char
*
opt_name
=
nullptr
;
static
const
char
*
opt_output
=
nullptr
;
static
spot
::
option_map
extra_options
;
static
int
...
...
@@ -168,32 +93,15 @@ parse_opt(int key, char* arg, struct argp_state*)
// This switch is alphabetically-ordered.
switch
(
key
)
{
case
'8'
:
spot
::
enable_utf8
();
break
;
case
'B'
:
type
=
spot
::
postprocessor
::
BA
;
break
;
case
'F'
:
jobs
.
emplace_back
(
arg
,
true
);
break
;
case
'H'
:
format
=
Hoa
;
hoa_opt
=
arg
;
break
;
case
'M'
:
type
=
spot
::
postprocessor
::
Monitor
;
break
;
case
'o'
:
opt_output
=
arg
;
break
;
case
's'
:
format
=
Spin
;
if
(
type
!=
spot
::
postprocessor
::
Monitor
)
type
=
spot
::
postprocessor
::
BA
;
if
(
arg
)
opt_never
=
arg
;
break
;
case
'x'
:
{
const
char
*
opt
=
extra_options
.
parse_options
(
arg
);
...
...
@@ -201,34 +109,14 @@ parse_opt(int key, char* arg, struct argp_state*)
error
(
2
,
0
,
"failed to parse --options near '%s'"
,
opt
);
}
break
;
case
OPT_DOT
:
format
=
Dot
;
opt_dot
=
arg
;
break
;
case
OPT_LBTT
:
format
=
Lbtt
;
opt_lbtt
=
arg
;
if
(
arg
&&
(
arg
[
0
]
!=
't'
||
arg
[
1
]
!=
0
))
error
(
2
,
0
,
"unknown argument for --lbtt: '%s'"
,
arg
);
break
;
case
OPT_NAME
:
opt_name
=
arg
;
break
;
case
OPT_STATS
:
if
(
!*
arg
)
error
(
2
,
0
,
"empty format string for --stats"
);
stats
=
arg
;
format
=
Stats
;
break
;
case
OPT_TGBA
:
if
(
format
==
Spin
)
if
(
automaton_
format
==
Spin
)
error
(
2
,
0
,
"--spin and --tgba are incompatible"
);
type
=
spot
::
postprocessor
::
TGBA
;
break
;
case
ARGP_KEY_ARG
:
jobs
.
emplace_back
(
arg
,
true
);
break
;
default:
return
ARGP_ERR_UNKNOWN
;
}
...
...
@@ -238,102 +126,14 @@ parse_opt(int key, char* arg, struct argp_state*)
namespace
{
/// \brief prints various statistics about a TGBA
///
/// This object can be configured to display various statistics
/// about a TGBA. Some %-sequence of characters are interpreted in
/// the format string, and replaced by the corresponding statistics.
class
dstar_stat_printer
:
protected
spot
::
stat_printer
{
public:
dstar_stat_printer
(
std
::
ostream
&
os
,
const
char
*
format
)
:
spot
::
stat_printer
(
os
,
format
)
{
declare
(
'A'
,
&
daut_acc_
);
declare
(
'C'
,
&
daut_scc_
);
declare
(
'E'
,
&
daut_edges_
);
declare
(
'F'
,
&
filename_
);
declare
(
'f'
,
&
filename_
);
// Override the formula printer.
declare
(
'S'
,
&
daut_states_
);
declare
(
'T'
,
&
daut_trans_
);
declare
(
'm'
,
&
aut_name_
);
}
using
spot
::
formater
::
set_output
;
/// \brief print the configured statistics.
///
/// The \a f argument is not needed if the Formula does not need
/// to be output.
std
::
ostream
&
print
(
const
spot
::
const_parsed_aut_ptr
&
daut
,
const
spot
::
const_twa_graph_ptr
&
aut
,
const
char
*
filename
,
double
run_time
)
{
filename_
=
filename
;
if
(
has
(
'T'
))
{
spot
::
tgba_sub_statistics
s
=
sub_stats_reachable
(
daut
->
aut
);
daut_states_
=
s
.
states
;
daut_edges_
=
s
.
transitions
;
daut_trans_
=
s
.
sub_transitions
;
}
else
if
(
has
(
'E'
))
{
spot
::
tgba_sub_statistics
s
=
sub_stats_reachable
(
daut
->
aut
);
daut_states_
=
s
.
states
;
daut_edges_
=
s
.
transitions
;
}
else
if
(
has
(
'S'
))
{
daut_states_
=
daut
->
aut
->
num_states
();
}
if
(
has
(
'A'
))
daut_acc_
=
daut
->
aut
->
num_sets
()
/
2
;
if
(
has
(
'C'
))
daut_scc_
=
spot
::
scc_info
(
daut
->
aut
).
scc_count
();
if
(
has
(
'm'
))
{
auto
n
=
aut
->
get_named_prop
<
std
::
string
>
(
"automaton-name"
);
if
(
n
)
aut_name_
=
*
n
;
else
aut_name_
.
val
().
clear
();
}
return
this
->
spot
::
stat_printer
::
print
(
aut
,
0
,
run_time
);
}
private:
spot
::
printable_value
<
const
char
*>
filename_
;
spot
::
printable_value
<
unsigned
>
daut_states_
;
spot
::
printable_value
<
unsigned
>
daut_edges_
;
spot
::
printable_value
<
unsigned
>
daut_trans_
;
spot
::
printable_value
<
unsigned
>
daut_acc_
;
spot
::
printable_value
<
unsigned
>
daut_scc_
;
spot
::
printable_value
<
std
::
string
>
aut_name_
;
};
class
dstar_processor
:
public
job_processor
{
public:
spot
::
postprocessor
&
post
;
dstar_stat_printer
statistics
;
std
::
ostringstream
name
;
dstar_stat_printer
namer
;
std
::
ostringstream
outputname
;
dstar_stat_printer
outputnamer
;
std
::
map
<
std
::
string
,
std
::
unique_ptr
<
output_file
>>
outputfiles
;
automaton_printer
printer
;
dstar_processor
(
spot
::
postprocessor
&
post
)
:
post
(
post
),
statistics
(
std
::
cout
,
stats
),
namer
(
name
,
opt_name
),
outputnamer
(
outputname
,
opt_output
)
:
post
(
post
),
printer
(
aut_input
)
{
}
...
...
@@ -360,45 +160,7 @@ namespace
auto
aut
=
post
.
run
(
nba
,
0
);
const
double
conversion_time
=
sw
.
stop
();
// Name the output automaton.
if
(
opt_name
)
{
name
.
str
(
""
);
namer
.
print
(
daut
,
aut
,
filename
,
conversion_time
);
aut
->
set_named_prop
(
"automaton-name"
,
new
std
::
string
(
name
.
str
()));
}
std
::
ostream
*
out
=
&
std
::
cout
;
if
(
opt_output
)
{
outputname
.
str
(
""
);
outputnamer
.
print
(
daut
,
aut
,
filename
,
conversion_time
);
std
::
string
fname
=
outputname
.
str
();
auto
p
=
outputfiles
.
emplace
(
fname
,
nullptr
);
if
(
p
.
second
)
p
.
first
->
second
.
reset
(
new
output_file
(
fname
.
c_str
()));
out
=
&
p
.
first
->
second
->
ostream
();
}
switch
(
format
)
{
case
Dot
:
spot
::
print_dot
(
*
out
,
aut
,
opt_dot
);
break
;
case
Lbtt
:
spot
::
print_lbtt
(
*
out
,
aut
,
opt_lbtt
);
break
;
case
Hoa
:
spot
::
print_hoa
(
*
out
,
aut
,
hoa_opt
)
<<
'\n'
;
break
;
case
Spin
:
spot
::
print_never_claim
(
*
out
,
aut
,
opt_never
);
break
;
case
Stats
:
statistics
.
set_output
(
*
out
);
statistics
.
print
(
daut
,
aut
,
filename
,
conversion_time
)
<<
'\n'
;
break
;
}
printer
.
print
(
aut
,
nullptr
,
filename
,
-
1
,
conversion_time
,
daut
);
flush_cout
();
return
0
;
}
...
...
Write
Preview
Markdown
is supported
0%
Try again
or
attach a new file
.
Attach a file
Cancel
You are about to add
0
people
to the discussion. Proceed with caution.
Finish editing this message first!
Cancel
Please
register
or
sign in
to comment