diff --git a/booster/test/rpc-integration/test-remainder-predicates/response-test1.booster-dev b/booster/test/rpc-integration/test-remainder-predicates/response-test1.booster-dev new file mode 100644 index 0000000000..0f9d372681 --- /dev/null +++ b/booster/test/rpc-integration/test-remainder-predicates/response-test1.booster-dev @@ -0,0 +1,779 @@ +{ + "jsonrpc": "2.0", + "id": 1, + "result": { + "reason": "branching", + "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": "kseq", + "sorts": [], + "args": [ + { + "tag": "App", + "name": "inj", + "sorts": [ + { + "tag": "SortApp", + "name": "SortState", + "args": [] + }, + { + "tag": "SortApp", + "name": "SortKItem", + "args": [] + } + ], + "args": [ + { + "tag": "App", + "name": "Lbltest1State1'LParRParUnds'REMAINDER-PREDICATES'Unds'State", + "sorts": [], + "args": [] + } + ] + }, + { + "tag": "App", + "name": "dotk", + "sorts": [], + "args": [] + } + ] + } + ] + }, + { + "tag": "App", + "name": "Lbl'-LT-'int'-GT-'", + "sorts": [], + "args": [ + { + "tag": "EVar", + "name": "Var'QuesUnds'X0", + "sort": { + "tag": "SortApp", + "name": "SortInt", + "args": [] + } + } + ] + }, + { + "tag": "App", + "name": "Lbl'-LT-'generatedCounter'-GT-'", + "sorts": [], + "args": [ + { + "tag": "DV", + "sort": { + "tag": "SortApp", + "name": "SortInt", + "args": [] + }, + "value": "0" + } + ] + } + ] + } + } + }, + "next-states": [ + { + "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": "kseq", + "sorts": [], + "args": [ + { + "tag": "App", + "name": "inj", + "sorts": [ + { + "tag": "SortApp", + "name": "SortState", + "args": [] + }, + { + "tag": "SortApp", + "name": "SortKItem", + "args": [] + } + ], + "args": [ + { + "tag": "App", + "name": "Lbltest1State2'LParRParUnds'REMAINDER-PREDICATES'Unds'State", + "sorts": [], + "args": [] + } + ] + }, + { + "tag": "App", + "name": "dotk", + "sorts": [], + "args": [] + } + ] + } + ] + }, + { + "tag": "App", + "name": "Lbl'-LT-'int'-GT-'", + "sorts": [], + "args": [ + { + "tag": "EVar", + "name": "Var'QuesUnds'X0", + "sort": { + "tag": "SortApp", + "name": "SortInt", + "args": [] + } + } + ] + }, + { + "tag": "App", + "name": "Lbl'-LT-'generatedCounter'-GT-'", + "sorts": [], + "args": [ + { + "tag": "DV", + "sort": { + "tag": "SortApp", + "name": "SortInt", + "args": [] + }, + "value": "0" + } + ] + } + ] + } + }, + "substitution": { + "format": "KORE", + "version": 1, + "term": { + "tag": "Equals", + "argSort": { + "tag": "SortApp", + "name": "SortInt", + "args": [] + }, + "sort": { + "tag": "SortApp", + "name": "SortGeneratedTopCell", + "args": [] + }, + "first": { + "tag": "EVar", + "name": "Var'QuesUnds'X0", + "sort": { + "tag": "SortApp", + "name": "SortInt", + "args": [] + } + }, + "second": { + "tag": "DV", + "sort": { + "tag": "SortApp", + "name": "SortInt", + "args": [] + }, + "value": "0" + } + } + }, + "rule-id": "19324e71a2876d53182665d69d04b38dc1f290da170cdcd9ba4cc1bad08f88b7", + "rule-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": "Lbl'UndsEqlsEqls'Int'Unds'", + "sorts": [], + "args": [ + { + "tag": "EVar", + "name": "Var'QuesUnds'X0", + "sort": { + "tag": "SortApp", + "name": "SortInt", + "args": [] + } + }, + { + "tag": "DV", + "sort": { + "tag": "SortApp", + "name": "SortInt", + "args": [] + }, + "value": "0" + } + ] + } + } + }, + "rule-substitution": { + "format": "KORE", + "version": 1, + "term": { + "tag": "And", + "sort": { + "tag": "SortApp", + "name": "SortBool", + "args": [] + }, + "patterns": [ + { + "tag": "Equals", + "argSort": { + "tag": "SortApp", + "name": "SortGeneratedCounterCell", + "args": [] + }, + "sort": { + "tag": "SortApp", + "name": "SortBool", + "args": [] + }, + "first": { + "tag": "EVar", + "name": "RuleVar'Unds'DotVar0", + "sort": { + "tag": "SortApp", + "name": "SortGeneratedCounterCell", + "args": [] + } + }, + "second": { + "tag": "App", + "name": "Lbl'-LT-'generatedCounter'-GT-'", + "sorts": [], + "args": [ + { + "tag": "DV", + "sort": { + "tag": "SortApp", + "name": "SortInt", + "args": [] + }, + "value": "0" + } + ] + } + }, + { + "tag": "Equals", + "argSort": { + "tag": "SortApp", + "name": "SortInt", + "args": [] + }, + "sort": { + "tag": "SortApp", + "name": "SortBool", + "args": [] + }, + "first": { + "tag": "EVar", + "name": "RuleVarX", + "sort": { + "tag": "SortApp", + "name": "SortInt", + "args": [] + } + }, + "second": { + "tag": "EVar", + "name": "Var'QuesUnds'X0", + "sort": { + "tag": "SortApp", + "name": "SortInt", + "args": [] + } + } + }, + { + "tag": "Equals", + "argSort": { + "tag": "SortApp", + "name": "SortIntCell", + "args": [] + }, + "sort": { + "tag": "SortApp", + "name": "SortBool", + "args": [] + }, + "first": { + "tag": "EVar", + "name": "RuleVar'Unds'Gen4", + "sort": { + "tag": "SortApp", + "name": "SortIntCell", + "args": [] + } + }, + "second": { + "tag": "App", + "name": "Lbl'-LT-'int'-GT-'", + "sorts": [], + "args": [ + { + "tag": "EVar", + "name": "Var'QuesUnds'X0", + "sort": { + "tag": "SortApp", + "name": "SortInt", + "args": [] + } + } + ] + } + }, + { + "tag": "Equals", + "argSort": { + "tag": "SortApp", + "name": "SortK", + "args": [] + }, + "sort": { + "tag": "SortApp", + "name": "SortBool", + "args": [] + }, + "first": { + "tag": "EVar", + "name": "RuleVar'Unds'DotVar1", + "sort": { + "tag": "SortApp", + "name": "SortK", + "args": [] + } + }, + "second": { + "tag": "App", + "name": "dotk", + "sorts": [], + "args": [] + } + } + ] + } + } + }, + { + "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": "kseq", + "sorts": [], + "args": [ + { + "tag": "App", + "name": "inj", + "sorts": [ + { + "tag": "SortApp", + "name": "SortState", + "args": [] + }, + { + "tag": "SortApp", + "name": "SortKItem", + "args": [] + } + ], + "args": [ + { + "tag": "App", + "name": "Lbltest1State3'LParRParUnds'REMAINDER-PREDICATES'Unds'State", + "sorts": [], + "args": [] + } + ] + }, + { + "tag": "App", + "name": "dotk", + "sorts": [], + "args": [] + } + ] + } + ] + }, + { + "tag": "App", + "name": "Lbl'-LT-'int'-GT-'", + "sorts": [], + "args": [ + { + "tag": "EVar", + "name": "Var'QuesUnds'X0", + "sort": { + "tag": "SortApp", + "name": "SortInt", + "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": "LblnotBool'Unds'", + "sorts": [], + "args": [ + { + "tag": "App", + "name": "Lbl'UndsEqlsEqls'Int'Unds'", + "sorts": [], + "args": [ + { + "tag": "EVar", + "name": "Var'QuesUnds'X0", + "sort": { + "tag": "SortApp", + "name": "SortInt", + "args": [] + } + }, + { + "tag": "DV", + "sort": { + "tag": "SortApp", + "name": "SortInt", + "args": [] + }, + "value": "0" + } + ] + } + ] + } + } + }, + "rule-id": "f01efa7b27949e9bd90357b1fbe2870e50e1188b7232ef382d6e4edb424e862f", + "rule-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": "LblnotBool'Unds'", + "sorts": [], + "args": [ + { + "tag": "App", + "name": "Lbl'UndsEqlsEqls'Int'Unds'", + "sorts": [], + "args": [ + { + "tag": "EVar", + "name": "Var'QuesUnds'X0", + "sort": { + "tag": "SortApp", + "name": "SortInt", + "args": [] + } + }, + { + "tag": "DV", + "sort": { + "tag": "SortApp", + "name": "SortInt", + "args": [] + }, + "value": "0" + } + ] + } + ] + } + } + }, + "rule-substitution": { + "format": "KORE", + "version": 1, + "term": { + "tag": "And", + "sort": { + "tag": "SortApp", + "name": "SortBool", + "args": [] + }, + "patterns": [ + { + "tag": "Equals", + "argSort": { + "tag": "SortApp", + "name": "SortGeneratedCounterCell", + "args": [] + }, + "sort": { + "tag": "SortApp", + "name": "SortBool", + "args": [] + }, + "first": { + "tag": "EVar", + "name": "RuleVar'Unds'DotVar0", + "sort": { + "tag": "SortApp", + "name": "SortGeneratedCounterCell", + "args": [] + } + }, + "second": { + "tag": "App", + "name": "Lbl'-LT-'generatedCounter'-GT-'", + "sorts": [], + "args": [ + { + "tag": "DV", + "sort": { + "tag": "SortApp", + "name": "SortInt", + "args": [] + }, + "value": "0" + } + ] + } + }, + { + "tag": "Equals", + "argSort": { + "tag": "SortApp", + "name": "SortInt", + "args": [] + }, + "sort": { + "tag": "SortApp", + "name": "SortBool", + "args": [] + }, + "first": { + "tag": "EVar", + "name": "RuleVarX", + "sort": { + "tag": "SortApp", + "name": "SortInt", + "args": [] + } + }, + "second": { + "tag": "EVar", + "name": "Var'QuesUnds'X0", + "sort": { + "tag": "SortApp", + "name": "SortInt", + "args": [] + } + } + }, + { + "tag": "Equals", + "argSort": { + "tag": "SortApp", + "name": "SortIntCell", + "args": [] + }, + "sort": { + "tag": "SortApp", + "name": "SortBool", + "args": [] + }, + "first": { + "tag": "EVar", + "name": "RuleVar'Unds'Gen4", + "sort": { + "tag": "SortApp", + "name": "SortIntCell", + "args": [] + } + }, + "second": { + "tag": "App", + "name": "Lbl'-LT-'int'-GT-'", + "sorts": [], + "args": [ + { + "tag": "EVar", + "name": "Var'QuesUnds'X0", + "sort": { + "tag": "SortApp", + "name": "SortInt", + "args": [] + } + } + ] + } + }, + { + "tag": "Equals", + "argSort": { + "tag": "SortApp", + "name": "SortK", + "args": [] + }, + "sort": { + "tag": "SortApp", + "name": "SortBool", + "args": [] + }, + "first": { + "tag": "EVar", + "name": "RuleVar'Unds'DotVar1", + "sort": { + "tag": "SortApp", + "name": "SortK", + "args": [] + } + }, + "second": { + "tag": "App", + "name": "dotk", + "sorts": [], + "args": [] + } + } + ] + } + } + } + ] + } +} \ No newline at end of file