diff --git a/1.RASD/res/alloy/AlloyPowerEnjoy.als b/1.RASD/res/alloy/AlloyPowerEnjoy.als index 933172e..043a87c 100644 --- a/1.RASD/res/alloy/AlloyPowerEnjoy.als +++ b/1.RASD/res/alloy/AlloyPowerEnjoy.als @@ -297,7 +297,9 @@ fact noMultipleUsersForTheSameRequest { // The same Request cannot be performed by two different User fact noDifferentUserForTheSameRequest { - all r : RMSS | r in r.user.request + (all u1, u2 : User | u1 != u2 implies + (no r : RMSS | r in u1.request and r in u2.request) + ) } // The same User cannot have two ACTIVE Requests