From b494e177c2d4095ded968591eb3c5f0594d0277c Mon Sep 17 00:00:00 2001 From: Giulio De Pasquale Date: Sun, 22 Jan 2017 13:45:37 +0100 Subject: [PATCH] No duplicate payments, alloy --- 1.RASD/res/alloy/AlloyPowerEnjoy.als | 6 ++++++ 1 file changed, 6 insertions(+) diff --git a/1.RASD/res/alloy/AlloyPowerEnjoy.als b/1.RASD/res/alloy/AlloyPowerEnjoy.als index deecc3d..7a25f90 100644 --- a/1.RASD/res/alloy/AlloyPowerEnjoy.als +++ b/1.RASD/res/alloy/AlloyPowerEnjoy.als @@ -266,6 +266,12 @@ fact pendingPaymentForActiveRequest { (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 fact noMultipleUsersForTheSameRequest { no disj u1, u2 : User | u1.request & u2.request != none