MODULE main

DEFINE
numroles := <numRoles>;
numadminroles := <numAdminRoles>;  -- Might be used later as a optimization
numusers := <numUsers>; -- should be = numroles + 1
numtimeslots := <numTimeSlots>;

-- 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=" & ">)

VAR
rule : {
    -- CanAssign
	<caruleslist>
	-- CanRevoke
	<crruleslist>
	-- CanEnable
	<ceruleslist>
	-- CanDisable
	<cdruleslist>
};
user : 1 .. numusers;
admin: 1 .. numusers;

ASSIGN



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

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

ASSIGN
-- Disabling User Role Assignments
<users:{u|init(<u>):=FALSE;}; separator="\n">

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