-- This NuSMV specification was automatically generated by Mohawk 2.0

-- Stats
-- Number of role without rules: 	$roleWithoutRules$
-- Number of role with rules: 		$roleWithRules$
-- Ratio without / with: 			$roleWithoutWithRatio$
-- Ratio without / total: 			$roleWithoutTotalRatio$

MODULE main
VAR

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

$userarrays; separator=";\n"$;

-- This section will contain enumerations for users and actions
act : {ADD, REMOVE};
user : {$users; separator=","$};
admin : {$admin; separator=","$};
role : $role$;

ASSIGN
-- Assigning UA
$ua; separator=";\n"$;

-- This section will contain state transition rules
$transitions; separator= "\n\n\n-- ----------------------------------\n-- Another user \n\n\n" $

-- LTLSPEC: "G p" means that a certain condition p holds in all future time instants 
LTLSPEC G ($user$[$roleindex$]=$falseWord$)