*** This is NuSMV 2.4.3 (compiled on Mon Feb 23 20:34:39 UTC 2009)
*** For more information on NuSMV see <http://nusmv.irst.itc.it>
*** or email to <nusmv-users@irst.itc.it>.
*** Please report bugs to <nusmv@irst.itc.it>.

-- specification  G (perform ->  Y (!perform S ((!rt S (add & (!rt S (rt & (!leave S join))))) | ((!rt S ((rt & ((!remove & !leave) S add)) & (!leave S join))) & ((!request & !perform) S request)))))  is true
-- specification  G (perform ->  Y (!perform S (((!remove & !leave) S (add & (!leave S join))) & ((!request & !perform) S request))))  is true
-- specification  G (perform -> ( Y ((!perform & (!rt | (rt & authzcc))) S (request & (!rt S (rt & authzcc)))) |  Y ((!perform & !rt) S ((rt & authzcc) & (!perform S request)))))  is true
-- specification  G (perform ->  Y ((!perform & !rt) S ((rt & authzcc) & (!perform S request))))  is true
-- specification  G !((perform &  Y ((!perform & (!rt | (rt & authzcc))) S (request & (!rt S (rt & authzcc))))) & !( Y ((!perform & !rt) S ((rt & authzcc) & (!perform S request)))))  is true