diff --git a/booster/test/rpc-integration/test-questionmark-vars/response-one-ques-substitution.json b/booster/test/rpc-integration/test-questionmark-vars/response-one-ques-substitution.json index 44aefb1934..812dbd3a09 100644 --- a/booster/test/rpc-integration/test-questionmark-vars/response-one-ques-substitution.json +++ b/booster/test/rpc-integration/test-questionmark-vars/response-one-ques-substitution.json @@ -86,73 +86,63 @@ }, "patterns": [ { - "tag": "And", + "tag": "Equals", + "argSort": { + "tag": "SortApp", + "name": "SortState", + "args": [] + }, "sort": { "tag": "SortApp", "name": "SortGeneratedTopCell", "args": [] }, - "patterns": [ - { - "tag": "Equals", - "argSort": { - "tag": "SortApp", - "name": "SortState", - "args": [] - }, - "sort": { - "tag": "SortApp", - "name": "SortGeneratedTopCell", - "args": [] - }, - "first": { - "tag": "EVar", - "name": "Var'Ques'X", - "sort": { - "tag": "SortApp", - "name": "SortState", - "args": [] - } - }, - "second": { - "tag": "App", - "name": "Lblb'Unds'QUESTIONMARK-VARS'Unds'State", - "sorts": [], - "args": [] - } - }, - { - "tag": "Equals", - "argSort": { - "tag": "SortApp", - "name": "SortState", - "args": [] - }, - "sort": { - "tag": "SortApp", - "name": "SortGeneratedTopCell", - "args": [] - }, - "first": { - "tag": "EVar", - "name": "Var'Ques'X0", - "sort": { - "tag": "SortApp", - "name": "SortState", - "args": [] - } - }, - "second": { - "tag": "EVar", - "name": "Var'Ques'X1", - "sort": { - "tag": "SortApp", - "name": "SortState", - "args": [] - } - } + "first": { + "tag": "EVar", + "name": "Var'Ques'X", + "sort": { + "tag": "SortApp", + "name": "SortState", + "args": [] } - ] + }, + "second": { + "tag": "App", + "name": "Lblb'Unds'QUESTIONMARK-VARS'Unds'State", + "sorts": [], + "args": [] + } + }, + { + "tag": "Equals", + "argSort": { + "tag": "SortApp", + "name": "SortState", + "args": [] + }, + "sort": { + "tag": "SortApp", + "name": "SortGeneratedTopCell", + "args": [] + }, + "first": { + "tag": "EVar", + "name": "Var'Ques'X0", + "sort": { + "tag": "SortApp", + "name": "SortState", + "args": [] + } + }, + "second": { + "tag": "EVar", + "name": "Var'Ques'X1", + "sort": { + "tag": "SortApp", + "name": "SortState", + "args": [] + } + } }, { "tag": "Equals", diff --git a/booster/test/rpc-integration/test-questionmark-vars/response-one-ques-substitution.booster-dev b/booster/test/rpc-integration/test-questionmark-vars/response-one-ques-substitution.kore-rpc-dev similarity index 67% rename from booster/test/rpc-integration/test-questionmark-vars/response-one-ques-substitution.booster-dev rename to booster/test/rpc-integration/test-questionmark-vars/response-one-ques-substitution.kore-rpc-dev index 812dbd3a09..44aefb1934 100644 --- a/booster/test/rpc-integration/test-questionmark-vars/response-one-ques-substitution.booster-dev +++ b/booster/test/rpc-integration/test-questionmark-vars/response-one-ques-substitution.kore-rpc-dev @@ -86,63 +86,73 @@ }, "patterns": [ { - "tag": "Equals", - "argSort": { - "tag": "SortApp", - "name": "SortState", - "args": [] - }, + "tag": "And", "sort": { "tag": "SortApp", "name": "SortGeneratedTopCell", "args": [] }, - "first": { - "tag": "EVar", - "name": "Var'Ques'X", - "sort": { - "tag": "SortApp", - "name": "SortState", - "args": [] - } - }, - "second": { - "tag": "App", - "name": "Lblb'Unds'QUESTIONMARK-VARS'Unds'State", - "sorts": [], - "args": [] - } - }, - { - "tag": "Equals", - "argSort": { - "tag": "SortApp", - "name": "SortState", - "args": [] - }, - "sort": { - "tag": "SortApp", - "name": "SortGeneratedTopCell", - "args": [] - }, - "first": { - "tag": "EVar", - "name": "Var'Ques'X0", - "sort": { - "tag": "SortApp", - "name": "SortState", - "args": [] - } - }, - "second": { - "tag": "EVar", - "name": "Var'Ques'X1", - "sort": { - "tag": "SortApp", - "name": "SortState", - "args": [] + "patterns": [ + { + "tag": "Equals", + "argSort": { + "tag": "SortApp", + "name": "SortState", + "args": [] + }, + "sort": { + "tag": "SortApp", + "name": "SortGeneratedTopCell", + "args": [] + }, + "first": { + "tag": "EVar", + "name": "Var'Ques'X", + "sort": { + "tag": "SortApp", + "name": "SortState", + "args": [] + } + }, + "second": { + "tag": "App", + "name": "Lblb'Unds'QUESTIONMARK-VARS'Unds'State", + "sorts": [], + "args": [] + } + }, + { + "tag": "Equals", + "argSort": { + "tag": "SortApp", + "name": "SortState", + "args": [] + }, + "sort": { + "tag": "SortApp", + "name": "SortGeneratedTopCell", + "args": [] + }, + "first": { + "tag": "EVar", + "name": "Var'Ques'X0", + "sort": { + "tag": "SortApp", + "name": "SortState", + "args": [] + } + }, + "second": { + "tag": "EVar", + "name": "Var'Ques'X1", + "sort": { + "tag": "SortApp", + "name": "SortState", + "args": [] + } + } } - } + ] }, { "tag": "Equals", diff --git a/booster/test/rpc-integration/test-questionmark-vars/response-one-ques.booster-dev b/booster/test/rpc-integration/test-questionmark-vars/response-one-ques.json similarity index 100% rename from booster/test/rpc-integration/test-questionmark-vars/response-one-ques.booster-dev rename to booster/test/rpc-integration/test-questionmark-vars/response-one-ques.json diff --git a/booster/test/rpc-integration/test-questionmark-vars/response-one-ques.kore-rpc-dev b/booster/test/rpc-integration/test-questionmark-vars/response-one-ques.kore-rpc-dev deleted file mode 100644 index 8852423b90..0000000000 --- a/booster/test/rpc-integration/test-questionmark-vars/response-one-ques.kore-rpc-dev +++ /dev/null @@ -1,121 +0,0 @@ -{ - "jsonrpc": "2.0", - "id": 1, - "result": { - "reason": "stuck", - "depth": 1, - "state": { - "term": { - "format": "KORE", - "version": 1, - "term": { - "tag": "App", - "name": "Lbl'-LT-'generatedTop'-GT-'", - "sorts": [], - "args": [ - { - "tag": "App", - "name": "Lbl'-LT-'k'-GT-'", - "sorts": [], - "args": [ - { - "tag": "App", - "name": "dotk", - "sorts": [], - "args": [] - } - ] - }, - { - "tag": "App", - "name": "Lbl'-LT-'a-state'-GT-'", - "sorts": [], - "args": [ - { - "tag": "EVar", - "name": "Var'Ques'X", - "sort": { - "tag": "SortApp", - "name": "SortState", - "args": [] - } - } - ] - }, - { - "tag": "App", - "name": "Lbl'-LT-'b-state'-GT-'", - "sorts": [], - "args": [ - { - "tag": "App", - "name": "Lbl'Stop'State'Unds'QUESTIONMARK-VARS'Unds'State", - "sorts": [], - "args": [] - } - ] - }, - { - "tag": "App", - "name": "Lbl'-LT-'generatedCounter'-GT-'", - "sorts": [], - "args": [ - { - "tag": "DV", - "sort": { - "tag": "SortApp", - "name": "SortInt", - "args": [] - }, - "value": "0" - } - ] - } - ] - } - }, - "predicate": { - "format": "KORE", - "version": 1, - "term": { - "tag": "Equals", - "argSort": { - "tag": "SortApp", - "name": "SortBool", - "args": [] - }, - "sort": { - "tag": "SortApp", - "name": "SortGeneratedTopCell", - "args": [] - }, - "first": { - "tag": "DV", - "sort": { - "tag": "SortApp", - "name": "SortBool", - "args": [] - }, - "value": "true" - }, - "second": { - "tag": "App", - "name": "Lblcondition'LParUndsRParUnds'QUESTIONMARK-VARS'Unds'Bool'Unds'State", - "sorts": [], - "args": [ - { - "tag": "EVar", - "name": "Var'Ques'X", - "sort": { - "tag": "SortApp", - "name": "SortState", - "args": [] - } - } - ] - } - } - } - } - } -} \ No newline at end of file diff --git a/booster/test/rpc-integration/test-questionmark-vars/response-two-ques-external.booster-dev b/booster/test/rpc-integration/test-questionmark-vars/response-two-ques-external.json similarity index 100% rename from booster/test/rpc-integration/test-questionmark-vars/response-two-ques-external.booster-dev rename to booster/test/rpc-integration/test-questionmark-vars/response-two-ques-external.json diff --git a/booster/test/rpc-integration/test-questionmark-vars/response-two-ques-external.kore-rpc-dev b/booster/test/rpc-integration/test-questionmark-vars/response-two-ques-external.kore-rpc-dev deleted file mode 100644 index eb9ba3ab36..0000000000 --- a/booster/test/rpc-integration/test-questionmark-vars/response-two-ques-external.kore-rpc-dev +++ /dev/null @@ -1,124 +0,0 @@ -{ - "jsonrpc": "2.0", - "id": 1, - "result": { - "reason": "stuck", - "depth": 1, - "state": { - "term": { - "format": "KORE", - "version": 1, - "term": { - "tag": "App", - "name": "Lbl'-LT-'generatedTop'-GT-'", - "sorts": [], - "args": [ - { - "tag": "App", - "name": "Lbl'-LT-'k'-GT-'", - "sorts": [], - "args": [ - { - "tag": "App", - "name": "dotk", - "sorts": [], - "args": [] - } - ] - }, - { - "tag": "App", - "name": "Lbl'-LT-'a-state'-GT-'", - "sorts": [], - "args": [ - { - "tag": "EVar", - "name": "Var'Ques'X", - "sort": { - "tag": "SortApp", - "name": "SortState", - "args": [] - } - } - ] - }, - { - "tag": "App", - "name": "Lbl'-LT-'b-state'-GT-'", - "sorts": [], - "args": [ - { - "tag": "EVar", - "name": "Var'Ques'X0", - "sort": { - "tag": "SortApp", - "name": "SortState", - "args": [] - } - } - ] - }, - { - "tag": "App", - "name": "Lbl'-LT-'generatedCounter'-GT-'", - "sorts": [], - "args": [ - { - "tag": "DV", - "sort": { - "tag": "SortApp", - "name": "SortInt", - "args": [] - }, - "value": "0" - } - ] - } - ] - } - }, - "predicate": { - "format": "KORE", - "version": 1, - "term": { - "tag": "Equals", - "argSort": { - "tag": "SortApp", - "name": "SortBool", - "args": [] - }, - "sort": { - "tag": "SortApp", - "name": "SortGeneratedTopCell", - "args": [] - }, - "first": { - "tag": "DV", - "sort": { - "tag": "SortApp", - "name": "SortBool", - "args": [] - }, - "value": "true" - }, - "second": { - "tag": "App", - "name": "Lblcondition'LParUndsRParUnds'QUESTIONMARK-VARS'Unds'Bool'Unds'State", - "sorts": [], - "args": [ - { - "tag": "EVar", - "name": "Var'Ques'X0", - "sort": { - "tag": "SortApp", - "name": "SortState", - "args": [] - } - } - ] - } - } - } - } - } -} \ No newline at end of file diff --git a/booster/test/rpc-integration/test-questionmark-vars/response-two-ques-internal-with-counter.booster-dev b/booster/test/rpc-integration/test-questionmark-vars/response-two-ques-internal-with-counter.json similarity index 100% rename from booster/test/rpc-integration/test-questionmark-vars/response-two-ques-internal-with-counter.booster-dev rename to booster/test/rpc-integration/test-questionmark-vars/response-two-ques-internal-with-counter.json diff --git a/booster/test/rpc-integration/test-questionmark-vars/response-two-ques-internal.booster-dev b/booster/test/rpc-integration/test-questionmark-vars/response-two-ques-internal.json similarity index 100% rename from booster/test/rpc-integration/test-questionmark-vars/response-two-ques-internal.booster-dev rename to booster/test/rpc-integration/test-questionmark-vars/response-two-ques-internal.json diff --git a/booster/test/rpc-integration/test-questionmark-vars/response-two-ques-internal.kore-rpc-dev b/booster/test/rpc-integration/test-questionmark-vars/response-two-ques-internal.kore-rpc-dev deleted file mode 100644 index a450b120fc..0000000000 --- a/booster/test/rpc-integration/test-questionmark-vars/response-two-ques-internal.kore-rpc-dev +++ /dev/null @@ -1,172 +0,0 @@ -{ - "jsonrpc": "2.0", - "id": 1, - "result": { - "reason": "stuck", - "depth": 2, - "state": { - "term": { - "format": "KORE", - "version": 1, - "term": { - "tag": "App", - "name": "Lbl'-LT-'generatedTop'-GT-'", - "sorts": [], - "args": [ - { - "tag": "App", - "name": "Lbl'-LT-'k'-GT-'", - "sorts": [], - "args": [ - { - "tag": "App", - "name": "dotk", - "sorts": [], - "args": [] - } - ] - }, - { - "tag": "App", - "name": "Lbl'-LT-'a-state'-GT-'", - "sorts": [], - "args": [ - { - "tag": "EVar", - "name": "Var'Ques'X", - "sort": { - "tag": "SortApp", - "name": "SortState", - "args": [] - } - } - ] - }, - { - "tag": "App", - "name": "Lbl'-LT-'b-state'-GT-'", - "sorts": [], - "args": [ - { - "tag": "EVar", - "name": "Var'Ques'X0", - "sort": { - "tag": "SortApp", - "name": "SortState", - "args": [] - } - } - ] - }, - { - "tag": "App", - "name": "Lbl'-LT-'generatedCounter'-GT-'", - "sorts": [], - "args": [ - { - "tag": "DV", - "sort": { - "tag": "SortApp", - "name": "SortInt", - "args": [] - }, - "value": "0" - } - ] - } - ] - } - }, - "predicate": { - "format": "KORE", - "version": 1, - "term": { - "tag": "And", - "sort": { - "tag": "SortApp", - "name": "SortGeneratedTopCell", - "args": [] - }, - "patterns": [ - { - "tag": "Equals", - "argSort": { - "tag": "SortApp", - "name": "SortBool", - "args": [] - }, - "sort": { - "tag": "SortApp", - "name": "SortGeneratedTopCell", - "args": [] - }, - "first": { - "tag": "DV", - "sort": { - "tag": "SortApp", - "name": "SortBool", - "args": [] - }, - "value": "true" - }, - "second": { - "tag": "App", - "name": "Lblcondition'LParUndsRParUnds'QUESTIONMARK-VARS'Unds'Bool'Unds'State", - "sorts": [], - "args": [ - { - "tag": "EVar", - "name": "Var'Ques'X", - "sort": { - "tag": "SortApp", - "name": "SortState", - "args": [] - } - } - ] - } - }, - { - "tag": "Equals", - "argSort": { - "tag": "SortApp", - "name": "SortBool", - "args": [] - }, - "sort": { - "tag": "SortApp", - "name": "SortGeneratedTopCell", - "args": [] - }, - "first": { - "tag": "DV", - "sort": { - "tag": "SortApp", - "name": "SortBool", - "args": [] - }, - "value": "true" - }, - "second": { - "tag": "App", - "name": "Lblcondition'LParUndsRParUnds'QUESTIONMARK-VARS'Unds'Bool'Unds'State", - "sorts": [], - "args": [ - { - "tag": "EVar", - "name": "Var'Ques'X0", - "sort": { - "tag": "SortApp", - "name": "SortState", - "args": [] - } - } - ] - } - } - ] - } - } - } - } -} \ No newline at end of file