module online

open util/sequence[History]

sig OnlineEntity {}
sig TStore, CaaS, Attacker extends OnlineEntity {}

sig Value {
}

sig Message {
  sender, receiver: OnlineEntity,
  val: Value
}

sig Signed extends Message {
   signedBy: OnlineEntity
}

enum Direction {send, receive}

sig SequenceID {
   num: Int,
   dir: Direction,
   cause: set SequenceID
}

sig History extends Seq {}

pred takeStep [h: History, msg: Message, h2:History] {
     h2[last[h2]] = msg
}