Counter Example Trace: Role to check REACHABILITY: 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: ThirdParty ==> Step 2: Target User: user4 CAN ASSIGN rule applied to user4: Administrative user to invoke the rule: user1 Role configuration of user4 before applying rule: Doctor Role configuration of user4 after applying rule: Doctor ThirdParty ==> Step 3: Target User: user0 CAN ASSIGN rule applied to user0: Administrative user to invoke the rule: user1031 Role configuration of user0 before applying rule: ThirdParty Role configuration of user0 after applying rule: ThirdParty Patient ==> Step 4: Target User: user0 CAN ASSIGN rule applied to user0: Administrative user to invoke the rule: user0 Role configuration of user0 before applying rule: ThirdParty Patient Role configuration of user0 after applying rule: ThirdParty Patient PatientWithTPC ==> Step 5: Target User: user4 CAN ASSIGN rule applied to user4: Administrative user to invoke the rule: user1031 Role configuration of user4 before applying rule: Doctor ThirdParty Role configuration of user4 after applying rule: Doctor ThirdParty Patient ==> Step 6: Target User: user4 CAN ASSIGN rule applied to user4: Administrative user to invoke the rule: user4 Role configuration of user4 before applying rule: Doctor ThirdParty Patient Role configuration of user4 after applying rule: Doctor ThirdParty Patient PatientWithTPC ==> 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: ThirdParty Patient PatientWithTPC Role configuration of user0 after applying rule: ThirdParty Patient PatientWithTPC target user0 can REACH target target is REACHABLE