| 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 successfully |
|---|
| 8 | parsed, then each formula is printed to stdout, followed by the equivalent |
|---|
| 9 | existential normal form formula. The formulas read are not stored. For the |
|---|
| 10 | 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 20100410 00h02 |
|---|
| 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.