smvtemplatev2.st

-- 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>)