LSE GTT Order Expiry Verification

from dataclasses import dataclass
from enum import Enum
from typing import Optional, List
 
# Define your types
class TradingMode(Enum):
    CONTINUOUS = "continuous"
    AUCTION_CALL = "auction_call"
 
@dataclass
class State:
    time: int
    mode: TradingMode
    # ... other fields
 
# Define state transitions
def process_tick(state: State) -> State:
    # Your business logic here
    pass
 
# Define verification property
def conflict_reachable(messages: List, state: State) -> bool:
    """Check if bad state is reachable."""
    final_state = run(state, messages)
    return bad_condition_holds(final_state)

from code_logician import create_thread, init_state
 
# Create a verification thread
thread_id = create_thread()
 
# Load your Python code
with open("your_model.py", "r") as f:
    src_code = f.read()
 
# Initialize formalization
init_state(thread_id, src_code=src_code, src_lang="python")

from code_logician import agent_formalizer
 
# Run automatic Python → IML transformation
result = agent_formalizer(thread_id, no_refactor=False)
 
# Check formalization status
if result["status"] == "TRANSPARENT":
    print("✅ Model fully formalized")
else:
    print("⚠️ Manual review needed")

from code_logician import gen_vgs
 
# Describe what you want to verify
gen_vgs(
    thread_id,
    description="""
    Verify that the critical business property holds:
 
    For all valid initial states and message sequences,
    the conflict_reachable function should return false.
 
    Specifically:
    1. Check that valid states exist (VG1)
    2. Prove that conflict is impossible (VG2)
    """
)

# Update your model with the fix
# Then re-verify
init_state(thread_id, src_code=fixed_code, src_lang="python")
agent_formalizer(thread_id)
gen_vgs(thread_id, description="Same VG - verify fix works")
 
# Expected: ✅ PROVED (no counterexample)