- Timestamp:
- Jan 8, 2012, 5:12:00 PM (13 years ago)
- Location:
- vis_dev
- Files:
-
- 10 edited
Legend:
- Unmodified
- Added
- Removed
-
vis_dev/cusp-1.1/configure
r12 r40 4815 4815 # loading this file, other *unset* `ac_cv_foo' will be assigned the 4816 4816 # following values. 4817 4818 _ACEOF 4819 4817 _ACEOF 4818 4819 echo "lala" 4820 4820 # The following way of writing the cache mishandles newlines in values, 4821 4821 # but we know of no workaround that is simple, portable, and efficient. -
vis_dev/cusp-1.1/helpers/mkinstalldirs
r13 r40 6 6 7 7 errstatus=0 8 dirmode=". "8 dirmode="./" 9 9 10 10 usage="\ -
vis_dev/vis-2.3/models/debug/test.script
r38 r40 1 1 rlmv and2.mv 2 2 init 3 #_createAbn3 _createAbn 4 4 aig 5 5 _sat_debug -k 1 -p and2.ltl -o and2_prop.cnf -v 1 -
vis_dev/vis-2.3/models/transition/f.ctl
r28 r40 1 1 !EX(state[1:0] = 1); 2 EX(state[1:0] = 3); -
vis_dev/vis-2.3/models/transition/script
r31 r40 2 2 init 3 3 compute_reach -v 1 4 _transition 4 _transition -v 1 -
vis_dev/vis-2.3/src/debug/debug.c
r38 r40 296 296 return 1; 297 297 } 298 298 299 /* 299 300 We need the bdd when building the transition relation of the automaton … … 308 309 } 309 310 } 310 311 Dbg_Abnormal_t * abn = Dbg_NetworkReadAbnormal(network); 312 printf("abnormal %d \n",array_n(Dbg_ReadAbn(abn))); 311 313 /* 312 314 * Read the formula … … 394 396 int l; 395 397 // return the clause number 396 int noLoopIndex = BmcGenerateCnfForLtl(network, ltlFormula, 0, k, -1, cnfClauses);398 int noLoopIndex = BmcGenerateCnfForLtl(network, ltlFormula, 0, k, k, cnfClauses); 397 399 398 400 int leftValue = checkIndex(noLoopIndex, cnfClauses); 399 401 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 444 410 445 411 -
vis_dev/vis-2.3/src/debug/debug.h
r36 r40 55 55 /* Constant declarations */ 56 56 /*---------------------------------------------------------------------------*/ 57 57 #define DBG_NETWORK_APPL_KEY "Dbg_NetworkApplKey" 58 58 59 59 /*---------------------------------------------------------------------------*/ … … 124 124 EXTERN void Debug_End(void); 125 125 EXTERN Dbg_Abnormal_t * Dbg_DebugAbnormalAlloc(Ntk_Network_t * network); 126 EXTERN void Dbg_DebugAbnormalFree(Dbg_Abnormal_t * abn); 126 EXTERN void Dbg_DebugAbnormalFree(Dbg_Abnormal_t * abn); 127 EXTERN void Dbg_AbnormalFreeCallback(void *data); 127 128 EXTERN void Dbg_AddAbnormalPredicatetoNetwork(Dbg_Abnormal_t* abnormal); 128 129 EXTERN void Dbg_AddAbnormalPredicate(Dbg_Abnormal_t * abn, Ntk_Node_t* abnNode); … … 130 131 EXTERN array_t* Dbg_ReadFreeInputs(Dbg_Abnormal_t *abnormal); 131 132 EXTERN array_t* Dbg_ReadAbn(Dbg_Abnormal_t *abnormal); 133 EXTERN Dbg_Abnormal_t * Dbg_NetworkReadAbnormal(Ntk_Network_t * network); 132 134 /**AutomaticEnd***************************************************************/ 133 135 -
vis_dev/vis-2.3/src/debug/debugAbnormal.c
r36 r40 114 114 } 115 115 } 116 Ntk_NetworkAddApplInfo(ntk, DBG_NETWORK_APPL_KEY, 117 (Ntk_ApplInfoFreeFn) Dbg_AbnormalFreeCallback, 118 (void *) abnormal); 116 119 } 117 120 /**Function******************************************************************** … … 157 160 FREE(abn); 158 161 } 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 ******************************************************************************/ 176 void 177 Dbg_AbnormalFreeCallback( 178 void *data) 179 { 180 Dbg_DebugAbnormalFree((Dbg_Abnormal_t *) data); 181 } /* End of Part_PartitionFreeCallback */ 159 182 160 183 … … 227 250 return abnormal->abnormal; 228 251 } 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 ******************************************************************************/ 263 Dbg_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 1039 1039 mAig_quit(network->mAigManager); 1040 1040 } 1041 1042 1041 FREE(network); 1043 1042 }
Note: See TracChangeset
for help on using the changeset viewer.