source: vis_dev/vis-2.3/src/ctlp/ctlpCmd.c @ 56

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

vis2.3

File size: 10.0 KB
Line 
1/**CFile***********************************************************************
2
3  FileName    [ctlpCmd.c]
4
5  PackageName [ctlp]
6
7  Synopsis    [Command to read in a file containing CTL formulas.]
8
9  Author      [Tom Shiple, In-Ho Moon]
10
11  Copyright   [Copyright (c) 1994-1996 The Regents of the Univ. of California.
12  All rights reserved.
13
14  Permission is hereby granted, without written agreement and without license
15  or royalty fees, to use, copy, modify, and distribute this software and its
16  documentation for any purpose, provided that the above copyright notice and
17  the following two paragraphs appear in all copies of this software.
18
19  IN NO EVENT SHALL THE UNIVERSITY OF CALIFORNIA BE LIABLE TO ANY PARTY FOR
20  DIRECT, INDIRECT, SPECIAL, INCIDENTAL, OR CONSEQUENTIAL DAMAGES ARISING OUT
21  OF THE USE OF THIS SOFTWARE AND ITS DOCUMENTATION, EVEN IF THE UNIVERSITY OF
22  CALIFORNIA HAS BEEN ADVISED OF THE POSSIBILITY OF SUCH DAMAGE.
23
24  THE UNIVERSITY OF CALIFORNIA SPECIFICALLY DISCLAIMS ANY WARRANTIES,
25  INCLUDING, BUT NOT LIMITED TO, THE IMPLIED WARRANTIES OF MERCHANTABILITY AND
26  FITNESS FOR A PARTICULAR PURPOSE.  THE SOFTWARE PROVIDED HEREUNDER IS ON AN
27  "AS IS" BASIS, AND THE UNIVERSITY OF CALIFORNIA HAS NO OBLIGATION TO PROVIDE
28  MAINTENANCE, SUPPORT, UPDATES, ENHANCEMENTS, OR MODIFICATIONS.]
29
30******************************************************************************/
31
32#include "ctlpInt.h"
33
34static char rcsid[] UNUSED = "$Id: ctlpCmd.c,v 1.14 2005/05/19 02:35:25 awedh Exp $";
35
36/**AutomaticStart*************************************************************/
37
38/*---------------------------------------------------------------------------*/
39/* Static function prototypes                                                */
40/*---------------------------------------------------------------------------*/
41
42static int CommandCtlpTest(Hrc_Manager_t ** hmgr, int argc, char ** argv);
43static int FormulaArrayCountSubformulae(array_t *formulaArray);
44static void FormulaVisitUnvisitedSubformulae(Ctlp_Formula_t *formula, int *ptr);
45
46/**AutomaticEnd***************************************************************/
47
48
49/*---------------------------------------------------------------------------*/
50/* Definition of exported functions                                          */
51/*---------------------------------------------------------------------------*/
52/**Function********************************************************************
53
54  Synopsis    [Initializes the CTL parser package.]
55
56  SideEffects []
57
58  SeeAlso     [Ctlp_End]
59
60******************************************************************************/
61void
62Ctlp_Init(void)
63{
64  Cmd_CommandAdd("_ctlp_test",   CommandCtlpTest,   0);
65}
66
67
68/**Function********************************************************************
69
70  Synopsis    [Ends the CTL parser package.]
71
72  SideEffects []
73
74  SeeAlso     [Ctlp_Init]
75
76******************************************************************************/
77void
78Ctlp_End(void)
79{
80}
81
82
83/*---------------------------------------------------------------------------*/
84/* Definition of internal functions                                          */
85/*---------------------------------------------------------------------------*/
86
87/**Function********************************************************************
88
89  Synopsis    [Sets the field states in every subformula of formula to
90  NULL.]
91
92  Description [The function sets the field states in every subformula
93  of formula to NULL.]
94 
95  SideEffects []
96
97******************************************************************************/
98void
99CtlpFormulaSetStatesToNULL(
100  Ctlp_Formula_t *formula)
101{
102  if(formula!=NIL(Ctlp_Formula_t)) {
103    formula->states = NIL(mdd_t);
104    if(formula->type != Ctlp_ID_c) {
105      CtlpFormulaSetStatesToNULL(formula->left);
106      CtlpFormulaSetStatesToNULL(formula->right);
107    }
108  }
109}
110
111/*---------------------------------------------------------------------------*/
112/* Definition of static functions                                            */
113/*---------------------------------------------------------------------------*/
114
115/**Function********************************************************************
116
117  Synopsis    [Implements the _ctlp_test command.]
118
119  Description [Implements the _ctlp_test command.  This command is only meant to
120  test the CTL command parser.]
121 
122  CommandName [_ctlp_test]
123
124  CommandSynopsis [test the CTL parser]
125
126  CommandArguments [\[-h\] <file_name>]
127 
128  CommandDescription [Test the CTL parser.  If the entire file of CTL
129  formulas is successfully parsed, then each formula is printed to
130  stdout, followed by the equivalent existential normal form formula.
131  The formulas read are not stored.  For the input file containing:
132  <pre> AG(foo=bar); </pre> the following is produced: <pre> original
133  formula: AG(foo=bar) => equivalent existential formula: !(E(TRUE U
134  !(foo=bar))) </pre> For the syntax of CTL formulas, refer to <A
135  HREF="../ctl/ctl/ctl.html"> the VIS CTL and LTL syntax manual</A>.
136
137  Command options:<p> 
138
139  <dl><dt> -h
140  <dd> Print the command usage.
141  </dl>
142  ]
143
144  SideEffects []
145
146******************************************************************************/
147static int
148CommandCtlpTest(
149  Hrc_Manager_t ** hmgr,
150  int  argc,
151  char ** argv)
152{
153  int     c;
154  int      i;
155  FILE    *fp;
156  array_t *formulaArray;
157  array_t *convertedArray;
158  array_t *existentialConvertedArray;
159  array_t *forwardExistentialArray = NIL(array_t);
160  int     forwardTraversal = 0;
161 
162  /*
163   * Parse command line options.
164   */
165  util_getopt_reset();
166  while ((c = util_getopt(argc, argv, "Fh")) != EOF) {
167    switch(c) {
168      case 'F':
169        forwardTraversal = 1;
170        break;
171      case 'h':
172        goto usage;
173      default:
174        goto usage;
175    }
176  }
177
178  /*
179   * Open the ctl file.
180   */
181  if (argc - util_optind == 0) {
182    (void) fprintf(vis_stderr, "** ctl error: ctl file not provided\n");
183    goto usage;
184  }
185  else if (argc - util_optind > 1) {
186    (void) fprintf(vis_stderr, "** ctl error: too many arguments\n");
187    goto usage;
188  }
189
190  fp = Cmd_FileOpen(argv[util_optind], "r", NIL(char *), 0);
191  if (fp == NIL(FILE)) {
192    (void)fprintf(vis_stderr, "** ctl error: Cannot open the file %s\n", argv[util_optind]);
193    return 1;
194  }
195
196  /*
197   * Parse the formulas in the file.
198   */
199  formulaArray = Ctlp_FileParseFormulaArray(fp);
200  (void) fclose(fp);
201
202  if (formulaArray == NIL(array_t)) {
203    fflush(vis_stdout);
204    fflush(vis_stderr);
205    return 1;
206  }
207
208  if (forwardTraversal)
209    forwardExistentialArray =
210      Ctlp_FormulaArrayConvertToForward(formulaArray, 1, FALSE);
211
212  convertedArray = Ctlp_FormulaArrayConvertToDAG(formulaArray);
213  array_free(formulaArray);
214  existentialConvertedArray =
215      Ctlp_FormulaDAGConvertToExistentialFormDAG(convertedArray);
216 
217  /*
218   * Print each original formula and its corresponding converted formula.
219   */
220  for (i = 0; i < array_n(convertedArray); i++) {
221    Ctlp_Formula_t *formula;
222
223    formula = array_fetch(Ctlp_Formula_t *, convertedArray, i);
224    (void) fprintf(vis_stdout, "original formula: ");
225    Ctlp_FormulaPrint(vis_stdout, formula);
226    (void) fprintf(vis_stdout, "\n");
227
228    formula = array_fetch(Ctlp_Formula_t *, existentialConvertedArray, i);
229    (void) fprintf(vis_stdout, "=> equivalent existential formula: ");
230    Ctlp_FormulaPrint(vis_stdout, formula);
231    (void) fprintf(vis_stdout, "\n");
232
233    if (forwardTraversal) {
234      formula = array_fetch(Ctlp_Formula_t *, forwardExistentialArray, i);
235      (void) fprintf(vis_stdout, "=> equivalent forward existential formula: ");
236      Ctlp_FormulaPrint(vis_stdout, formula);
237      (void) fprintf(vis_stdout, "\n");
238    }
239  }
240
241  (void)fprintf(vis_stdout, "No. of subformulae (including formulae) = %d\n",
242                FormulaArrayCountSubformulae(existentialConvertedArray));
243  if (forwardTraversal) {
244    (void)fprintf(vis_stdout,
245                  "No. of forward subformulae (including formulae) = %d\n",
246                  FormulaArrayCountSubformulae(forwardExistentialArray));
247  }
248
249
250  Ctlp_FormulaArrayFree(convertedArray);
251  Ctlp_FormulaArrayFree(existentialConvertedArray);
252  if (forwardTraversal)
253    Ctlp_FormulaArrayFree(forwardExistentialArray);
254 
255  fflush(vis_stdout);
256  fflush(vis_stderr);
257
258  return 0;             /* normal exit */
259
260usage:
261  (void) fprintf(vis_stderr, "usage: _ctlp_test file [-h]\n");
262  (void) fprintf(vis_stderr, "   -h  print the command usage\n");
263  return 1;             /* error exit */
264}
265
266
267/**Function********************************************************************
268
269  Synopsis    [Counts the number of subformulae in formulaArray.]
270
271  Description [The function counts the number of subformulae in formulaArray
272  (including the formulae themselves) by traversing the DAG. It uses the field
273  states in Ctlp_Formula_t to mark the visited states.]
274 
275  SideEffects [The field states is set to 1.]
276
277******************************************************************************/
278static int
279FormulaArrayCountSubformulae(
280  array_t *formulaArray)
281{
282  int num, i;
283  Ctlp_Formula_t *formula;
284  int count = 0;
285 
286  num = array_n(formulaArray);
287  for(i=0; i<num; i++){
288    formula = array_fetch(Ctlp_Formula_t *, formulaArray, i);
289    FormulaVisitUnvisitedSubformulae(formula, &count);
290  }
291  /* Set the field states to NULL */
292  for(i=0; i<num; i++){
293    formula = array_fetch(Ctlp_Formula_t *, formulaArray, i);
294    CtlpFormulaSetStatesToNULL(formula);
295  }
296  return count;
297}
298
299/**Function********************************************************************
300
301  Synopsis    [Visits each unvisited subformula of formula.]
302
303  Description [The formula visits each unvisited subformula of formula and
304  increments *ptr by 1 each time. It also marks each of those as visited.]
305 
306  SideEffects []
307
308******************************************************************************/
309static void
310FormulaVisitUnvisitedSubformulae(
311  Ctlp_Formula_t *formula,
312  int *ptr)
313{
314  if(formula!=NIL(Ctlp_Formula_t)) {
315    if(formula->states == NIL(mdd_t)) {
316      (*ptr)++;
317      formula->states = (mdd_t *) 1;
318      if(formula->type != Ctlp_ID_c) {
319        FormulaVisitUnvisitedSubformulae(formula->left, ptr);
320        FormulaVisitUnvisitedSubformulae(formula->right, ptr);
321      }
322    }
323  }
324}
325
326
327 
328 
329
330
331
332
333
334
335
336
Note: See TracBrowser for help on using the repository browser.