Graded-CTL NuSMV

Source Code for "Table"

-- Example of two processes sharing a table without concurrency control
-- The array has empty entries (value 0), and a process
-- is allowed to put an object in any empty spot, or remove an object from
-- any non-empty spot (replacing it with 0)

MODULE main
VAR
table: array 1..3 of {0, a, b, c};
proc1 : process user(table);
proc2 : process user(table);
ASSIGN
init(table[1]) := 0;
init(table[2]) := 0;
init(table[3]) := 0;

MODULE user(table)
VAR
state: {idle, reading, writing};
-- position in table being examined
pos: 1..3;
-- true if position in table is empty
isempty: boolean;
ASSIGN
init(state) := idle;
init(pos) := 1;
init(isempty) := 0;
next(state) := case
state = idle : {idle, reading};
state = reading: {writing};
state = writing: {idle};
esac;
next(pos) := case
state = idle : 1..3;
1: pos;
esac;
next(isempty) := case
state = reading & ((pos = 1 & table[1] = 0) | (pos = 2 & table[2] = 0) | (pos = 3 & table[3] = 0)) : 1;
state = reading : 0;
1: isempty;
esac;
next(table[1]) := case
-- if table entry is empty, keep empty or put in something
-- pos = 1 & state = writing & isempty : {0, a, b, c};
state = writing & isempty & pos = 1 : {0, a, b, c};
-- if table entry is not empty keep the contents, or decide to empty
-- pos = 1 & state = writing & ! isempty : table[1] union {0};
state = writing & ! isempty & pos = 1 : table[1] union {0};
1: table[1];
esac;
next(table[2]) := case
-- if table entry is empty, keep empty or put in something
pos = 2 & state = writing & isempty : {0, a, b, c};
-- if table entry is not empty keep the contents, or decide to empty
pos = 2 & state = writing & ! isempty : table[2] union {0};
1: table[2];
esac;
next(table[3]) := case
-- if table entry is empty, keep empty or put in something
pos = 3 & state = writing & isempty : {0, a, b, c};
-- if table entry is not empty keep the contents, or decide to empty
pos = 3 & state = writing & ! isempty : table[3] union {0};
1: table[3];
esac;

FAIRNESS running