*** This is NuSMV 2.4.3 (compiled on Mon Feb 23 20:34:39 UTC 2009) *** For more information on NuSMV see *** or email to . *** Please report bugs to . -- 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 false -- as demonstrated by the following execution sequence Trace Description: LTL Counterexample Trace Type: Counterexample -> State: 1.1 <- user.request_perform = 0 user.action_perform = 0 trm.object_add_ts = 0 trm.object_remove_ts = 0 trm.user_join_ts = 0 trm.user_leave_ts = 0 trm.ready = 1 trm.question.responding = 0 trm.question.respond = 0 trm.action_refresh = 0 trm.request_response = 0 cc.object_add_ts = 0 cc.object_remove_ts = 0 cc.user_join_ts = 0 cc.user_leave_ts = 0 ga.action_add_object = 0 ga.action_remove_object = 0 ga.action_join_user = 0 ga.action_leave_user = 0 clock.t = 0 join = 0 add = 0 leave = 0 remove = 0 request = 0 authzcc = 0 authztrm = 0 rt = 0 perform = 0 respond = 0 trm.RESPOND = 0 trm.RESPONDING = 0 trm.POLICY = 0 cc.super_distro = 0 ga.user_joined = 0 ga.object_added = 0 clock.HAS_MORE = 1 -> Input: 1.2 <- -> State: 1.2 <- trm.user_join_ts = 1 trm.action_refresh = 1 cc.user_join_ts = 1 ga.action_join_user = 1 clock.t = 1 join = 1 rt = 1 ga.user_joined = 1 -> Input: 1.3 <- -> State: 1.3 <- user.request_perform = 1 trm.object_add_ts = 2 trm.question.responding = 1 trm.question.respond = 1 trm.action_refresh = 0 trm.request_response = 1 cc.object_add_ts = 2 cc.user_leave_ts = 2 ga.action_add_object = 1 ga.action_join_user = 0 ga.action_leave_user = 1 clock.t = 2 join = 0 add = 1 leave = 1 request = 1 authztrm = 1 rt = 0 respond = 1 trm.RESPOND = 1 trm.RESPONDING = 1 trm.POLICY = 1 cc.super_distro = 1 ga.user_joined = 0 ga.object_added = 1 -> Input: 1.4 <- -> State: 1.4 <- user.action_perform = 1 trm.object_remove_ts = 3 trm.user_join_ts = 3 trm.user_leave_ts = 2 trm.question.respond = 0 trm.action_refresh = 1 trm.request_response = 0 cc.object_remove_ts = 3 cc.user_join_ts = 3 ga.action_add_object = 0 ga.action_remove_object = 1 ga.action_join_user = 1 ga.action_leave_user = 0 clock.t = 3 join = 1 add = 0 leave = 0 remove = 1 authztrm = 0 rt = 1 perform = 1 respond = 0 trm.RESPOND = 0 trm.POLICY = 0 cc.super_distro = 0 ga.user_joined = 1 ga.object_added = 0 -> Input: 1.5 <- -> State: 1.5 <- user.request_perform = 0 user.action_perform = 0 ga.action_remove_object = 0 ga.action_join_user = 0 clock.t = 4 join = 0 remove = 0 request = 0 perform = 0 -> Input: 1.6 <- -- Loop starts here -> State: 1.6 <- trm.action_refresh = 0 clock.t = 5 rt = 0 clock.HAS_MORE = 0 -> Input: 1.7 <- -> State: 1.7 <- -- specification G (perform -> ( Y ((!perform & (!rt | (rt & authzcc))) S (request & (!rt S (rt & authzcc)))) | Y ((!perform & !rt) S ((rt & authzcc) & (!perform S request))))) is false -- as demonstrated by the following execution sequence Trace Description: LTL Counterexample Trace Type: Counterexample -> State: 2.1 <- user.request_perform = 0 user.action_perform = 0 trm.object_add_ts = 0 trm.object_remove_ts = 0 trm.user_join_ts = 0 trm.user_leave_ts = 0 trm.ready = 1 trm.question.responding = 0 trm.question.respond = 0 trm.action_refresh = 0 trm.request_response = 0 cc.object_add_ts = 0 cc.object_remove_ts = 0 cc.user_join_ts = 0 cc.user_leave_ts = 0 ga.action_add_object = 0 ga.action_remove_object = 0 ga.action_join_user = 0 ga.action_leave_user = 0 clock.t = 0 join = 0 add = 0 leave = 0 remove = 0 request = 0 authzcc = 0 authztrm = 0 rt = 0 perform = 0 respond = 0 trm.RESPOND = 0 trm.RESPONDING = 0 trm.POLICY = 0 cc.super_distro = 0 ga.user_joined = 0 ga.object_added = 0 clock.HAS_MORE = 1 -> Input: 2.2 <- -> State: 2.2 <- trm.user_join_ts = 1 trm.action_refresh = 1 cc.user_join_ts = 1 ga.action_join_user = 1 clock.t = 1 join = 1 rt = 1 ga.user_joined = 1 -> Input: 2.3 <- -> State: 2.3 <- user.request_perform = 1 trm.object_add_ts = 2 trm.question.responding = 1 trm.question.respond = 1 trm.action_refresh = 0 trm.request_response = 1 cc.object_add_ts = 2 cc.user_leave_ts = 2 ga.action_add_object = 1 ga.action_join_user = 0 ga.action_leave_user = 1 clock.t = 2 join = 0 add = 1 leave = 1 request = 1 authztrm = 1 rt = 0 respond = 1 trm.RESPOND = 1 trm.RESPONDING = 1 trm.POLICY = 1 cc.super_distro = 1 ga.user_joined = 0 ga.object_added = 1 -> Input: 2.4 <- -> State: 2.4 <- user.action_perform = 1 trm.object_remove_ts = 3 trm.user_join_ts = 3 trm.user_leave_ts = 2 trm.question.respond = 0 trm.action_refresh = 1 trm.request_response = 0 cc.object_remove_ts = 3 cc.user_join_ts = 3 ga.action_add_object = 0 ga.action_remove_object = 1 ga.action_join_user = 1 ga.action_leave_user = 0 clock.t = 3 join = 1 add = 0 leave = 0 remove = 1 authztrm = 0 rt = 1 perform = 1 respond = 0 trm.RESPOND = 0 trm.POLICY = 0 cc.super_distro = 0 ga.user_joined = 1 ga.object_added = 0 -> Input: 2.5 <- -> State: 2.5 <- user.request_perform = 0 user.action_perform = 0 ga.action_remove_object = 0 ga.action_join_user = 0 clock.t = 4 join = 0 remove = 0 request = 0 perform = 0 -> Input: 2.6 <- -- Loop starts here -> State: 2.6 <- trm.action_refresh = 0 clock.t = 5 rt = 0 clock.HAS_MORE = 0 -> Input: 2.7 <- -> State: 2.7 <- -- specification G (perform -> Y ((!perform & !rt) S ((rt & authzcc) & (!perform S request)))) is false -- as demonstrated by the following execution sequence Trace Description: LTL Counterexample Trace Type: Counterexample -> State: 3.1 <- user.request_perform = 0 user.action_perform = 0 trm.object_add_ts = 0 trm.object_remove_ts = 0 trm.user_join_ts = 0 trm.user_leave_ts = 0 trm.ready = 1 trm.question.responding = 0 trm.question.respond = 0 trm.action_refresh = 0 trm.request_response = 0 cc.object_add_ts = 0 cc.object_remove_ts = 0 cc.user_join_ts = 0 cc.user_leave_ts = 0 ga.action_add_object = 0 ga.action_remove_object = 0 ga.action_join_user = 0 ga.action_leave_user = 0 clock.t = 0 join = 0 add = 0 leave = 0 remove = 0 request = 0 authzcc = 0 authztrm = 0 rt = 0 perform = 0 respond = 0 trm.RESPOND = 0 trm.RESPONDING = 0 trm.POLICY = 0 cc.super_distro = 0 ga.user_joined = 0 ga.object_added = 0 clock.HAS_MORE = 1 -> Input: 3.2 <- -> State: 3.2 <- trm.user_join_ts = 1 trm.action_refresh = 1 cc.user_join_ts = 1 ga.action_join_user = 1 clock.t = 1 join = 1 rt = 1 ga.user_joined = 1 -> Input: 3.3 <- -> State: 3.3 <- user.request_perform = 1 trm.object_add_ts = 2 trm.question.responding = 1 trm.question.respond = 1 trm.action_refresh = 0 trm.request_response = 1 cc.object_add_ts = 2 cc.user_leave_ts = 2 ga.action_add_object = 1 ga.action_join_user = 0 ga.action_leave_user = 1 clock.t = 2 join = 0 add = 1 leave = 1 request = 1 authztrm = 1 rt = 0 respond = 1 trm.RESPOND = 1 trm.RESPONDING = 1 trm.POLICY = 1 cc.super_distro = 1 ga.user_joined = 0 ga.object_added = 1 -> Input: 3.4 <- -> State: 3.4 <- user.action_perform = 1 trm.object_remove_ts = 3 trm.user_join_ts = 3 trm.user_leave_ts = 2 trm.question.respond = 0 trm.action_refresh = 1 trm.request_response = 0 cc.object_remove_ts = 3 cc.user_join_ts = 3 ga.action_add_object = 0 ga.action_remove_object = 1 ga.action_join_user = 1 ga.action_leave_user = 0 clock.t = 3 join = 1 add = 0 leave = 0 remove = 1 authztrm = 0 rt = 1 perform = 1 respond = 0 trm.RESPOND = 0 trm.POLICY = 0 cc.super_distro = 0 ga.user_joined = 1 ga.object_added = 0 -> Input: 3.5 <- -> State: 3.5 <- user.request_perform = 0 user.action_perform = 0 ga.action_remove_object = 0 ga.action_join_user = 0 clock.t = 4 join = 0 remove = 0 request = 0 perform = 0 -> Input: 3.6 <- -- Loop starts here -> State: 3.6 <- trm.action_refresh = 0 clock.t = 5 rt = 0 clock.HAS_MORE = 0 -> Input: 3.7 <- -> State: 3.7 <- -- 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