Skip to content

Commit f8f74b7

Browse files
geo2ageo2a
committed
Separate kore-rpc-dev and kore-rpc-booster responses for test-substitution
1 parent 059a6d4 commit f8f74b7

6 files changed

+508
-36
lines changed

‎booster/test/rpc-integration/test-diamond/response-infeasible-branching.kore-rpc-dev

Lines changed: 136 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,136 @@
1+
{
2+
"jsonrpc": "2.0",
3+
"id": 1,
4+
"result": {
5+
"reason": "terminal-rule",
6+
"depth": 3,
7+
"rule": "TEST.BD",
8+
"state": {
9+
"term": {
10+
"format": "KORE",
11+
"version": 1,
12+
"term": {
13+
"tag": "App",
14+
"name": "Lbl'-LT-'generatedTop'-GT-'",
15+
"sorts": [],
16+
"args": [
17+
{
18+
"tag": "App",
19+
"name": "Lbl'-LT-'k'-GT-'",
20+
"sorts": [],
21+
"args": [
22+
{
23+
"tag": "App",
24+
"name": "kseq",
25+
"sorts": [],
26+
"args": [
27+
{
28+
"tag": "App",
29+
"name": "inj",
30+
"sorts": [
31+
{
32+
"tag": "SortApp",
33+
"name": "SortState",
34+
"args": []
35+
},
36+
{
37+
"tag": "SortApp",
38+
"name": "SortKItem",
39+
"args": []
40+
}
41+
],
42+
"args": [
43+
{
44+
"tag": "DV",
45+
"sort": {
46+
"tag": "SortApp",
47+
"name": "SortState",
48+
"args": []
49+
},
50+
"value": "d"
51+
}
52+
]
53+
},
54+
{
55+
"tag": "App",
56+
"name": "dotk",
57+
"sorts": [],
58+
"args": []
59+
}
60+
]
61+
}
62+
]
63+
},
64+
{
65+
"tag": "App",
66+
"name": "Lbl'-LT-'int'-GT-'",
67+
"sorts": [],
68+
"args": [
69+
{
70+
"tag": "DV",
71+
"sort": {
72+
"tag": "SortApp",
73+
"name": "SortInt",
74+
"args": []
75+
},
76+
"value": "42"
77+
}
78+
]
79+
},
80+
{
81+
"tag": "App",
82+
"name": "Lbl'-LT-'generatedCounter'-GT-'",
83+
"sorts": [],
84+
"args": [
85+
{
86+
"tag": "DV",
87+
"sort": {
88+
"tag": "SortApp",
89+
"name": "SortInt",
90+
"args": []
91+
},
92+
"value": "0"
93+
}
94+
]
95+
}
96+
]
97+
}
98+
},
99+
"substitution": {
100+
"format": "KORE",
101+
"version": 1,
102+
"term": {
103+
"tag": "Equals",
104+
"argSort": {
105+
"tag": "SortApp",
106+
"name": "SortInt",
107+
"args": []
108+
},
109+
"sort": {
110+
"tag": "SortApp",
111+
"name": "SortGeneratedTopCell",
112+
"args": []
113+
},
114+
"first": {
115+
"tag": "EVar",
116+
"name": "X",
117+
"sort": {
118+
"tag": "SortApp",
119+
"name": "SortInt",
120+
"args": []
121+
}
122+
},
123+
"second": {
124+
"tag": "DV",
125+
"sort": {
126+
"tag": "SortApp",
127+
"name": "SortInt",
128+
"args": []
129+
},
130+
"value": "42"
131+
}
132+
}
133+
}
134+
}
135+
}
136+
}

‎booster/test/rpc-integration/test-substitutions/response-concrete-substitution.json

Lines changed: 32 additions & 16 deletions
Original file line numberDiff line numberDiff line change
@@ -67,13 +67,13 @@
6767
"sorts": [],
6868
"args": [
6969
{
70-
"tag": "DV",
70+
"tag": "EVar",
71+
"name": "X",
7172
"sort": {
7273
"tag": "SortApp",
7374
"name": "SortInt",
7475
"args": []
75-
},
76-
"value": "42"
76+
}
7777
}
7878
]
7979
},
@@ -112,14 +112,14 @@
112112
]
113113
}
114114
},
115-
"substitution": {
115+
"predicate": {
116116
"format": "KORE",
117117
"version": 1,
118118
"term": {
119119
"tag": "Equals",
120120
"argSort": {
121121
"tag": "SortApp",
122-
"name": "SortInt",
122+
"name": "SortBool",
123123
"args": []
124124
},
125125
"sort": {
@@ -128,22 +128,38 @@
128128
"args": []
129129
},
130130
"first": {
131-
"tag": "EVar",
132-
"name": "X",
133-
"sort": {
134-
"tag": "SortApp",
135-
"name": "SortInt",
136-
"args": []
137-
}
138-
},
139-
"second": {
140131
"tag": "DV",
141132
"sort": {
142133
"tag": "SortApp",
143-
"name": "SortInt",
134+
"name": "SortBool",
144135
"args": []
145136
},
146-
"value": "42"
137+
"value": "true"
138+
},
139+
"second": {
140+
"tag": "App",
141+
"name": "Lbl'UndsEqlsEqls'Int'Unds'",
142+
"sorts": [],
143+
"args": [
144+
{
145+
"tag": "EVar",
146+
"name": "X",
147+
"sort": {
148+
"tag": "SortApp",
149+
"name": "SortInt",
150+
"args": []
151+
}
152+
},
153+
{
154+
"tag": "DV",
155+
"sort": {
156+
"tag": "SortApp",
157+
"name": "SortInt",
158+
"args": []
159+
},
160+
"value": "42"
161+
}
162+
]
147163
}
148164
}
149165
}

‎booster/test/rpc-integration/test-substitutions/response-concrete-substitution.kore-rpc-dev

Lines changed: 152 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,152 @@
1+
{
2+
"jsonrpc": "2.0",
3+
"id": 1,
4+
"result": {
5+
"reason": "terminal-rule",
6+
"depth": 1,
7+
"rule": "TEST.concrete-subst",
8+
"state": {
9+
"term": {
10+
"format": "KORE",
11+
"version": 1,
12+
"term": {
13+
"tag": "App",
14+
"name": "Lbl'-LT-'generatedTop'-GT-'",
15+
"sorts": [],
16+
"args": [
17+
{
18+
"tag": "App",
19+
"name": "Lbl'-LT-'k'-GT-'",
20+
"sorts": [],
21+
"args": [
22+
{
23+
"tag": "App",
24+
"name": "kseq",
25+
"sorts": [],
26+
"args": [
27+
{
28+
"tag": "App",
29+
"name": "inj",
30+
"sorts": [
31+
{
32+
"tag": "SortApp",
33+
"name": "SortState",
34+
"args": []
35+
},
36+
{
37+
"tag": "SortApp",
38+
"name": "SortKItem",
39+
"args": []
40+
}
41+
],
42+
"args": [
43+
{
44+
"tag": "DV",
45+
"sort": {
46+
"tag": "SortApp",
47+
"name": "SortState",
48+
"args": []
49+
},
50+
"value": "a"
51+
}
52+
]
53+
},
54+
{
55+
"tag": "App",
56+
"name": "dotk",
57+
"sorts": [],
58+
"args": []
59+
}
60+
]
61+
}
62+
]
63+
},
64+
{
65+
"tag": "App",
66+
"name": "Lbl'-LT-'int'-GT-'",
67+
"sorts": [],
68+
"args": [
69+
{
70+
"tag": "DV",
71+
"sort": {
72+
"tag": "SortApp",
73+
"name": "SortInt",
74+
"args": []
75+
},
76+
"value": "42"
77+
}
78+
]
79+
},
80+
{
81+
"tag": "App",
82+
"name": "Lbl'-LT-'jnt'-GT-'",
83+
"sorts": [],
84+
"args": [
85+
{
86+
"tag": "EVar",
87+
"name": "Y",
88+
"sort": {
89+
"tag": "SortApp",
90+
"name": "SortInt",
91+
"args": []
92+
}
93+
}
94+
]
95+
},
96+
{
97+
"tag": "App",
98+
"name": "Lbl'-LT-'generatedCounter'-GT-'",
99+
"sorts": [],
100+
"args": [
101+
{
102+
"tag": "DV",
103+
"sort": {
104+
"tag": "SortApp",
105+
"name": "SortInt",
106+
"args": []
107+
},
108+
"value": "0"
109+
}
110+
]
111+
}
112+
]
113+
}
114+
},
115+
"substitution": {
116+
"format": "KORE",
117+
"version": 1,
118+
"term": {
119+
"tag": "Equals",
120+
"argSort": {
121+
"tag": "SortApp",
122+
"name": "SortInt",
123+
"args": []
124+
},
125+
"sort": {
126+
"tag": "SortApp",
127+
"name": "SortGeneratedTopCell",
128+
"args": []
129+
},
130+
"first": {
131+
"tag": "EVar",
132+
"name": "X",
133+
"sort": {
134+
"tag": "SortApp",
135+
"name": "SortInt",
136+
"args": []
137+
}
138+
},
139+
"second": {
140+
"tag": "DV",
141+
"sort": {
142+
"tag": "SortApp",
143+
"name": "SortInt",
144+
"args": []
145+
},
146+
"value": "42"
147+
}
148+
}
149+
}
150+
}
151+
}
152+
}

0 commit comments

Comments
 (0)