Changeset 15 for vis_dev/vis-2.3

Timestamp:

Jul 13, 2011, 11:05:09 AM (13 years ago)

Author:

cecile

Message:

Vis main file for expermeriments

Location:

vis_dev/vis-2.3

Files:

• Makefile.in (modified) (1 diff)
• src/bmc/bmcCmd.c (modified) (2 diffs)
• src/fsm/fsmInt.h (modified) (1 diff)
• src/fsm/fsmReach.c (modified) (2 diffs)
• src/vm/vmInit.c (modified) (2 diffs)

vis_dev/vis-2.3/Makefile.in

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

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

@@ -46 +46 @@
 /*---------------------------------------------------------------------------*/
 
-static BmcOption_t * ParseBmcOptions(int argc, char **argv);
+/*static*/ BmcOption_t * ParseBmcOptions(int argc, char **argv);
 static int CommandBmc(Hrc_Manager_t ** hmgr, int argc, char ** argv);
 static void TimeOutHandle(void);
@@ -104 +104 @@
 
 ******************************************************************************/
-static BmcOption_t *
+/*static*/ BmcOption_t *
 ParseBmcOptions(
   int argc,

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

@@ -180 +180 @@
     boolean createVarCubesFlag;
   } fsmData;
+
+    // For robustness computation
+  struct {
+    mdd_t * originalreachableStates;
+    mdd_t * Safe; FILE* fSafe;
+    mdd_t * Forb; FILE* fForb;
+    mdd_t * Req;  FILE* fReq;
+  } RobSets;
+
 };
 

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

@@ -65 +65 @@
 
 static int CheckImageValidity(mdd_manager *mddManager, mdd_t *image, array_t *domainVarMddIdArray, array_t *quantifyVarMddIdArray);
-static int ComputeNumberOfBinaryStateVariables(mdd_manager *mddManager, array_t *mddIdArray);
+/*static*/ int ComputeNumberOfBinaryStateVariables(mdd_manager *mddManager, array_t *mddIdArray);
 static mdd_t * AddStates(mdd_t *a, mdd_t *b, int freeA, int freeB);
 static void RandomSimulation(int simNVec, Fsm_Fsm_t *fsm, Fsm_RchType_t approxFlag, mdd_t *initialStates, mdd_t **reachableStates, mdd_t **fromLowerBound, FsmHdStruct_t *hdInfo);
@@ -1162 +1162 @@
 
 ******************************************************************************/
-static int
+/*static*/ int
 ComputeNumberOfBinaryStateVariables(mdd_manager *mddManager,
                                array_t *mddIdArray)

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

@@ -105 +105 @@
   Bmc_Init();
   PureSat_Init();
+  Rob_Init();
 }
 
@@ -154 +155 @@
   ntmaig_End();
   Bmc_End();
-
+  Rob_End();
   if (vis_stdout != stdout) {  
     (void) fclose(vis_stdout);