From 28a2738f3e15b2381cbd76feaa3a74514f469fef Mon Sep 17 00:00:00 2001 From: Antonio Iannopollo Date: Wed, 5 Nov 2014 11:21:10 -0800 Subject: [PATCH] fixed readme --- README.md | 9 +++++++++ 1 file changed, 9 insertions(+) diff --git a/README.md b/README.md index 079fb3b..eb03b3a 100644 --- 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: antonio@berkeley.edu