From 38d89d52b7ba70bc88417f668f9c79b2f1c58536 Mon Sep 17 00:00:00 2001 From: Markus Alexander Kuppe Date: Tue, 20 Feb 2024 15:12:42 -0800 Subject: [PATCH 1/6] WIP --- controllers/pyctrl/samples/apalache.py | 78 ++++++++++++++++++++++++++ 1 file changed, 78 insertions(+) create mode 100644 controllers/pyctrl/samples/apalache.py diff --git a/controllers/pyctrl/samples/apalache.py b/controllers/pyctrl/samples/apalache.py new file mode 100644 index 00000000..b6b6e8bb --- /dev/null +++ b/controllers/pyctrl/samples/apalache.py @@ -0,0 +1,78 @@ +import pyaici.server as aici + +# note that VSCode syntax highlighting is not perfect r""" ... """ (it assumes regexp) +c_yacc = r""" + +%start T +%% + +SKIP + : "/\n?[ \t\v\f]*/" ; // white-space, newline, tabs, ... + +field + : "/[a-zA-Z_][a-zA-Z0-9_]*/" ; + +typeConst + : "/[A-Z_][A-Z0-9_]*/" ; + +typeVar + : "/[a-z]/" ; + +List + : T + | List "," T + ; + +T + // integers + : "Int" + // immutable constant strings + | "Str" + // boolean + | "Bool" + // functions + | T "->" T + // sets + | "Set" "(" T ")" + // sequences + | "Seq" "(" T ")" + // tuples + | "<<" List ">>" + // operators + | "(" List ")" "=>" T + // constant types (uninterpreted types) + | typeConst + // type variables + | typeVar + // parentheses, e.g., to change associativity of functions + | "(" T ")" + ; + +%% +""" + +sample_apalache = """ +(Str, Bool) => Bool +Set(Int) -> Set(Int) +""" + +async def test_grammar(): + await aici.FixedTokens("Start") + + +tokens = aici.tokenize(sample_apalache) +print(tokens) +constr = aici.CfgConstraint(c_yacc) +outp = [] +for t in tokens: + if not constr.token_allowed(t): + 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()}") + +aici.test(test_grammar()) +print("Hello") From ba2aa8bd1a2e3d1baf51a5ee64cc8bc31a543bf9 Mon Sep 17 00:00:00 2001 From: Markus Alexander Kuppe Date: Tue, 20 Feb 2024 15:58:15 -0800 Subject: [PATCH 2/6] WIP --- controllers/pyctrl/samples/apalache.py | 71 +++++++++++++++++--------- 1 file changed, 47 insertions(+), 24 deletions(-) diff --git a/controllers/pyctrl/samples/apalache.py b/controllers/pyctrl/samples/apalache.py index b6b6e8bb..cab62432 100644 --- a/controllers/pyctrl/samples/apalache.py +++ b/controllers/pyctrl/samples/apalache.py @@ -1,7 +1,8 @@ +import sys import pyaici.server as aici # note that VSCode syntax highlighting is not perfect r""" ... """ (it assumes regexp) -c_yacc = r""" +apalache = r""" %start T %% @@ -18,6 +19,9 @@ typeVar : "/[a-z]/" ; +aliasName + : "/[a-z]+(?:[A-Z][a-z]*)*/" ; + List : T | List "," T @@ -38,41 +42,60 @@ | "Seq" "(" T ")" // tuples | "<<" List ">>" - // operators - | "(" List ")" "=>" T // constant types (uninterpreted types) | typeConst // type variables | typeVar // parentheses, e.g., to change associativity of functions | "(" T ")" + // operators + | "(" T ")" "=>" T + | "(" List ")" "=>" T + // type all rules + | "$" aliasName ; - + %% """ -sample_apalache = """ -(Str, Bool) => Bool -Set(Int) -> Set(Int) -""" - async def test_grammar(): await aici.FixedTokens("Start") +aici.test(test_grammar()) -tokens = aici.tokenize(sample_apalache) -print(tokens) -constr = aici.CfgConstraint(c_yacc) -outp = [] -for t in tokens: - if not constr.token_allowed(t): - 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()}") -aici.test(test_grammar()) -print("Hello") +## define a list of test inputs +inputs = [ + "Int", + "Int", + "Str", + "(Int)", + "Bool", + "Int -> Int", + "Set(Int)", + "Seq(Int)", + "Set(Int) -> Set(Int)", + "Set(<> -> Int)", + "<>", + "(Int,Int) => Int", + "(Int,Bool) => Int", + "((Int,Bool) => Int) => Bool" +] + +## loop over the inputs and test the grammar +for input in inputs: + print(f"Testing input: {input}") + tokens = aici.tokenize(input) + # print(tokens) + constr = aici.CfgConstraint(apalache) + outp = [] + for t in tokens: + 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"))) + sys.exit(1) + outp.append(t) + constr.append_token(t) + # print(f"EOS allowed: {constr.eos_allowed()}") From b317f2424dd37d7a92274d3713e27493898c1ae7 Mon Sep 17 00:00:00 2001 From: Markus Alexander Kuppe Date: Tue, 20 Feb 2024 20:17:44 -0800 Subject: [PATCH 3/6] Prefix all reguluar expressions to disambiguate. --- controllers/pyctrl/samples/apalache.py | 13 ++++++++----- 1 file changed, 8 insertions(+), 5 deletions(-) diff --git a/controllers/pyctrl/samples/apalache.py b/controllers/pyctrl/samples/apalache.py index cab62432..0f6e16be 100644 --- a/controllers/pyctrl/samples/apalache.py +++ b/controllers/pyctrl/samples/apalache.py @@ -10,17 +10,19 @@ SKIP : "/\n?[ \t\v\f]*/" ; // white-space, newline, tabs, ... +// Prefix all reguluar expressions to disambiguate them. +// The tool first tries a regex and only then looks at the grammar. :-( field - : "/[a-zA-Z_][a-zA-Z0-9_]*/" ; + : "/f[a-zA-Z_][a-zA-Z0-9_]*/" ; typeConst - : "/[A-Z_][A-Z0-9_]*/" ; + : "/t[A-Z_][A-Z0-9_]*/" ; typeVar - : "/[a-z]/" ; + : "/v[a-z]?/" ; aliasName - : "/[a-z]+(?:[A-Z][a-z]*)*/" ; + : "/a[a-z]+(?:[A-Z][a-z]*)*/" ; List : T @@ -79,7 +81,8 @@ async def test_grammar(): "<>", "(Int,Int) => Int", "(Int,Bool) => Int", - "((Int,Bool) => Int) => Bool" + "((Int,Bool) => Int) => Bool", + "$aalias", ] ## loop over the inputs and test the grammar From 709edc6cf9e781dea3bd3d845cd1bf7104d55d04 Mon Sep 17 00:00:00 2001 From: Markus Alexander Kuppe Date: Wed, 21 Feb 2024 13:32:10 -0800 Subject: [PATCH 4/6] Extract and deactivate advanced parts of the grammar. --- controllers/pyctrl/samples/apalache.py | 57 +++++++++++++++++--------- 1 file changed, 38 insertions(+), 19 deletions(-) diff --git a/controllers/pyctrl/samples/apalache.py b/controllers/pyctrl/samples/apalache.py index 0f6e16be..b60fdb89 100644 --- a/controllers/pyctrl/samples/apalache.py +++ b/controllers/pyctrl/samples/apalache.py @@ -10,20 +10,6 @@ SKIP : "/\n?[ \t\v\f]*/" ; // white-space, newline, tabs, ... -// Prefix all reguluar expressions to disambiguate them. -// The tool first tries a regex and only then looks at the grammar. :-( -field - : "/f[a-zA-Z_][a-zA-Z0-9_]*/" ; - -typeConst - : "/t[A-Z_][A-Z0-9_]*/" ; - -typeVar - : "/v[a-z]?/" ; - -aliasName - : "/a[a-z]+(?:[A-Z][a-z]*)*/" ; - List : T | List "," T @@ -44,22 +30,55 @@ | "Seq" "(" T ")" // tuples | "<<" List ">>" - // constant types (uninterpreted types) - | typeConst - // type variables - | typeVar // parentheses, e.g., to change associativity of functions | "(" T ")" // operators | "(" T ")" "=>" T | "(" List ")" "=>" T + ; +%% +""" + +t12 = r""" + +// Prefix all reguluar expressions to disambiguate them. +// The tool first tries a regex and only then looks at the grammar. :-( +field + : "/f[a-zA-Z_][a-zA-Z0-9_]*/" ; + +typeConst + : "/t[A-Z_][A-Z0-9_]*/" ; + +typeVar + : "/v[a-z]?/" ; + +aliasName + : "/a[a-z]+(?:[A-Z][a-z]*)*/" ; + +T12 // type all rules - | "$" aliasName + : "$" aliasName + // constant types (uninterpreted types) + | typeConst + // type variables + | typeVar + // A new record type with a fully defined structure. + // The set of fields may be empty. If typeVar is present, + // the record type is parameterized (typeVar must be of the 'row' kind). + // | "{" field ":" T "," ..."," field ":" T ["," typeVar] "}" + // A variant that contains several options, + // optionally parameterized (typeVar must be of the "row" kind). + // | variantOption "|" ... "|" variantOption "|" [typeVar] + // A purely parameterized variant (typeVar must be of the "row" kind). + | "Variant" "(" typeVar ")" ; %% """ + +# async def gen_and_test_grammar(): + async def test_grammar(): await aici.FixedTokens("Start") From 9c7ca2094a2fd877fe11abed3d476da8ae0531fa Mon Sep 17 00:00:00 2001 From: Markus Alexander Kuppe Date: Wed, 21 Feb 2024 13:33:40 -0800 Subject: [PATCH 5/6] Refactor grammar test into a function. --- controllers/pyctrl/samples/apalache.py | 79 +++++++++++++------------- 1 file changed, 39 insertions(+), 40 deletions(-) diff --git a/controllers/pyctrl/samples/apalache.py b/controllers/pyctrl/samples/apalache.py index b60fdb89..4c7e1556 100644 --- a/controllers/pyctrl/samples/apalache.py +++ b/controllers/pyctrl/samples/apalache.py @@ -81,43 +81,42 @@ async def test_grammar(): await aici.FixedTokens("Start") - -aici.test(test_grammar()) - - -## define a list of test inputs -inputs = [ - "Int", - "Int", - "Str", - "(Int)", - "Bool", - "Int -> Int", - "Set(Int)", - "Seq(Int)", - "Set(Int) -> Set(Int)", - "Set(<> -> Int)", - "<>", - "(Int,Int) => Int", - "(Int,Bool) => Int", - "((Int,Bool) => Int) => Bool", - "$aalias", -] - -## loop over the inputs and test the grammar -for input in inputs: - print(f"Testing input: {input}") - tokens = aici.tokenize(input) - # print(tokens) - constr = aici.CfgConstraint(apalache) - outp = [] - for t in tokens: - 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"))) - sys.exit(1) - outp.append(t) - constr.append_token(t) - # print(f"EOS allowed: {constr.eos_allowed()}") + ## define a list of test inputs + inputs = [ + "Int", + "Int", + "Str", + "(Int)", + "Bool", + "Int -> Int", + "Set(Int)", + "Seq(Int)", + "Set(Int) -> Set(Int)", + "Set(<> -> Int)", + "<>", + "(Int,Int) => Int", + "(Int,Bool) => Int", + "((Int,Bool) => Int) => Bool" + # "$aalias", + # "Variant(va)" + ] + + ## loop over the inputs and test the grammar + for input in inputs: + print(f"Testing input: {input}") + tokens = aici.tokenize(input) + # print(tokens) + constr = aici.CfgConstraint(apalache) + outp = [] + for t in tokens: + 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()}") + +aici.test(test_grammar()) \ No newline at end of file From 09c044fdfbf10f916f66edc760340bfdfd9314dc Mon Sep 17 00:00:00 2001 From: Markus Alexander Kuppe Date: Wed, 21 Feb 2024 13:36:07 -0800 Subject: [PATCH 6/6] Add gen and test grammar function. --- controllers/pyctrl/samples/apalache.py | 35 ++++++++++++++++++++++++-- 1 file changed, 33 insertions(+), 2 deletions(-) diff --git a/controllers/pyctrl/samples/apalache.py b/controllers/pyctrl/samples/apalache.py index 4c7e1556..818ea473 100644 --- a/controllers/pyctrl/samples/apalache.py +++ b/controllers/pyctrl/samples/apalache.py @@ -1,4 +1,3 @@ -import sys import pyaici.server as aici # note that VSCode syntax highlighting is not perfect r""" ... """ (it assumes regexp) @@ -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")