# The Client class is our main interface to SpecLogician
from imandra.u.agents.spec_logician import Client

# First we instantiate a Client with our Imandra Universe API key
client = Client(api_key="...")

# Let's define a simple spec, using Gherkin syntax and plain English
friday_spec = """
Feature: Is it Friday yet?
  Everybody wants to know when it's Friday

  Scenario: Thursday isn't Friday
    Given today is Thursday
    When I ask whether it's Friday yet
    Then I should be told "Nope"

  Scenario: Thursday becomes Friday
    Given today is Thursday
    When next day comes
    Then it's Friday

  Scenario: Friday is Friday
    Given today is Friday
    When I ask whether it's Friday yet
    Then I should be told "Yep"
"""

# Every SpecLogician session begins by initializing the state with our natural language spec
await client.init_state(friday_spec)

# We can now formalize the spec. Let's try the agentic workflow
await client.automatic_workflow()

# We can print out the FormalSpec code that SpecLogician produced
formal_spec = await client.get_pprinted_formal_spec()
print(formal_spec)

# We can also generate an IPL model from the formalized spec
ipl_model = await client.get_ipl_spec()
print(ipl_model)