module ECommerce

open Shimanto[Time]

sig Time {}

sig WebEvent extends Event {
   // the message sent in this event
  message: one Message,  
  // previous history of messages
  sent: Message -> Time
}{
    sent.pre in sent.post
}

sig OrderID {}
sig Amount {}

abstract sig Value {}

sig Item extends Value {}

sig Order extends Value {
     gross: Amount,   // total price of the order
     store: Store,        // which store the order is for
     items: set Item   // what items are in this order
}{
	#items > 0
}

sig PaidOrder extends Order {}

sig Token extends Value {}

sig SignedToken extends Token {
     signer: OnlineEntity
}
    
abstract sig OnlineEntity {}

abstract sig Store extends OnlineEntity {
	owner: OnlineEntity
}

one sig TStore extends Store {
	orders: OrderID -> one Order -> Time,
	nextOrderID: OrderID one -> Time
}{
	owner = TStore	
}

pred freshOrderID[ts: TStore, freshOne: OrderID]  {
	freshOne not in orderIDsUsed[ts]
}

fun orderIDsUsed[t: TStore] : set OrderID {
      t.orders.univ.univ
}

one sig CaaS extends OnlineEntity {
      paidOrderIDs: Token -> Store -> OrderID -> Time,
      paymentAmount: Store -> OrderID -> Amount -> Time
}{
      all s: Store, oid: OrderID |
             (s -> oid) in univ.paidOrderIDs.Time
             iff (s -> oid) in paymentAmount.Time.univ
}

abstract sig Customer extends OnlineEntity {
          // orders that the customer has paid for
	ordersPaid: OrderID -> one PaidOrder -> Time
}

one sig Attacker extends Customer {}

abstract sig Message {
  sender, receiver: OnlineEntity,
  val: Value
}{
	sender != receiver
}

sig Unsigned extends Message {
   controlledBy: OnlineEntity
}{
   sender in Attacker => controlledBy in Attacker
}

sig Signed extends Message {
   signedBy: OnlineEntity
}

// initial state of the system
pred init [t: Time] {
	 WebEvent.sent.t = none
          no TStore.orders.t
	no Attacker.ordersPaid.t
          no CaaS.paidOrderIDs
	no CaaS.paymentAmount
}

fact traces {
	init [first]
}

pred show() {}
run show