module NEGOTIATION_TYPES is ------------------------------------------------------------------------------- -- Data type of books for the book auction example ------------------------------------------------------------------------------- -- Books are represented by four-tuples , where -- * ref is the reference number of the book, -- * price is the price of the book, -- * days is the number of days for delivery of the book, and -- * returnok equals true iff the book can be returned after purchase. type BOOK is Book (ref, price, days: Nat, returnok: Bool) with get, set end type ------------------------------------------------------------------------------- -- Predefined invariants and conformance tests for the book auction example ------------------------------------------------------------------------------- -- Invariants or conformance tests are used by processes to decide if a value -- proposed during a negotiation round is acceptable. type Inv is -- predefined invariants -- pMinYYY: the price has to be at least 'YYY' pMin2, pMin3, pMin4, pMin5, pMin6, -- pMaxYYY: the price has to be at most 'YYY' pMax3, pMax4, pMax5 end type ------------------------------------------------------------------------------- function conform (price: Nat, iv: Inv) : Bool is -- function evaluating conformance of price and invariant case iv in pMin2 -> return price >= 2 | pMin3 -> return price >= 3 | pMin4 -> return price >= 4 | pMin5 -> return price >= 5 | pMin6 -> return price >= 6 | pMax3 -> return price <= 3 | pMax4 -> return price <= 4 | pMax5 -> return price <= 5 end case end function ------------------------------------------------------------------------------- -- Data type of bookstores for the book auction example ------------------------------------------------------------------------------- -- Bookstores are sets of triples , represented as lists, where -- * b is a book -- * q is the number of available copies of b, and -- * inv is the invariant associated to b type BOOKSTORE is emptyBS, addBS (b: Book, q: Nat, iv: Inv, bs: BookStore) end type ------------------------------------------------------------------------------- function retrieveInv (r: Nat, in var bs: BookStore) : Inv is loop case bs var b: Book, iv: Inv, bs1: Bookstore in emptyBS -> raise UNEXPECTED | addBS (b, any Nat, iv, bs1) -> if b.ref == r then return iv end if; bs := bs1 end case end loop end function ------------------------------------------------------------------------------- function retrievePrice (r: Nat, in var bs: BookStore) : Nat is loop case bs var b: Book, bs1: Bookstore in emptyBS -> raise UNEXPECTED | addBS (b, any Nat, any Inv, bs1) -> if b.ref == r then return b.price end if; bs := bs1 end case end loop end function ------------------------------------------------------------------------------- function isAvailable (r: Nat, in var bs: BookStore) : Bool is loop case bs var b: Book, q: Nat, bs1: Bookstore in emptyBS -> return false | addBS (b, q, any Inv, bs1) -> if b.ref == r then return q > 0 end if; bs := bs1 end case end loop end function ------------------------------------------------------------------------------- function isIn (r: Nat, in var bs: BookStore) : Bool is loop case bs var b: Book, bs1: Bookstore in emptyBS -> return false | addBS (b, any Nat, any Inv, bs1) -> if b.ref == r then return true end if; bs := bs1 end case end loop end function ------------------------------------------------------------------------------- function decrease (r: Nat, q: Nat, bs: BookStore) : BookStore is -- recursive implementation to preserve the ordering case bs var b: Book, q1: Nat, iv: Inv, bs1: Bookstore in emptyBS -> raise UNEXPECTED | addBS (b, q1, iv, bs1) -> if b.ref == r then return addBS (b, q1 - q, iv, bs1) else return addBS (b, q1, iv, decrease (r, q, bs1)) end if end case end function ------------------------------------------------------------------------------- -- Definitions of the initial stocks of all bookstores ------------------------------------------------------------------------------- function bs1 : BOOKSTORE is -- The bookstore bs1 contains eight books; three copies of the first book -- are still available, and each copy of the first book should be sold for -- at least three euros return addBS (book (0, 2, 6, true), 3, pMin3, addBS (book (1, 4, 2, false), 8, pMin5, addBS (book (2, 3, 6, true), 6, pMin4, addBS (book (3, 3, 3, false), 7, pMin4, addBS (book (4, 4, 7, true), 3, pMin4, addBS (book (5, 5, 8, true), 3, pMin5, addBS (book (6, 5, 3, true), 9, pMin6, addBS (book (7, 3, 2, false), 3, pMin5, emptyBS)))))))) end function ------------------------------------------------------------------------------- function bs2 : BOOKSTORE is return addBS (book (0, 5, 2, true), 4, pMin4, addBS (book (1, 4, 3, false), 0, pMin4, addBS (book (2, 3, 6, true), 6, pMin4, addBS (book (3, 3, 3, false), 7, pMin4, addBS (book (4, 4, 7, true), 3, pMin4, addBS (book (5, 5, 8, true), 3, pMin5, addBS (book (6, 5, 3, true), 9, pMin6, addBS (book (7, 3, 2, false), 3, pMin5, addBS (book (8, 3, 6, true), 6, pMin4, addBS (book (9, 3, 3, false), 7, pMin4, addBS (book (10, 4, 7, true), 3, pMin4, addBS (book (11, 5, 8, true), 3, pMin5, addBS (book (12, 5, 3, true), 9, pMin6, addBS (book (13, 3, 2, false), 3, pMin5, addBS (book (14, 3, 6, true), 6, pMin4, addBS (book (15, 3, 3, false), 7, pMin4, addBS (book (16, 4, 7, true), 3, pMin4, addBS (book (17, 5, 8, true), 3, pMin5, addBS (book (18, 5, 3, true), 9, pMin6, addBS (book (19, 3, 2, false), 3, pMin5, addBS (book (20, 3, 6, true), 6, pMin4, addBS (book (21, 3, 3, false), 7, pMin4, addBS (book (22, 4, 7, true), 3, pMin4, addBS (book (23, 5, 8, true), 3, pMin5, addBS (book (24, 5, 3, true), 9, pMin6, addBS (book (25, 3, 2, false), 3, pMin5, emptyBS)))))))))))))))))))))))))) end function ------------------------------------------------------------------------------- function bs3 : BOOKSTORE is return addBS (book (0, 4, 3, true), 0, pMin5, addBS (book (1, 2, 4, false), 2, pMin5, addBS (book (2, 3, 6, true), 6, pMin4, addBS (book (3, 3, 3, false), 7, pMin4, addBS (book (4, 4, 7, true), 3, pMin4, addBS (book (5, 5, 8, true), 3, pMin5, addBS (book (6, 5, 3, true), 9, pMin6, addBS (book (7, 3, 2, false), 3, pMin5, addBS (book (8, 3, 6, true), 6, pMin4, addBS (book (9, 3, 3, false), 7, pMin4, emptyBS)))))))))) end function ------------------------------------------------------------------------------- function bs4 : BOOKSTORE is return addBS (book (1, 4, 5, false), 0, pMin4, addBS (book (2, 3, 4, false), 2, pMin5, emptyBS)) end function ------------------------------------------------------------------------------- function bs5 : BOOKSTORE is return addBS (book (0, 4, 3, true), 0, pMin5, addBS (book (1, 3, 4, false), 6, pMin4, addBS (book (2, 3, 4, true), 2, pMin4, addBS (book (4, 4, 7, false), 3, pMin4, addBS (book (6, 5, 8, true), 3, pMin5, addBS (book (9, 5, 3, true), 9, pMin6, emptyBS)))))) end function ------------------------------------------------------------------------------- function bs6 : BOOKSTORE is return addBS (book (1, 4, 5, true), 0, pMin4, addBS (book (3, 2, 5, true), 2, pMin6, addBS (book (4, 3, 4, false), 2, pMin5, addBS (book (9, 3, 4, false), 2, pMin5, addBS (book (13, 3, 2, false), 3, pMin5, addBS (book (14, 3, 6, true), 6, pMin4, addBS (book (15, 3, 3, false), 7, pMin4, addBS (book (16, 4, 7, true), 3, pMin4, addBS (book (17, 5, 8, true), 3, pMin5, addBS (book (18, 5, 3, true), 9, pMin6, addBS (book (19, 3, 2, false), 3, pMin5, addBS (book (20, 3, 6, true), 6, pMin4, addBS (book (21, 3, 3, false), 7, pMin4, emptyBS))))))))))))) end function ------------------------------------------------------------------------------- function bs7 : BOOKSTORE is return addBS (book (0, 4, 3, true), 4, pMin4, addBS (book (1, 3, 4, false), 6, pMin4, addBS (book (4, 3, 4, false), 2, pMin5, emptyBS))) end function ------------------------------------------------------------------------------- function bs8 : BOOKSTORE is return addBS (book (1, 4, 5, true), 0, pMin5, addBS (book (3, 2, 5, true), 5, pMin6, addBS (book (4, 3, 4, false), 2, pMin5, addBS (book (6, 3, 4, false), 2, pMin4, addBS (book (13, 4, 6, true), 5, pMin5, addBS (book (14, 3, 6, true), 6, pMin4, addBS (book (15, 3, 3, false), 7, pMin4, addBS (book (16, 5, 6, false), 3, pMin4, addBS (book (17, 5, 8, true), 3, pMin5, addBS (book (18, 5, 3, true), 9, pMin6, addBS (book (19, 3, 2, false), 3, pMin5, addBS (book (20, 3, 6, false), 6, pMin4, addBS (book (21, 3, 3, false), 7, pMin4, emptyBS))))))))))))) end function ------------------------------------------------------------------------------- function bs9 : BOOKSTORE is return addBS (book (0, 4, 3, true), 0, pMin5, addBS (book (1, 3, 4, false), 6, pMin4, addBS (book (2, 3, 4, true), 2, pMin4, addBS (book (4, 4, 7, false), 3, pMin4, addBS (book (6, 5, 8, true), 3, pMin5, addBS (book (9, 5, 3, true), 9, pMin6, emptyBS)))))) end function ------------------------------------------------------------------------------- function bs10 : BOOKSTORE is return addBS (book (0, 4, 3, true), 0, pMin5, addBS (book (1, 3, 4, false), 6, pMin4, addBS (book (2, 3, 4, true), 2, pMin4, addBS (book (4, 4, 7, false), 3, pMin4, addBS (book (6, 5, 8, true), 3, pMin5, addBS (book (9, 5, 3, true), 9, pMin6, addBS (book (12, 3, 6, true), 6, pMin4, addBS (book (13, 3, 3, false), 7, pMin4, addBS (book (14, 4, 7, true), 3, pMin4, emptyBS))))))))) end function end module