(* ******************************************************************
   Petstore post_pet: creates a new pet entry

   - validate input
      - validation ok    --> enter_pet to database
      - validation error --> raise an application error "pet input not valid"

 * ******************************************************************)
procedure s_post_pet( input ) {

  pet_post_start:

       {{^PREFERENCES.debug-output}}\* {{/PREFERENCES.debug-output}} print <<"Pet post, input=", input >>;

       (* Valid input received *)
       if ( ~ValidatePetData( input.pet ) ) {
           pet_application_error( "Invalid input" );
       	  return;
       };

  pet_post_data_valid:

       (* Referential integrity pet.tag --> tag.tag *)
       if (  ~ValidTagExists( input.pet.tag ) ) {
           {{^PREFERENCES.debug-output}}\* {{/PREFERENCES.debug-output}} print <<"Pet post, v_tags=", v_tags >>;
           pet_application_error( "Tag not found" );
       	   return;
       };


  pet_post_tag_exist:

       if (  PetStore_GetPetByTag( input.pet.tag ) # {} ) {

           {{^PREFERENCES.debug-output}}\* {{/PREFERENCES.debug-output}} print <<"Pet post, tag-not free, v_pets=", v_pets >>;
           pet_application_error( "Tag not free" );
       	   return;
       };


  pet_post_tag_valid_and_used:


  

       (* Generate id using infrastructure service /id/{type}(get) *)
       call infrastructure_id_get( "pet" );
       
  post_pet_id_generated:

      (* Id generation failure? *)
      if ( InfrastructureServiceGetStatus( "/id/{type}(get)" ) # "status_200" ) {

           {{^PREFERENCES.debug-output}}\* {{/PREFERENCES.debug-output}} print <<"Pet post, v_ids=", v_ids >>;

           pet_application_error( "no id " );
	   return;

      };

  post_pet_ok:

      assert(     InfrastructureServiceGetStatus( "/id/{type}(get)" ) = "status_200"
	           /\  ValidatePet( New_Pet( input.pet, InfrastructureServiceGetResponse( "/id/{type}(get)" ).id ) )
       );


        (* Database transaction: create pet *) 
       enter_pet( New_Pet( input.pet, InfrastructureServiceGetResponse( "/id/{type}(get)" ).id ));

       {{^PREFERENCES.debug-output}}\* {{/PREFERENCES.debug-output}} print <<"Pet post, SUCCESS!!, v_pets=", v_pets >>;
      
  pet_post_done:
  
       return;
  
}; \* post_pet