-- This NuSMV specification was automatically generated by the 
-- RBAC2SMV tool.

MODULE main
VAR

-- This section will contain state variables. For each user, we will have 
-- an array. 

user0 : array 0..3 of boolean;
user1 : array 0..3 of boolean;
user2 : array 0..3 of boolean;
user3 : array 0..3 of boolean;
user4 : array 0..3 of boolean;

-- This section will contain enumerations for users and actions
act : {ADD, REMOVE};
user : {user0,user1,user2,user3,user4};
admin : {user4};
role : 0 .. 3;

ASSIGN

-- Assigning UA
init(user0[0]) := 0;
init(user0[1]) := 0;
init(user0[2]) := 0;
init(user0[3]) := 0;
init(user1[0]) := 0;
init(user1[1]) := 0;
init(user1[2]) := 0;
init(user1[3]) := 0;
init(user2[0]) := 0;
init(user2[1]) := 0;
init(user2[2]) := 0;
init(user2[3]) := 0;
init(user3[0]) := 0;
init(user3[1]) := 0;
init(user3[2]) := 0;
init(user3[3]) := 0;
init(user4[0]) := 0;
init(user4[1]) := 0;
init(user4[2]) := 0;
init(user4[3]) := 1;

-- This section will contain state transition rules

next(user0[0]) := 
case
user = user0 & admin = user4 & user4[3] = 1 & user0[1]=1 & user0[2]=1 & role = 0 & act = ADD: 1;
user = user0 & admin = user4 & user4[3] = 1 & user0[1]=0 & role = 0 & act = ADD: 1;
user = user0 & admin = user4 & user4[3] = 1 & user0[1]=0 & user0[2]=1 & role = 0 & act = ADD: 1;
1 : user0[0]; 
esac;

next(user0[1]) := 
case
user = user0 & admin = user4 & user4[3] = 1 & user0[0]=1 & user0[2]=1 & role = 1 & act = ADD: 1;
user = user0 & admin = user4 & user4[3] = 1 & user0[0]=0 & user0[2]=1 & role = 1 & act = ADD: 1;
user = user0 & admin = user4 & user4[3] = 1 & user0[0]=0 & role = 1 & act = ADD: 1;
1 : user0[1]; 
esac;

next(user0[2]) := 
case
user = user0 & admin = user4 & user4[3] = 1 & user0[0]=1 & user0[1]=1 & role = 2 & act = ADD: 1;
user = user0 & admin = user4 & user4[3] = 1 & user0[0]=1 & user0[1]=0 & role = 2 & act = ADD: 1;
user = user0 & admin = user4 & 0 & role = 2 & act = REMOVE: 0;
1 : user0[2]; 
esac;

next(user0[3]) := user0[3];
-- Another user 
next(user1[0]) := 
case
user = user1 & admin = user4 & user4[3] = 1 & user1[1]=1 & user1[2]=1 & role = 0 & act = ADD: 1;
user = user1 & admin = user4 & user4[3] = 1 & user1[1]=0 & role = 0 & act = ADD: 1;
user = user1 & admin = user4 & user4[3] = 1 & user1[1]=0 & user1[2]=1 & role = 0 & act = ADD: 1;
1 : user1[0]; 
esac;

next(user1[1]) := 
case
user = user1 & admin = user4 & user4[3] = 1 & user1[0]=1 & user1[2]=1 & role = 1 & act = ADD: 1;
user = user1 & admin = user4 & user4[3] = 1 & user1[0]=0 & user1[2]=1 & role = 1 & act = ADD: 1;
user = user1 & admin = user4 & user4[3] = 1 & user1[0]=0 & role = 1 & act = ADD: 1;
1 : user1[1]; 
esac;

next(user1[2]) := 
case
user = user1 & admin = user4 & user4[3] = 1 & user1[0]=1 & user1[1]=1 & role = 2 & act = ADD: 1;
user = user1 & admin = user4 & user4[3] = 1 & user1[0]=1 & user1[1]=0 & role = 2 & act = ADD: 1;
user = user1 & admin = user4 & 0 & role = 2 & act = REMOVE: 0;
1 : user1[2]; 
esac;

next(user1[3]) := user1[3];
-- Another user 
next(user2[0]) := 
case
user = user2 & admin = user4 & user4[3] = 1 & user2[1]=1 & user2[2]=1 & role = 0 & act = ADD: 1;
user = user2 & admin = user4 & user4[3] = 1 & user2[1]=0 & role = 0 & act = ADD: 1;
user = user2 & admin = user4 & user4[3] = 1 & user2[1]=0 & user2[2]=1 & role = 0 & act = ADD: 1;
1 : user2[0]; 
esac;

next(user2[1]) := 
case
user = user2 & admin = user4 & user4[3] = 1 & user2[0]=1 & user2[2]=1 & role = 1 & act = ADD: 1;
user = user2 & admin = user4 & user4[3] = 1 & user2[0]=0 & user2[2]=1 & role = 1 & act = ADD: 1;
user = user2 & admin = user4 & user4[3] = 1 & user2[0]=0 & role = 1 & act = ADD: 1;
1 : user2[1]; 
esac;

next(user2[2]) := 
case
user = user2 & admin = user4 & user4[3] = 1 & user2[0]=1 & user2[1]=1 & role = 2 & act = ADD: 1;
user = user2 & admin = user4 & user4[3] = 1 & user2[0]=1 & user2[1]=0 & role = 2 & act = ADD: 1;
user = user2 & admin = user4 & 0 & role = 2 & act = REMOVE: 0;
1 : user2[2]; 
esac;

next(user2[3]) := user2[3];
-- Another user 
next(user3[0]) := 
case
user = user3 & admin = user4 & user4[3] = 1 & user3[1]=1 & user3[2]=1 & role = 0 & act = ADD: 1;
user = user3 & admin = user4 & user4[3] = 1 & user3[1]=0 & role = 0 & act = ADD: 1;
user = user3 & admin = user4 & user4[3] = 1 & user3[1]=0 & user3[2]=1 & role = 0 & act = ADD: 1;
1 : user3[0]; 
esac;

next(user3[1]) := 
case
user = user3 & admin = user4 & user4[3] = 1 & user3[0]=1 & user3[2]=1 & role = 1 & act = ADD: 1;
user = user3 & admin = user4 & user4[3] = 1 & user3[0]=0 & user3[2]=1 & role = 1 & act = ADD: 1;
user = user3 & admin = user4 & user4[3] = 1 & user3[0]=0 & role = 1 & act = ADD: 1;
1 : user3[1]; 
esac;

next(user3[2]) := 
case
user = user3 & admin = user4 & user4[3] = 1 & user3[0]=1 & user3[1]=1 & role = 2 & act = ADD: 1;
user = user3 & admin = user4 & user4[3] = 1 & user3[0]=1 & user3[1]=0 & role = 2 & act = ADD: 1;
user = user3 & admin = user4 & 0 & role = 2 & act = REMOVE: 0;
1 : user3[2]; 
esac;

next(user3[3]) := user3[3];
-- Another user 
next(user4[0]) := 
case
user = user4 & admin = user4 & user4[3] = 1 & user4[1]=1 & user4[2]=1 & role = 0 & act = ADD: 1;
user = user4 & admin = user4 & user4[3] = 1 & user4[1]=0 & role = 0 & act = ADD: 1;
user = user4 & admin = user4 & user4[3] = 1 & user4[1]=0 & user4[2]=1 & role = 0 & act = ADD: 1;
1 : user4[0]; 
esac;

next(user4[1]) := 
case
user = user4 & admin = user4 & user4[3] = 1 & user4[0]=1 & user4[2]=1 & role = 1 & act = ADD: 1;
user = user4 & admin = user4 & user4[3] = 1 & user4[0]=0 & user4[2]=1 & role = 1 & act = ADD: 1;
user = user4 & admin = user4 & user4[3] = 1 & user4[0]=0 & role = 1 & act = ADD: 1;
1 : user4[1]; 
esac;

next(user4[2]) := 
case
user = user4 & admin = user4 & user4[3] = 1 & user4[0]=1 & user4[1]=1 & role = 2 & act = ADD: 1;
user = user4 & admin = user4 & user4[3] = 1 & user4[0]=1 & user4[1]=0 & role = 2 & act = ADD: 1;
user = user4 & admin = user4 & 0 & role = 2 & act = REMOVE: 0;
1 : user4[2]; 
esac;

next(user4[3]) := user4[3];

-- LTLSPEC

LTLSPEC G (user1[1]=0)