source: vis_dev/vis-2.3/share/help/ltl_to_autCmd.txt @ 41

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

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