#include "ctlpInt.h"
Include dependency graph for ctlpCmd.c:
Go to the source code of this file.
Functions | |
| static int | CommandCtlpTest (Hrc_Manager_t **hmgr, int argc, char **argv) |
| static int | FormulaArrayCountSubformulae (array_t *formulaArray) |
| static void | FormulaVisitUnvisitedSubformulae (Ctlp_Formula_t *formula, int *ptr) |
| void | Ctlp_Init (void) |
| void | Ctlp_End (void) |
| void | CtlpFormulaSetStatesToNULL (Ctlp_Formula_t *formula) |
Variables | |
| static char rcsid[] | UNUSED = "$Id: ctlpCmd.c,v 1.14 2005/05/19 02:35:25 awedh Exp $" |
Function Documentation
| static int CommandCtlpTest | ( | Hrc_Manager_t ** | hmgr, |
| int | argc, | ||
| char ** | argv | ||
| ) | [static] |
AutomaticStart
Function********************************************************************
Synopsis [Implements the _ctlp_test command.]
Description [Implements the _ctlp_test command. This command is only meant to test the CTL command parser.]
CommandName [_ctlp_test]
CommandSynopsis [test the CTL parser]
CommandArguments [\[-h\] <file_name>]
CommandDescription [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.
]
SideEffects []
Definition at line 148 of file ctlpCmd.c.
{
int c;
int i;
FILE *fp;
array_t *formulaArray;
array_t *convertedArray;
array_t *existentialConvertedArray;
array_t *forwardExistentialArray = NIL(array_t);
int forwardTraversal = 0;
/*
* Parse command line options.
*/
util_getopt_reset();
while ((c = util_getopt(argc, argv, "Fh")) != EOF) {
switch(c) {
case 'F':
forwardTraversal = 1;
break;
case 'h':
goto usage;
default:
goto usage;
}
}
/*
* Open the ctl file.
*/
if (argc - util_optind == 0) {
(void) fprintf(vis_stderr, "** ctl error: ctl file not provided\n");
goto usage;
}
else if (argc - util_optind > 1) {
(void) fprintf(vis_stderr, "** ctl error: too many arguments\n");
goto usage;
}
fp = Cmd_FileOpen(argv[util_optind], "r", NIL(char *), 0);
if (fp == NIL(FILE)) {
(void)fprintf(vis_stderr, "** ctl error: Cannot open the file %s\n", argv[util_optind]);
return 1;
}
/*
* Parse the formulas in the file.
*/
formulaArray = Ctlp_FileParseFormulaArray(fp);
(void) fclose(fp);
if (formulaArray == NIL(array_t)) {
fflush(vis_stdout);
fflush(vis_stderr);
return 1;
}
if (forwardTraversal)
forwardExistentialArray =
Ctlp_FormulaArrayConvertToForward(formulaArray, 1, FALSE);
convertedArray = Ctlp_FormulaArrayConvertToDAG(formulaArray);
array_free(formulaArray);
existentialConvertedArray =
Ctlp_FormulaDAGConvertToExistentialFormDAG(convertedArray);
/*
* Print each original formula and its corresponding converted formula.
*/
for (i = 0; i < array_n(convertedArray); i++) {
Ctlp_Formula_t *formula;
formula = array_fetch(Ctlp_Formula_t *, convertedArray, i);
(void) fprintf(vis_stdout, "original formula: ");
Ctlp_FormulaPrint(vis_stdout, formula);
(void) fprintf(vis_stdout, "\n");
formula = array_fetch(Ctlp_Formula_t *, existentialConvertedArray, i);
(void) fprintf(vis_stdout, "=> equivalent existential formula: ");
Ctlp_FormulaPrint(vis_stdout, formula);
(void) fprintf(vis_stdout, "\n");
if (forwardTraversal) {
formula = array_fetch(Ctlp_Formula_t *, forwardExistentialArray, i);
(void) fprintf(vis_stdout, "=> equivalent forward existential formula: ");
Ctlp_FormulaPrint(vis_stdout, formula);
(void) fprintf(vis_stdout, "\n");
}
}
(void)fprintf(vis_stdout, "No. of subformulae (including formulae) = %d\n",
FormulaArrayCountSubformulae(existentialConvertedArray));
if (forwardTraversal) {
(void)fprintf(vis_stdout,
"No. of forward subformulae (including formulae) = %d\n",
FormulaArrayCountSubformulae(forwardExistentialArray));
}
Ctlp_FormulaArrayFree(convertedArray);
Ctlp_FormulaArrayFree(existentialConvertedArray);
if (forwardTraversal)
Ctlp_FormulaArrayFree(forwardExistentialArray);
fflush(vis_stdout);
fflush(vis_stderr);
return 0; /* normal exit */
usage:
(void) fprintf(vis_stderr, "usage: _ctlp_test file [-h]\n");
(void) fprintf(vis_stderr, " -h print the command usage\n");
return 1; /* error exit */
}
Here is the call graph for this function:
Here is the caller graph for this function:
| void Ctlp_End | ( | void | ) |
| void Ctlp_Init | ( | void | ) |
AutomaticEnd Function********************************************************************
Synopsis [Initializes the CTL parser package.]
SideEffects []
SeeAlso [Ctlp_End]
Definition at line 62 of file ctlpCmd.c.
{
Cmd_CommandAdd("_ctlp_test", CommandCtlpTest, 0);
}
Here is the call graph for this function:
Here is the caller graph for this function:
| void CtlpFormulaSetStatesToNULL | ( | Ctlp_Formula_t * | formula | ) |
Function********************************************************************
Synopsis [Sets the field states in every subformula of formula to NULL.]
Description [The function sets the field states in every subformula of formula to NULL.]
SideEffects []
Definition at line 99 of file ctlpCmd.c.
{
if(formula!=NIL(Ctlp_Formula_t)) {
formula->states = NIL(mdd_t);
if(formula->type != Ctlp_ID_c) {
CtlpFormulaSetStatesToNULL(formula->left);
CtlpFormulaSetStatesToNULL(formula->right);
}
}
}
Here is the caller graph for this function:
| static int FormulaArrayCountSubformulae | ( | array_t * | formulaArray | ) | [static] |
Function********************************************************************
Synopsis [Counts the number of subformulae in formulaArray.]
Description [The function counts the number of subformulae in formulaArray (including the formulae themselves) by traversing the DAG. It uses the field states in Ctlp_Formula_t to mark the visited states.]
SideEffects [The field states is set to 1.]
Definition at line 279 of file ctlpCmd.c.
{
int num, i;
Ctlp_Formula_t *formula;
int count = 0;
num = array_n(formulaArray);
for(i=0; i<num; i++){
formula = array_fetch(Ctlp_Formula_t *, formulaArray, i);
FormulaVisitUnvisitedSubformulae(formula, &count);
}
/* Set the field states to NULL */
for(i=0; i<num; i++){
formula = array_fetch(Ctlp_Formula_t *, formulaArray, i);
CtlpFormulaSetStatesToNULL(formula);
}
return count;
}
Here is the call graph for this function:
Here is the caller graph for this function:
| static void FormulaVisitUnvisitedSubformulae | ( | Ctlp_Formula_t * | formula, |
| int * | ptr | ||
| ) | [static] |
Function********************************************************************
Synopsis [Visits each unvisited subformula of formula.]
Description [The formula visits each unvisited subformula of formula and increments *ptr by 1 each time. It also marks each of those as visited.]
SideEffects []
Definition at line 310 of file ctlpCmd.c.
{
if(formula!=NIL(Ctlp_Formula_t)) {
if(formula->states == NIL(mdd_t)) {
(*ptr)++;
formula->states = (mdd_t *) 1;
if(formula->type != Ctlp_ID_c) {
FormulaVisitUnvisitedSubformulae(formula->left, ptr);
FormulaVisitUnvisitedSubformulae(formula->right, ptr);
}
}
}
}
Here is the caller graph for this function:
Variable Documentation
char rcsid [] UNUSED = "$Id: ctlpCmd.c,v 1.14 2005/05/19 02:35:25 awedh Exp $" [static] |
CFile***********************************************************************
FileName [ctlpCmd.c]
PackageName [ctlp]
Synopsis [Command to read in a file containing CTL formulas.]
Author [Tom Shiple, In-Ho Moon]
Copyright [Copyright (c) 1994-1996 The Regents of the Univ. of California. All rights reserved.
Permission is hereby granted, without written agreement and without license or royalty fees, to use, copy, modify, and distribute this software and its documentation for any purpose, provided that the above copyright notice and the following two paragraphs appear in all copies of this software.
IN NO EVENT SHALL THE UNIVERSITY OF CALIFORNIA BE LIABLE TO ANY PARTY FOR DIRECT, INDIRECT, SPECIAL, INCIDENTAL, OR CONSEQUENTIAL DAMAGES ARISING OUT OF THE USE OF THIS SOFTWARE AND ITS DOCUMENTATION, EVEN IF THE UNIVERSITY OF CALIFORNIA HAS BEEN ADVISED OF THE POSSIBILITY OF SUCH DAMAGE.
THE UNIVERSITY OF CALIFORNIA SPECIFICALLY DISCLAIMS ANY WARRANTIES, INCLUDING, BUT NOT LIMITED TO, THE IMPLIED WARRANTIES OF MERCHANTABILITY AND FITNESS FOR A PARTICULAR PURPOSE. THE SOFTWARE PROVIDED HEREUNDER IS ON AN "AS IS" BASIS, AND THE UNIVERSITY OF CALIFORNIA HAS NO OBLIGATION TO PROVIDE MAINTENANCE, SUPPORT, UPDATES, ENHANCEMENTS, OR MODIFICATIONS.]
