Counter Example Trace: Specification of query: Can user1 REACH role1 ? ==> Step 1: Target User: user0 CAN ASSIGN rule applied to user0: Administrative user to invoke the rule: user4 Role configuration of user0 before applying rule: No role Role configuration of user0 after applying rule: role1 ==> Step 2: Target User: user1 CAN ASSIGN rule applied to user1: Administrative user to invoke the rule: user4 Role configuration of user1 before applying rule: No role Role configuration of user1 after applying rule: role1 user1 can REACH role1 role1 is REACHABLE