Compiling.rar contains the following executable files: 1. FPTA.tab.exe: compile .xml files into .obj, which can be used by both version of verifiers. 2. prop.tab.exe: compile property files and append it to the compiled files for the model. 3. ProcessInfo.exe: input model description. 4. CJ60lib.dll: the dynamic link library for the verifier with SDS structure. General instructions for model verification: 1. Write a .xml or .txt file to describe the processes of the model. 2. Compile the file by the menu of the verifier. 3. Write a property file to explain what will be verified. 4. Compile the property file by the menu of the verifier. 5. Verify the model by .obj files, statistic information will be output by files and dialogs.