; Declare options and fixedpoint (set-logic HORN) ;---------- FUNCTION DECLARATION --------- ; Declare the relations, each relation manage one intended user (declare-fun u0 (Int Int Int Int) Bool) (declare-fun u1 (Int Int Int Int) Bool) ;---------- INITIALIZE VARIABLES --------- (assert (forall ( (b_0 Int) (track_0_Nurse Int) (track_0_target Int) (track_0_SUPER_ROLE Int)) (=> (and (= b_0 0) (= track_0_Nurse 0) (= track_0_target 0) (= track_0_SUPER_ROLE 0)) (u0 b_0 track_0_Nurse track_0_target track_0_SUPER_ROLE)))) (assert (forall ( (b_1 Int) (track_1_Nurse Int) (track_1_target Int) (track_1_SUPER_ROLE Int)) (=> (and (= b_1 0) (= track_1_Nurse 0) (= track_1_target 0) (= track_1_SUPER_ROLE 0)) (u1 b_1 track_1_Nurse track_1_target track_1_SUPER_ROLE)))) ;---------- CONFIGURATION_USERS --------- ; Configuration of user0 (assert (forall ( (b_0 Int) (b_0_1 Int) (track_0_Nurse Int) (track_0_target Int) (track_0_SUPER_ROLE Int)) (=> (and (u0 b_0 track_0_Nurse track_0_target track_0_SUPER_ROLE) (= b_0 0) (= b_0_1 1) (= track_0_Nurse 0) (= track_0_target 0) (= track_0_SUPER_ROLE 0)) (u0 b_0_1 track_0_Nurse track_0_target track_0_SUPER_ROLE)))) (assert (forall ( (b_1 Int) (b_1_1 Int) (track_1_Nurse Int) (track_1_target Int) (track_1_SUPER_ROLE Int)) (=> (and (u1 b_1 track_1_Nurse track_1_target track_1_SUPER_ROLE) (= b_1 0) (= b_1_1 1) (= track_1_Nurse 0) (= track_1_target 0) (= track_1_SUPER_ROLE 0)) (u1 b_1_1 track_1_Nurse track_1_target track_1_SUPER_ROLE)))) ; Configuration of user1 (assert (forall ( (b_0 Int) (b_0_1 Int) (track_0_Nurse Int) (track_0_target Int) (track_0_SUPER_ROLE Int)) (=> (and (u0 b_0 track_0_Nurse track_0_target track_0_SUPER_ROLE) (= b_0 0) (= b_0_1 1) (= track_0_Nurse 0) (= track_0_target 0) (= track_0_SUPER_ROLE 0)) (u0 b_0_1 track_0_Nurse track_0_target track_0_SUPER_ROLE)))) (assert (forall ( (b_1 Int) (b_1_1 Int) (track_1_Nurse Int) (track_1_target Int) (track_1_SUPER_ROLE Int)) (=> (and (u1 b_1 track_1_Nurse track_1_target track_1_SUPER_ROLE) (= b_1 0) (= b_1_1 1) (= track_1_Nurse 0) (= track_1_target 0) (= track_1_SUPER_ROLE 0)) (u1 b_1_1 track_1_Nurse track_1_target track_1_SUPER_ROLE)))) ; Configuration of SUPER_USER (assert (forall ( (b_0 Int) (b_0_1 Int) (track_0_Nurse Int) (track_0_target Int) (track_0_SUPER_ROLE Int) (track_0_SUPER_ROLE_1 Int)) (=> (and (u0 b_0 track_0_Nurse track_0_target track_0_SUPER_ROLE) (= b_0 0) (= b_0_1 1) (= track_0_Nurse 0) (= track_0_target 0) (= track_0_SUPER_ROLE 0) (= track_0_SUPER_ROLE_1 1)) (u0 b_0_1 track_0_Nurse track_0_target track_0_SUPER_ROLE_1)))) (assert (forall ( (b_1 Int) (b_1_1 Int) (track_1_Nurse Int) (track_1_target Int) (track_1_SUPER_ROLE Int) (track_1_SUPER_ROLE_1 Int)) (=> (and (u1 b_1 track_1_Nurse track_1_target track_1_SUPER_ROLE) (= b_1 0) (= b_1_1 1) (= track_1_Nurse 0) (= track_1_target 0) (= track_1_SUPER_ROLE 0) (= track_1_SUPER_ROLE_1 1)) (u1 b_1_1 track_1_Nurse track_1_target track_1_SUPER_ROLE_1)))) ; Configuration of user131 (assert (forall ( (b_0 Int) (b_0_1 Int) (track_0_Nurse Int) (track_0_Nurse_1 Int) (track_0_target Int) (track_0_SUPER_ROLE Int)) (=> (and (u0 b_0 track_0_Nurse track_0_target track_0_SUPER_ROLE) (= b_0 0) (= b_0_1 1) (= track_0_Nurse 0) (= track_0_Nurse_1 1) (= track_0_target 0) (= track_0_SUPER_ROLE 0)) (u0 b_0_1 track_0_Nurse_1 track_0_target track_0_SUPER_ROLE)))) (assert (forall ( (b_1 Int) (b_1_1 Int) (track_1_Nurse Int) (track_1_Nurse_1 Int) (track_1_target Int) (track_1_SUPER_ROLE Int)) (=> (and (u1 b_1 track_1_Nurse track_1_target track_1_SUPER_ROLE) (= b_1 0) (= b_1_1 1) (= track_1_Nurse 0) (= track_1_Nurse_1 1) (= track_1_target 0) (= track_1_SUPER_ROLE 0)) (u1 b_1_1 track_1_Nurse_1 track_1_target track_1_SUPER_ROLE)))) ; Configuration of user132 (assert (forall ( (b_0 Int) (b_0_1 Int) (track_0_Nurse Int) (track_0_Nurse_1 Int) (track_0_target Int) (track_0_SUPER_ROLE Int)) (=> (and (u0 b_0 track_0_Nurse track_0_target track_0_SUPER_ROLE) (= b_0 0) (= b_0_1 1) (= track_0_Nurse 0) (= track_0_Nurse_1 1) (= track_0_target 0) (= track_0_SUPER_ROLE 0)) (u0 b_0_1 track_0_Nurse_1 track_0_target track_0_SUPER_ROLE)))) (assert (forall ( (b_1 Int) (b_1_1 Int) (track_1_Nurse Int) (track_1_Nurse_1 Int) (track_1_target Int) (track_1_SUPER_ROLE Int)) (=> (and (u1 b_1 track_1_Nurse track_1_target track_1_SUPER_ROLE) (= b_1 0) (= b_1_1 1) (= track_1_Nurse 0) (= track_1_Nurse_1 1) (= track_1_target 0) (= track_1_SUPER_ROLE 0)) (u1 b_1_1 track_1_Nurse_1 track_1_target track_1_SUPER_ROLE)))) ;---------- SIMULATION OF RULES --------- ;--------------------------Can assign rule------------------------ ;--------- ;--------------------------------------------------------------- (assert (forall ( (b_0 Int) (track_0_Nurse Int) (track_0_target Int) (track_0_target_1 Int) (track_0_SUPER_ROLE Int)) (=> (and (and (u0 b_0 track_0_Nurse track_0_target track_0_SUPER_ROLE) (= b_0 1) (= track_0_SUPER_ROLE 1)) (= b_0 1) (= track_0_Nurse 1) (= track_0_target 0) (= track_0_target_1 1))(u0 b_0 track_0_Nurse track_0_target_1 track_0_SUPER_ROLE)))) (assert (forall ( (b_0 Int) (track_0_Nurse Int) (track_0_target Int) (track_0_target_1 Int) (track_0_SUPER_ROLE Int) (b_1 Int) (track_1_Nurse Int) (track_1_target Int) (track_1_SUPER_ROLE Int)) (=> (and (and (u1 b_1 track_1_Nurse track_1_target track_1_SUPER_ROLE) (= b_1 1) (= track_1_SUPER_ROLE 1)) (= b_0 1) (= track_0_Nurse 1) (= track_0_target 0) (u0 b_0 track_0_Nurse track_0_target track_0_SUPER_ROLE) (= track_0_target_1 1))(u0 b_0 track_0_Nurse track_0_target_1 track_0_SUPER_ROLE)))) (assert (forall ( (b_1 Int) (track_1_Nurse Int) (track_1_target Int) (track_1_target_1 Int) (track_1_SUPER_ROLE Int) (b_0 Int) (track_0_Nurse Int) (track_0_target Int) (track_0_SUPER_ROLE Int)) (=> (and (and (u0 b_0 track_0_Nurse track_0_target track_0_SUPER_ROLE) (= b_0 1) (= track_0_SUPER_ROLE 1)) (= b_1 1) (= track_1_Nurse 1) (= track_1_target 0) (u1 b_1 track_1_Nurse track_1_target track_1_SUPER_ROLE) (= track_1_target_1 1))(u1 b_1 track_1_Nurse track_1_target_1 track_1_SUPER_ROLE)))) (assert (forall ( (b_1 Int) (track_1_Nurse Int) (track_1_target Int) (track_1_target_1 Int) (track_1_SUPER_ROLE Int)) (=> (and (and (u1 b_1 track_1_Nurse track_1_target track_1_SUPER_ROLE) (= b_1 1) (= track_1_SUPER_ROLE 1)) (= b_1 1) (= track_1_Nurse 1) (= track_1_target 0) (= track_1_target_1 1))(u1 b_1 track_1_Nurse track_1_target_1 track_1_SUPER_ROLE)))) ;-----------------------Can revoke rule------------------------ ;----------- ;------------------------------------------------------------ (assert (forall ( (b_0 Int) (track_0_Nurse Int) (track_0_Nurse_1 Int) (track_0_target Int) (track_0_SUPER_ROLE Int)) (=> (and (and (u0 b_0 track_0_Nurse track_0_target track_0_SUPER_ROLE) (= b_0 1) (= track_0_SUPER_ROLE 1)) (= b_0 1) (= track_0_Nurse 1) (= track_0_Nurse_1 0))(u0 b_0 track_0_Nurse_1 track_0_target track_0_SUPER_ROLE)))) (assert (forall ( (b_0 Int) (track_0_Nurse Int) (track_0_Nurse_1 Int) (track_0_target Int) (track_0_SUPER_ROLE Int) (b_1 Int) (track_1_Nurse Int) (track_1_target Int) (track_1_SUPER_ROLE Int)) (=> (and (and (u1 b_1 track_1_Nurse track_1_target track_1_SUPER_ROLE) (= b_1 1) (= track_1_SUPER_ROLE 1)) (= b_0 1) (= track_0_Nurse 1) (u0 b_0 track_0_Nurse track_0_target track_0_SUPER_ROLE) (= track_0_Nurse_1 0))(u0 b_0 track_0_Nurse_1 track_0_target track_0_SUPER_ROLE)))) (assert (forall ( (b_1 Int) (track_1_Nurse Int) (track_1_Nurse_1 Int) (track_1_target Int) (track_1_SUPER_ROLE Int) (b_0 Int) (track_0_Nurse Int) (track_0_target Int) (track_0_SUPER_ROLE Int)) (=> (and (and (u0 b_0 track_0_Nurse track_0_target track_0_SUPER_ROLE) (= b_0 1) (= track_0_SUPER_ROLE 1)) (= b_1 1) (= track_1_Nurse 1) (u1 b_1 track_1_Nurse track_1_target track_1_SUPER_ROLE) (= track_1_Nurse_1 0))(u1 b_1 track_1_Nurse_1 track_1_target track_1_SUPER_ROLE)))) (assert (forall ( (b_1 Int) (track_1_Nurse Int) (track_1_Nurse_1 Int) (track_1_target Int) (track_1_SUPER_ROLE Int)) (=> (and (and (u1 b_1 track_1_Nurse track_1_target track_1_SUPER_ROLE) (= b_1 1) (= track_1_SUPER_ROLE 1)) (= b_1 1) (= track_1_Nurse 1) (= track_1_Nurse_1 0))(u1 b_1 track_1_Nurse_1 track_1_target track_1_SUPER_ROLE)))) ;------------- The query ------------ (assert (not (exists ( (b_0 Int) (track_0_Nurse Int) (track_0_target Int) (track_0_SUPER_ROLE Int)) (and (= track_0_target 1) (u0 b_0 track_0_Nurse track_0_target track_0_SUPER_ROLE))))) (assert (not (exists ( (b_1 Int) (track_1_Nurse Int) (track_1_target Int) (track_1_SUPER_ROLE Int)) (and (= track_1_target 1) (u1 b_1 track_1_Nurse track_1_target track_1_SUPER_ROLE))))) (check-sat)