fixed readme

ianno · Nov 5, 2014 · 28a2738 · 28a2738
1 parent b266dc7
commit 28a2738
Showing 1 changed file with 9 additions and 0 deletions.
diff --git a/README.md b/README.md
@@ -11,6 +11,15 @@ The LTL properties are:
 3. [](count == 0) -> <>(state == OFF)
 4. []( (state == HOLD) -> ((x != DISABLE) && (x != RESUME) )) -> <>(state == STANDBY) 
 
+To compile and verify the model you can use 'ispin' (SPIN graphical environment),
+or, using the command line, with:
+
+- spin -a cruise.pml
+- gcc -o pan pan.c
+- ./pan -N p1 (for property p1)
+- ./pan -N p2 (for property p2)
+- ...
+
 Author: Antonio Iannopollo
 Email: [email protected]