Add test notebook and models for :modelcheck

notebooks/models/CarlaTravelAgencyErr.mch

+MACHINE  CarlaTravelAgencyErr
+/* contains an error that can be found by model checking */
+/* machine developed by Carla Ferreira (the final machine contains no errors) */
+SETS
+    USER = {user1,user2};
+    SESSION = {sess1,sess2, sess3};
+    SESSION_REQUEST = {bc, br, uc, ur, none};
+    SESSION_STATE = {s0, s1, s2, s3, s4, s5, s6, s7};
+    HOTEL = {h1, h2, noHotel};
+    CAR_RENT = {c1, c2, noCarRent};
+    CARD = {valid, wrong, unknown};
+    ROOM = {h1a, h1b, h2a, h2b};
+    CAR = {c1a, c1b, c2a, c2b};
+    RESP = {done, impossible, undef}
+
+CONSTANTS
+    AGENCY_USER
+
+PROPERTIES
+    AGENCY_USER <: USER & AGENCY_USER /= {}
+
+VARIABLES
+    session,
+    session_response,
+    session_card,
+    session_state,
+    session_request,
+    user_hotel_bookings,
+    user_rental_bookings,
+    rooms_hotel,
+    cars_rental,
+    global_room_bookings,
+    global_car_bookings
+
+DEFINITIONS
+    rooms_available(h) == (dom(global_room_bookings)/\rooms_hotel~[{h}]) /= rooms_hotel~[{h}];
+    cars_available(r) == (dom(global_car_bookings)/\cars_rental~[{r}]) /= cars_rental~[{r}]
+
+INVARIANT
+
+    session: SESSION +-> USER & /*AGENCY_USER & */
+    session_response: SESSION +-> RESP &
+    session_card: SESSION +->  CARD &
+    session_state: SESSION +->  SESSION_STATE &
+    session_request: SESSION +->  SESSION_REQUEST &
+    user_hotel_bookings: USER +-> HOTEL & /* AGENCY_USER +->  HOTEL & */
+    user_rental_bookings: USER +->  CAR_RENT & /* AGENCY_USER +->  CAR_RENT & */
+    rooms_hotel: ROOM --> HOTEL &
+    cars_rental: CAR --> CAR_RENT &
+    global_room_bookings: ROOM >+> USER  &
+    global_car_bookings: CAR >+> USER &
+
+
+    dom(session)=dom(session_response) & dom(session)=dom(session_card) &
+    dom(session)=dom(session_state) & dom(session)=dom(session_request) &
+
+    dom(user_hotel_bookings)=dom(user_rental_bookings) &
+
+    ran(session) <: dom(user_hotel_bookings)
+    
+    &
+
+         
+         ( sess1:dom(session) & session_card(sess1) /= valid =>
+            session_response(sess1) = undef )
+    
+
+
+INITIALISATION
+
+    session := {} ||
+    session_response := {} ||
+    session_card := {} ||
+    session_state := {} ||
+    session_request := {} ||
+    user_hotel_bookings := {} ||
+    user_rental_bookings := {} ||
+    rooms_hotel := {h1a |-> h1, h1b |-> h1, h2a |-> h2, h2b |-> h2} ||
+    cars_rental := {c1a |-> c1, c1b |-> c1, c2a |-> c2, c2b |-> c2} ||
+    /* global_room_bookings : ( global_room_bookings : ROOM >+>USER ) ||
+    global_car_bookings : ( global_car_bookings : CAR >+> USER ) */
+    global_room_bookings := {} ||
+    global_car_bookings := {}
+
+
+OPERATIONS
+
+    sid_ <-- login(uu) =
+    PRE uu : USER /* AGENCY_USER */
+    THEN
+      SELECT uu : dom(user_hotel_bookings) /* New session for a known user */
+      THEN
+        skip
+      WHEN uu /: dom(user_hotel_bookings)  /* A new user - information needs to be created */
+      THEN
+        user_hotel_bookings(uu) := noHotel ||
+        user_rental_bookings(uu) := noCarRent
+      END
+      ||
+      ANY sid WHERE sid : SESSION & sid /: dom(session)  /* Creating a new session for the user */
+      THEN
+        session(sid) := uu ||
+        session_response(sid) := undef ||
+        session_card(sid) := unknown ||
+        session_state(sid) := s1 ||
+        session_request(sid) := none ||
+    sid_ := sid
+      END
+    END;
+
+   bookRoom(sid)=
+    PRE sid : SESSION
+        THEN
+          SELECT sid:dom(session) & session_state(sid) = s1 & session_request(sid) = none
+          THEN
+            session_state(sid) := s3 ||
+            session_request(sid) := br
+          END
+        END;
+
+    bookCar(sid)=
+    PRE sid : SESSION
+        THEN
+          SELECT sid:dom(session) & session_state(sid) = s1 & session_request(sid) = none
+          THEN
+            session_state(sid) := s5 ||
+            session_request(sid) := bc
+          END
+        END;
+
+    unbookRoom(sid)=
+    PRE sid : SESSION
+        THEN
+          SELECT sid:dom(session) & session_state(sid) = s1 & session_request(sid) = none
+          THEN
+            session_state(sid) := s2 ||
+            session_request(sid) := ur
+          END
+        END;
+
+    unbookCar(sid)=
+    PRE sid : SESSION
+        THEN
+          SELECT sid:dom(session) & session_state(sid) = s1  & session_request(sid) = none
+          THEN
+            session_state(sid) := s4 ||
+            session_request(sid) := uc
+          END
+        END;
+
+    enterCard(sid)=
+        PRE sid : SESSION
+        THEN
+          SELECT sid:dom(session) & session_state(sid) : {s2,s3,s4,s5}
+          THEN
+            session_state(sid) := s6 ||
+            ANY cc WHERE cc: (CARD-{unknown})
+            THEN
+              session_card(sid) := cc
+            END
+          END
+        END;
+
+    retryCard(sid)=
+        PRE  sid : SESSION
+        THEN
+          SELECT sid:dom(session) & session_state(sid) = s6 & session_card(sid) = wrong
+          THEN
+            ANY cc WHERE cc: (CARD-{unknown})
+            THEN
+              session_card(sid) := cc
+            END
+          END
+        END;
+
+            
+    response(sid)=
+        PRE sid : SESSION
+        THEN
+          SELECT sid:dom(session) & session_state(sid)  = s6
+          THEN
+            session_state(sid) := s7
+          END
+          ||
+          SELECT session_request(sid) = br & user_hotel_bookings(session(sid)) = noHotel
+          THEN
+            IF dom(global_room_bookings) <<: ROOM
+            THEN
+              ANY rr, hh WHERE rr:ROOM-dom(global_room_bookings) & hh:HOTEL & rooms_hotel(rr) = hh
+              THEN
+                global_room_bookings(rr) := session(sid) ||
+                user_hotel_bookings(session(sid)) := hh  ||
+                session_response(sid) := done
+              END
+            ELSE session_response(sid) := impossible
+            END
+      WHEN session_request(sid) = br & user_hotel_bookings(session(sid)) /= noHotel
+          THEN
+            IF (dom(global_room_bookings)/\
+                 rooms_hotel~[{user_hotel_bookings(session(sid))}]) /=
+                   rooms_hotel~[{user_hotel_bookings(session(sid))}]
+            THEN
+              ANY rr WHERE rr:ROOM-dom(global_room_bookings) & rooms_hotel(rr) = user_hotel_bookings(session(sid))
+              THEN
+                global_room_bookings := global_room_bookings \/ { rr |-> session(sid)} ||
+                session_response(sid) := done
+              END
+            ELSE
+              session_response(sid) := impossible
+            END
+
+      WHEN session_request(sid) = bc & user_rental_bookings(session(sid)) = noCarRent
+          THEN
+            IF dom(global_car_bookings) <<: CAR
+            THEN
+              ANY cc, re WHERE cc:CAR-dom(global_car_bookings) & re:CAR_RENT & cars_rental(cc) = re
+              THEN
+                global_car_bookings(cc) := session(sid) ||
+                user_rental_bookings(session(sid)) := re  ||
+                session_response(sid) := done
+              END
+            ELSE session_response(sid) := impossible
+            END
+
+          WHEN session_request(sid) = bc & user_rental_bookings(session(sid)) /= noCarRent
+          THEN
+            IF (dom(global_car_bookings) /\ cars_rental~[{user_rental_bookings(session(sid))}]) 
+              /= cars_rental~[{user_rental_bookings(session(sid))}]
+            THEN
+              ANY cc WHERE cc:CAR-dom(global_car_bookings) & cars_rental(cc) = user_rental_bookings(session(sid))
+              THEN
+                global_car_bookings(cc) := session(sid) ||
+                session_response(sid) := done
+              END
+            ELSE
+              session_response(sid) := impossible
+            END
+
+          WHEN session_request(sid) = ur
+          THEN
+            IF session(sid) : ran(global_room_bookings)
+            THEN
+              ANY rr WHERE rr:dom(global_room_bookings) & global_room_bookings(rr) = session(sid)
+              THEN
+                global_room_bookings := {rr} <<| global_room_bookings ||
+                session_response(sid) := done ||
+                IF {xx | xx:dom(global_room_bookings) & global_room_bookings(xx) = session(sid)} = {rr}
+                THEN user_hotel_bookings(session(sid)) := noHotel END
+              END
+            ELSE
+              session_response(sid) := impossible
+            END
+
+          WHEN session_request(sid) = uc
+          THEN
+            IF session(sid) : ran(global_car_bookings)
+            THEN
+              ANY cc WHERE cc:dom(global_car_bookings) & global_car_bookings(cc) = session(sid)
+              THEN
+                global_car_bookings := {cc} <<| global_car_bookings ||
+                session_response(sid) := done ||
+                IF {xx | xx:dom(global_car_bookings) & global_car_bookings(xx) = session(sid)} = {cc}
+                THEN user_rental_bookings(session(sid)) := noCarRent END
+              END
+            ELSE
+              session_response(sid) := impossible
+            END
+      END
+        END;
+
+   again(sid)=
+        PRE sid : SESSION
+        THEN
+          SELECT sid:dom(session) & session_state(sid)  = s7
+          THEN
+            session_state(sid) := s1 ||
+            session_request(sid) := none ||
+            session_response(sid) := undef ||
+            session_card(sid) := unknown
+          END
+        END;
+
+    logout(sid)=
+        PRE sid : SESSION
+        THEN
+          SELECT sid:dom(session) & session_state(sid) : {s6,s7}
+          THEN
+            session := {sid} <<| session ||
+            session_response := {sid} <<| session_response ||
+            session_card := {sid} <<| session_card ||
+            session_state := {sid} <<| session_state ||
+            session_request := {sid} <<| session_request
+          END
+        END
+
+END
+

notebooks/models/scheduler_large.mch

+MACHINE scheduler
+
+SETS
+	PID 
+
+/* LTL Formulas:
+  G (e(del) -> {card(ready \\/ waiting)>0})  TRUE
+  G ({card(ready \\/ waiting)>0} -> e(del))    FALSE
+  G ({card(active)>0} -> (e(swap) U {card(active)=0}))  FALSE
+  G ({card(active)>0} -> ((G e(swap)) | (e(swap) U {card(active)=0})))  TRUE
+*/
+
+VARIABLES active, ready, waiting
+
+DEFINITIONS
+    scope_PID == 1..8
+
+INVARIANT  active : POW(PID) & ready : POW(PID) & waiting: POW(PID) & /* the types */
+           /* and now the rest of the invariant */
+           active <: PID &
+           ready <: PID   &
+           waiting <: PID &
+           (ready /\ waiting) = {} &
+           active /\ (ready \/ waiting) = {} &
+           card(active) <= 1 &
+           ((active = {})  => (ready = {}))
+              
+INITIALISATION  
+	active := {} || ready := {} || waiting := {}
+	
+OPERATIONS
+
+rr <-- nr_ready = rr:= card(ready);
+
+new(pp) =
+	SELECT
+		pp : PID  &
+		pp /: active &
+		pp /: (ready \/ waiting) 
+	THEN
+		waiting := (waiting \/ { pp })
+	END;
+
+del(pp) =
+	SELECT
+		pp : waiting 
+	THEN
+		waiting := waiting - { pp }
+	END;
+	
+ready(rr) =
+        SELECT
+                rr : waiting
+        THEN
+                waiting := (waiting - {rr}) ||
+                IF (active = {}) THEN
+                   active := {rr}
+                ELSE
+                   ready := ready \/ {rr} 
+                END
+        END; 
+        	
+swap =
+        SELECT
+                active /= {}
+        THEN
+                waiting := (waiting \/ active) ||
+                IF (ready = {}) THEN
+                   active := {}
+                ELSE
+                   ANY pp WHERE pp : ready
+                   THEN
+                       active := {pp} ||
+                       ready := ready - {pp} 
+                   END
+                END
+        END       
+END
+

notebooks/tests/modelcheck.ipynb

+{
+ "cells": [
+  {
+   "cell_type": "code",
+   "execution_count": 1,
+   "metadata": {},
+   "outputs": [
+    {
+     "data": {
+      "text/markdown": [
+       "```\n",
+       ":modelcheck\n",
+       "```\n",
+       "\n",
+       "Run the ProB model checker on the current model.\n",
+       "\n",
+       "If an error state is found, it is made the current state, so that it can be inspected using `:trace`, `:check`, etc."
+      ],
+      "text/plain": [
+       ":modelcheck\n",
+       "Run the ProB model checker on the current model.\n",
+       "\n",
+       "If an error state is found, it is made the current state, so that it can be inspected using `:trace`, `:check`, etc."
+      ]
+     },
+     "execution_count": 1,
+     "metadata": {},
+     "output_type": "execute_result"
+    }
+   ],
+   "source": [
+    ":help :modelcheck"
+   ]
+  },
+  {
+   "cell_type": "code",
+   "execution_count": 2,
+   "metadata": {},
+   "outputs": [
+    {
+     "data": {
+      "text/plain": [
+       "Loaded machine: scheduler"
+      ]
+     },
+     "execution_count": 2,
+     "metadata": {},
+     "output_type": "execute_result"
+    }
+   ],
+   "source": [
+    ":load ../models/scheduler.mch"
+   ]
+  },
+  {
+   "cell_type": "code",
+   "execution_count": 3,
+   "metadata": {},
+   "outputs": [
+    {
+     "data": {
+      "text/plain": [
+       "0.265 sec, 36 of 36 states processed, 156 transitions"
+      ]
+     },
+     "metadata": {},
+     "output_type": "display_data"
+    },
+    {
+     "data": {
+      "text/plain": [
+       "Model Checking complete. No error nodes found."
+      ]
+     },
+     "execution_count": 3,
+     "metadata": {},
+     "output_type": "execute_result"
+    }
+   ],
+   "source": [
+    ":modelcheck"
+   ]
+  },
+  {
+   "cell_type": "code",
+   "execution_count": 4,
+   "metadata": {},
+   "outputs": [
+    {
+     "data": {
+      "text/plain": [
+       "Loaded machine: CarlaTravelAgencyErr"
+      ]
+     },
+     "execution_count": 4,
+     "metadata": {},
+     "output_type": "execute_result"
+    }
+   ],
+   "source": [
+    ":load ../models/CarlaTravelAgencyErr.mch"
+   ]
+  },
+  {
+   "cell_type": "code",
+   "execution_count": 5,
+   "metadata": {},
+   "outputs": [
+    {
+     "data": {
+      "text/plain": [
+       "0.519 sec, 84 of 455 states processed, 625 transitions"
+      ]
+     },
+     "metadata": {},
+     "output_type": "display_data"
+    },
+    {
+     "data": {
+      "text/plain": [
+       "Model check uncovered an error: Invariant violation found.\n",
+       "Use :trace to view the trace to the error state."
+      ]
+     },
+     "execution_count": 5,
+     "metadata": {},
+     "output_type": "execute_result"
+    }
+   ],
+   "source": [
+    ":modelcheck"
+   ]
+  },
+  {
+   "cell_type": "code",
+   "execution_count": 6,
+   "metadata": {},
+   "outputs": [
+    {
+     "data": {
+      "text/plain": [
+       "Loaded machine: scheduler"
+      ]
+     },
+     "execution_count": 6,
+     "metadata": {},
+     "output_type": "execute_result"
+    }
+   ],
+   "source": [
+    ":load ../models/scheduler_large.mch"
+   ]
+  },
+  {
+   "cell_type": "markdown",
+   "metadata": {},
+   "source": [
+    "Checking this machine can take a short while."
+   ]
+  },
+  {
+   "cell_type": "code",
+   "execution_count": 7,
+   "metadata": {},
+   "outputs": [
+    {
+     "data": {
+      "text/plain": [
+       "25.925 sec, 17753 of 17753 states processed, 185145 transitions"
+      ]
+     },
+     "metadata": {},
+     "output_type": "display_data"
+    },
+    {
+     "data": {
+      "text/plain": [
+       "Model Checking complete. No error nodes found."
+      ]
+     },
+     "execution_count": 7,
+     "metadata": {},
+     "output_type": "execute_result"
+    }
+   ],
+   "source": [
+    ":modelcheck"
+   ]
+  }
+ ],
+ "metadata": {
+  "kernelspec": {
+   "display_name": "ProB 2",
+   "language": "prob",
+   "name": "prob2"
+  },
+  "language_info": {
+   "codemirror_mode": "prob2_jupyter_repl",
+   "file_extension": ".prob",
+   "mimetype": "text/x-prob2-jupyter-repl",
+   "name": "prob"
+  }
+ },
+ "nbformat": 4,
+ "nbformat_minor": 2
+}