From 8e622f9873ce5af40d1cfce9eadbb102bb719024 Mon Sep 17 00:00:00 2001 From: Georgy Lukyanov Date: Tue, 22 Oct 2024 14:06:52 +0200 Subject: [PATCH] Update test-questionmark-vars --- .../response-one-ques-substitution.json | 112 ++++++------ ...sponse-one-ques-substitution.kore-rpc-dev} | 112 ++++++------ ...ues.booster-dev => response-one-ques.json} | 0 .../response-one-ques.kore-rpc-dev | 121 ------------ ...er-dev => response-two-ques-external.json} | 0 .../response-two-ques-external.kore-rpc-dev | 124 ------------- ...ponse-two-ques-internal-with-counter.json} | 0 ...er-dev => response-two-ques-internal.json} | 0 .../response-two-ques-internal.kore-rpc-dev | 172 ------------------ 9 files changed, 112 insertions(+), 529 deletions(-) rename booster/test/rpc-integration/test-questionmark-vars/{response-one-ques-substitution.booster-dev => response-one-ques-substitution.kore-rpc-dev} (67%) rename booster/test/rpc-integration/test-questionmark-vars/{response-one-ques.booster-dev => response-one-ques.json} (100%) delete mode 100644 booster/test/rpc-integration/test-questionmark-vars/response-one-ques.kore-rpc-dev rename booster/test/rpc-integration/test-questionmark-vars/{response-two-ques-external.booster-dev => response-two-ques-external.json} (100%) delete mode 100644 booster/test/rpc-integration/test-questionmark-vars/response-two-ques-external.kore-rpc-dev rename booster/test/rpc-integration/test-questionmark-vars/{response-two-ques-internal-with-counter.booster-dev => response-two-ques-internal-with-counter.json} (100%) rename booster/test/rpc-integration/test-questionmark-vars/{response-two-ques-internal.booster-dev => response-two-ques-internal.json} (100%) delete mode 100644 booster/test/rpc-integration/test-questionmark-vars/response-two-ques-internal.kore-rpc-dev 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