Changeset 15 for vis_dev/vis-2.3/src/fsm

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/src/fsm

Files:

• fsmInt.h (modified) (1 diff)
• fsmReach.c (modified) (2 diffs)

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)