K-user mailing list

[samira kherfellah <samira.kherfellah AT gmail.com>]

Hi All;

I have a small problem when handling boolean varibles in k.

 

I have the following rules:

 

rule <k> provided E:Exp ; nextstate S:Id ; =>  nextstate S ; ...</k> when E = true

 

rule <k> provided E:Exp ; nextstate S:Id ; =>  .  ...</k> when E = false

 

but at the execution of an example, it never pass in the next state, it hangs in the current state.

 

If, for example we have:

 

process A (1) ;

 

state idle #start ;

 

task i:= i +2 ;

nextstate wait;

 

endstate;

 

 

state wait ;

 

provided i < 0;

nextstate ab;

 

provided i > 0;

nextstate cd;

 

endstate

 

state ab ;

...

endstate;

 

state cd ;

....

endstate;

 

endprocess;

 

 

The writing of the rules is correct? it should add something else to evaluate E?

 

 

Thank you all.
Samira