DYNAMO Para Tools Instructions

Set up

To run this demo you need the following files:

  • Demo.argo
  • Demo_client.pgml
  • Demo_server.pgml
  • Demo_usecasediagram1.pgml
  • Demo.xmi
  • Demo.ctl
  • uml13.dtd
  • stripcr.sh

    • These files are available for download here.  

    This demo requires running executables of Argo Uml, SMV model checker, ParaGen, and Para2Smv.   These executables are available from the Dynamo Tools download page.

    uml13.dtd needs to be in the same directory as the xmi file.

    If you are using Windows, xerces-c_1_4D.dll needs to be in the same directory as the ParaGen executable.

    If you are using Solaris, include libxerces-c1_3.so in the same directory as the ParaGen executable.

    It may be necessary to set your LD_LIBRARY_PATH to the directory where these libraries are included.

    Running ParaTools

    1. Start ArgoUML. Open the Demo.argo file. This example is a client-server. It has two classes. Argo UML saves the Demo example in two forms, Demo.argo and Demo.xmi. Demo.xmi is the generated xmi file we will need for the rest of our demonstration.
    2. ParaGen parses the xmi file into an intermediate "para" file. To display the results to the screen type "ParaGen Demo.xmi". To write this output to a file type "ParaGen Demo.xmi > Demo.out". Demo.out is the pre-generated para file.
    3. If you are running these executables under windows it may be necessary to remove carriage returns from your Demo.out file before continuing. stripcr.sh is a shell script necessary for this task. To run the script type "sh stripcr.sh Demo.out" and you will get a file called Demo.out.nocr.
    4. Now it's time to automatically generate the input for the SMV model checker. If you skipped the procedure 4, then type "Para2SMV -c Demo.CTL Demo.out". If you didn't skip the procedure, then "Para2SMV -c Demo.ctl Demo.out.nocr". This automatically combines the model information from the UML diagram and the CTL information from Demo.ctl. The resulting file is called Demo.smv.
    5. To run the SMV model checker on the file, just type "smv Demo.smv".

    Point of Contact

    dynamo-support@cc.gatech.edu
    Last modified: Mon Mar 11 13:42:43 EST 2002