smvtemplatev2.st 918 Bytes
Newer Older
1 2 3 4 5 6 7 8 9 10 11 12 13 14 15 16 17 18 19 20 21 22 23 24 25 26 27 28 29 30 31
-- 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>)