automaton ResolvedChooser
  signature
    output action1, action2(n:Int)
  states
    chosen: Int := 22
  transitions
    output action1
      eff chosen := choose x where 1 <= x /\ x <= 30
                      det do
                            yield 1; yield 2; yield 3
                          od
    output action2(n)
      pre n = chosen
  schedule do
    while true do
      fire output action1;
      fire output action2(chosen)
    od
  od