press.als

open util/ordering[Time]

sig Time {}
sig Key {
  pressed: set Time
}

abstract sig Event {
  pre, post: Time,
  key: Key
}

sig Press extends Event {} {
  pre not in key.pressed
  post in key.pressed

  noPressChangeExcept [key]
}

sig Release extends Event {} {
  pre in key.pressed
  post not in key.pressed

  noPressChangeExcept [key]
}

pred Event.noPressChangeExcept (key: Key) {
  all k: Key - key | {
    (this.pre) in k.pressed implies (this.post) in k.pressed
    (this.pre) not in k.pressed implies (this.post) not in k.pressed
  }
}

pred init (t: Time) {
  t not in Key.pressed
}

fact Traces {
  first.init
  all t: Time - last | let t' = t.next |
   some e: Event {
     e.pre = t and e.post = t'
   }
}