From 2947b54c40b21df8bb11e3c7fc331a7f0835c29d Mon Sep 17 00:00:00 2001
From: dgelessus <dgelessus@users.noreply.github.com>
Date: Wed, 4 Dec 2019 17:41:14 +0100
Subject: [PATCH] Add test notebook and models for :modelcheck
---
notebooks/models/CarlaTravelAgencyErr.mch | 297 ++++++++++++++++++++++
notebooks/models/scheduler_large.mch | 79 ++++++
notebooks/tests/modelcheck.ipynb | 206 +++++++++++++++
3 files changed, 582 insertions(+)
create mode 100644 notebooks/models/CarlaTravelAgencyErr.mch
create mode 100644 notebooks/models/scheduler_large.mch
create mode 100644 notebooks/tests/modelcheck.ipynb
diff --git a/notebooks/models/CarlaTravelAgencyErr.mch b/notebooks/models/CarlaTravelAgencyErr.mch
new file mode 100644
index 0000000..4e8a39f
--- /dev/null
+++ b/notebooks/models/CarlaTravelAgencyErr.mch
@@ -0,0 +1,297 @@
+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
+
diff --git a/notebooks/models/scheduler_large.mch b/notebooks/models/scheduler_large.mch
new file mode 100644
index 0000000..9595425
--- /dev/null
+++ b/notebooks/models/scheduler_large.mch
@@ -0,0 +1,79 @@
+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
+
diff --git a/notebooks/tests/modelcheck.ipynb b/notebooks/tests/modelcheck.ipynb
new file mode 100644
index 0000000..ebfd01f
--- /dev/null
+++ b/notebooks/tests/modelcheck.ipynb
@@ -0,0 +1,206 @@
+{
+ "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
+}
--
GitLab