automaton Chooser
  signature
    output action1, action2(n:Int)
  states
    chosen: Int % initially arbitrary
  transitions
    output action1
      eff chosen := choose x where 1 <= x /\ x <= 30
    output action2(n)
      pre n = chosen