from pyspect.logics import *
from pyspect.tlt import TLT, ContLTL
from pyspect.set_builder import AlignedBoxSet, Union, HalfSpaceSet
from pyspect.impls.hj_reachability import TVHJImpl

# Choose fragment
TLT.select(ContLTL)

# Write spec: avoid D, stay in corridor, reach goal
phi = UNTIL(AND(NOT('D'), 'corridor'), 'goal')

# Bind propositions later
tlt = TLT(phi, where={
    'D': Union(AlignedBoxSet(...), AlignedBoxSet(...)),
    'corridor': AlignedBoxSet(...),
    'goal': HalfSpaceSet(...),
})

# Realize on a backend
impl = TVHJImpl(...)
Phi = tlt.realize(impl)
print("Satisfaction set:", Phi)