FILES in p1/random boolean concurrent programs:
===============================================

The files are named ABCDEF.vvm and ABCDEF.smv
which are supposed to represent the same verication problem for 
a given ABCDEF in this subdirectory.

The files with .vvm in the extension is in the input format 
of the model verifier VERDS, and the files with .smv in the 
extension is in the input format of the model verifier NuSMV.

The meaning of the string ABCDEF in the file name in p1 is as follows.
AB   is the number of the property in the model;
CD*6 is the number of boolean variables in the model;
EF   is the sequence number of the randomly generated program;

FILES in p2/random boolean concurrent sequential programs:
==========================================================

The files are named ABCDEF.vvm and ABCDEF.smv
which are supposed to represent the same verication problem for 
a given ABCDEF in this subdirectory.

The files with .vvm in the extension is in the input format 
of the model verifier VERDS, and the files with .smv in the 
extension is in the input format of the model verifier NuSMV.

The meaning of the string ABCDEF in the file name in p2 is as follows.
AB   is the number of the property in the model;
CD*4 is the number of boolean variables in the model;
EF   is the sequence number of the randomly generated program;

