K-user mailing list

[Stefan Ciobaca <stefan.ciobaca AT gmail.com>]

How did you define the "=" in "E = true"? Did you mean to use "==Bool"?

Stefan

On Mon, Jul 22, 2013 at 5:53 PM, samira kherfellah
<samira.kherfellah AT gmail.com>
 wrote:
> 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
>
> _______________________________________________
> k-user mailing list
> k-user AT cs.uiuc.edu
> http://lists.cs.uiuc.edu/mailman/listinfo/k-user
>