smvtemplatev1.st 919 Bytes
Newer Older
1 2 3 4 5 6 7
-- 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$
8 9 10 11 12 13 14 15 16 17 18 19 20 21 22 23 24 25 26 27

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
28
$transitions; separator= "\n\n\n-- ----------------------------------\n-- Another user \n\n\n" $
29

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