peperunas/swing2
1
0
Fork 0
Code Issues 3 Pull Requests Releases Wiki Activity

noDifferentUserForTheSameRequest fixed

Browse Source
This commit is contained in:
Giulio De Pasquale 2017-01-22 16:55:06 +01:00
parent 19dced1ec5
commit 3c020cf42f
1 changed files with 3 additions and 1 deletions
Show Stats Download Patch File Download Diff File Expand all files Collapse all files

4
1.RASD/res/alloy/AlloyPowerEnjoy.als
View File

@ -297,7 +297,9 @@ fact noMultipleUsersForTheSameRequest {
// The same Request cannot be performed by two different User // The same Request cannot be performed by two different User
fact noDifferentUserForTheSameRequest { 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 // The same User cannot have two ACTIVE Requests