From 3c020cf42fe7d2e1d6862d8bdb4d4536df315d0c Mon Sep 17 00:00:00 2001 From: Giulio De Pasquale Date: Sun, 22 Jan 2017 16:55:06 +0100 Subject: [PATCH] noDifferentUserForTheSameRequest fixed --- 1.RASD/res/alloy/AlloyPowerEnjoy.als | 4 +++- 1 file changed, 3 insertions(+), 1 deletion(-) 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