source: vis_dev/vis-2.1/share/help/ltl_to_autCmd.txt @ 14

Last change on this file since 14 was 11, checked in by cecile, 13 years ago

Add vis
File size: 2.3 KB
Line 
1
2  ltl_to_aut - translate LTL formulae into Buechi automata
3     _________________________________________________________________
4
5   ltl_to_aut  [-f  <ltl_file>]  [-m  <algorithm>] [-o <output_file>] [-t
6   <output_format>]  [-w]  [-b] [-p] [-d] [-r] [-i] [-M] [-v <verbosity>]
7   [-h]
8
9   Translate  the given LTL formulae into Buechi automata, and output the
10   automaton into a file.
11
12   The   translation   algorithms  are  the  same  as  the  one  used  in
13   [1]ltl_model_check . However, more flexible combination of the options
14   can be used with this command.
15
16   The  automaton can be displayed on the screen and written into a file.
17   The format of the output can be dot, blifmv, verilog and smv.
18
19   Command options:
20
21   -f <ltl_file>
22          The input file containing LTL formulae.
23
24   -m <algorithm>
25          Specify  the  algorithm used in LTL formula -> Buechi automaton
26          translation algorithm.
27
28          algorithm must be one of the following:
29
30          0: GPVW.
31
32          1: GPVW+.
33
34          2: LTL2AUT.
35
36          3: WRING (default).
37
38   -o <output_file>
39          Write the automata into this file.
40
41   -t <output_format>
42          Specify the output format of the automata.
43
44          output_format must be one of the following:
45
46          0: dot.
47
48          1: blif_mv.
49
50          2: verilog.
51
52          3: all of the formats above (default).
53
54   -w
55          Rewriting the formula before translation.
56
57   -b
58          Boolean minimization during the translation.
59
60   -p
61          Pruning the fair states in the Buechi automaton.
62
63   -d
64          Direct-simulation minimization of the Buechi automaton.
65
66   -r
67          Reverse-simulation minimization of the Buechi automaton.
68
69   -i
70          Minimization based ont the I/O structural information.
71
72   -M
73          Maximize   (adding  arcs  to)  Buechi  automaton  using  Direct
74          Simulation.
75
76   -v <verbosity_level>
77          Specify  verbosity  level.  It  must  be  one of the following:
78          0,1,2,3.
79
80   -h
81          Print the command usage.
82     _________________________________________________________________
83
84   Last updated on 20050519 10h16
85
86References
87
88   1. file://localhost/projects/development/hsv/vis/common/doc/html/ltl_model_checkCmd.html
Note: See TracBrowser for help on using the repository browser.