#include <stdio.h>
#include <string.h>
#include <assert.h>
#include <stdlib.h>
#include "aig/aig/aig.h"
#include "base/abc/abc.h"
#include "base/main/mainInt.h"

Data Structures
struct	ltlNode_t

Typedefs
typedef enum ltlToken	tokenType

typedef enum ltlGrammerToken	ltlGrammerTokenType

typedef struct ltlNode_t	ltlNode

Enumerations
enum	ltlToken { AND, OR, NOT, IMPLY, GLOBALLY, EVENTUALLY, NEXT, UNTIL, BOOL }

enum	ltlGrammerToken { OPERAND, LTL, BINOP, UOP }

Functions
ltlNode *	generateTypedNode (tokenType new_type)

Aig_Obj_t *	buildLogicFromLTLNode_combinationalOnly (Aig_Man_t pAig, ltlNode pLtlNode)

static int	isNotVarNameSymbol (char c)

void	Abc_FrameCopyLTLDataBase (Abc_Frame_t pAbc, Abc_Ntk_t pNtk)

char *	getVarName (char suffixFormula, int startLoc, int endLocation)

int	isUnexpectedEOS (char *formula, int index)

int	isTemporalOperator (char *formula, int index)

ltlNode *	readLtlFormula (char *formula)

void	resetGlobalVar ()

ltlNode *	parseFormulaCreateAST (char *inputFormula)

void	traverseAbstractSyntaxTree (ltlNode *node)

void	traverseAbstractSyntaxTree_postFix (ltlNode *node)

void	populateAigPointerUnitGF (Aig_Man_t pAigNew, ltlNode topASTNode, Vec_Ptr_t vSignal, Vec_Vec_t vAigGFMap)

Aig_Obj_t *	buildLogicFromLTLNode (Aig_Man_t pAig, ltlNode pLtlNode)

int	isNonTemporalSubformula (ltlNode *topNode)

int	isWellFormed (ltlNode *topNode)

int	checkBooleanConstant (char *targetName)

int	checkSignalNameExistence (Abc_Ntk_t pNtk, ltlNode topASTNode)

void	populateBoolWithAigNodePtr (Abc_Ntk_t pNtk, Aig_Man_t pAigOld, Aig_Man_t pAigNew, ltlNode topASTNode)

int	checkAllBoolHaveAIGPointer (ltlNode *topASTNode)

void	setAIGNodePtrOfGloballyNode (ltlNode astNode, Aig_Obj_t pObjLo)

Aig_Obj_t *	retriveAIGPointerFromLTLNode (ltlNode *astNode)

Variables
int	startOfSuffixString = 0

Typedef Documentation

typedef enum ltlGrammerToken ltlGrammerTokenType

Definition at line 35 of file ltl_parser.c.

typedef struct ltlNode_t ltlNode

Definition at line 46 of file ltl_parser.c.

typedef enum ltlToken tokenType

Definition at line 34 of file ltl_parser.c.

Enumeration Type Documentation

enum ltlGrammerToken

Enumerator
OPERAND
LTL
BINOP
UOP

Definition at line 33 of file ltl_parser.c.

33 { OPERAND, LTL, BINOP, UOP };

OPERAND

Definition: ltl_parser.c:33

UOP

Definition: ltl_parser.c:33

LTL

Definition: ltl_parser.c:33

BINOP

Definition: ltl_parser.c:33

enum ltlToken

CFile****************************************************************

FileName [ltl_parser.c]

SystemName [ABC: Logic synthesis and verification system.]

PackageName [Liveness property checking.]

Synopsis [LTL checker.]

Author [Sayak Ray]

Affiliation [UC Berkeley]

Date [Ver. 1.0. Started - January 1, 2009.]

Revision [

Id:: ltl_parser.c,v 1.00 2009/01/01 00:00:00 alanmi Exp

]

Enumerator
AND
OR
NOT
IMPLY
GLOBALLY
EVENTUALLY
NEXT
UNTIL
BOOL

Definition at line 32 of file ltl_parser.c.

32 { AND, OR, NOT, IMPLY, GLOBALLY, EVENTUALLY, NEXT, UNTIL, BOOL };

IMPLY

Definition: ltl_parser.c:32

GLOBALLY

Definition: ltl_parser.c:32

OR

Definition: ltl_parser.c:32

NOT

Definition: ltl_parser.c:32

EVENTUALLY

Definition: ltl_parser.c:32

BOOL

Definition: ltl_parser.c:32

AND

Definition: ltl_parser.c:32

UNTIL

Definition: ltl_parser.c:32

Function Documentation

void Abc_FrameCopyLTLDataBase	(	Abc_Frame_t *	pAbc,
		Abc_Ntk_t *	pNtk
	)

Definition at line 73 of file ltl_parser.c.

 {
     char *pLtlFormula, *tempFormula;
     int i;
 
     if( pAbc->vLTLProperties_global != NULL )
     {
 //      printf("Deleting exisitng LTL database from the frame\n");
         Vec_PtrFree( pAbc->vLTLProperties_global );
         pAbc->vLTLProperties_global = NULL;
     }
     pAbc->vLTLProperties_global = Vec_PtrAlloc(Vec_PtrSize(pNtk->vLtlProperties));
     Vec_PtrForEachEntry( char *, pNtk->vLtlProperties, pLtlFormula, i )
     {
         tempFormula = (char *)malloc( sizeof(char)*(strlen(pLtlFormula)+1) );
         sprintf( tempFormula, "%s", pLtlFormula );
         Vec_PtrPush( pAbc->vLTLProperties_global, tempFormula );
     }
 }

Aig_Obj_t* buildLogicFromLTLNode	(	Aig_Man_t *	pAig,
		ltlNode *	pLtlNode
	)

Definition at line 601 of file ltl_parser.c.

 {
     Aig_Obj_t *leftAigObj, *rightAigObj;
 
     if( pLtlNode->pObj != NULL )
         return pLtlNode->pObj;
     else
     {
         assert( pLtlNode->type != BOOL );
         switch( pLtlNode->type ){
             case AND:
                 assert( pLtlNode->left ); assert( pLtlNode->right );
                 leftAigObj = buildLogicFromLTLNode( pAig, pLtlNode->left );
                 rightAigObj = buildLogicFromLTLNode( pAig, pLtlNode->right );
                 assert( leftAigObj ); assert( rightAigObj );
                 pLtlNode->pObj = Aig_And( pAig, leftAigObj, rightAigObj );
                 return pLtlNode->pObj;
             case OR:
                 assert( pLtlNode->left ); assert( pLtlNode->right );
                 leftAigObj = buildLogicFromLTLNode( pAig, pLtlNode->left );
                 rightAigObj = buildLogicFromLTLNode( pAig, pLtlNode->right );
                 assert( leftAigObj ); assert( rightAigObj );
                 pLtlNode->pObj = Aig_Or( pAig, leftAigObj, rightAigObj );
                 return pLtlNode->pObj;
             case NOT:
                 assert( pLtlNode->left ); assert( pLtlNode->right == NULL ); 
                 leftAigObj = buildLogicFromLTLNode( pAig, pLtlNode->left );
                 assert( leftAigObj );
                 pLtlNode->pObj = Aig_Not( leftAigObj );
                 return pLtlNode->pObj;
             case GLOBALLY:
             case EVENTUALLY:
             case NEXT:
             case UNTIL:
                 printf("\nAttempting to create circuit with missing AIG pointer in a TEMPORAL node: ABORTING!!\n");
                 exit(0);
             default:
                 printf("\nSerious ERROR: attempting to create AIG node from a temporal node\n");
                 exit(0);
         }
     }
 }

Aig_Obj_t * buildLogicFromLTLNode_combinationalOnly	(	Aig_Man_t *	pAig,
		ltlNode *	pLtlNode
	)

Definition at line 558 of file ltl_parser.c.

 {
     Aig_Obj_t *leftAigObj, *rightAigObj;
 
     if( pLtlNode->pObj != NULL )
         return pLtlNode->pObj;
     else
     {
         assert( pLtlNode->type != BOOL );
         switch( pLtlNode->type ){
             case AND:
                 assert( pLtlNode->left ); assert( pLtlNode->right );
                 leftAigObj = buildLogicFromLTLNode_combinationalOnly( pAigNew, pLtlNode->left );
                 rightAigObj = buildLogicFromLTLNode_combinationalOnly( pAigNew, pLtlNode->right );
                 assert( leftAigObj ); assert( rightAigObj );
                 pLtlNode->pObj = Aig_And( pAigNew, leftAigObj, rightAigObj );
                 return pLtlNode->pObj;
             case OR:
                 assert( pLtlNode->left ); assert( pLtlNode->right );
                 leftAigObj = buildLogicFromLTLNode_combinationalOnly( pAigNew, pLtlNode->left );
                 rightAigObj = buildLogicFromLTLNode_combinationalOnly( pAigNew, pLtlNode->right );
                 assert( leftAigObj ); assert( rightAigObj );
                 pLtlNode->pObj = Aig_Or( pAigNew, leftAigObj, rightAigObj );
                 return pLtlNode->pObj;
             case NOT:
                 assert( pLtlNode->left ); assert( pLtlNode->right == NULL ); 
                 leftAigObj = buildLogicFromLTLNode_combinationalOnly( pAigNew, pLtlNode->left );
                 assert( leftAigObj );
                 pLtlNode->pObj = Aig_Not( leftAigObj );
                 return pLtlNode->pObj;
             case GLOBALLY:
             case EVENTUALLY:
             case NEXT:
             case UNTIL:
                 printf("FORBIDDEN node: ABORTING!!\n");
                 exit(0);
             default:
                 printf("\nSerious ERROR: attempting to create AIG node from a temporal node\n");
                 exit(0);
         }
     }
 }

int checkAllBoolHaveAIGPointer ( ltlNode * topASTNode )

Definition at line 795 of file ltl_parser.c.

 {
     
     switch( topASTNode->type ){
         case BOOL:
             if( topASTNode->pObj != NULL )
                 return 1;
             else
             {
                 printf("\nfaulting PODMANDYO topASTNode->name = %s\n", topASTNode->name);
                 return 0;
             }
         case AND:
         case OR:
         case IMPLY:
         case UNTIL:
             assert( topASTNode->left != NULL );
             assert( topASTNode->right != NULL );
             return checkAllBoolHaveAIGPointer( topASTNode->left ) && checkAllBoolHaveAIGPointer( topASTNode->right );
             
         case NOT:
         case NEXT:
         case GLOBALLY:
         case EVENTUALLY:
             assert( topASTNode->left != NULL );
             assert( topASTNode->right == NULL );
             return checkAllBoolHaveAIGPointer( topASTNode->left );
         default:
             printf("\nUNSUPPORTED LTL NODE TYPE:: Aborting execution\n");
             exit(0);
     }
 }

int checkBooleanConstant ( char * targetName )

Definition at line 690 of file ltl_parser.c.

 {
     if( strcmp( targetName, "true" ) == 0 ) 
         return 1;
     if( strcmp( targetName, "false" ) == 0 )
         return 0;
     return -1;
 }

int checkSignalNameExistence	(	Abc_Ntk_t *	pNtk,
		ltlNode *	topASTNode
	)

Definition at line 699 of file ltl_parser.c.

 {
     char *targetName;
     Abc_Obj_t * pNode;
     int i;
         
     switch( topASTNode->type ){
         case BOOL:
             targetName = topASTNode->name;
             //printf("\nTrying to match name %s\n", targetName);
             if( checkBooleanConstant( targetName ) != -1 )
                 return 1;
             Abc_NtkForEachPo( pNtk, pNode, i )
             {
                 if( strcmp( Abc_ObjName( pNode ), targetName ) == 0 )
                 {
                     //printf("\nVariable name \"%s\" MATCHED\n", targetName);
                     return 1;
                 }
             }
             printf("\nVariable name \"%s\" not found in the PO name list\n", targetName);
             return 0;
         case AND:
         case OR:
         case IMPLY:
         case UNTIL:
             assert( topASTNode->left != NULL );
             assert( topASTNode->right != NULL );
             return checkSignalNameExistence( pNtk, topASTNode->left ) && checkSignalNameExistence( pNtk, topASTNode->right );
             
         case NOT:
         case NEXT:
         case GLOBALLY:
         case EVENTUALLY:
             assert( topASTNode->left != NULL );
             assert( topASTNode->right == NULL );
             return checkSignalNameExistence( pNtk, topASTNode->left );
         default:
             printf("\nUNSUPPORTED LTL NODE TYPE:: Aborting execution\n");
             exit(0);
     }
 }

ltlNode* generateTypedNode ( tokenType new_type )

Definition at line 48 of file ltl_parser.c.

 {
     ltlNode *new_node;
 
     new_node = (ltlNode *)malloc( sizeof(ltlNode) );
     if( new_node )
     {
         new_node->type = new_type;
         new_node->pObj = NULL;
         new_node->name = NULL;
         new_node->left = NULL;
         new_node->right = NULL;
     }
 
     return new_node;
 }

char* getVarName	(	char *	suffixFormula,
		int	startLoc,
		int *	endLocation
	)

Definition at line 93 of file ltl_parser.c.

 {
     int i = startLoc, length;
     char *name;
 
     if( isNotVarNameSymbol( suffixFormula[startLoc] ) )
         return NULL;
 
     while( !isNotVarNameSymbol( suffixFormula[i] ) )
         i++;
     *endLocation = i;
     length = i - startLoc;
     name = (char *)malloc( sizeof(char) * (length + 1));
     for( i=0; i<length; i++ )
         name[i] = suffixFormula[i+startLoc];
     name[i] = '\0';
 
     return name;
 }

int isNonTemporalSubformula ( ltlNode * topNode )

Definition at line 644 of file ltl_parser.c.

 {
     switch( topNode->type ){
         case AND:
         case OR:
         case IMPLY:
             return isNonTemporalSubformula( topNode->left) && isNonTemporalSubformula( topNode->right ) ;
         case NOT:
             assert( topNode->right == NULL );
             return isNonTemporalSubformula( topNode->left );
         case BOOL:
             return 1;
         default:
             return 0;
     }
 }

static int isNotVarNameSymbol ( char c )

inlinestatic

Definition at line 68 of file ltl_parser.c.

 {
     return ( c == ' ' || c == '\t' || c == '\n' || c == ':' || c == '\0' );
 }

int isTemporalOperator	(	char *	formula,
		int	index
	)

Definition at line 127 of file ltl_parser.c.

 {
     if( !(isUnexpectedEOS( formula, index ) || formula[ index ] == 'G' || formula[ index ] == 'F' || formula[ index ] == 'U' || formula[ index ] == 'X') )
     {
         printf("\nInvalid LTL formula: expecting temporal operator at the position %d....\n", index);
         return 0;
     }
     return 1;
 }

int isUnexpectedEOS	(	char *	formula,
		int	index
	)

Definition at line 116 of file ltl_parser.c.

 {
     assert( formula );
     if( index >= (int)strlen( formula ) )
     {
         printf("\nInvalid LTL formula: unexpected end of string..." );
         return 1;
     }
     return 0;
 }

int isWellFormed ( ltlNode * topNode )

Definition at line 661 of file ltl_parser.c.

 {
     ltlNode *nextNode;
 
     switch( topNode->type ){
         case AND:
         case OR:
         case IMPLY:
             return isWellFormed( topNode->left) && isWellFormed( topNode->right ) ;
         case NOT:
             assert( topNode->right == NULL );
             return isWellFormed( topNode->left );
         case BOOL:
             return 1;
         case GLOBALLY:
             nextNode = topNode->left;
             assert( topNode->right == NULL );
             if( nextNode->type != EVENTUALLY )
                 return 0;
             else
             {
                 assert( nextNode->right == NULL );
                 return isNonTemporalSubformula( nextNode->left );
             }
         default:
             return 0;
     }
 }

ltlNode* parseFormulaCreateAST ( char * inputFormula )

Definition at line 366 of file ltl_parser.c.

 {
     ltlNode *temp;
 
     temp = readLtlFormula( inputFormula );
     //if( temp == NULL )
     //  printf("\nAST creation failed for formula %s", inputFormula );
     resetGlobalVar();
     return temp;
 }

void populateAigPointerUnitGF	(	Aig_Man_t *	pAigNew,
		ltlNode *	topASTNode,
		Vec_Ptr_t *	vSignal,
		Vec_Vec_t *	vAigGFMap
	)

Definition at line 505 of file ltl_parser.c.

 {
     ltlNode *nextNode, *nextToNextNode;
     int serialNumSignal;
 
     switch( topASTNode->type ){
         case AND:
         case OR:
         case IMPLY:
             populateAigPointerUnitGF( pAigNew, topASTNode->left, vSignal, vAigGFMap );
             populateAigPointerUnitGF( pAigNew, topASTNode->right, vSignal, vAigGFMap );
             return;
         case NOT:
             populateAigPointerUnitGF( pAigNew, topASTNode->left, vSignal, vAigGFMap );
             return;
         case GLOBALLY:
             nextNode = topASTNode->left;
             assert( nextNode->type = EVENTUALLY );
             nextToNextNode = nextNode->left;
             if( nextToNextNode->type == BOOL )
             {
                 assert( nextToNextNode->pObj );
                 serialNumSignal = Vec_PtrFind( vSignal, nextToNextNode->pObj );
                 if( serialNumSignal == -1 )
                 {                   
                     Vec_PtrPush( vSignal, nextToNextNode->pObj );
                     serialNumSignal = Vec_PtrFind( vSignal, nextToNextNode->pObj );
                 }
                 //Vec_PtrPush( vGLOBALLY, topASTNode );
                 Vec_VecPush( vAigGFMap, serialNumSignal, topASTNode );
             }
             else
             {
                 assert( nextToNextNode->pObj == NULL );
                 buildLogicFromLTLNode_combinationalOnly( pAigNew, nextToNextNode );
                 serialNumSignal = Vec_PtrFind( vSignal, nextToNextNode->pObj );
                 if( serialNumSignal == -1 )
                 {
                     Vec_PtrPush( vSignal, nextToNextNode->pObj );
                     serialNumSignal = Vec_PtrFind( vSignal, nextToNextNode->pObj );
                 }
                 //Vec_PtrPush( vGLOBALLY, topASTNode );
                 Vec_VecPush( vAigGFMap, serialNumSignal, topASTNode );
             }
             return;
         case BOOL:
             return;
         default:
             printf("\nINVALID situation: aborting...\n");
             exit(0);
     }
 }

void populateBoolWithAigNodePtr	(	Abc_Ntk_t *	pNtk,
		Aig_Man_t *	pAigOld,
		Aig_Man_t *	pAigNew,
		ltlNode *	topASTNode
	)

Definition at line 742 of file ltl_parser.c.

 {
     char *targetName;
     Abc_Obj_t * pNode;
     int i;
     Aig_Obj_t *pObj, *pDriverImage;
     
     switch( topASTNode->type ){
         case BOOL:
             targetName = topASTNode->name;
             if( checkBooleanConstant( targetName ) == 1 )
             {
                 topASTNode->pObj = Aig_ManConst1( pAigNew );
                 return;
             }
             if( checkBooleanConstant( targetName ) == 0 )
             {
                 topASTNode->pObj = Aig_Not(topASTNode->pObj = Aig_ManConst1( pAigNew ));
                 return;
             }
             Abc_NtkForEachPo( pNtk, pNode, i )
                 if( strcmp( Abc_ObjName( pNode ), targetName ) == 0 )
                 {
                     pObj = Aig_ManCo( pAigOld, i );
                     assert( Aig_ObjIsCo( pObj ));
                     pDriverImage = Aig_NotCond((Aig_Obj_t *)Aig_Regular(Aig_ObjChild0( pObj ))->pData, Aig_ObjFaninC0(pObj));
                     topASTNode->pObj = pDriverImage;
                     return;
                 }
             assert(0);
         case AND:
         case OR:
         case IMPLY:
         case UNTIL:
             assert( topASTNode->left != NULL );
             assert( topASTNode->right != NULL );
             populateBoolWithAigNodePtr( pNtk, pAigOld, pAigNew, topASTNode->left );
             populateBoolWithAigNodePtr( pNtk, pAigOld, pAigNew, topASTNode->right );
             return;
         case NOT:
         case NEXT:
         case GLOBALLY:
         case EVENTUALLY:
             assert( topASTNode->left != NULL );
             assert( topASTNode->right == NULL );
             populateBoolWithAigNodePtr( pNtk, pAigOld, pAigNew, topASTNode->left );
             return;
         default:
             printf("\nUNSUPPORTED LTL NODE TYPE:: Aborting execution\n");
             exit(0);
     }
 }

ltlNode* readLtlFormula ( char * formula )

Definition at line 137 of file ltl_parser.c.

 {
     char ch;
     char *varName;
     int formulaLength, rememberEnd;
     int i = startOfSuffixString;
     ltlNode *curr_node, *temp_node_left, *temp_node_right;
     char prevChar;
     
     formulaLength = strlen( formula );
     if( isUnexpectedEOS( formula, startOfSuffixString ) )
     {
         printf("\nFAULTING POINT: formula = %s\nstartOfSuffixString = %d, formula[%d] = %c\n\n", formula, startOfSuffixString, startOfSuffixString - 1, formula[startOfSuffixString-1]);
         return NULL;
     }
             
     while( i < formulaLength )
     {
         ch = formula[i];
 
         switch(ch){
             case ' ':
             case '\n':
             case '\r':
             case '\t':
             case '\v':
             case '\f':
                         i++;
                         startOfSuffixString = i;
                         break;
             case ':':
                         i++;
                         if( !isTemporalOperator( formula, i ) )
                             return NULL;
                         startOfSuffixString = i;
                         break;
             case 'G':
                         prevChar = formula[i-1];
                         if( prevChar == ':' ) //i.e. 'G' is a temporal operator
                         {
                             i++;
                             startOfSuffixString = i;
                             temp_node_left = readLtlFormula( formula );
                             if( temp_node_left == NULL )
                                 return NULL;
                             else
                             {
                                 curr_node = generateTypedNode(GLOBALLY);
                                 curr_node->left = temp_node_left;
                                 return curr_node;
                             }
                         }
                         else    //i.e. 'G' must be starting a variable name
                         {
                             varName = getVarName( formula, i, &rememberEnd );
                             if( !varName )
                             {
                                 printf("\nInvalid LTL formula: expecting valid variable name token...aborting" );
                                 return NULL;
                             }
                             curr_node = generateTypedNode(BOOL);
                             curr_node->name = varName;
                             i = rememberEnd;
                             startOfSuffixString = i;
                             return curr_node;
                         }
             case 'F':
                         prevChar = formula[i-1];
                         if( prevChar == ':' ) //i.e. 'F' is a temporal operator
                         {
                             i++;
                             startOfSuffixString = i;
                             temp_node_left = readLtlFormula( formula );
                             if( temp_node_left == NULL )
                                 return NULL;
                             else
                             {
                                 curr_node = generateTypedNode(EVENTUALLY);
                                 curr_node->left = temp_node_left;
                                 return curr_node;
                             }
                         }
                         else //i.e. 'F' must be starting a variable name
                         {
                             varName = getVarName( formula, i, &rememberEnd );
                             if( !varName )
                             {
                                 printf("\nInvalid LTL formula: expecting valid variable name token...aborting" );
                                 return NULL;
                             }
                             curr_node = generateTypedNode(BOOL);
                             curr_node->name = varName;
                             i = rememberEnd;
                             startOfSuffixString = i;
                             return curr_node;
                         }   
             case 'X':
                         prevChar = formula[i-1];
                         if( prevChar == ':' ) //i.e. 'X' is a temporal operator
                         {
                             i++;
                             startOfSuffixString = i;
                             temp_node_left = readLtlFormula( formula );
                             if( temp_node_left == NULL )
                                 return NULL;
                             else
                             {
                                 curr_node = generateTypedNode(NEXT);
                                 curr_node->left = temp_node_left;
                                 return curr_node;
                             }
                         }
                         else //i.e. 'X' must be starting a variable name
                         {
                             varName = getVarName( formula, i, &rememberEnd );
                             if( !varName )
                             {
                                 printf("\nInvalid LTL formula: expecting valid variable name token...aborting" );
                                 return NULL;
                             }
                             curr_node = generateTypedNode(BOOL);
                             curr_node->name = varName;
                             i = rememberEnd;
                             startOfSuffixString = i;
                             return curr_node;
                         }   
             case 'U':
                         prevChar = formula[i-1];
                         if( prevChar == ':' ) //i.e. 'X' is a temporal operator
                         {
                             i++;
                             startOfSuffixString = i;
                             temp_node_left = readLtlFormula( formula );
                             if( temp_node_left == NULL )
                                 return NULL;
                             temp_node_right = readLtlFormula( formula );
                             if( temp_node_right == NULL )
                             {
                                 //need to do memory management: if right subtree is NULL then left
                                 //subtree must be freed.
                                 return NULL;
                             }
                             curr_node = generateTypedNode(UNTIL);
                             curr_node->left = temp_node_left;
                             curr_node->right = temp_node_right;
                             return curr_node;
                         }
                         else //i.e. 'U' must be starting a variable name
                         {
                             varName = getVarName( formula, i, &rememberEnd );
                             if( !varName )
                             {
                                 printf("\nInvalid LTL formula: expecting valid variable name token...aborting" );
                                 return NULL;
                             }
                             curr_node = generateTypedNode(BOOL);
                             curr_node->name = varName;
                             i = rememberEnd;
                             startOfSuffixString = i;
                             return curr_node;
                         }   
             case '+':
                         i++;
                         startOfSuffixString = i;
                         temp_node_left = readLtlFormula( formula );
                         if( temp_node_left == NULL )
                             return NULL;
                         temp_node_right = readLtlFormula( formula );
                         if( temp_node_right == NULL )
                         {
                             //need to do memory management: if right subtree is NULL then left
                             //subtree must be freed.
                             return NULL;
                         }
                         curr_node = generateTypedNode(OR);
                         curr_node->left = temp_node_left;
                         curr_node->right = temp_node_right;
                         return curr_node;
             case '&':
                         i++;
                         startOfSuffixString = i;
                         temp_node_left = readLtlFormula( formula );
                         if( temp_node_left == NULL )
                             return NULL;
                         temp_node_right = readLtlFormula( formula );
                         if( temp_node_right == NULL )
                         {
                             //need to do memory management: if right subtree is NULL then left
                             //subtree must be freed.
                             return NULL;
                         }
                         curr_node = generateTypedNode(AND);
                         curr_node->left = temp_node_left;
                         curr_node->right = temp_node_right;
                         return curr_node;
             case '!':
                         i++;
                         startOfSuffixString = i;
                         temp_node_left = readLtlFormula( formula );
                         if( temp_node_left == NULL )
                             return NULL;
                         else
                         {
                             curr_node = generateTypedNode(NOT);
                             curr_node->left = temp_node_left;
                             return curr_node;
                         }
             default:
                 varName = getVarName( formula, i, &rememberEnd );
                 if( !varName )
                 {
                     printf("\nInvalid LTL formula: expecting valid variable name token...aborting" );
                     return NULL;
                 }
                 curr_node = generateTypedNode(BOOL);
                 curr_node->name = varName;
                 i = rememberEnd;
                 startOfSuffixString = i;
                 return curr_node;
         }
     }
     return NULL;
 }

void resetGlobalVar ( )

Definition at line 361 of file ltl_parser.c.

 {
     startOfSuffixString = 0;
 }

Aig_Obj_t* retriveAIGPointerFromLTLNode ( ltlNode * astNode )

Definition at line 833 of file ltl_parser.c.

 {
     return astNode->pObj;
 }

void setAIGNodePtrOfGloballyNode	(	ltlNode *	astNode,
		Aig_Obj_t *	pObjLo
	)

Definition at line 828 of file ltl_parser.c.

 {
     astNode->pObj = pObjLo;
 }

void traverseAbstractSyntaxTree ( ltlNode * node )

Definition at line 377 of file ltl_parser.c.

 {
     switch(node->type){
         case( AND ):
             printf("& ");
             assert( node->left != NULL );
             assert( node->right != NULL );
             traverseAbstractSyntaxTree( node->left );
             traverseAbstractSyntaxTree( node->right );
             return;
         case( OR ):
             printf("+ ");
             assert( node->left != NULL );
             assert( node->right != NULL );
             traverseAbstractSyntaxTree( node->left );
             traverseAbstractSyntaxTree( node->right );
             return;
         case( NOT ):
             printf("~ ");
             assert( node->left != NULL );
             traverseAbstractSyntaxTree( node->left );
             assert( node->right == NULL );
             return;
         case( GLOBALLY ):
             printf("G ");
             assert( node->left != NULL );
             traverseAbstractSyntaxTree( node->left );
             assert( node->right == NULL );
             return;
         case( EVENTUALLY ):
             printf("F ");
             assert( node->left != NULL );
             traverseAbstractSyntaxTree( node->left );
             assert( node->right == NULL );
             return;
         case( NEXT ):
             printf("X ");
             assert( node->left != NULL );
             traverseAbstractSyntaxTree( node->left );
             assert( node->right == NULL );
             return;
         case( UNTIL ):
             printf("U ");
             assert( node->left != NULL );
             assert( node->right != NULL );
             traverseAbstractSyntaxTree( node->left );
             traverseAbstractSyntaxTree( node->right );
             return;
         case( BOOL ):
             printf("%s ", node->name);
             assert( node->left == NULL );
             assert( node->right == NULL );
             return;
         default:
             printf("\nUnsupported token type: Exiting execution\n");
             exit(0);
     }
 }

void traverseAbstractSyntaxTree_postFix ( ltlNode * node )

Definition at line 436 of file ltl_parser.c.

 {
     switch(node->type){
         case( AND ):
             printf("( ");
             assert( node->left != NULL );
             assert( node->right != NULL );
             traverseAbstractSyntaxTree_postFix( node->left );
             printf("& ");
             traverseAbstractSyntaxTree_postFix( node->right );
             printf(") ");
             return;
         case( OR ):
             printf("( ");
             assert( node->left != NULL );
             assert( node->right != NULL );
             traverseAbstractSyntaxTree_postFix( node->left );
             printf("+ ");
             traverseAbstractSyntaxTree_postFix( node->right );
             printf(") ");
             return;
         case( NOT ):
             printf("~ ");
             assert( node->left != NULL );
             traverseAbstractSyntaxTree_postFix( node->left );
             assert( node->right == NULL );
             return;
         case( GLOBALLY ):
             printf("G ");
             //printf("( ");
             assert( node->left != NULL );
             traverseAbstractSyntaxTree_postFix( node->left );
             assert( node->right == NULL );
             //printf(") ");
             return;
         case( EVENTUALLY ):
             printf("F ");
             //printf("( ");
             assert( node->left != NULL );
             traverseAbstractSyntaxTree_postFix( node->left );
             assert( node->right == NULL );
             //printf(") ");
             return;
         case( NEXT ):
             printf("X ");
             assert( node->left != NULL );
             traverseAbstractSyntaxTree_postFix( node->left );
             assert( node->right == NULL );
             return;
         case( UNTIL ):
             printf("( ");
             assert( node->left != NULL );
             assert( node->right != NULL );
             traverseAbstractSyntaxTree_postFix( node->left );
             printf("U ");
             traverseAbstractSyntaxTree_postFix( node->right );
             printf(") ");
             return;
         case( BOOL ):
             printf("%s ", node->name);
             assert( node->left == NULL );
             assert( node->right == NULL );
             return;
         default:
             printf("\nUnsupported token type: Exiting execution\n");
             exit(0);
     }
 }

Variable Documentation

int startOfSuffixString = 0

Definition at line 114 of file ltl_parser.c.

Data Structures

Typedefs

Enumerations

Functions

Variables

Typedef Documentation

Enumeration Type Documentation

Function Documentation

Variable Documentation