Counter Example Trace:
Specification of query: Can user1 REACH role1 ?

==> Step 1:
Target User: user1
CAN ASSIGN rule applied to user1: <role3,-role0,role1>
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