Changeset 40 for vis_dev


Ignore:
Timestamp:
Jan 8, 2012, 5:12:00 PM (13 years ago)
Author:
cecile
Message:

abnormal structure in network

Location:
vis_dev
Files:
10 edited

Legend:

Unmodified
Added
Removed
  • vis_dev/cusp-1.1/configure

    r12 r40  
    48154815# loading this file, other *unset* `ac_cv_foo' will be assigned the
    48164816# following values.
    4817 
    4818 _ACEOF
    4819 
     4817_ACEOF
     4818
     4819echo "lala"
    48204820# The following way of writing the cache mishandles newlines in values,
    48214821# but we know of no workaround that is simple, portable, and efficient.
  • vis_dev/cusp-1.1/helpers/mkinstalldirs

    r13 r40  
    66
    77errstatus=0
    8 dirmode="."
     8dirmode="./"
    99
    1010usage="\
  • vis_dev/vis-2.3/models/debug/test.script

    r38 r40  
    11rlmv and2.mv
    22init
    3 #_createAbn
     3_createAbn
    44aig
    55_sat_debug  -k 1 -p and2.ltl -o and2_prop.cnf -v 1 
  • vis_dev/vis-2.3/models/transition/f.ctl

    r28 r40  
    11!EX(state[1:0] = 1);
     2EX(state[1:0] = 3);
  • vis_dev/vis-2.3/models/transition/script

    r31 r40  
    22init
    33compute_reach -v 1
    4 _transition
     4_transition -v 1
  • vis_dev/vis-2.3/src/debug/debug.c

    r38 r40  
    296296    return 1;
    297297  }
     298
    298299  /*
    299300    We need the bdd when building the transition relation of the automaton
     
    308309    }
    309310  }
    310 
     311Dbg_Abnormal_t * abn = Dbg_NetworkReadAbnormal(network);
     312printf("abnormal %d \n",array_n(Dbg_ReadAbn(abn)));
    311313/*
    312314 * Read the formula
     
    394396    int l;
    395397    // return the clause number
    396     int noLoopIndex = BmcGenerateCnfForLtl(network, ltlFormula, 0, k, -1, cnfClauses);
     398    int noLoopIndex = BmcGenerateCnfForLtl(network, ltlFormula, 0, k, k, cnfClauses);
    397399   
    398400    int leftValue   = checkIndex(noLoopIndex, cnfClauses);
    399401    printf("noLoopIndex %d , leftValue %d \n", noLoopIndex,leftValue);
    400     int rightValue,loop,andIndex;
    401     array_t           *orClause = NIL(array_t);
    402     array_t           *loopClause, *tmpclause;
    403 
    404     if (leftValue != 1) {
    405       orClause = array_alloc(int, 0);   
    406       if (leftValue == -1){
    407             array_insert_last(int, orClause, noLoopIndex);
    408       }
    409       loopClause = array_alloc(int, k+1);
    410       for(l=0; l<=k; l++){
    411             int loopIndex = BmcGenerateCnfForLtl(network, ltlFormula, 0, k, l, cnfClauses);
    412             rightValue = checkIndex(loopIndex, cnfClauses);
    413           if (rightValue == 0){
    414             break;
    415           }
    416       if (rightValue !=0){
    417             loop = cnfClauses->cnfGlobalIndex++;
    418             BmcCnfGenerateClausesFromStateToState(network, k, l, cnfClauses,
    419                                                 nodeToMvfAigTable, CoiTable, loop);
    420           array_insert(int, loopClause, l, loop);
    421           if(rightValue == -1){
    422            
    423             andIndex   = cnfClauses->cnfGlobalIndex++;
    424             tmpclause  = array_alloc(int, 2);
    425             array_insert(int, tmpclause, 0, loop);
    426             array_insert(int, tmpclause, 1, -andIndex);
    427             BmcCnfInsertClause(cnfClauses, tmpclause);
    428 
    429             array_insert(int, tmpclause, 0, loopIndex);
    430             array_insert(int, tmpclause, 1, -andIndex);
    431             BmcCnfInsertClause(cnfClauses, tmpclause);
    432         array_free(tmpclause);
    433             array_insert_last(int, orClause, andIndex);
    434       }
    435       else {
    436             array_insert_last(int, orClause, loop);
    437           }
    438       }} // for l loop
    439       }
    440        BmcCnfInsertClause(cnfClauses, orClause);
    441         array_free(orClause);
    442 
    443 
     402        array_t           *objClause = NIL(array_t);
     403        objClause = array_alloc(int, 0);   
     404        array_insert_last(int, objClause, noLoopIndex);
     405        BmcCnfInsertClause(cnfClauses, objClause);
     406    array_free(objClause);
     407
     408       
     409//TODO Add abnormal formula
    444410
    445411
  • vis_dev/vis-2.3/src/debug/debug.h

    r36 r40  
    5555/* Constant declarations                                                     */
    5656/*---------------------------------------------------------------------------*/
    57 
     57#define DBG_NETWORK_APPL_KEY "Dbg_NetworkApplKey"
    5858
    5959/*---------------------------------------------------------------------------*/
     
    124124EXTERN void Debug_End(void);
    125125EXTERN Dbg_Abnormal_t * Dbg_DebugAbnormalAlloc(Ntk_Network_t * network);
    126 EXTERN void  Dbg_DebugAbnormalFree(Dbg_Abnormal_t * abn);
     126EXTERN void Dbg_DebugAbnormalFree(Dbg_Abnormal_t * abn);
     127EXTERN void Dbg_AbnormalFreeCallback(void *data);
    127128EXTERN void Dbg_AddAbnormalPredicatetoNetwork(Dbg_Abnormal_t* abnormal);
    128129EXTERN void Dbg_AddAbnormalPredicate(Dbg_Abnormal_t * abn, Ntk_Node_t* abnNode);
     
    130131EXTERN array_t* Dbg_ReadFreeInputs(Dbg_Abnormal_t *abnormal);
    131132EXTERN array_t* Dbg_ReadAbn(Dbg_Abnormal_t *abnormal);
     133EXTERN Dbg_Abnormal_t * Dbg_NetworkReadAbnormal(Ntk_Network_t * network);
    132134/**AutomaticEnd***************************************************************/
    133135
  • vis_dev/vis-2.3/src/debug/debugAbnormal.c

    r36 r40  
    114114        }
    115115}
     116 Ntk_NetworkAddApplInfo(ntk, DBG_NETWORK_APPL_KEY,
     117 (Ntk_ApplInfoFreeFn) Dbg_AbnormalFreeCallback,
     118 (void *) abnormal);
    116119}
    117120/**Function********************************************************************
     
    157160         FREE(abn);
    158161}       
     162/**Function********************************************************************
     163
     164  Synopsis    [Call-back function to free an abnormal structure.]
     165
     166  Description [This function will be stored in the network together with the
     167  pointer to the structure. Whenever the network deletes the partitioning
     168  information, this function is called and it will deallocate the abnormal and
     169  the information attached to it.]
     170
     171  SideEffects []
     172
     173  SeeAlso     [Ntk_NetworkAddApplInfo]
     174
     175******************************************************************************/
     176void
     177Dbg_AbnormalFreeCallback(
     178   void *data)
     179{
     180  Dbg_DebugAbnormalFree((Dbg_Abnormal_t *) data);
     181} /* End of Part_PartitionFreeCallback */
    159182
    160183
     
    227250        return abnormal->abnormal;
    228251}
    229 
     252/**Function********************************************************************
     253 
     254  Synopsis    [returns the abnormal structure]
     255
     256  Description [returns the abnormal structure associated to the network]
     257
     258  SideEffects []
     259
     260  SeeAlso     []
     261
     262******************************************************************************/
     263Dbg_Abnormal_t * Dbg_NetworkReadAbnormal(Ntk_Network_t * network)
     264{
     265        Dbg_Abnormal_t * abn = (Dbg_Abnormal_t *) Ntk_NetworkReadApplInfo(network, DBG_NETWORK_APPL_KEY);
     266
     267        return abn;
     268}
  • vis_dev/vis-2.3/src/ntk/ntkNtk.c

    r14 r40  
    10391039    mAig_quit(network->mAigManager);
    10401040  }
    1041 
    10421041  FREE(network);
    10431042}
Note: See TracChangeset for help on using the changeset viewer.