Graded-CTL NuSMV

Source Code for "P_Queue"

-- This file describes three processes simulator, sort and
-- sim_const, which are ever running. The buffer used
-- consists of six positions, whose three are called in and
-- three are called out. The simulator process writes
-- randomically values on the buffer, whenever the first
-- position of in is free. In other case it waits until
-- values are consumed. This process represents a simulator,
-- which would generate data. Whenever a data is inserted, a
-- flag indicating the buffer has to be sorted is set. The
-- process sim_cons consumes the data of the buffer, when the
-- buffer is sorted. After sorting, the first position of out
-- contains the value to be consumed. Finally, the process
-- sort sorts the buffer using a rotation algorithm presented
-- in the paper of Flemming Hoeg, Niels Mellergaard and
-- Jorgen Staunstrup.

MODULE main

VAR
in_f: array 1..3 of {0,1,2,3,4,5,6,7,8};
out_l: array 1..3 of {0,1,2,3,4,5,6,7,8};
sim: process sim_cons(in_f,out_l,sort_OK,sort_req);
sm : process simulator(in_f,sort_req);
srt: process sort(in_f,out_l,sort_OK,sort_req);
pq_full: boolean;
pq_empty: boolean;
sort_OK : boolean;
sort_req : boolean;
lock : boolean;

ASSIGN
init(in_f[1]) := 0;
init(in_f[2]) := 0;
init(in_f[3]) := 0;
init(out_l[1]) := 0;
init(out_l[2]) := 0;
init(out_l[3]) := 0;
init(sort_OK) := 1;

MODULE simulator(in_f,sort_req)

VAR
state : {initial,ins_val};

ASSIGN
init(state) := initial;
next(state) :=
case
state=initial & in_f[1]=0 : ins_val;
state=initial & in_f[1]!=0 : initial;
state=ins_val : initial;
1: state;
esac;
next(in_f[1]) :=
case
state=ins_val: {1,2,3,4,5,6,7,8};
1: in_f[1];
esac;
next(sort_req) :=
case
state=ins_val: 1;
1: {0, 1};
esac;

FAIRNESS
running

MODULE sim_cons(in_f,out_l,sort_OK,sort_req)
VAR
state: {initial,cons};
ASSIGN
next(state) :=
case
state=initial & out_l[1]!=0: cons;
state=cons & out_l[1]=0 : initial;
1: state;
esac;
next(out_l[1]) :=
case
state=cons & sort_OK=1 : 0;
1: out_l[1];
esac;

MODULE sort(in_f,out_l,sort_OK,sort_req)
VAR
state: {initial,cell1,cell1_p,cell1_m,cell2,cell2_p,cell2_m,cell3,cell3_m, cell3_p,ready};
tmp: {0,1,2,3,4,5,6,7,8};
reg: {0,1,2,3};
ASSIGN
init(tmp) := 0;
init(reg) := 0;
next(state) :=
case
state=initial & in_f[1]!=0: cell1;
state=cell1: cell1_p;
state=cell1_p: cell1_m;
state=cell1_m: cell2;
state=cell2: cell2_p;
state=cell2_p: cell2_m;
state=cell2_m: cell3;
state=cell3: cell3_p;
state=cell3_p: cell3_m;
state=cell3_m: ready;
1: state;
esac;
next(sort_OK) :=
case
state=cell1 : 0;
state=ready : 1;
1: sort_OK;
esac;
next(reg) :=
case
state=cell1 & out_l[1]<=in_f[1] & in_f[1]<=in_f[2] & in_f[1]<=out_l[2]:1;
state=cell1 & out_l[1]<=in_f[2] & in_f[2]<=in_f[1] & in_f[2]<=out_l[2]:2;
state=cell1 & out_l[1]<=out_l[2] & out_l[2]<=in_f[1] & out_l[2]<= in_f[2]:3;
state=cell2 & out_l[2]<=in_f[2] & in_f[2]<=in_f[3] & in_f[2]<=out_l[3]:1;
state=cell2 & out_l[2]<=in_f[3] & in_f[3]<=in_f[2] & in_f[3]<=out_l[3]:2;
state=cell2 & out_l[2]<=out_l[3] & out_l[3]<=in_f[2] & out_l[3]<= in_f[3]:3;
state=cell3 & out_l[3]<=in_f[3]: 1;
1: 0;
esac;
next(tmp) :=
case
state=cell1_p: out_l[1];
state=cell2_p: out_l[2];
state=cell3_p: out_l[3];
1: tmp;
esac;
next(out_l[1]) :=
case
state=cell1_m & reg=1: in_f[1];
state=cell1_m & reg=2: in_f[2];
state=cell1_m & reg=3: out_l[2];
1: out_l[1];
esac;
next(in_f[1]) :=
case
state=cell1_m & reg=1: tmp;
1: in_f[1];
esac;
next(in_f[2]) :=
case
state=cell1_m & reg=2: tmp;
state=cell2_m & reg=1: tmp;
1: in_f[2];
esac;
next(in_f[3]) :=
case
state=cell2_m & reg=2: tmp;
state=cell3_m & reg=1: tmp;
1:in_f[3];
esac;
next(out_l[2]) :=
case
state=cell1_m & reg=3: tmp;
state=cell2_m & reg=1: in_f[2];
state=cell2_m & reg=2: in_f[3];
state=cell2_m & reg=3: out_l[3];
1: out_l[2];
esac;
next(out_l[3]) :=
case
state=cell3_m & reg=1: in_f[3];
1: out_l[3];
esac;
next(sort_req) :=
case
state=ready: 0;
1: sort_req;
esac;