K-user mailing list

["Park, Daejun" <dpark69 AT illinois.edu>]

Hi Xiaoran,

It might be the case that count is a partial function, and count(B) remains as a unresolved term instead of an integer value. In this case, `count(B) ==K count(B)` becomes true, because ==K checks the structural equality, while ==Int makes no sense.

Could you double-check if count(B) is a total function, being evaluated to an integer value?

Best,

Daejun

On Dec 7, 2015, at 8:41 AM, 朱晓冉 <zhuxrsandra AT 163.com> wrote:

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 resu lt 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