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

No duplicate payments, alloy

Browse Source
This commit is contained in:
Giulio De Pasquale 2017-01-22 13:45:37 +01:00
parent 5ef9863bf3
commit b494e177c2
1 changed files with 6 additions and 0 deletions
Show Stats Download Patch File Download Diff File Expand all files Collapse all files

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

@ -266,6 +266,12 @@ fact pendingPaymentForActiveRequest {
(all r : RMSS | r.status = ACTIVE implies r.paymentStatus = PENDING) (all r : RMSS | r.status = ACTIVE implies r.paymentStatus = PENDING)
} }
// There are no duplicate payments
fact noDuplicatePayments {
(all r1, r2 : RMSS | r1 != r2 and r1.paymentStatus = PENDING and r2.paymentStatus = PENDING implies
(all p1, p2 : Payment | p1 != p2 and p1 in r1.events and p2 in r2.events)
)
}
// No Multiple Users for the same Request // No Multiple Users for the same Request
fact noMultipleUsersForTheSameRequest { fact noMultipleUsersForTheSameRequest {
no disj u1, u2 : User | u1.request & u2.request != none no disj u1, u2 : User | u1.request & u2.request != none