Line | |
---|
1 | |
---|
2 | _ctlsp_test - test the CTL* parser |
---|
3 | _________________________________________________________________ |
---|
4 | |
---|
5 | _ctlsp_test [-h] <file_name> |
---|
6 | |
---|
7 | Test the CTL* parser. If the entire file of CTL* formulas is |
---|
8 | successfully parsed, then each formula is printed to stdout, followed |
---|
9 | by the equivalent existential normal form formula. The formulas read |
---|
10 | are not stored. For the input file containing: |
---|
11 | AG(foo=bar); |
---|
12 | |
---|
13 | the following is produced: |
---|
14 | original |
---|
15 | formula: AG(foo=bar) => equivalent existential formula: !(E(TRUE U |
---|
16 | !(foo=bar))) |
---|
17 | |
---|
18 | For the syntax of CTL formulas, refer to [1]the VIS CTL and LTL syntax |
---|
19 | manual. Command options: |
---|
20 | |
---|
21 | -h |
---|
22 | Print the command usage. |
---|
23 | _________________________________________________________________ |
---|
24 | |
---|
25 | Last updated on 20050519 10h16 |
---|
26 | |
---|
27 | References |
---|
28 | |
---|
29 | 1. file://localhost/projects/development/hsv/vis/common/doc/ctl/ctl/ctl.html |
---|
Note: See
TracBrowser
for help on using the repository browser.