| 16 Apr 2021 |
 kunwangyml | Why it ask for a Statement😂 | 07:02:06 |
| kunwangyml | 
Download image.png | 07:04:03 |
 Ali | * Here is a small self-contained example that demonstrates the likely bug mentioned above in the java backend:
module TEST-SYNTAX
imports ID
syntax X ::= "x"
endmodule
module TEST
imports DOMAINS
imports TEST-SYNTAX
configuration
<k> $PGM:X </k>
<ts>
<t multiplicity="*" type="Set">
<name> .K </name>
</t>
</ts>
syntax Y ::= "y1" | "y2"
rule <k> _:X => y2 </k>
<ts>
(.Bag => <t> <name> y1 </name> </t>)
(.Bag => <t> <name> y2 </name> </t>)
...
</ts>
syntax KItem ::= "SUCCESS"
rule <k> I:Y => SUCCESS </k>
<ts>
<t> <name> I </name> </t>
...
</ts>
endmodule
The execution gets stuck at:
<generatedTop>
<k>
y2
</k>
<ts>
SetItem ( <t>
<name>
y1
</name>
</t> )
SetItem ( <t>
<name>
y2
</name>
</t> )
</ts>
</generatedTop>
| 07:52:55 |
| Ali | Question: is the java backend deprecated? I am encountering other bugs/problems even on simple examples. Was wondering if I should abandon that backend or not. | 10:44:20 |
 everett.hildenbrandt | Yes, we are not maintaining the Java backend at all anymore. | 12:41:13 |
| everett.hildenbrandt | It will remain around while there are still large semantics working with it. | 12:41:31 |
| everett.hildenbrandt | But it will not receive anything but the simplest of updates. | 12:41:44 |
| everett.hildenbrandt | Please switch to the haskell backend. | 12:41:51 |
| 17 Apr 2021 |
| Ali | Followup: Are all the features supported by the java backend already implemented in the haskell backend, if not, I was wondering what is missing. E.g. seems like keq is only supported with the java backend. | 08:18:52 |
| Ali | * Followup: Are all the features supported by the java backend already implemented in the haskell backend, if not, I was wondering what is missing. E.g. seems like keq is only supported with the java backend. | 08:29:58 |
| Ali | Can someone kindly explain the meaning of the output of search running with the haskel backend. Does it just say whether the pattern is reachable or not or does it give the conditions for the pattern to be reachable. E.g. for the following
module TEST-SYNTAX
imports ID
syntax X ::= "x"
endmodule
module TEST
imports DOMAINS
imports TEST-SYNTAX
configuration
<k> $PGM:X </k>
<ts> .K </ts>
rule <k> _:X => .K </k>
<ts> _ => ?L:List </ts>
syntax KItem ::= "o1" | "o2" | "o3" | "o4"
rule <k> .K => o1 </k>
<ts> ListItem(10) </ts>
rule <k> .K => o2 </k>
<ts> ListItem(10) </ts>
rule <k> .K => o3 </k>
<ts> ListItem(20) ListItem(30) </ts>
endmodule
if I run krun x --search --pattern "<k> o1 </k>” I get
#TOP
Now if I run krun x --search --pattern "<k> I:KItem </k>” I get
{
I:KItem
#Equals
o3
}
#Or
{
I:KItem
#Equals
o1
}
#Or
{
I:KItem
#Equals
o2
}
And for krun x --search --pattern "<k> I:K </k>” ,
#Not ( {
?L:List
#Equals
ListItem ( 10 )
} )
#And
#Not ( {
?L:List
#Equals
ListItem ( 20 )
ListItem ( 30 )
} )
#And
{
I:K
#Equals
.
}
#Or
{
I:K
#Equals
o1 ~> .
}
#Or
{
I:K
#Equals
o2 ~> .
}
#Or
{
I:K
#Equals
o3 ~> .
}
In any case result.kore seems to contain some conditions, it is kprint that picks what to display. So I was wondering what is the logic behind selecting what to display in kprint (e.g. why it sometimes shows the condition on ?L and sometimes doesn't).
| 10:34:20 |
| Ali | * Can someone kindly explain the meaning of the output running in the haskel backend. Does it just say the pattern is reachable or not or does it give the conditions for the pattern to be reachable. E.g. for the following
module TEST-SYNTAX
imports ID
syntax X ::= "x"
endmodule
module TEST
imports DOMAINS
imports TEST-SYNTAX
configuration
<k> $PGM:X </k>
<ts> .K </ts>
rule <k> _:X => .K </k>
<ts> _ => ?L:List </ts>
syntax KItem ::= "o1" | "o2" | "o3" | "o4"
rule <k> .K => o1 </k>
<ts> ListItem(10) </ts>
rule <k> .K => o2 </k>
<ts> ListItem(10) </ts>
rule <k> .K => o3 </k>
<ts> ListItem(20) ListItem(30) </ts>
endmodule
if I run krun x --search --pattern "<k> o1 </k>” I get
#TOP
Now if I run krun x --search --pattern "<k> I:KItem </k>” I get
{
I:KItem
#Equals
o3
}
#Or
{
I:KItem
#Equals
o1
}
#Or
{
I:KItem
#Equals
o2
}
And for krun x --search --pattern "<k> I:K </k>” ,
#Not ( {
?L:List
#Equals
ListItem ( 10 )
} )
#And
#Not ( {
?L:List
#Equals
ListItem ( 20 )
ListItem ( 30 )
} )
#And
{
I:K
#Equals
.
}
#Or
{
I:K
#Equals
o1 ~> .
}
#Or
{
I:K
#Equals
o2 ~> .
}
#Or
{
I:K
#Equals
o3 ~> .
}
| 10:34:53 |
| Ali | * Can someone kindly explain the meaning of the output running in the haskel backend. Does it just say the pattern is reachable or not or does it give the conditions for the pattern to be reachable. E.g. for the following
module TEST-SYNTAX
imports ID
syntax X ::= "x"
endmodule
module TEST
imports DOMAINS
imports TEST-SYNTAX
configuration
<k> $PGM:X </k>
<ts> .K </ts>
rule <k> _:X => .K </k>
<ts> _ => ?L:List </ts>
syntax KItem ::= "o1" | "o2" | "o3" | "o4"
rule <k> .K => o1 </k>
<ts> ListItem(10) </ts>
rule <k> .K => o2 </k>
<ts> ListItem(10) </ts>
rule <k> .K => o3 </k>
<ts> ListItem(20) ListItem(30) </ts>
endmodule
if I run krun x --search --pattern "<k> o1 </k>” I get
#TOP
Now if I run krun x --search --pattern "<k> I:KItem </k>” I get
{
I:KItem
#Equals
o3
}
#Or
{
I:KItem
#Equals
o1
}
#Or
{
I:KItem
#Equals
o2
}
And for krun x --search --pattern "<k> I:K </k>” ,
#Not ( {
?L:List
#Equals
ListItem ( 10 )
} )
#And
#Not ( {
?L:List
#Equals
ListItem ( 20 )
ListItem ( 30 )
} )
#And
{
I:K
#Equals
.
}
#Or
{
I:K
#Equals
o1 ~> .
}
#Or
{
I:K
#Equals
o2 ~> .
}
#Or
{
I:K
#Equals
o3 ~> .
}
In any case result.kore seems to contain all conditions, it is kprint that picks what to display. So more concretely I was wondering what is the logic behind selecting what to display in kprint.
| 10:44:30 |
| Ali | * Can someone kindly explain the meaning of the output running in the haskel backend. Does it just say the pattern is reachable or not or does it give the conditions for the pattern to be reachable. E.g. for the following
module TEST-SYNTAX
imports ID
syntax X ::= "x"
endmodule
module TEST
imports DOMAINS
imports TEST-SYNTAX
configuration
<k> $PGM:X </k>
<ts> .K </ts>
rule <k> _:X => .K </k>
<ts> _ => ?L:List </ts>
syntax KItem ::= "o1" | "o2" | "o3" | "o4"
rule <k> .K => o1 </k>
<ts> ListItem(10) </ts>
rule <k> .K => o2 </k>
<ts> ListItem(10) </ts>
rule <k> .K => o3 </k>
<ts> ListItem(20) ListItem(30) </ts>
endmodule
if I run krun x --search --pattern "<k> o1 </k>” I get
#TOP
Now if I run krun x --search --pattern "<k> I:KItem </k>” I get
{
I:KItem
#Equals
o3
}
#Or
{
I:KItem
#Equals
o1
}
#Or
{
I:KItem
#Equals
o2
}
And for krun x --search --pattern "<k> I:K </k>” ,
#Not ( {
?L:List
#Equals
ListItem ( 10 )
} )
#And
#Not ( {
?L:List
#Equals
ListItem ( 20 )
ListItem ( 30 )
} )
#And
{
I:K
#Equals
.
}
#Or
{
I:K
#Equals
o1 ~> .
}
#Or
{
I:K
#Equals
o2 ~> .
}
#Or
{
I:K
#Equals
o3 ~> .
}
In any case result.kore seems to contain all conditions, it is kprint that picks what to display. So more concretely I was wondering what is the logic behind selecting what to display in kprint (e.g. why it sometimes show the condition on ?L and sometimes doesn't)
| 10:47:01 |
| Ali | * Can someone kindly explain the meaning of the output running in the haskel backend. Does it just say the pattern is reachable or not or does it give the conditions for the pattern to be reachable. E.g. for the following
module TEST-SYNTAX
imports ID
syntax X ::= "x"
endmodule
module TEST
imports DOMAINS
imports TEST-SYNTAX
configuration
<k> $PGM:X </k>
<ts> .K </ts>
rule <k> _:X => .K </k>
<ts> _ => ?L:List </ts>
syntax KItem ::= "o1" | "o2" | "o3" | "o4"
rule <k> .K => o1 </k>
<ts> ListItem(10) </ts>
rule <k> .K => o2 </k>
<ts> ListItem(10) </ts>
rule <k> .K => o3 </k>
<ts> ListItem(20) ListItem(30) </ts>
endmodule
if I run krun x --search --pattern "<k> o1 </k>” I get
#TOP
Now if I run krun x --search --pattern "<k> I:KItem </k>” I get
{
I:KItem
#Equals
o3
}
#Or
{
I:KItem
#Equals
o1
}
#Or
{
I:KItem
#Equals
o2
}
And for krun x --search --pattern "<k> I:K </k>” ,
#Not ( {
?L:List
#Equals
ListItem ( 10 )
} )
#And
#Not ( {
?L:List
#Equals
ListItem ( 20 )
ListItem ( 30 )
} )
#And
{
I:K
#Equals
.
}
#Or
{
I:K
#Equals
o1 ~> .
}
#Or
{
I:K
#Equals
o2 ~> .
}
#Or
{
I:K
#Equals
o3 ~> .
}
In any case result.kore seems to contain all conditions, it is kprint that picks what to display. So more concretely I was wondering what is the logic behind selecting what to display in kprint (e.g. why it sometimes shows the condition on ?L and sometimes doesn't)
| 10:47:18 |
| Ali | * Can someone kindly explain the meaning of the output running in the haskel backend. Does it just say the pattern is reachable or not or does it give the conditions for the pattern to be reachable. E.g. for the following
module TEST-SYNTAX
imports ID
syntax X ::= "x"
endmodule
module TEST
imports DOMAINS
imports TEST-SYNTAX
configuration
<k> $PGM:X </k>
<ts> .K </ts>
rule <k> _:X => .K </k>
<ts> _ => ?L:List </ts>
syntax KItem ::= "o1" | "o2" | "o3" | "o4"
rule <k> .K => o1 </k>
<ts> ListItem(10) </ts>
rule <k> .K => o2 </k>
<ts> ListItem(10) </ts>
rule <k> .K => o3 </k>
<ts> ListItem(20) ListItem(30) </ts>
endmodule
if I run krun x --search --pattern "<k> o1 </k>” I get
#TOP
Now if I run krun x --search --pattern "<k> I:KItem </k>” I get
{
I:KItem
#Equals
o3
}
#Or
{
I:KItem
#Equals
o1
}
#Or
{
I:KItem
#Equals
o2
}
And for krun x --search --pattern "<k> I:K </k>” ,
#Not ( {
?L:List
#Equals
ListItem ( 10 )
} )
#And
#Not ( {
?L:List
#Equals
ListItem ( 20 )
ListItem ( 30 )
} )
#And
{
I:K
#Equals
.
}
#Or
{
I:K
#Equals
o1 ~> .
}
#Or
{
I:K
#Equals
o2 ~> .
}
#Or
{
I:K
#Equals
o3 ~> .
}
In any case result.kore seems to contain all conditions, it is kprint that picks what to display. So more concretely I was wondering what is the logic behind selecting what to display in kprint (e.g. why it sometimes shows the condition on ?L and sometimes doesn't).
| 10:51:04 |
| Ali | * Can someone kindly explain the meaning of the output running in the haskel backend. Does it just say the pattern is reachable or not or does it give the conditions for the pattern to be reachable. E.g. for the following
module TEST-SYNTAX
imports ID
syntax X ::= "x"
endmodule
module TEST
imports DOMAINS
imports TEST-SYNTAX
configuration
<k> $PGM:X </k>
<ts> .K </ts>
rule <k> _:X => .K </k>
<ts> _ => ?L:List </ts>
syntax KItem ::= "o1" | "o2" | "o3" | "o4"
rule <k> .K => o1 </k>
<ts> ListItem(10) </ts>
rule <k> .K => o2 </k>
<ts> ListItem(10) </ts>
rule <k> .K => o3 </k>
<ts> ListItem(20) ListItem(30) </ts>
endmodule
if I run krun x --search --pattern "<k> o1 </k>” I get
#TOP
Now if I run krun x --search --pattern "<k> I:KItem </k>” I get
{
I:KItem
#Equals
o3
}
#Or
{
I:KItem
#Equals
o1
}
#Or
{
I:KItem
#Equals
o2
}
And for krun x --search --pattern "<k> I:K </k>” ,
#Not ( {
?L:List
#Equals
ListItem ( 10 )
} )
#And
#Not ( {
?L:List
#Equals
ListItem ( 20 )
ListItem ( 30 )
} )
#And
{
I:K
#Equals
.
}
#Or
{
I:K
#Equals
o1 ~> .
}
#Or
{
I:K
#Equals
o2 ~> .
}
#Or
{
I:K
#Equals
o3 ~> .
}
In any case result.kore seems to contain some conditions, it is kprint that picks what to display. So I was wondering what is the logic behind selecting what to display in kprint (e.g. why it sometimes shows the condition on ?L and sometimes doesn't).
| 11:06:40 |
| 18 Apr 2021 |
| Ali | * Can someone kindly explain the meaning of the output of search running with the haskel backend. Does it just say the pattern is reachable or not or does it give the conditions for the pattern to be reachable. E.g. for the following
module TEST-SYNTAX
imports ID
syntax X ::= "x"
endmodule
module TEST
imports DOMAINS
imports TEST-SYNTAX
configuration
<k> $PGM:X </k>
<ts> .K </ts>
rule <k> _:X => .K </k>
<ts> _ => ?L:List </ts>
syntax KItem ::= "o1" | "o2" | "o3" | "o4"
rule <k> .K => o1 </k>
<ts> ListItem(10) </ts>
rule <k> .K => o2 </k>
<ts> ListItem(10) </ts>
rule <k> .K => o3 </k>
<ts> ListItem(20) ListItem(30) </ts>
endmodule
if I run krun x --search --pattern "<k> o1 </k>” I get
#TOP
Now if I run krun x --search --pattern "<k> I:KItem </k>” I get
{
I:KItem
#Equals
o3
}
#Or
{
I:KItem
#Equals
o1
}
#Or
{
I:KItem
#Equals
o2
}
And for krun x --search --pattern "<k> I:K </k>” ,
#Not ( {
?L:List
#Equals
ListItem ( 10 )
} )
#And
#Not ( {
?L:List
#Equals
ListItem ( 20 )
ListItem ( 30 )
} )
#And
{
I:K
#Equals
.
}
#Or
{
I:K
#Equals
o1 ~> .
}
#Or
{
I:K
#Equals
o2 ~> .
}
#Or
{
I:K
#Equals
o3 ~> .
}
In any case result.kore seems to contain some conditions, it is kprint that picks what to display. So I was wondering what is the logic behind selecting what to display in kprint (e.g. why it sometimes shows the condition on ?L and sometimes doesn't).
| 07:00:32 |
| 19 Apr 2021 |
| Ali | * Can someone kindly explain the meaning of the output of search running with the haskel backend. Does it just say whether the pattern is reachable or not or does it give the conditions for the pattern to be reachable. E.g. for the following
module TEST-SYNTAX
imports ID
syntax X ::= "x"
endmodule
module TEST
imports DOMAINS
imports TEST-SYNTAX
configuration
<k> $PGM:X </k>
<ts> .K </ts>
rule <k> _:X => .K </k>
<ts> _ => ?L:List </ts>
syntax KItem ::= "o1" | "o2" | "o3" | "o4"
rule <k> .K => o1 </k>
<ts> ListItem(10) </ts>
rule <k> .K => o2 </k>
<ts> ListItem(10) </ts>
rule <k> .K => o3 </k>
<ts> ListItem(20) ListItem(30) </ts>
endmodule
if I run krun x --search --pattern "<k> o1 </k>” I get
#TOP
Now if I run krun x --search --pattern "<k> I:KItem </k>” I get
{
I:KItem
#Equals
o3
}
#Or
{
I:KItem
#Equals
o1
}
#Or
{
I:KItem
#Equals
o2
}
And for krun x --search --pattern "<k> I:K </k>” ,
#Not ( {
?L:List
#Equals
ListItem ( 10 )
} )
#And
#Not ( {
?L:List
#Equals
ListItem ( 20 )
ListItem ( 30 )
} )
#And
{
I:K
#Equals
.
}
#Or
{
I:K
#Equals
o1 ~> .
}
#Or
{
I:K
#Equals
o2 ~> .
}
#Or
{
I:K
#Equals
o3 ~> .
}
In any case result.kore seems to contain some conditions, it is kprint that picks what to display. So I was wondering what is the logic behind selecting what to display in kprint (e.g. why it sometimes shows the condition on ?L and sometimes doesn't).
| 07:33:50 |
| Ali | Question: is the following a bug or an expected behavior? :
module TEST-SYNTAX
imports ID
syntax X ::= "x"
endmodule
module TEST
imports DOMAINS
imports TEST-SYNTAX
configuration
<k> $PGM:X </k>
<ts> .K </ts>
syntax A ::= "a1" | "a2" | "a3"
rule <k> _:X => .K </k>
<ts> _ => ?I:A </ts>
syntax O ::= "o1" | "o2" | "o3" | "o4"
rule <k> .K => #check(Ts) </k>
<ts> Ts:A </ts>
syntax O ::= #check(A) [function, functional, smtlib(check)]
rule #check(a1) => o1 [smt-lemma]
rule #check(a2) => o2 [smt-lemma]
rule #check(a3) => o3 [smt-lemma]
endmodule
$ kompile --backend haskell test.k --syntax-module TEST-SYNTAX --main-module TEST
$ krun x —search —pattern “<k> o4 </k>
{
o4
#Equals
#check ( ?I:A )
}
Shouldn’t it give “#Bottom” as output ?
| 11:22:47 |
 rikard.hjort | 5GE6G57G Is it safe to do reverse lookups on maps through matching? As in:
```
k foo(VAL) => KEY ... /k
m ... KEY |-> VAL ... /m | 12:23:37 |
| Ali | * Question: is the following a bug or an expected behavior? :
module TEST-SYNTAX
imports ID
syntax X ::= "x"
endmodule
module TEST
imports DOMAINS
imports TEST-SYNTAX
configuration
<k> $PGM:X </k>
<ts> .K </ts>
syntax A ::= "a1" | "a2" | "a3"
rule <k> _:X => .K </k>
<ts> _ => ?I:A </ts>
syntax O ::= "o1" | "o2" | "o3" | "o4"
rule <k> .K => #check(Ts) </k>
<ts> Ts:A </ts>
syntax O ::= #check(A) [function, functional, smtlib(check)]
rule #check(a1) => o1 [smt-lemma]
rule #check(a2) => o2 [smt-lemma]
rule #check(a3) => o3 [smt-lemma]
endmodule
$ kompile --backend haskell test.k --syntax-module TEST-SYNTAX --main-module TEST
$ krun x —search —pattern “<k> o4 </k>
{
o4
#Equals
#check ( ?I:A )
}
Shouldn’t it give “#Bottom” as output ?
| 12:24:05 |
 dwight.guth | I mean, in theory it's allowed, but you're going to be paying the price for a map choice rather than a deterministic lookup | 14:28:59 |
| dwight.guth | It's much better to just maintain two maps if you need something like that | 14:29:29 |
| rikard.hjort | In this case maintaining two maps would be a big hassle, (we are extending an existing semantics) and the maps won't be all that big. Is the map choice a very slow operation compared to direct lookup? Or is it more like the difference of iterating over the elements in a hashmap vs direct lookup? | 14:49:53 |
| dwight.guth | I mean, two map lookups are 2*log(n), whereas two map choices are n^2 | 14:53:22 |
| dwight.guth | three map lookups are 3*log(n), 3 map choices are n^3 | 14:53:53 |
| dwight.guth | so it's a pretty significant difference if you nest them | 14:53:59 |
| dwight.guth | if you don't nest them, then yeah, it's about what you would expect from iterating through the elements rather than a direct lookup | 14:54:16 |
| dwight.guth | and by "nest" I mean they both appear in the same rule | 14:55:16 |
