randomly initialize seed

diff --git a/Robust/src/Runtime/runtime.c b/Robust/src/Runtime/runtime.c
index 8a0ecbac3da1186cfc72a819a309a9fee4867b7d..0a804eba1ae88f45fa71b259b9c504045578a7c4 100644 (file)
--- a/Robust/src/Runtime/runtime.c
+++ b/Robust/src/Runtime/runtime.c
@@ -72,7 +72,6 @@ void processOptions() {
       if (options==NULL)
        break;
 
-
       sscanf(options, "%f", &instfailurechance);
       options=strchr(options,' ');
       if (options!=NULL) options++;
@@ -94,6 +93,11 @@ void processOptions() {
       if (options!=NULL) options++;
       debugtask=1;
       printf("Debug task option on.\n");
+    } else if (strncmp(options, "-initializerandom", sizeof("-initializerandom")-1)==0) {
+      options=strchr(options,' ');
+      if (options!=NULL) options++;
+      printf("Initializing random number generator.\n");
+      srandomdev();
     } else
       break;
   }