Skip to content

Commit

Permalink
Add gen and test grammar function.
Browse files Browse the repository at this point in the history
  • Loading branch information
lemmy committed Feb 21, 2024
1 parent 9c7ca20 commit 09c044f
Showing 1 changed file with 33 additions and 2 deletions.
35 changes: 33 additions & 2 deletions controllers/pyctrl/samples/apalache.py
Original file line number Diff line number Diff line change
@@ -1,4 +1,3 @@
import sys
import pyaici.server as aici

# note that VSCode syntax highlighting is not perfect r""" ... """ (it assumes regexp)
Expand Down Expand Up @@ -77,7 +76,39 @@
"""


# async def gen_and_test_grammar():
async def gen_and_test_grammar():
await aici.FixedTokens(
"""
---- MODULE Counter ----
VARIABLE
b
Init == b = TRUE
Next == b' = FALSE
====
The type of the variable declaration of b in the following TLA+ spec is:
"""
)
tokens = await aici.gen_tokens(yacc=apalache, max_tokens=10, store_var="b")
print(tokens)

## No need to tokenize the input, as it is already tokenized?!
# tokens = aici.tokenize(input)
constr = aici.CfgConstraint(apalache)
outp = []
for t in tokens:
print(f"Testing token: {t}")
if not constr.token_allowed(t):
## Abort/terminate if token is not allowed.
print(f"Token {t} not allowed")
print("OK: " + repr(aici.detokenize(outp).decode("utf-8", "ignore")))
print("fail: " + repr(aici.detokenize([t]).decode("utf-8", "ignore")))
break
outp.append(t)
constr.append_token(t)
print(f"EOS allowed: {constr.eos_allowed()}")


async def test_grammar():
await aici.FixedTokens("Start")
Expand Down

0 comments on commit 09c044f

Please sign in to comment.