automaton Switch

  signature
    input  on
    output off

  states
    burning: Bool
     initially ~burning

  transitions
    input on
      eff burning := choose
      ensuring
	 burning' = true

    output off
      eff burning := choose
      ensuring
	burning /\ ~burning'