| 69 | | == Running CIVL == |
| 70 | | 1. Somewhere on your system, create a plain text file containing exactly the following two lines: |
| | 69 | == Running CIVL from command line == |
| | 70 | 1. We will create a script that will sit on your `PATH` that will allow you to conveniently run `CIVL` from the `.class` files built in Eclipse. |
| | 71 | 1. Create two new environment variables: |
| | 72 | * `ECLIPSE_WORKSPACE` should be the path to your Eclipse workspace folder. |
| | 73 | * `VSL_DEPS` should be the path to your `vsl-X.XX` dependencies folder. |
| | 74 | 1. Somewhere on your system, create a plain text file named `civl` containing exactly the following two lines: |
| 75 | | where {{{/Path/To/Your/workspace}}} is replaced with the path to your Eclipse workspace directory. Name this file `civl`, put it in your `PATH`, and make it executable (`chmod ugo+x civl`). Alternatively, you can define an alias in your `.profile`, `.bash_profile`, `.bashrc`, or equivalent: |
| 76 | | {{{ |
| 77 | | alias civl='java -jar /Path/To/Your/workspace/CIVL/civl.jar' |
| 78 | | }}} |
| 79 | | 1. From the shell (terminal window), execute `civl config`. This should find the theorem provers in your `PATH` and create a file `.sarl` in your home directory. |
| 80 | | 1. In Eclipse, navigate to "Run->Run Configurations... Create a new JUnit configuration." Name it "CIVL Regression Tests". Select "Run all tests in the selected project..." and navigate to the folder `test/regress` in the CIVL project. The Test runner should be JUnit 4. Under the Arguments tab, type `-ea` in the VM arguments area (to enable assertion checking). |
| 81 | | 1. An example of how to set up a single test from within Eclipse: \\ create a new Run Configuration via the Run->Run Configurations... menu. Create a new "Java Application" configuration. Call it `CIVLbarrier2`. The Project is CIVL. The main class is `edu.udel.cis.vsl.civl.CIVL`. Under the Arguments tab, set the Program arguments to `verify examples/concurrency/barrier2.cvl`. Modify the VM arguments as in the step above. You should now be able to run the test by clicking "Run". |
| | 79 | 1. Make it executable with the command `chmod ugo+x civl`. |
| | 80 | 1. Move this file to somewhere on your `PATH`. |
| | 81 | 1. Run `civl help` from the command line to ensure that it worked. You should get a long list of command line options that CIVL accepts. \\\\ |
| | 82 | 1. Execute the command `civl config`. This should find the theorem provers in your `PATH` and create a file `.sarl` in your home directory. You can now run `civl` from the command line. Go to the example files found in `dev.civl.com/examples` and try running `civl verify` on some of them! |
| | 83 | |
| | 84 | == Running CIVL from within Eclipse == |
| | 85 | 1. In Eclipse, navigate to "Run->Run Configurations... Create a new JUnit configuration." Name it "CIVL Regression Tests". Select "Run all tests in the selected project..." and navigate to the folder `test/regress` in the CIVL project. The Test runner should be JUnit 4. Under the Arguments tab, type `-ea` in the VM arguments area (to enable assertion checking). \\\\ |
| | 86 | 1. An example of how to set up a single test from within Eclipse: \\ create a new Run Configuration via the Run->Run Configurations... menu. Create a new "Java Application" configuration. Call it `CIVLbarrier2`. The Project is `dev.civl.mc`. The main class is `dev.civl.mc.CIVL`. Under the Arguments tab, set the Program arguments to `verify examples/concurrency/barrier2.cvl`. Modify the VM arguments as in the step above. You should now be able to run the test by clicking "Run". |
