Counter Example Trace: Specification of query: Can user0 REACH target ? ==> Step 1: Target User: user0 CAN ASSIGN rule applied to user0: Administrative user to invoke the rule: user1 Role configuration of user0 before applying rule: No role Role configuration of user0 after applying rule: Employee ==> Step 2: Target User: user0 CAN ASSIGN rule applied to user0: Administrative user to invoke the rule: user1 Role configuration of user0 before applying rule: Employee Role configuration of user0 after applying rule: Employee FA3 ==> Step 3: Target User: user0 CAN ASSIGN rule applied to user0: Administrative user to invoke the rule: user1 Role configuration of user0 before applying rule: Employee FA3 Role configuration of user0 after applying rule: Employee FA3 FAClerk3 ==> Step 4: Target User: user0 CAN ASSIGN rule applied to user0: Administrative user to invoke the rule: user1 Role configuration of user0 before applying rule: Employee FA3 FAClerk3 Role configuration of user0 after applying rule: Employee FA3 FAClerk3 FASenior3 ==> Step 5: Target User: user0 CAN ASSIGN rule applied to user0: Administrative user to invoke the rule: user1 Role configuration of user0 before applying rule: Employee FA3 FAClerk3 FASenior3 Role configuration of user0 after applying rule: Employee FA3 FAClerk3 FASenior3 FAJunior3 ==> Step 6: Target User: user0 CAN ASSIGN rule applied to user0: Administrative user to invoke the rule: user1 Role configuration of user0 before applying rule: Employee FA3 FAClerk3 FASenior3 FAJunior3 Role configuration of user0 after applying rule: Employee FA3 FAClerk3 FASenior3 FAJunior3 FASpecial3 ==> Step 7: Target User: user0 CAN ASSIGN rule applied to user0: Administrative user to invoke the rule: user1 Role configuration of user0 before applying rule: Employee FA3 FAClerk3 FASenior3 FAJunior3 FASpecial3 Role configuration of user0 after applying rule: Employee FA3 FAClerk3 FASenior3 FAJunior3 FASpecial3 anyfour3 ==> Step 8: Target User: user0 CAN ASSIGN rule applied to user0: Administrative user to invoke the rule: user1 Role configuration of user0 before applying rule: Employee FA3 FAClerk3 FASenior3 FAJunior3 FASpecial3 anyfour3 Role configuration of user0 after applying rule: Employee FA3 FAClerk3 FASenior3 FAJunior3 FASpecial3 anyfour3 FA4 ==> Step 9: Target User: user0 CAN ASSIGN rule applied to user0: Administrative user to invoke the rule: user1 Role configuration of user0 before applying rule: Employee FA3 FAClerk3 FASenior3 FAJunior3 FASpecial3 anyfour3 FA4 Role configuration of user0 after applying rule: Employee FA3 FAClerk3 FASenior3 FAJunior3 FASpecial3 anyfour3 FA4 FAClerk4 ==> Step 10: Target User: user0 CAN ASSIGN rule applied to user0: Administrative user to invoke the rule: user1 Role configuration of user0 before applying rule: Employee FA3 FAClerk3 FASenior3 FAJunior3 FASpecial3 anyfour3 FA4 FAClerk4 Role configuration of user0 after applying rule: Employee FA3 FAClerk3 FASenior3 FAJunior3 FASpecial3 anyfour3 FA4 FAClerk4 FASenior4 ==> Step 11: Target User: user0 CAN ASSIGN rule applied to user0: Administrative user to invoke the rule: user1 Role configuration of user0 before applying rule: Employee FA3 FAClerk3 FASenior3 FAJunior3 FASpecial3 anyfour3 FA4 FAClerk4 FASenior4 Role configuration of user0 after applying rule: Employee FA3 FAClerk3 FASenior3 FAJunior3 FASpecial3 anyfour3 FA4 FAClerk4 FASenior4 FAJunior4 ==> Step 12: Target User: user0 CAN ASSIGN rule applied to user0: Administrative user to invoke the rule: user1 Role configuration of user0 before applying rule: Employee FA3 FAClerk3 FASenior3 FAJunior3 FASpecial3 anyfour3 FA4 FAClerk4 FASenior4 FAJunior4 Role configuration of user0 after applying rule: Employee FA3 FAClerk3 FASenior3 FAJunior3 FASpecial3 anyfour3 FA4 FAClerk4 FASenior4 FAJunior4 FASpecial4 ==> Step 13: Target User: user0 CAN ASSIGN rule applied to user0: Administrative user to invoke the rule: user1 Role configuration of user0 before applying rule: Employee FA3 FAClerk3 FASenior3 FAJunior3 FASpecial3 anyfour3 FA4 FAClerk4 FASenior4 FAJunior4 FASpecial4 Role configuration of user0 after applying rule: Employee FA3 FAClerk3 FASenior3 FAJunior3 FASpecial3 anyfour3 FA4 FAClerk4 FASenior4 FAJunior4 FASpecial4 anyfour4 ==> Step 14: Target User: user0 CAN ASSIGN rule applied to user0: Administrative user to invoke the rule: user1 Role configuration of user0 before applying rule: Employee FA3 FAClerk3 FASenior3 FAJunior3 FASpecial3 anyfour3 FA4 FAClerk4 FASenior4 FAJunior4 FASpecial4 anyfour4 Role configuration of user0 after applying rule: Employee FA3 FAClerk3 FASenior3 FAJunior3 FASpecial3 anyfour3 FA4 FAClerk4 FASenior4 FAJunior4 FASpecial4 anyfour4 FA1 ==> Step 15: Target User: user0 CAN ASSIGN rule applied to user0: Administrative user to invoke the rule: user1 Role configuration of user0 before applying rule: Employee FA3 FAClerk3 FASenior3 FAJunior3 FASpecial3 anyfour3 FA4 FAClerk4 FASenior4 FAJunior4 FASpecial4 anyfour4 FA1 Role configuration of user0 after applying rule: Employee FA3 FAClerk3 FASenior3 FAJunior3 FASpecial3 anyfour3 FA4 FAClerk4 FASenior4 FAJunior4 FASpecial4 anyfour4 FA1 FAClerk1 ==> Step 16: Target User: user0 CAN ASSIGN rule applied to user0: Administrative user to invoke the rule: user1 Role configuration of user0 before applying rule: Employee FA3 FAClerk3 FASenior3 FAJunior3 FASpecial3 anyfour3 FA4 FAClerk4 FASenior4 FAJunior4 FASpecial4 anyfour4 FA1 FAClerk1 Role configuration of user0 after applying rule: Employee FA3 FAClerk3 FASenior3 FAJunior3 FASpecial3 anyfour3 FA4 FAClerk4 FASenior4 FAJunior4 FASpecial4 anyfour4 FA1 FAClerk1 FASenior1 ==> Step 17: Target User: user0 CAN ASSIGN rule applied to user0: Administrative user to invoke the rule: user1 Role configuration of user0 before applying rule: Employee FA3 FAClerk3 FASenior3 FAJunior3 FASpecial3 anyfour3 FA4 FAClerk4 FASenior4 FAJunior4 FASpecial4 anyfour4 FA1 FAClerk1 FASenior1 Role configuration of user0 after applying rule: Employee FA3 FAClerk3 FASenior3 FAJunior3 FASpecial3 anyfour3 FA4 FAClerk4 FASenior4 FAJunior4 FASpecial4 anyfour4 FA1 FAClerk1 FASenior1 FAJunior1 ==> Step 18: Target User: user0 CAN ASSIGN rule applied to user0: Administrative user to invoke the rule: user1 Role configuration of user0 before applying rule: Employee FA3 FAClerk3 FASenior3 FAJunior3 FASpecial3 anyfour3 FA4 FAClerk4 FASenior4 FAJunior4 FASpecial4 anyfour4 FA1 FAClerk1 FASenior1 FAJunior1 Role configuration of user0 after applying rule: Employee FA3 FAClerk3 FASenior3 FAJunior3 FASpecial3 anyfour3 FA4 FAClerk4 FASenior4 FAJunior4 FASpecial4 anyfour4 FA1 FAClerk1 FASenior1 FAJunior1 FASpecial1 ==> Step 19: Target User: user0 CAN ASSIGN rule applied to user0: Administrative user to invoke the rule: user1 Role configuration of user0 before applying rule: Employee FA3 FAClerk3 FASenior3 FAJunior3 FASpecial3 anyfour3 FA4 FAClerk4 FASenior4 FAJunior4 FASpecial4 anyfour4 FA1 FAClerk1 FASenior1 FAJunior1 FASpecial1 Role configuration of user0 after applying rule: Employee FA3 FAClerk3 FASenior3 FAJunior3 FASpecial3 anyfour3 FA4 FAClerk4 FASenior4 FAJunior4 FASpecial4 anyfour4 FA1 FAClerk1 FASenior1 FAJunior1 FASpecial1 anyfour1 ==> Step 20: Target User: user0 CAN ASSIGN rule applied to user0: Administrative user to invoke the rule: user1 Role configuration of user0 before applying rule: Employee FA3 FAClerk3 FASenior3 FAJunior3 FASpecial3 anyfour3 FA4 FAClerk4 FASenior4 FAJunior4 FASpecial4 anyfour4 FA1 FAClerk1 FASenior1 FAJunior1 FASpecial1 anyfour1 Role configuration of user0 after applying rule: Employee FA3 FAClerk3 FASenior3 FAJunior3 FASpecial3 anyfour3 FA4 FAClerk4 FASenior4 FAJunior4 FASpecial4 anyfour4 FA1 FAClerk1 FASenior1 FAJunior1 FASpecial1 anyfour1 FA2 ==> Step 21: Target User: user0 CAN ASSIGN rule applied to user0: Administrative user to invoke the rule: user1 Role configuration of user0 before applying rule: Employee FA3 FAClerk3 FASenior3 FAJunior3 FASpecial3 anyfour3 FA4 FAClerk4 FASenior4 FAJunior4 FASpecial4 anyfour4 FA1 FAClerk1 FASenior1 FAJunior1 FASpecial1 anyfour1 FA2 Role configuration of user0 after applying rule: Employee FA3 FAClerk3 FASenior3 FAJunior3 FASpecial3 anyfour3 FA4 FAClerk4 FASenior4 FAJunior4 FASpecial4 anyfour4 FA1 FAClerk1 FASenior1 FAJunior1 FASpecial1 anyfour1 FA2 FAClerk2 ==> Step 22: Target User: user0 CAN ASSIGN rule applied to user0: Administrative user to invoke the rule: user1 Role configuration of user0 before applying rule: Employee FA3 FAClerk3 FASenior3 FAJunior3 FASpecial3 anyfour3 FA4 FAClerk4 FASenior4 FAJunior4 FASpecial4 anyfour4 FA1 FAClerk1 FASenior1 FAJunior1 FASpecial1 anyfour1 FA2 FAClerk2 Role configuration of user0 after applying rule: Employee FA3 FAClerk3 FASenior3 FAJunior3 FASpecial3 anyfour3 FA4 FAClerk4 FASenior4 FAJunior4 FASpecial4 anyfour4 FA1 FAClerk1 FASenior1 FAJunior1 FASpecial1 anyfour1 FA2 FAClerk2 FASenior2 ==> Step 23: Target User: user0 CAN ASSIGN rule applied to user0: Administrative user to invoke the rule: user1 Role configuration of user0 before applying rule: Employee FA3 FAClerk3 FASenior3 FAJunior3 FASpecial3 anyfour3 FA4 FAClerk4 FASenior4 FAJunior4 FASpecial4 anyfour4 FA1 FAClerk1 FASenior1 FAJunior1 FASpecial1 anyfour1 FA2 FAClerk2 FASenior2 Role configuration of user0 after applying rule: Employee FA3 FAClerk3 FASenior3 FAJunior3 FASpecial3 anyfour3 FA4 FAClerk4 FASenior4 FAJunior4 FASpecial4 anyfour4 FA1 FAClerk1 FASenior1 FAJunior1 FASpecial1 anyfour1 FA2 FAClerk2 FASenior2 FAJunior2 ==> Step 24: Target User: user0 CAN ASSIGN rule applied to user0: Administrative user to invoke the rule: user1 Role configuration of user0 before applying rule: Employee FA3 FAClerk3 FASenior3 FAJunior3 FASpecial3 anyfour3 FA4 FAClerk4 FASenior4 FAJunior4 FASpecial4 anyfour4 FA1 FAClerk1 FASenior1 FAJunior1 FASpecial1 anyfour1 FA2 FAClerk2 FASenior2 FAJunior2 Role configuration of user0 after applying rule: Employee FA3 FAClerk3 FASenior3 FAJunior3 FASpecial3 anyfour3 FA4 FAClerk4 FASenior4 FAJunior4 FASpecial4 anyfour4 FA1 FAClerk1 FASenior1 FAJunior1 FASpecial1 anyfour1 FA2 FAClerk2 FASenior2 FAJunior2 FASpecial2 ==> Step 25: Target User: user0 CAN ASSIGN rule applied to user0: Administrative user to invoke the rule: user1 Role configuration of user0 before applying rule: Employee FA3 FAClerk3 FASenior3 FAJunior3 FASpecial3 anyfour3 FA4 FAClerk4 FASenior4 FAJunior4 FASpecial4 anyfour4 FA1 FAClerk1 FASenior1 FAJunior1 FASpecial1 anyfour1 FA2 FAClerk2 FASenior2 FAJunior2 FASpecial2 Role configuration of user0 after applying rule: Employee FA3 FAClerk3 FASenior3 FAJunior3 FASpecial3 anyfour3 FA4 FAClerk4 FASenior4 FAJunior4 FASpecial4 anyfour4 FA1 FAClerk1 FASenior1 FAJunior1 FASpecial1 anyfour1 FA2 FAClerk2 FASenior2 FAJunior2 FASpecial2 anyfour2 ==> Step 26: Target User: user0 CAN ASSIGN rule applied to user0: Administrative user to invoke the rule: user1 Role configuration of user0 before applying rule: Employee FA3 FAClerk3 FASenior3 FAJunior3 FASpecial3 anyfour3 FA4 FAClerk4 FASenior4 FAJunior4 FASpecial4 anyfour4 FA1 FAClerk1 FASenior1 FAJunior1 FASpecial1 anyfour1 FA2 FAClerk2 FASenior2 FAJunior2 FASpecial2 anyfour2 Role configuration of user0 after applying rule: Employee FA3 FAClerk3 FASenior3 FAJunior3 FASpecial3 anyfour3 FA4 FAClerk4 FASenior4 FAJunior4 FASpecial4 anyfour4 FA1 FAClerk1 FASenior1 FAJunior1 FASpecial1 anyfour1 FA2 FAClerk2 FASenior2 FAJunior2 FASpecial2 anyfour2 target user0 can REACH target target is REACHABLE