sig Event {}

pred event_convexity[t:Trace] {
  // If (e1,e2) and (e2,e3) are in the trace,  then so is (e2,e2).
  all e1,e2,e3 : Event {
    ((e1 -> e2) in t.arrow and (e2 -> e3) in t.arrow)
      implies (e2 -> e2) in t.arrow
  }
}

sig Trace {
  arrow : Event -> Event,
  input : Event -> Event,
  output : Event -> Event,
  internal : set Event
} {

  // define internal events
  internal = univ . (iden & arrow)

  // inputs and outputs are special kinds of arrows
  (input + output) in arrow

  // inputs are arrows from external events to internal events
  input = arrow & ((Event - internal) -> internal)

  // outputs are arrows from internal events to external events
  output = arrow & (internal -> (Event - internal))

  // there are no arrows from external events to external events
  no (arrow & ((Event - internal) -> (Event - internal)))

  // the trace must satisfy "event convexity"
  event_convexity[this]
}

pred p[t:Trace] {
  // To make things interesting: there must be at least one "input" arrow.
  (some a : t.arrow | a in t.input)
}

// Ask Alloy for a trace with up to two events
run p for 2 Event, 1 Trace

/*
 * Next step: "Arrow Convexity"
 * If e1 and e2 are events in the trace on the same object
 * then they must be linked via a chain of "vertical" arrows
 * all of which are in the trace.
 */