Skip to content

Commit

Permalink
Further #6 and #14
Browse files Browse the repository at this point in the history
  • Loading branch information
@rgcv
rgcv committed Nov 7, 2018
1 parent 14d78a4 commit a2f640d
Showing 1 changed file with 183 additions and 68 deletions.
251 changes: 183 additions & 68 deletions AdventureBuilderG12P11819.als
View file
Original file line number Diff line number Diff line change
Expand Up @@ -4,16 +4,17 @@
* 81045 - Rui Ventura
* 81728 - Madalena Assembleia
*/
open util/boolean
open util/ordering [Date] as D
open util/ordering [Time] as T

sig Date, Time {}

one sig AdventureBuilder {
accounts: set Account -> Time,
roomRes: set RoomReservation -> Time,
offers: set ActivityOffer -> Time,
actRes: set ActivityReservation -> Time
actRes: set ActivityReservation -> Time,
adventures: set Adventure -> Time
}

sig Client {}
Expand All @@ -22,7 +23,7 @@ sig Broker extends Client {}


sig Bank {
accounts: set Account
accounts: some Account
}

sig Account {
Expand All @@ -31,37 +32,33 @@ sig Account {
balance: Int one -> Time
}

//
//sig Hotel {
// rooms: set Room // 10
//}
//
//sig Room {
// hotel: one Hotel, // 11
// type: one RoomType // 12
//}
//
//abstract sig RoomType {} // 12
//one sig Single, Double extends RoomType {} // 12
//
//sig RoomReservation {
// room: one Room,
// client: one Client,
// arrival, departure: one Date,
// cancelled: Bool one -> Time
//}
//

sig Hotel {
rooms: some Room // 10
}

sig Room {
hotel: one Hotel, // 11
type: one RoomType // 12
}

abstract sig RoomType {} // 12
one sig Single, Double extends RoomType {} // 12

sig RoomReservation {
room: one Room,
client: one Client,
arrival, departure: one Date
}


sig ActivityProvider {
activities: set Activity
activities: some Activity
}

sig Activity {
provider: one ActivityProvider,
capacity: one Int
}{
// HACK: Cheesy way of ensuring activities' cap is positive
capacity > 0 // 15
}

sig ActivityOffer {
Expand All @@ -76,22 +73,21 @@ sig ActivityReservation {
people: one Int
}

//
//sig Adventure {
// client: one Client,
// people: one Int,
// broker: one Broker,
// roomRes: some RoomReservation,
// actRes: one ActivityReservation,
// cost: one Int,
// clientAcc: one Account,
// brokerAcc: one Account,
// state: one AdventureState // 21
//}
//
//abstract sig AdventureState {} // 21
//one sig Initial, Payed, Confirmed extends AdventureState {}
//
sig Adventure {
client: one Client,
people: one Int,
broker: one Broker,
roomRes: some RoomReservation,
actRes: one ActivityReservation,
cost: one Int,
clientAcc: one Account,
brokerAcc: one Account,
state: AdventureState one -> Time // 21
}

abstract sig AdventureState {} // 21
one sig InitialState, PayedState, ConfirmedState extends AdventureState {}

//sig Invoice {
// client: one Client,
// type: one PurchaseType,
Expand All @@ -106,18 +102,44 @@ sig ActivityReservation {
// Operations ------------------------------------------------------------------
// Auxiliary

// accounts
pred accountIsOpen[t: Time, acc: Account] {
acc in AdventureBuilder.accounts.t
}

pred noOpenChangeExcept[t, t': Time, acc: Account] {
pred noAccountsChangeExcept[t, t': Time, acc: Account] {
AdventureBuilder.accounts.t' = AdventureBuilder.accounts.t + acc
}

pred noAccountChangeExcept[t, t': Time, acc: Account] {
pred noAccBalanceChangeExcept[t, t': Time, acc: Account] {
all a: Account - acc | a.balance.t' = a.balance.t
}

// rooms
pred roomResExists[t: Time, res: RoomReservation] {
res in AdventureBuilder.roomRes.t
}

pred noRoomResMadeExcept[t, t': Time, res: RoomReservation] {
AdventureBuilder.roomRes.t' = AdventureBuilder.roomRes.t + res
}

pred noRoomResCancelledExcept[t, t': Time, res: RoomReservation] {
AdventureBuilder.roomRes.t' = AdventureBuilder.roomRes.t - res
}

pred datesConflict[a, a', d, d': Date] {
a' = d || (a' = a || gt[a', a] && lt[a', d])
|| (d' = d || lt[d', d] && gt[d', a])
|| (lt[a', a] && gt[d', d])
}

pred roomResConflict[r, r': RoomReservation] {
let a = r.arrival, a' = r'.arrival, d = r.departure, d' = r'.departure |
r.room = r'.room || datesConflict[a, a', d, d']
}

// activities
pred offerExists[t: Time, off: ActivityOffer] {
off in AdventureBuilder.offers.t
}
Expand All @@ -134,10 +156,31 @@ pred activityResExists[t: Time, res: ActivityReservation] {
res in AdventureBuilder.actRes.t
}

pred noActResChangeExcept[t, t': Time, res: ActivityReservation] {
pred noActResMadeExcept[t, t': Time, res: ActivityReservation] {
AdventureBuilder.actRes.t' = AdventureBuilder.actRes.t + res
}

pred noActResCancelledExcept[t, t': Time, res: ActivityReservation] {
AdventureBuilder.actRes.t' = AdventureBuilder.actRes.t - res
}

// adventures
pred adventureExists[t: Time, adv: Adventure] {
adv in AdventureBuilder.adventures.t
}

pred noAdventureCreatedExcept[t, t': Time, adv: Adventure] {
AdventureBuilder.adventures.t' = AdventureBuilder.adventures.t + adv
}

pred noAdventureCancelledExcept[t, t': Time, adv: Adventure] {
AdventureBuilder.adventures.t' = AdventureBuilder.adventures.t - adv
}

pred noAdvStateChangeExcept[t, t': Time, adv: Adventure] {
all a: Adventure - adv | a.state.t' = a.state.t
}

// Helper Ops

pred reserveActivity[t, t': Time, res: ActivityReservation] {
Expand All @@ -153,12 +196,7 @@ pred reserveActivity[t, t': Time, res: ActivityReservation] {
result >= 0 &&
res.offer.availability.t' = result
// post/frame cond
AdventureBuilder.actRes.t' = AdventureBuilder.actRes.t + res
// frame cond
noOpenChangeExcept[t, t', none]
noAccountChangeExcept[t, t', none]
noOffersChangeExcept[t, t', none]
noOfferAvailChangeExcept[t, t', res.offer]
noActResMadeExcept[t, t', res]
}

pred cancelActivityReservation[t, t': Time, res: ActivityReservation] {
Expand All @@ -172,14 +210,26 @@ pred cancelActivityReservation[t, t': Time, res: ActivityReservation] {
result = plus[avail, res.people] |
res.offer.availability.t' = result
// post/frame
AdventureBuilder.actRes.t' = AdventureBuilder.actRes.t - res
noActResCancelledExcept[t, t', res]
// frame cond
noOpenChangeExcept[t, t', none]
noAccountChangeExcept[t, t', none]
noAccountsChangeExcept[t, t', none]
noAccBalanceChangeExcept[t, t', none]
noOffersChangeExcept[t, t', none]
noOfferAvailChangeExcept[t, t', res.offer]
}

pred reserveRooms[t, t': Time, res: RoomReservation] {
// pre cond
not roomResExists[t, res]
lt[res.arrival, res.departure]
all r: RoomReservation - res | not roomResConflict[r, res]
all r: res.room | one h: Hotel | r.hotel = h && r in h.rooms // 24
// post cond
roomResExists[t', res]
// frame cond
noRoomResMadeExcept[t, t', res]
}

// Main Ops

pred openAccount[t, t': Time, acc: Account] {
Expand All @@ -189,11 +239,14 @@ pred openAccount[t, t': Time, acc: Account] {
accountIsOpen[t', acc] // 2
acc.balance.t' = 0
// frame cond
noOpenChangeExcept[t, t', acc]
noAccountChangeExcept[t, t', acc]
noAccountsChangeExcept[t, t', acc]
noAccBalanceChangeExcept[t, t', acc]
noOffersChangeExcept[t, t', none]
noOfferAvailChangeExcept[t, t', none]
noActResChangeExcept[t, t', none]
noRoomResMadeExcept[t, t', none]
noActResMadeExcept[t, t', none]
noAdventureCreatedExcept[t, t', none]
noAdvStateChangeExcept[t, t', none]
}

pred clientDeposit[t, t': Time, acc: Account, amt: Int] {
Expand All @@ -206,11 +259,14 @@ pred clientDeposit[t, t': Time, acc: Account, amt: Int] {
acc.balance.t' = result
}
// frame cond
noOpenChangeExcept[t, t', none] // 9
noAccountChangeExcept[t, t', acc]
noAccountsChangeExcept[t, t', none] // 9
noAccBalanceChangeExcept[t, t', acc]
noOffersChangeExcept[t, t', none]
noOfferAvailChangeExcept[t, t', none]
noActResChangeExcept[t, t', none]
noRoomResMadeExcept[t, t', none]
noActResMadeExcept[t, t', none]
noAdventureCreatedExcept[t, t', none]
noAdvStateChangeExcept[t, t', none]
}

pred makeActivityOffer[t, t': Time, off: ActivityOffer, avail: Int] {
Expand All @@ -224,11 +280,42 @@ pred makeActivityOffer[t, t': Time, off: ActivityOffer, avail: Int] {
offerExists[t', off]
off.availability.t' = avail
// frame cond
noOpenChangeExcept[t, t', none]
noAccountChangeExcept[t, t', none]
noAccountsChangeExcept[t, t', none]
noAccBalanceChangeExcept[t, t', none]
noOffersChangeExcept[t, t', off]
noOfferAvailChangeExcept[t, t', off]
noActResChangeExcept[t, t', none]
noRoomResMadeExcept[t, t', none]
noActResMadeExcept[t, t', none]
noAdventureCreatedExcept[t, t', none]
noAdvStateChangeExcept[t, t', none]
}

pred createAdventure[t, t': Time, adv: Adventure] {
// pre cond
not adventureExists[t, adv]
accountIsOpen[t, adv.brokerAcc]
accountIsOpen[t, adv.clientAcc]
adv.broker = adv.brokerAcc.client
adv.client = adv.clientAcc.client
adv.client not in Broker
adv.people > 0 // 22

adv.cost > 0
adv.client = adv.actRes.client // 23
adv.client = adv.roomRes.client // 23
// post cond
adventureExists[t', adv]
adv.state.t' = InitialState
// post/frame
reserveActivity[t, t', adv.actRes]
reserveRooms[t, t', adv.roomRes]
// frame cond
noAccountsChangeExcept[t, t', none]
noAccBalanceChangeExcept[t, t', none]
noOffersChangeExcept[t, t', none]
noOfferAvailChangeExcept[t, t', adv.actRes.offer]
noAdventureCreatedExcept[t, t', adv]
noAdvStateChangeExcept[t, t', adv]
}

// Asserts ---------------------------------------------------------------------
Expand Down Expand Up @@ -279,9 +366,16 @@ assert openAccountsRemainOpen {
}
check openAccountsRemainOpen // 9

// reserveRooms
assert roomResArrivalLessThanDeparture {
all t: Time, res: AdventureBuilder.roomRes.t |
lt[res.arrival, res.departure]
}
check roomResArrivalLessThanDeparture for 5 // 13

// makeActivityOffer
assert activityCapacityIsPositive {
all act: Activity | act.capacity > 0
all t: Time, act: AdventureBuilder.offers.t.activity | act.capacity > 0
}
check activityCapacityIsPositive // 15

Expand Down Expand Up @@ -310,20 +404,41 @@ assert offerAvailChangesUponReserv {
}
check offerAvailChangesUponReserv // 19

// createAdventure
assert adventureIsForSomePeople {
all t: Time | no adv: AdventureBuilder.adventures.t |
adventureExists[t, adv] && adv.people < 1
}
check adventureIsForSomePeople for 5 // 22

assert advClientIsClientOfReservations {
all t: Time, adv: AdventureBuilder.adventures.t |
adv.client = adv.roomRes.client && adv.client = adv.actRes.client
}
check advClientIsClientOfReservations for 5 // 23

assert advRoomResAreInSameHotel {
all t: Time, res: AdventureBuilder.adventures.t.roomRes |
one h: Hotel | res.room.hotel = h
}
check advRoomResAreInSameHotel for 5 // 24
// Transitions -----------------------------------------------------------------

pred init[t: Time] {
no AdventureBuilder.(accounts +
roomRes +
offers +
actRes).t
actRes +
adventures).t
}

fact traces {
init [T/first]
all t: Time - T/last | let t' = t.next |
some acc: Account, off: ActivityOffer, avail, amt: Int {
some acc: Account, off: ActivityOffer, adv: Adventure, avail, amt: Int {
openAccount[t, t', acc] or
clientDeposit[t, t', acc, amt] or
makeActivityOffer[t, t', off, avail]
makeActivityOffer[t, t', off, avail] or
createAdventure[t, t', adv]
}
}

0 comments on commit a2f640d

Please sign in to comment.