Changeset 15 for vis_dev


Ignore:
Timestamp:
Jul 13, 2011, 11:05:09 AM (13 years ago)
Author:
cecile
Message:

Vis main file for expermeriments

Location:
vis_dev
Files:
5 added
7 edited

Legend:

Unmodified
Added
Removed

  • vis_dev/glu-2.3/src/array/array.c

    r13 r15  
    6565    }
    6666    (void) memcpy(newa->space, old->space, old->num * old->obj_size);
     67    return newa;
     68}
     69
     70array_t *
     71array_partial_dup(array_t *old, int i)
     72{
     73    array_t *newa;
     74
     75    newa = ALLOC(array_t, 1);
     76    if (newa == NIL(array_t)) {
     77        return NIL(array_t);
     78    }
     79    newa->num = old->num - 1;
     80    newa->n_size = old->num - 1;
     81    newa->obj_size = old->obj_size;
     82    newa->index = -newa->obj_size;
     83    newa->space = ALLOC(char, newa->n_size * newa->obj_size);
     84    if (newa->space == NIL(char)) {
     85        FREE(newa);
     86        return NIL(array_t);
     87    }
     88    if (i > 0)
     89      (void) memcpy(newa->space, old->space, i * old->obj_size);
     90    if (i < old->num - 1)
     91      (void) memcpy(newa->space + ((i) * old->obj_size),
     92                    old->space + ((i+1) * old->obj_size), (old->num - (i + 1)) * old->obj_size);
    6793    return newa;
    6894}

  • vis_dev/glu-2.3/src/array/array.h

    r13 r15  
    3434EXTERN int array_resize ARGS((array_t *, int));
    3535EXTERN char *array_do_data ARGS((array_t *));
     36EXTERN array_t * array_partial_dup(array_t *old, int i);
    3637
    3738extern int unsigned array_global_index;

  • vis_dev/vis-2.3/Makefile.in

    r14 r15  
    9494#----------------------------------------------------------------------
    9595
    96 ALL_PKGS = abs amc baig bmc cmd ctlp ctlsp eqv fsm grab hrc imc img io ltl \
     96ALL_PKGS = abs amc baig bmc cmd ctlp ctlsp eqv fsm rob grab hrc imc img io ltl \
    9797        maig mark mc mvf mvfaig ntk ntm ntmaig ord part puresat rst res restr \
    9898        rt sat sim spfd synth tbl truesim tst var vm

  • vis_dev/vis-2.3/src/bmc/bmcCmd.c

    r14 r15  
    4646/*---------------------------------------------------------------------------*/
    4747
    48 static BmcOption_t * ParseBmcOptions(int argc, char **argv);
     48/*static*/ BmcOption_t * ParseBmcOptions(int argc, char **argv);
    4949static int CommandBmc(Hrc_Manager_t ** hmgr, int argc, char ** argv);
    5050static void TimeOutHandle(void);
    … …  
    104104
    105105******************************************************************************/
    106 static BmcOption_t *
     106/*static*/ BmcOption_t *
    107107ParseBmcOptions(
    108108  int argc,

  • vis_dev/vis-2.3/src/fsm/fsmInt.h

    r14 r15  
    180180    boolean createVarCubesFlag;
    181181  } fsmData;
     182
     183    // For robustness computation
     184  struct {
     185    mdd_t * originalreachableStates;
     186    mdd_t * Safe; FILE* fSafe;
     187    mdd_t * Forb; FILE* fForb;
     188    mdd_t * Req;  FILE* fReq;
     189  } RobSets;
     190
    182191};
    183192

  • vis_dev/vis-2.3/src/fsm/fsmReach.c

    r14 r15  
    6565
    6666static int CheckImageValidity(mdd_manager *mddManager, mdd_t *image, array_t *domainVarMddIdArray, array_t *quantifyVarMddIdArray);
    67 static int ComputeNumberOfBinaryStateVariables(mdd_manager *mddManager, array_t *mddIdArray);
     67/*static*/ int ComputeNumberOfBinaryStateVariables(mdd_manager *mddManager, array_t *mddIdArray);
    6868static mdd_t * AddStates(mdd_t *a, mdd_t *b, int freeA, int freeB);
    6969static void RandomSimulation(int simNVec, Fsm_Fsm_t *fsm, Fsm_RchType_t approxFlag, mdd_t *initialStates, mdd_t **reachableStates, mdd_t **fromLowerBound, FsmHdStruct_t *hdInfo);
    … …  
    11621162
    11631163******************************************************************************/
    1164 static int
     1164/*static*/ int
    11651165ComputeNumberOfBinaryStateVariables(mdd_manager *mddManager,
    11661166                               array_t *mddIdArray)

  • vis_dev/vis-2.3/src/vm/vmInit.c

    r14 r15  
    105105  Bmc_Init();
    106106  PureSat_Init();
     107  Rob_Init();
    107108}
    108109
    … …  
    154155  ntmaig_End();
    155156  Bmc_End();
    156 
     157  Rob_End();
    157158  if (vis_stdout != stdout) { 
    158159    (void) fclose(vis_stdout);
Note: See TracChangeset for help on using the changeset viewer.