K-user mailing list

[朱晓冉 <zhuxrsandra AT 163.com>]

Hi, 

I define a function with type of Int in K, the code just like this:  

syntax Int ::= "count" "(" Bag ")"     [function]

But it seems that the the data returned by this function is not Int. Because when I write the LTL rule  (rule B:Bag |=Ltl countvalue(I)=>true  when (count(B) ==Int count(B)) [ltl, anywhere]), the running result shows that my input property is false. However, if the rule is changed into  rule B:Bag |=Ltl countvalue(I)=>true  when (count(B) ==K count(B)) [ltl, anywhere], the running result is true.

So does the return type of function  count(B) is Int? How can I do comparison between count(B) and a parameter with type Int.

By the way, the version of K framework that I'm using is K 3.5.

Thanks,

Sincerely,

Xiaoran Zhu