_ctlsp_test - test the CTL* parser


_ctlsp_test [-h] <file_name>

Test the CTL* parser. If the entire file of CTL* formulas is successfully parsed, then each formula is printed to stdout, followed by the equivalent existential normal form formula. The formulas read are not stored. For the input file containing:

 AG(foo=bar); 
the following is produced:
 original
  formula: AG(foo=bar) => equivalent existential formula: !(E(TRUE U
  !(foo=bar))) 
For the syntax of CTL formulas, refer to the VIS CTL and LTL syntax manual. Command options:

-h
Print the command usage.

Last updated on 20050519 00h50