33NL2TLA+ Translation Script
44
55Translates natural language descriptions of TLA+ specifications into TLA+ specifications.
6- This is a Python migration of the GenAI script translate.genai.mts using LiteLLM and MCP tools.
6+ This is a Python migration of the GenAI script translate.genai.mts using LiteLLM with MCP tool calling.
7+
8+ MCP Tool Calling:
9+ This script supports two modes of tool calling with **automatic detection**:
10+
11+ 1. **MCP Tool Calling** (Auto-detected):
12+ Uses LiteLLM's native MCP tool calling as described in:
13+ - Anthropic: https://docs.litellm.ai/docs/providers/anthropic#mcp-tool-calling
14+ - OpenAI: https://platform.openai.com/docs/guides/tools-connectors-mcp
15+ Passes MCP server configuration directly to the LLM provider's API.
16+ Requires publicly accessible MCP server.
17+ Known to work with: Anthropic Claude, OpenAI GPT-5
18+
19+ 2. **Native Tool Calling** (Fallback):
20+ Converts MCP tools to OpenAI function calling format.
21+ Works with any LiteLLM-supported provider.
22+ Executes tools locally via MCP server manager.
23+ Works with: Bedrock, Azure, GitHub, GPT-4, and any other provider
24+
25+ The script automatically tries MCP format first, then falls back to native tools if unsupported.
26+ No manual configuration needed!
727
828USAGE:
929 python translate.py [puzzle_files...]
@@ -142,6 +162,7 @@ def __init__(self, model: str = "azure/gpt-4.1", model_id: Optional[str] = None,
142162 self .available_tools = []
143163 self .available_resources = []
144164 self .workspace_root = detect_workspace_root ()
165+ self ._mcp_tool_calling_supported = None # Cache for MCP support detection
145166
146167 async def setup_mcp_connection (self , max_retries : int = 3 , timeout : float = 30.0 ):
147168 """Initialize MCP server connection and discover available tools with retry logic."""
@@ -449,7 +470,12 @@ async def gpt_call(self, messages: List[Dict[str, Any]], tools: Optional[List[Di
449470 }
450471
451472 async def call_mcp_tool (self , tool_name : str , params : Dict [str , Any ], max_retries : int = 3 , timeout : float = 60.0 ) -> Dict [str , Any ]:
452- """Call an MCP tool and return the result with retry logic and timeout handling."""
473+ """Call an MCP tool locally and return the result with retry logic and timeout handling.
474+
475+ This method executes tools via our local MCP server manager connection.
476+ When using MCP tool calling, the LLM provider may also execute tools directly
477+ by connecting to the publicly accessible MCP server.
478+ """
453479 for attempt in range (max_retries ):
454480 try :
455481 logger .debug (f"🔧 Calling MCP tool: { tool_name } with { params } (attempt { attempt + 1 } /{ max_retries } )" )
@@ -532,8 +558,46 @@ def run_tlc_and_validate(
532558 logger .error (f"❌ Failed to run TLC: { e } " )
533559 raise
534560
561+ async def create_mcp_tools_config (self ) -> List [Dict [str , Any ]]:
562+ """Create MCP tools configuration for direct MCP tool calling.
563+
564+ Uses LiteLLM's native MCP tool calling support as described in:
565+ - Anthropic: https://docs.litellm.ai/docs/providers/anthropic#mcp-tool-calling
566+ - OpenAI: https://platform.openai.com/docs/guides/tools-connectors-mcp
567+
568+ Instead of converting MCP tools to OpenAI function calling format,
569+ we pass the MCP server configuration directly to the LLM provider.
570+ The LLM provider will:
571+ 1. Discover available tools from the publicly accessible MCP server
572+ 2. Execute tool calls by directly connecting to the MCP server
573+ 3. Return results in the tool calling conversation flow
574+
575+ IMPORTANT:
576+ - The MCP server must be publicly accessible by the LLM provider
577+ - For local development with localhost, use a tunnel service (ngrok, etc.)
578+ - This is auto-detected - if unsupported, the script falls back to native tools
579+ """
580+ mcp_tools = []
581+
582+ # Add MCP server configuration - URL must be publicly accessible
583+ mcp_tools .append ({
584+ "type" : "mcp" ,
585+ "server_label" : "tlaplus_mcp_server" ,
586+ "server_url" : self .mcp_url , # Must be publicly accessible URL
587+ "require_approval" : "never" , # Auto-approve all tool calls
588+ })
589+
590+ return mcp_tools
591+
535592 async def create_native_tools (self ) -> List [Dict [str , Any ]]:
536- """Convert MCP tools to native LLM tool format."""
593+ """Convert MCP tools to native OpenAI function calling format.
594+
595+ This is used as a fallback when MCP tool calling is not supported by the provider.
596+ The script automatically detects MCP support and falls back to this method when needed.
597+
598+ Works with all LiteLLM-supported providers and allows using localhost MCP servers
599+ since tools are executed locally via our MCP server manager.
600+ """
537601 native_tools = []
538602
539603 for tool in self .available_tools :
@@ -571,32 +635,6 @@ async def create_native_tools(self) -> List[Dict[str, Any]]:
571635
572636 native_tools .append (tool_schema )
573637
574- # Add resource reading tool if resources are available
575- if self .available_resources :
576- resource_uris = [resource .get ('uri' , '' ) for resource in self .available_resources if resource .get ('uri' )]
577- resource_tool = {
578- "type" : "function" ,
579- "function" : {
580- "name" : "read_mcp_resource" ,
581- "description" : f"Read content from MCP resources." ,
582- "parameters" : {
583- "type" : "object" ,
584- "properties" : {
585- "resource_uri" : {
586- "type" : "string" ,
587- "description" : f"URI of the resource to read. Available options: { ', ' .join (resource_uris )} "
588- },
589- "server_name" : {
590- "type" : "string" ,
591- "description" : "Optional server name (defaults to first available server)"
592- }
593- },
594- "required" : ["resource_uri" ]
595- }
596- }
597- }
598- native_tools .append (resource_tool )
599-
600638 return native_tools
601639
602640 async def create_tools_description (self ) -> str :
@@ -687,9 +725,40 @@ async def create_tools_description(self) -> str:
687725 return full_description
688726
689727 async def run_agent_prompt (self , user_prompt : str , max_turns : int = 15 ) -> str :
690- """Run an agent-based prompt with native tool calling support."""
691- # Get native tools format
692- native_tools = await self .create_native_tools ()
728+ """Run an agent-based prompt with MCP tool calling support or native tools."""
729+ # Determine which tool mode to use - try MCP first if not already cached
730+ if self ._mcp_tool_calling_supported is None :
731+ # Try MCP first with a simple test call
732+ logger .info ("🔍 Detecting MCP tool calling support..." )
733+ try :
734+ mcp_tools = await self .create_mcp_tools_config ()
735+ # Make a test call to see if MCP format is accepted
736+ test_messages = [
737+ {"role" : "user" , "content" : "Hello, can you see the available tools?" }
738+ ]
739+ test_response = await self .gpt_call (test_messages , tools = mcp_tools , tool_choice = "auto" )
740+ # If we get here without error, MCP is supported
741+ self ._mcp_tool_calling_supported = True
742+ logger .info ("✅ MCP tool calling supported by this model" )
743+ except Exception as e :
744+ # Check if it's an MCP-related error (validation, unsupported format, etc.)
745+ error_msg = str (e ).lower ()
746+ if any (keyword in error_msg for keyword in ['validation' , 'toolconfig' , 'tools.' , 'toolspec' , 'mcp' ]):
747+ logger .info (f"ℹ️ MCP tool calling not supported, falling back to native tools (error: { str (e )[:100 ]} )" )
748+ self ._mcp_tool_calling_supported = False
749+ else :
750+ # Some other error - re-raise it
751+ raise
752+
753+ # Use cached result
754+ if self ._mcp_tool_calling_supported :
755+ logger .info ("🔧 Using MCP tool calling format" )
756+ tools = await self .create_mcp_tools_config ()
757+ tool_mode = "MCP"
758+ else :
759+ logger .info ("🔧 Using native tool calling format" )
760+ tools = await self .create_native_tools ()
761+ tool_mode = "native"
693762
694763 system_prompt = f"""You are an autonomous AI agent that can use tools to accomplish TLA+ development tasks.
695764
@@ -704,6 +773,10 @@ async def run_agent_prompt(self, user_prompt: str, max_turns: int = 15) -> str:
704773- **File Paths**: Use absolute file paths when required by tools. Current working directory: { self .workspace_root }
705774
706775You have access to tools for TLA+ development including parsing, model checking, and file operations. Use them as needed to complete the task.
776+
777+ ## Available Tools
778+
779+ { await self .create_tools_description ()}
707780"""
708781
709782 messages = [
@@ -714,12 +787,12 @@ async def run_agent_prompt(self, user_prompt: str, max_turns: int = 15) -> str:
714787 final_result = ""
715788
716789 for turn in range (max_turns ):
717- logger .info (f"🤖 Agent turn { turn + 1 } /{ max_turns } " )
790+ logger .info (f"🤖 Agent turn { turn + 1 } /{ max_turns } (tool mode: { tool_mode } ) " )
718791
719792 # Get LLM response with tools
720- response = await self .gpt_call (messages , tools = native_tools , tool_choice = "auto" )
793+ response = await self .gpt_call (messages , tools = tools , tool_choice = "auto" )
721794
722- # Handle tool calls
795+ # Handle tool calls (LiteLLM still returns tool calls for us to execute)
723796 if "tool_calls" in response and response ["tool_calls" ]:
724797 # Add assistant message with tool calls
725798 assistant_message = {
@@ -741,14 +814,8 @@ async def run_agent_prompt(self, user_prompt: str, max_turns: int = 15) -> str:
741814
742815 logger .info (f"🔧 Calling tool: { tool_name } with { tool_args } " )
743816
744- # Handle special resource reading tool
745- if tool_name == "read_mcp_resource" :
746- resource_uri = tool_args .get ("resource_uri" , "" )
747- server_name = tool_args .get ("server_name" , "" )
748- tool_response = await self .read_mcp_resource (resource_uri , server_name )
749- else :
750- # Call the MCP tool
751- tool_response = await self .call_mcp_tool (tool_name , tool_args )
817+ # Call the MCP tool via the MCP server manager
818+ tool_response = await self .call_mcp_tool (tool_name , tool_args )
752819
753820 # Format tool response
754821 if tool_response .get ("isError" ):
@@ -757,27 +824,21 @@ async def run_agent_prompt(self, user_prompt: str, max_turns: int = 15) -> str:
757824 else :
758825 logger .info (f"✅ Tool { tool_name } completed successfully" )
759826
760- # Handle resource response format
761- if tool_name == "read_mcp_resource" :
762- content = tool_response .get ("content" , "" )
763- mime_type = tool_response .get ("mimeType" , "text/plain" )
764- tool_result = f"Resource Content ({ mime_type } ):\n { content } "
765- else :
766- # Extract content from MCP tool response
767- if "content" in tool_response :
768- if isinstance (tool_response ["content" ], list ):
769- # Handle list of content items
770- content_parts = []
771- for item in tool_response ["content" ]:
772- if isinstance (item , dict ) and "text" in item :
773- content_parts .append (item ["text" ])
774- else :
775- content_parts .append (str (item ))
776- tool_result = "\n " .join (content_parts )
777- else :
778- tool_result = str (tool_response ["content" ])
827+ # Extract content from MCP tool response
828+ if "content" in tool_response :
829+ if isinstance (tool_response ["content" ], list ):
830+ # Handle list of content items
831+ content_parts = []
832+ for item in tool_response ["content" ]:
833+ if isinstance (item , dict ) and "text" in item :
834+ content_parts .append (item ["text" ])
835+ else :
836+ content_parts .append (str (item ))
837+ tool_result = "\n " .join (content_parts )
779838 else :
780- tool_result = json .dumps (tool_response )
839+ tool_result = str (tool_response ["content" ])
840+ else :
841+ tool_result = json .dumps (tool_response )
781842
782843 # Add tool result message
783844 tool_message = {
0 commit comments