source: vis_dev/vis-2.3/src/ctlsp/ctlspCmd.c @ 64

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

vis2.3

File size: 12.3 KB
Line 
1/**CFile***********************************************************************
2
3  FileName    [ctlspCmd.c]
4
5  PackageName [ctlsp]
6
7  Synopsis    [Command to read in a file containing CTL* formulas.]
8
9  Author      [Mohammad Awedh]
10
11  Copyright   [This file was created at the University of Colorado at Boulder.
12  The University of Colorado at Boulder makes no warranty about the suitability
13  of this software for any purpose.  It is presented on an AS IS basis.]
14
15******************************************************************************/
16
17#include "ctlspInt.h"
18
19/**AutomaticStart*************************************************************/
20
21/*---------------------------------------------------------------------------*/
22/* Static function prototypes                                                */
23/*---------------------------------------------------------------------------*/
24
25static int CommandCtlspTest(Hrc_Manager_t ** hmgr, int argc, char ** argv);
26static int CommandLtlToSNF(Hrc_Manager_t ** hmgr, int argc, char ** argv);
27static int FormulaArrayCountSubformulae(array_t *formulaArray);
28static void FormulaVisitUnvisitedSubformulae(Ctlsp_Formula_t *formula, int *ptr);
29
30/**AutomaticEnd***************************************************************/
31
32
33/*---------------------------------------------------------------------------*/
34/* Definition of exported functions                                          */
35/*---------------------------------------------------------------------------*/
36/**Function********************************************************************
37
38  Synopsis    [Initializes the CTL* parser package.]
39
40  SideEffects []
41
42  SeeAlso     [Ctlsp_End]
43
44******************************************************************************/
45void
46Ctlsp_Init(void)
47{
48  Cmd_CommandAdd("_ctlsp_test",   CommandCtlspTest,   0);
49  Cmd_CommandAdd("ltl2snf", CommandLtlToSNF, 0);
50}
51
52
53/**Function********************************************************************
54
55  Synopsis    [Ends the CTL* parser package.]
56
57  SideEffects []
58
59  SeeAlso     [Ctlsp_Init]
60
61******************************************************************************/
62void
63Ctlsp_End(void)
64{
65}
66
67/*---------------------------------------------------------------------------*/
68/* Definition of internal functions                                          */
69/*---------------------------------------------------------------------------*/
70
71
72/**Function********************************************************************
73
74  Synopsis [Sets the field states in every subformula of CTL* formula
75  to NULL.]
76
77  Description [The function sets the field states in every subformula
78  of CTL* formula to NULL.]
79 
80  SideEffects []
81
82******************************************************************************/
83void
84CtlspFormulaSetStatesToNULL(
85  Ctlsp_Formula_t *formula)
86{
87  if(formula!=NIL(Ctlsp_Formula_t)) {
88    formula->states = NIL(mdd_t);
89    if(formula->type != Ctlsp_ID_c) {
90      CtlspFormulaSetStatesToNULL(formula->left);
91      CtlspFormulaSetStatesToNULL(formula->right);
92    }
93  }
94}
95
96
97/*---------------------------------------------------------------------------*/
98/* Definition of static functions                                            */
99/*---------------------------------------------------------------------------*/
100
101/**Function********************************************************************
102
103  Synopsis    [Implements the _ctlsp_test command.]
104
105  Description [Implements the _ctlsp_test command.  This command is only meant to
106  test the CTL* command parser.]
107 
108  CommandName [_ctlsp_test]
109
110  CommandSynopsis [test the CTL* parser]
111
112  CommandArguments [\[-h\] <file_name>]
113 
114  CommandDescription [Test the CTL* parser.  If the entire file of CTL*
115  formulas is successfully parsed, then each formula is printed to
116  stdout, followed by the equivalent existential normal form formula.
117
118  The formulas read are not stored.  For the input file containing:
119  <pre> AG(foo=bar); </pre> the following is produced: <pre> original
120  formula: AG(foo=bar) => equivalent existential formula: !(E(TRUE U
121  !(foo=bar))) </pre> For the syntax of CTL formulas, refer to <A
122  HREF="../ctl/ctl/ctl.html"> the VIS CTL and LTL syntax manual</A>.
123
124  Command options:<p> 
125
126  <dl><dt> -h
127  <dd> Print the command usage.
128  </dl>
129  ]
130
131  SideEffects []
132
133******************************************************************************/
134static int
135CommandCtlspTest(
136  Hrc_Manager_t ** hmgr,
137  int  argc,
138  char ** argv)
139{
140  int     c;
141  int      i;
142  FILE    *fp;
143  array_t *formulaArray;
144  array_t *CtlformulaArray;
145  array_t *LTLformulaArray;
146
147  array_t *convertedArray;  /* in DAG format */
148
149  /*
150   * Parse command line options.
151   */
152  util_getopt_reset();
153  while ((c = util_getopt(argc, argv, "h")) != EOF) {
154    switch(c) {
155      case 'h':
156        goto usage;
157      default:
158        goto usage;
159    }
160  }
161
162  /*
163   * Open the ctl file.
164   */
165  if (argc - util_optind == 0) {
166    (void) fprintf(vis_stderr, "** CTL* error: ctl* file not provided\n");
167    goto usage;
168  }
169  else if (argc - util_optind > 1) {
170    (void) fprintf(vis_stderr, "** CTL* error: too many arguments\n");
171    goto usage;
172  }
173
174  fp = Cmd_FileOpen(argv[util_optind], "r", NIL(char *), 0);
175  if (fp == NIL(FILE)) {
176    (void)fprintf(vis_stderr, "** CTL* error: Cannot open the file %s\n", argv[util_optind]);
177    return 1;
178  }
179
180  /*
181   * Parse the CTL* formulas in the file.
182   */
183  formulaArray = Ctlsp_FileParseFormulaArray(fp);
184  (void) fclose(fp);
185
186  if (formulaArray == NIL(array_t)) {
187    fflush(vis_stdout);
188    fflush(vis_stderr);
189    return 1;
190  }
191
192
193  convertedArray = Ctlsp_FormulaArrayConvertToDAG(formulaArray);
194  /*  array_free(formulaArray); */
195
196  /*
197   * Print each original formula and its corresponding converted formula.
198   */
199  for (i = 0; i < array_n(convertedArray); i++) {
200    Ctlsp_Formula_t *formula;
201
202    formula = array_fetch(Ctlsp_Formula_t *, convertedArray, i);
203    (void) fprintf(vis_stdout, "original formula: ");
204    Ctlsp_FormulaPrint(vis_stdout, formula);
205   
206    (void) fprintf(vis_stdout, " [CTL* ");
207
208    if (Ctlsp_isCtlFormula(formula)){
209       (void) fprintf(vis_stdout, ",CTL ");
210    }
211
212    if (Ctlsp_isLtlFormula(formula)){
213       (void) fprintf(vis_stdout, ",LTL ");
214    }
215   
216    (void) fprintf(vis_stdout, "]\n");
217
218  }
219 
220  (void)fprintf(vis_stdout, "No. of subformulae (including formulae) = %d\n",
221                FormulaArrayCountSubformulae(convertedArray));
222
223  /* Converts array of CTL* formula to CTL */
224  CtlformulaArray = Ctlsp_FormulaArrayConvertToCTL(formulaArray);
225  if (CtlformulaArray !=  NIL(array_t)){
226    for (i = 0; i < array_n(CtlformulaArray); i++) { 
227      Ctlp_Formula_t *newFormula;
228
229      newFormula = array_fetch(Ctlp_Formula_t *, CtlformulaArray, i);
230      (void) fprintf(vis_stdout, "CTL formula: ");
231      Ctlp_FormulaPrint(vis_stdout, newFormula);
232      (void) fprintf(vis_stdout, "\n");
233     
234    }
235  array_free(CtlformulaArray);
236  }
237
238  LTLformulaArray = Ctlsp_FormulaArrayConvertToLTL(formulaArray);
239  if (LTLformulaArray !=  NIL(array_t)){
240    for (i = 0; i < array_n(LTLformulaArray); i++) { 
241      Ctlsp_Formula_t *newFormula;
242
243      newFormula = array_fetch(Ctlsp_Formula_t *, LTLformulaArray, i);
244      (void) fprintf(vis_stdout, "LTL formula: ");
245      Ctlsp_FormulaPrint(vis_stdout, newFormula);
246      (void) fprintf(vis_stdout, "\n");
247     
248    }
249  array_free(LTLformulaArray);
250  } else {
251   (void) fprintf(vis_stdout, "No LTL \n");
252  }
253
254  array_free(formulaArray);
255  Ctlsp_FormulaArrayFree(convertedArray);
256
257  fflush(vis_stdout);
258  fflush(vis_stderr);
259
260  return 0;             /* normal exit */
261
262usage:
263  (void) fprintf(vis_stderr, "usage: _ctlsp_test file [-h]\n");
264  (void) fprintf(vis_stderr, "   -h  print the command usage\n");
265  return 1;             /* error exit */
266}
267
268
269/**Function********************************************************************
270
271  Synopsis    [Implements the ltl2snf command.]
272
273  Description [Implements the ltl2snf command.]
274 
275  CommandName [ltl2snf]
276
277  CommandSynopsis [Trnalate LTL formula into Separated Normal Form.]
278
279  CommandArguments [\[-h\] &lt;file_name&gt;]
280 
281  CommandDescription [
282
283  Command options:
284  <p> 
285  <dl>
286 
287  <dt> -f <code> &lt;ltl_file&gt; </code>
288  <dd> The input file containing LTL formulae.
289
290  <dt> -n
291  <dd> Negate the formulae.
292
293  <dt> -h
294  <dd> Print the command usage.
295 
296  </dl>
297  ]
298
299  SideEffects []
300
301******************************************************************************/
302static int
303CommandLtlToSNF(
304  Hrc_Manager_t ** hmgr,
305  int  argc,
306  char ** argv)
307{
308  int     c, i;
309  FILE    *fp;
310  array_t *formulaArray;
311  array_t *LTLformulaArray;
312  char    *ltlFileName = (char *)0;
313  int     negateFormula = 0;
314
315  /*
316   * Parse command line options.
317   */
318  util_getopt_reset();
319  while ((c = util_getopt(argc, argv, "hf:n")) != EOF) {
320    switch(c) {
321      case 'h':
322        goto usage;
323    case 'f':
324      ltlFileName = util_strsav(util_optarg);
325      break;
326    case 'n':
327      negateFormula = 1;
328      break;
329    default:
330      goto usage;
331    }
332  }
333  if (!ltlFileName){
334    (void) fprintf(vis_stderr, "** ltl2snf error: ltl file not provided\n");
335    goto usage;
336  }
337  fp = Cmd_FileOpen(ltlFileName, "r", NIL(char *), 0);
338  FREE(ltlFileName);
339  if (fp == NIL(FILE)) {
340    (void) fprintf(vis_stdout,  "** ltl2snf error: error in opening file %s\n", ltlFileName);
341    return 1;
342  }
343  /*
344   * Parse the CTL* formulas in the file.
345   */
346  formulaArray = Ctlsp_FileParseFormulaArray(fp);
347  (void) fclose(fp);
348
349  if (formulaArray == NIL(array_t)) {
350    fflush(vis_stdout);
351    fflush(vis_stderr);
352    return 1;
353  }
354
355  LTLformulaArray = Ctlsp_FormulaArrayConvertToLTL(formulaArray);
356  if (LTLformulaArray !=  NIL(array_t)){
357    for (i = 0; i < array_n(LTLformulaArray); i++) { 
358      Ctlsp_Formula_t *newFormula;
359
360      newFormula = array_fetch(Ctlsp_Formula_t *, LTLformulaArray, i);
361      (void) fprintf(vis_stdout, "LTL formula: ");
362      Ctlsp_FormulaPrint(vis_stdout, newFormula);
363      (void) fprintf(vis_stdout, "\n");
364
365      if(negateFormula){
366        newFormula = Ctlsp_LtllFormulaNegate(newFormula);
367       
368        (void) fprintf(vis_stdout, "Negated LTL formula: ");
369        Ctlsp_FormulaPrint(vis_stdout, newFormula);
370        (void) fprintf(vis_stdout, "\n");
371      }
372     
373      printf("SNF \n");
374      Ctlsp_LtlTranslateIntoSNF(newFormula);
375    }
376  array_free(LTLformulaArray);
377  } else {
378    (void) fprintf(vis_stdout, "No LTL \n");
379  }
380
381  array_free(formulaArray);
382
383  fflush(vis_stdout);
384  fflush(vis_stderr);
385
386  return 0;             /* normal exit */
387
388usage:
389  (void) fprintf(vis_stderr, "usage: ltl2snf  <-f ltl_file> [-h]\n");
390  (void) fprintf(vis_stderr, "   -f <ltl_file>\n");
391  (void) fprintf(vis_stderr, "   -n  negate formula\n");
392  (void) fprintf(vis_stderr, "   -h  print the command usage\n");
393  return 1;             /* error exit */
394}
395
396
397/**Function********************************************************************
398
399  Synopsis    [Counts the number of subformulae in formulaArray.]
400
401  Description [The function counts the number of subformulae in formulaArray
402  (including the formulae themselves) by traversing the DAG. It uses the field
403  states in Ctlsp_Formula_t to mark the visited states.]
404 
405  SideEffects [The field states is set to 1.]
406
407******************************************************************************/
408static int
409FormulaArrayCountSubformulae(
410  array_t *formulaArray)
411{
412  int num, i;
413  Ctlsp_Formula_t *formula;
414  int count = 0;
415 
416  num = array_n(formulaArray);
417  for(i=0; i<num; i++){
418    formula = array_fetch(Ctlsp_Formula_t *, formulaArray, i);
419    FormulaVisitUnvisitedSubformulae(formula, &count);
420  }
421  /* Set the field states to NULL */
422  for(i=0; i<num; i++){
423    formula = array_fetch(Ctlsp_Formula_t *, formulaArray, i);
424    CtlspFormulaSetStatesToNULL(formula);
425  }
426  return count;
427}
428
429/**Function********************************************************************
430
431  Synopsis    [Visits each unvisited subformula of formula.]
432
433  Description [The formula visits each unvisited subformula of formula and
434  increments *ptr by 1 each time. It also marks each of those as visited.]
435 
436  SideEffects []
437
438******************************************************************************/
439static void
440FormulaVisitUnvisitedSubformulae(
441  Ctlsp_Formula_t *formula,
442  int *ptr)
443{
444  if(formula!=NIL(Ctlsp_Formula_t)) {
445    if(formula->states == NIL(mdd_t)) {
446      (*ptr)++;
447      formula->states = (mdd_t *) 1;
448      if(formula->type != Ctlsp_ID_c) {
449        FormulaVisitUnvisitedSubformulae(formula->left, ptr);
450        FormulaVisitUnvisitedSubformulae(formula->right, ptr);
451      }
452    }
453  }
454}
455
456
457 
458 
459
460
461
462
463
464
465
466
467
468
469
470
471
472
473
474
Note: See TracBrowser for help on using the repository browser.