-- This NuSMV specification was automatically generated by Mohawk 2.0 -- Stats -- Number of role without rules: -- Number of role with rules: -- Ratio without / with: -- Ratio without / total: MODULE main VAR -- This section will contain state variables. For each user, we will have -- an array. ; -- This section will contain enumerations for users and actions act : {ADD, REMOVE}; user : {}; admin : {}; role : ; ASSIGN -- Assigning UA ; -- This section will contain state transition rules -- LTLSPEC: "G p" means that a certain condition p holds in all future time instants LTLSPEC G ([]=)