Skip to content

Commit 8246f99

Browse files
geo2ageo2a
committed
Update remainders integration test for booster-dev
1 parent 11ae8e0 commit 8246f99

13 files changed

+661
-2157
lines changed

‎booster/test/rpc-integration/resources/remainder-predicates.k

Lines changed: 33 additions & 7 deletions
Original file line numberDiff line numberDiff line change
@@ -37,6 +37,11 @@ module REMAINDER-PREDICATES
3737
| test6State4()
3838
| test6State5()
3939

40+
| test11Init()
41+
| test11State1()
42+
| test11State2()
43+
| test11State3()
44+
4045
configuration <k> $PGM:State ~> .K </k>
4146
<int> 0:Int </int>
4247

@@ -49,17 +54,38 @@ module REMAINDER-PREDICATES
4954

5055
rule [test1-1-2]: <k> test1State1() => test1State2() ... </k>
5156
<int> X </int>
52-
requires X >Int 0
57+
requires X ==Int 0
5358

5459
rule [test1-1-3]: <k> test1State1() => test1State3() ... </k>
5560
<int> X </int>
56-
requires X <=Int 0
61+
requires X =/=Int 0
62+
63+
////////////////////////////////////////////////////////////////////////////////
64+
/// two rules apply with UNSAT remainder predicate, //
65+
/// but only after function evaluation. No further rules apply. //
66+
/// Results in 2 branches. //
67+
////////////////////////////////////////////////////////////////////////////////
68+
rule [test11-init]: <k> test11Init() => test11State1() ... </k>
69+
<int> _ => ?_X </int>
70+
71+
rule [test11-1-2]: <k> test11State1() => test11State2() ... </k>
72+
<int> X </int>
73+
requires test11bool2Word(X ==Int 0) ==Int 1
74+
75+
rule [test11-1-3]: <k> test11State1() => test11State3() ... </k>
76+
<int> X </int>
77+
requires test11bool2Word(X =/=Int 0) ==Int 1
78+
79+
syntax Int ::= test11bool2Word ( Bool ) [symbol(bool2Word), function, total, injective, smtlib(bool2Word)]
80+
81+
rule [test11-b2w-eq-zero]: test11bool2Word(B) ==Int 0 => notBool B [simplification(30), comm]
82+
rule [test11-b2w-eq-one]: test11bool2Word(B) ==Int 1 => B [simplification(30), comm]
5783

5884
////////////////////////////////////////////////////////////////////////////////
5985
/// two rules apply with SAT remainder predicate, //
6086
/// have to consider the remainder branch where X ==Int 0, //
6187
/// no further rules apply. //
62-
/// Results in 2 branches. //
88+
/// Aborts with boosted-dev; results in 2 branches in kore-rpc-booster. //
6389
////////////////////////////////////////////////////////////////////////////////
6490
rule [test2-init]: <k> test2Init() => test2State1() ... </k>
6591
<int> _ => ?_X </int>
@@ -76,7 +102,7 @@ module REMAINDER-PREDICATES
76102
/// two rules apply with SAT remainder predicate, //
77103
/// have to consider the remainder branch where X ==Int 0, //
78104
/// but the are no further rules to apply. //
79-
/// Results in 2 branches. //
105+
/// Aborts with boosted-dev; results in 2 branches in kore-rpc-booster. //
80106
////////////////////////////////////////////////////////////////////////////////
81107
rule [test3-init]: <k> test3Init() => test3State1() ... </k>
82108
<int> _ => ?_X </int>
@@ -94,7 +120,7 @@ module REMAINDER-PREDICATES
94120
/// have to consider the remainder branch where X ==Int 0, //
95121
/// one further regular rule applies, //
96122
/// whose requires clause explicitly completes the space. //
97-
/// Results in 3 branches. //
123+
/// Aborts with boosted-dev; results in 3 branches in kore-rpc-booster. //
98124
////////////////////////////////////////////////////////////////////////////////
99125
rule [test4-init]: <k> test4Init() => test4State1() ... </k>
100126
<int> _ => ?_X </int>
@@ -119,7 +145,7 @@ module REMAINDER-PREDICATES
119145
/// have to consider the remainder branch where X ==Int 0, //
120146
/// one rule at a lower priority applies unconditionally, which means that //
121147
/// that the remainder is False. Rule test5-1-5 is unreachable. //
122-
/// Results in 3 branches. //
148+
/// Aborts with boosted-dev; results in 3 branches in kore-rpc-booster. //
123149
////////////////////////////////////////////////////////////////////////////////
124150
rule [test5-init]: <k> test5Init() => test5State1() ... </k>
125151
<int> _ => ?_X </int>
@@ -143,7 +169,7 @@ module REMAINDER-PREDICATES
143169
/// two hight-priorty rules apply with SAT remainder predicate, //
144170
/// have to consider the remainder branch where X ==Int 0, //
145171
/// two rule at a lower priority applies unconditionally. //
146-
/// Results in 4 branches. //
172+
/// Aborts with boosted-dev; results in 4 branches in kore-rpc-booster. //
147173
////////////////////////////////////////////////////////////////////////////////
148174
rule [test6-init]: <k> test6Init() => test6State1() ... </k>
149175
<int> _ => ?_X </int>

‎booster/test/rpc-integration/test-remainder-predicates/response-test2.json renamed to ‎booster/test/rpc-integration/test-remainder-predicates/response-test11.booster-dev

Lines changed: 55 additions & 41 deletions
Original file line numberDiff line numberDiff line change
@@ -41,7 +41,7 @@
4141
"args": [
4242
{
4343
"tag": "App",
44-
"name": "Lbltest2State1'LParRParUnds'REMAINDER-PREDICATES'Unds'State",
44+
"name": "Lbltest11State1'LParRParUnds'REMAINDER-PREDICATES'Unds'State",
4545
"sorts": [],
4646
"args": []
4747
}
@@ -131,7 +131,7 @@
131131
"args": [
132132
{
133133
"tag": "App",
134-
"name": "Lbltest2State2'LParRParUnds'REMAINDER-PREDICATES'Unds'State",
134+
"name": "Lbltest11State2'LParRParUnds'REMAINDER-PREDICATES'Unds'State",
135135
"sorts": [],
136136
"args": []
137137
}
@@ -208,7 +208,7 @@
208208
},
209209
"second": {
210210
"tag": "App",
211-
"name": "Lbl'Unds-GT-'Int'Unds'",
211+
"name": "Lbl'UndsEqlsEqls'Int'Unds'",
212212
"sorts": [],
213213
"args": [
214214
{
@@ -233,7 +233,7 @@
233233
}
234234
}
235235
},
236-
"rule-id": "f1062b57b8ba73d1fa8fa0a1b5cb828ee0c750f42a3ff3227b6ddb5c260b8c03",
236+
"rule-id": "f54071f2a0ee01e4094f9dea825a6b4e5cf15453acc52ff5b431e712ce1f1087",
237237
"rule-predicate": {
238238
"format": "KORE",
239239
"version": 1,
@@ -260,7 +260,7 @@
260260
},
261261
"second": {
262262
"tag": "App",
263-
"name": "Lbl'Unds-GT-'Int'Unds'",
263+
"name": "Lbl'UndsEqlsEqls'Int'Unds'",
264264
"sorts": [],
265265
"args": [
266266
{
@@ -323,7 +323,7 @@
323323
"args": [
324324
{
325325
"tag": "App",
326-
"name": "Lbltest2State3'LParRParUnds'REMAINDER-PREDICATES'Unds'State",
326+
"name": "Lbltest11State3'LParRParUnds'REMAINDER-PREDICATES'Unds'State",
327327
"sorts": [],
328328
"args": []
329329
}
@@ -400,32 +400,39 @@
400400
},
401401
"second": {
402402
"tag": "App",
403-
"name": "Lbl'Unds-LT-'Int'Unds'",
403+
"name": "LblnotBool'Unds'",
404404
"sorts": [],
405405
"args": [
406406
{
407-
"tag": "EVar",
408-
"name": "Var'QuesUnds'X0",
409-
"sort": {
410-
"tag": "SortApp",
411-
"name": "SortInt",
412-
"args": []
413-
}
414-
},
415-
{
416-
"tag": "DV",
417-
"sort": {
418-
"tag": "SortApp",
419-
"name": "SortInt",
420-
"args": []
421-
},
422-
"value": "0"
407+
"tag": "App",
408+
"name": "Lbl'UndsEqlsEqls'Int'Unds'",
409+
"sorts": [],
410+
"args": [
411+
{
412+
"tag": "EVar",
413+
"name": "Var'QuesUnds'X0",
414+
"sort": {
415+
"tag": "SortApp",
416+
"name": "SortInt",
417+
"args": []
418+
}
419+
},
420+
{
421+
"tag": "DV",
422+
"sort": {
423+
"tag": "SortApp",
424+
"name": "SortInt",
425+
"args": []
426+
},
427+
"value": "0"
428+
}
429+
]
423430
}
424431
]
425432
}
426433
}
427434
},
428-
"rule-id": "54a5fca77be17b0d99e953eded75809e0ed9046f73cab5027603a82df1f4c4b2",
435+
"rule-id": "b3179a4519053c503ae87c9c4ed9664840941bfc3946f3de50646292f474a038",
429436
"rule-predicate": {
430437
"format": "KORE",
431438
"version": 1,
@@ -452,26 +459,33 @@
452459
},
453460
"second": {
454461
"tag": "App",
455-
"name": "Lbl'Unds-LT-'Int'Unds'",
462+
"name": "LblnotBool'Unds'",
456463
"sorts": [],
457464
"args": [
458465
{
459-
"tag": "EVar",
460-
"name": "Var'QuesUnds'X0",
461-
"sort": {
462-
"tag": "SortApp",
463-
"name": "SortInt",
464-
"args": []
465-
}
466-
},
467-
{
468-
"tag": "DV",
469-
"sort": {
470-
"tag": "SortApp",
471-
"name": "SortInt",
472-
"args": []
473-
},
474-
"value": "0"
466+
"tag": "App",
467+
"name": "Lbl'UndsEqlsEqls'Int'Unds'",
468+
"sorts": [],
469+
"args": [
470+
{
471+
"tag": "EVar",
472+
"name": "Var'QuesUnds'X0",
473+
"sort": {
474+
"tag": "SortApp",
475+
"name": "SortInt",
476+
"args": []
477+
}
478+
},
479+
{
480+
"tag": "DV",
481+
"sort": {
482+
"tag": "SortApp",
483+
"name": "SortInt",
484+
"args": []
485+
},
486+
"value": "0"
487+
}
488+
]
475489
}
476490
]
477491
}

‎booster/test/rpc-integration/test-remainder-predicates/response-test2.booster-dev

Lines changed: 97 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,97 @@
1+
{
2+
"jsonrpc": "2.0",
3+
"id": 1,
4+
"result": {
5+
"reason": "aborted",
6+
"depth": 1,
7+
"state": {
8+
"term": {
9+
"format": "KORE",
10+
"version": 1,
11+
"term": {
12+
"tag": "App",
13+
"name": "Lbl'-LT-'generatedTop'-GT-'",
14+
"sorts": [],
15+
"args": [
16+
{
17+
"tag": "App",
18+
"name": "Lbl'-LT-'k'-GT-'",
19+
"sorts": [],
20+
"args": [
21+
{
22+
"tag": "App",
23+
"name": "kseq",
24+
"sorts": [],
25+
"args": [
26+
{
27+
"tag": "App",
28+
"name": "inj",
29+
"sorts": [
30+
{
31+
"tag": "SortApp",
32+
"name": "SortState",
33+
"args": []
34+
},
35+
{
36+
"tag": "SortApp",
37+
"name": "SortKItem",
38+
"args": []
39+
}
40+
],
41+
"args": [
42+
{
43+
"tag": "App",
44+
"name": "Lbltest2State1'LParRParUnds'REMAINDER-PREDICATES'Unds'State",
45+
"sorts": [],
46+
"args": []
47+
}
48+
]
49+
},
50+
{
51+
"tag": "App",
52+
"name": "dotk",
53+
"sorts": [],
54+
"args": []
55+
}
56+
]
57+
}
58+
]
59+
},
60+
{
61+
"tag": "App",
62+
"name": "Lbl'-LT-'int'-GT-'",
63+
"sorts": [],
64+
"args": [
65+
{
66+
"tag": "EVar",
67+
"name": "Var'QuesUnds'X0",
68+
"sort": {
69+
"tag": "SortApp",
70+
"name": "SortInt",
71+
"args": []
72+
}
73+
}
74+
]
75+
},
76+
{
77+
"tag": "App",
78+
"name": "Lbl'-LT-'generatedCounter'-GT-'",
79+
"sorts": [],
80+
"args": [
81+
{
82+
"tag": "DV",
83+
"sort": {
84+
"tag": "SortApp",
85+
"name": "SortInt",
86+
"args": []
87+
},
88+
"value": "0"
89+
}
90+
]
91+
}
92+
]
93+
}
94+
}
95+
}
96+
}
97+
}

0 commit comments

Comments
 (0)