/**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 $]
***********************************************************************/
#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"
ABC_NAMESPACE_IMPL_START
enum ltlToken { AND, OR, NOT, IMPLY, GLOBALLY, EVENTUALLY, NEXT, UNTIL, BOOL };
enum ltlGrammerToken { OPERAND, LTL, BINOP, UOP };
typedef enum ltlToken tokenType;
typedef enum ltlGrammerToken ltlGrammerTokenType;
struct ltlNode_t
{
tokenType type;
char *name;
Aig_Obj_t *pObj;
struct ltlNode_t *left;
struct ltlNode_t *right;
};
typedef struct ltlNode_t ltlNode;
ltlNode *generateTypedNode( tokenType new_type )
//void generateTypedNode( ltlNode *new_node, tokenType new_type )
{
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;
}
Aig_Obj_t *buildLogicFromLTLNode_combinationalOnly( Aig_Man_t *pAig, ltlNode *pLtlNode );
static inline int isNotVarNameSymbol( char c )
{
return ( c == ' ' || c == '\t' || c == '\n' || c == ':' || c == '\0' );
}
void Abc_FrameCopyLTLDataBase( Abc_Frame_t *pAbc, Abc_Ntk_t * pNtk )
{
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 );
}
}
char *getVarName( char *suffixFormula, int startLoc, int *endLocation )
{
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 startOfSuffixString = 0;
int isUnexpectedEOS( char *formula, int index )
{
assert( formula );
if( index >= (int)strlen( formula ) )
{
printf("\nInvalid LTL formula: unexpected end of string..." );
return 1;
}
return 0;
}
int isTemporalOperator( char *formula, int index )
{
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;
}
ltlNode *readLtlFormula( char *formula )
{
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()
{
startOfSuffixString = 0;
}
ltlNode *parseFormulaCreateAST( char *inputFormula )
{
ltlNode *temp;
temp = readLtlFormula( inputFormula );
//if( temp == NULL )
// printf("\nAST creation failed for formula %s", inputFormula );
resetGlobalVar();
return temp;
}
void traverseAbstractSyntaxTree( ltlNode *node )
{
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 )
{
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);
}
}
void populateAigPointerUnitGF( Aig_Man_t *pAigNew, ltlNode *topASTNode, Vec_Ptr_t *vSignal, Vec_Vec_t *vAigGFMap )
{
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);
}
}
Aig_Obj_t *buildLogicFromLTLNode_combinationalOnly( Aig_Man_t *pAigNew, ltlNode *pLtlNode )
{
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);
}
}
}
Aig_Obj_t *buildLogicFromLTLNode( Aig_Man_t *pAig, ltlNode *pLtlNode )
{
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);
}
}
}
int isNonTemporalSubformula( ltlNode *topNode )
{
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;
}
}
int isWellFormed( ltlNode *topNode )
{
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;
}
}
int checkBooleanConstant( char *targetName )
{
if( strcmp( targetName, "true" ) == 0 )
return 1;
if( strcmp( targetName, "false" ) == 0 )
return 0;
return -1;
}
int checkSignalNameExistence( Abc_Ntk_t *pNtk, ltlNode *topASTNode )
{
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);
}
}
void populateBoolWithAigNodePtr( Abc_Ntk_t *pNtk, Aig_Man_t *pAigOld, Aig_Man_t *pAigNew, ltlNode *topASTNode )
{
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);
}
}
int checkAllBoolHaveAIGPointer( ltlNode *topASTNode )
{
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);
}
}
void setAIGNodePtrOfGloballyNode( ltlNode *astNode, Aig_Obj_t *pObjLo )
{
astNode->pObj = pObjLo;
}
Aig_Obj_t *retriveAIGPointerFromLTLNode( ltlNode *astNode )
{
return astNode->pObj;
}
ABC_NAMESPACE_IMPL_END