{{!

      Place to define macros modifying application state.

      For example:

        macro enter_pet( new_pet ) {
        
          v_pets := v_pets \union { new_pet };
        
        }

}}


{{!>transaction_error.tla}}
{{!>transaction_enter_pet.tla}}
{{!>transaction_delete_pet.tla}}