+
+To generate those results, we actually need to pass a specific option to the
+scfence analysis, as follows.
+
+*******************************************************
+peizhaoo@dw-2:~/model-checker$ ./run.sh mcs-lock/testcase1 -m2 -b100 -y -tSCFENCE -o m
+*******************************************************
+
+The '-b100' is to terminate the execution in case of infinite loops because of
+improper synchronization at the beginning period. The 'm' option for SCFENCE
+analysis is to turn on the implyMO mode.