added model

README.md

@@ -1,4 +1,16 @@
 eecs149_spin
 ============
+SPIN model inspired by the Cruise control state machine used in UC Berkeley 
+EECS 149/249 (Fall 2014) midterm 1.
+The model sets a simple state machine, a non-deterministic environment and
+a set of 4 LTL properties are verified.
+
+The LTL properties are:
+1. (x == ENABLE) -> <> (state == OFF) 
+2. []((x == DISABLE) -> <>(state == OFF)) 
+3. [](count == 0) -> <>(state == OFF)
+4. []( (state == HOLD) -> ((x != DISABLE) && (x != RESUME) )) -> <>(state == STANDBY) 
+
+Author: Antonio Iannopollo
+Email: [email protected]
 
-Fall 2014 EECS 149/249 spin tutorial model

cruise.pml

@@ -0,0 +1,88 @@
+/*
+* SPIN model inspired by the Cruise control state machine used in UC Berkeley 
+* EECS 149/249 (Fall 2014) midterm 1.
+* The model sets a simple state machine, a non-deterministic environment and
+* a set of 4 LTL properties are verified.
+*
+* Author: Antonio Iannopollo
+*/
+
+//definition of input values
+mtype = {ENABLE, SET, CANCEL, BRAKE, RESUME, DISABLE};
+//state definition
+mtype = {OFF, STANDBY, CRUISE, HOLD};
+
+//state machine variables
+mtype state = OFF;
+byte count = 0;
+mtype x = SET;
+
+//communication channel
+chan input = [0] of {mtype};
+
+/*
+* Non-deterministic environment
+*/
+active proctype Environment() {
+    do
+        ::if
+            :: input ! ENABLE;
+            :: input ! SET;
+            :: input ! CANCEL;
+            :: input ! BRAKE;
+            :: input ! RESUME;
+            :: input ! DISABLE;
+        fi;
+        //or equivalently
+        //select(x : DISABLE .. ENABLE);
+    od;
+}
+
+/*
+* Cruise control state machine
+*/
+active proctype Cruise() {
+    do
+        :: atomic { input ? x ->
+            if 
+                :: (state == OFF) && (x == ENABLE) -> 
+                  count = 0; state = STANDBY;
+                :: (state == STANDBY) && (x == DISABLE) ->
+                    state = OFF;
+                :: (state == STANDBY) && (x == SET) ->
+                    state = CRUISE;
+                :: (state == CRUISE) && (x == DISABLE) ->
+                    state = OFF;
+                :: (state == CRUISE) && (x == CANCEL) ->
+                    state = STANDBY;
+                :: (state == CRUISE) && (x == BRAKE) ->
+                    state = HOLD;
+                :: (state == HOLD) && (x == RESUME) ->
+                    state = CRUISE;
+                :: (state == HOLD) && (x == DISABLE) ->
+                    state = OFF;
+                :: (state == HOLD) && ((count == 2) || (x == CANCEL)) ->
+                    count = 0; state = STANDBY
+                :: (state == HOLD) && ! ((x == RESUME) || \
+                    (x == DISABLE) || ((count == 2) || (x == CANCEL)) ) ->
+                    count = count + 1;
+                :: else -> skip;
+            fi;
+        }
+    od;
+
+}
+
+
+/*
+* LTL properties
+*/
+
+ltl p1 { (x == ENABLE) -> <> (state == OFF) }
+
+ltl p2 { []((x == DISABLE) -> <>(state == OFF)) }
+
+ltl p3 { [](count == 0) -> <>(state == OFF)}
+
+ltl p4 { []( (state == HOLD) -> ((x != DISABLE) && (x != RESUME) )) -> <>(state == STANDBY) }
+