nusmvTemplate.st 960 Bytes
Newer Older
Jonathan Shahen's avatar
Jonathan Shahen committed
1
MODULE main
2

Jonathan Shahen's avatar
Jonathan Shahen committed
3
DEFINE
4 5 6 7
numroles := <numRoles>;
numadminroles := <numAdminRoles>;  -- Might be used later as a optimization
numusers := <numUsers>; -- should be = numroles + 1
numtimeslots := <numTimeSlots>;
8

9 10 11
-- LTLSPEC: "G p" means that a certain condition p holds in all future time instants
-- <queryStr>
LTLSPEC G !(<goalRoles:{r|U1R<r.getName>T<goalTimeSlot> = TRUE}; separator=" & ">)
12

13 14 15 16 17 18 19 20 21 22 23
VAR
rule : {
    -- CanAssign
	<caruleslist>
	-- CanRevoke
	<crruleslist>
	-- CanEnable
	<ceruleslist>
	-- CanDisable
	<cdruleslist>
};
Jonathan Shahen's avatar
Jonathan Shahen committed
24 25
user : 1 .. numusers;
admin: 1 .. numusers;
26

27 28 29 30 31 32 33
ASSIGN



VAR
-- <numUsers> Users Variable
<users:{u|<roleTimeslots:{rt|U<u>R<rt.role>T<rt.time> : boolean;}; separator="\n">}; separator="\n">
34

35 36
-- <numRolesEnabled> RoleEnabled
<enabledRoles:{r|<r> : boolean;}; separator="\n">
37

Jonathan Shahen's avatar
Jonathan Shahen committed
38 39
ASSIGN
-- Disabling User Role Assignments
40
<users:{u|init(<u>):=FALSE;}; separator="\n">
Jonathan Shahen's avatar
Jonathan Shahen committed
41 42

-- Disabling Roles
43
<enabledRoles:{r|init(<r>) := FALSE;}; separator="\n">