; 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 Int) Bool) ;---------- INITIALIZE VARIABLES --------- (assert (forall ( (b_0 Int) (track_0_target Int) (track_0_SUPER_ROLE Int) (track_0_ToCheckRole Int) (track_0_TargetPrime Int)) (=> (and (= b_0 0) (= track_0_target 0) (= track_0_SUPER_ROLE 0) (= track_0_ToCheckRole 0) (= track_0_TargetPrime 0)) (u0 b_0 track_0_target track_0_SUPER_ROLE track_0_ToCheckRole track_0_TargetPrime)))) ;---------- CONFIGURATION_USERS --------- ; Configuration of SUPER_USER (assert (forall ( (b_0 Int) (b_0_1 Int) (track_0_target Int) (track_0_SUPER_ROLE Int) (track_0_SUPER_ROLE_1 Int) (track_0_ToCheckRole Int) (track_0_ToCheckRole_1 Int) (track_0_TargetPrime Int)) (=> (and (u0 b_0 track_0_target track_0_SUPER_ROLE track_0_ToCheckRole track_0_TargetPrime) (= b_0 0) (= b_0_1 1) (= track_0_target 0) (= track_0_SUPER_ROLE 0) (= track_0_SUPER_ROLE_1 1) (= track_0_ToCheckRole 0) (= track_0_ToCheckRole_1 1) (= track_0_TargetPrime 0)) (u0 b_0_1 track_0_target track_0_SUPER_ROLE_1 track_0_ToCheckRole_1 track_0_TargetPrime)))) ; Configuration of user1 (assert (forall ( (b_0 Int) (b_0_1 Int) (track_0_target Int) (track_0_SUPER_ROLE Int) (track_0_ToCheckRole Int) (track_0_TargetPrime Int)) (=> (and (u0 b_0 track_0_target track_0_SUPER_ROLE track_0_ToCheckRole track_0_TargetPrime) (= b_0 0) (= b_0_1 1) (= track_0_target 0) (= track_0_SUPER_ROLE 0) (= track_0_ToCheckRole 0) (= track_0_TargetPrime 0)) (u0 b_0_1 track_0_target track_0_SUPER_ROLE track_0_ToCheckRole track_0_TargetPrime)))) ;---------- SIMULATION OF RULES --------- ;--------------------------Can assign rule------------------------ ;--------- ;--------------------------------------------------------------- (assert (forall ( (b_0 Int) (track_0_target Int) (track_0_SUPER_ROLE Int) (track_0_ToCheckRole Int) (track_0_TargetPrime Int) (track_0_TargetPrime_1 Int)) (=> (and (and (u0 b_0 track_0_target track_0_SUPER_ROLE track_0_ToCheckRole track_0_TargetPrime) (= b_0 1) (= track_0_ToCheckRole 1)) (= b_0 1) (= track_0_ToCheckRole 1) (= track_0_target 1) (= track_0_TargetPrime 0) (= track_0_TargetPrime_1 1))(u0 b_0 track_0_target track_0_SUPER_ROLE track_0_ToCheckRole track_0_TargetPrime_1)))) ;------------- The query ------------ (assert (not (exists ( (b_0 Int) (track_0_target Int) (track_0_SUPER_ROLE Int) (track_0_ToCheckRole Int) (track_0_TargetPrime Int)) (and (= track_0_TargetPrime 1) (u0 b_0 track_0_target track_0_SUPER_ROLE track_0_ToCheckRole track_0_TargetPrime))))) (check-sat)