Commits

James Goppert  committed 0b572ed

Added trace and fixed model checking.

  • Participants
  • Parent commits 719bec1

Comments (0)

Files changed (2)

File model-checking/test.smv

     init(state) := stop;
     next(state) := case
 
-        state = fwd & request = stop : stop
-        state = fwd & request = fwd : fwd
-        state = fwd & request = back : {back, failure}
-        state = fwd & request = off : off
-
-        state = stop & request = stop : stop
-        state = stop & request = fwd : fwd
-        state = stop & request = back : back
-        state = stop & request = off : off
-
-        state = back & request = stop : stop
-        state = back & request = fwd : {fwd, failure}
-        state = back & request = back : back
-        state = back & request = off : off
-
-        state = off : off
+        state = fwd & request = stop : stop;
+        state = fwd & request = fwd : fwd;
+        state = fwd & request = back : {back, failure};
+        state = fwd & request = off : off;
+
+        state = stop & request = stop : stop;
+        state = stop & request = fwd : fwd;
+        state = stop & request = back : back;
+        state = stop & request = off : off;
+
+        state = back & request = stop : stop;
+        state = back & request = fwd : {fwd, failure};
+        state = back & request = back : back;
+        state = back & request = off : off;
+
+        state = off : off;
+
+        TRUE : {stop,fwd,back,off};
 
     esac;
 

File model-checking/trace.txt

+-- specification AG !(state = failure)  is false
+-- as demonstrated by the following execution sequence
+Trace Description: CTL Counterexample 
+Trace Type: Counterexample 
+-> State: 1.1 <-
+  request = back
+  state = stop
+-> State: 1.2 <-
+  request = fwd
+  state = back
+-> State: 1.3 <-
+  state = failure