K-user mailing list

["Moore, Brandon Michael" <bmmoore AT illinois.edu>]

Variables work fine. Running this program you can see that i becomes 10 (= 0 + 10).

system example;
process K1(1);
var i integer;
state idle #start ;
        task i := i + 10;
        stop ;
endstate;
endprocess;
endsystem;

You can see in the final configuration that execution gets stuck with code starting
#start ; ....

Your rule
rule  <states>... S |-> #start ;  R:TransitionItem T:Transition   ...</states>
     <k> . => R T </k>
     <state>  _ => S  </state> //[transition]
removes the option when first going to the start state, but the rule for nextstate leaves a term including the options in the <k> cell:

rule <k> nextstate St:Id ; => Bla ...</k>
     <states>... St |-> Bla ...</states>
   <state> _ => St </state> //[transition]

If you change
state idle; #start;

into
state start #start; nextstate idle; endstate;
state idle;

in each process, you'll see execution gets much farther, and finished with i |-> 101.

You also have something leaving a lot of trailing items like
.List{""} ~> .List{""} ~> .List{""} ~> .List{""} ~>
                  .List{""} ~> (provided (j > 100) ;) (nextstate end ;) ~> ...
in the K cell.
It looks like the rule for nextstate doesn't drop the remaining commands in the current state.

Brandon

---

From: samira kherfellah [samira.kherfellah AT gmail.com]
Sent: Friday, August 30, 2013 12:05 PM
To: Moore, Brandon Michael
Subject: Re: [K-user] Variable declaration

Thank you for your answer.

I think I have a little problem with this declaration of variables. The problem is that the variables take only two values 0 and 1 and do not take other values. 

Here is an example "ex3.if"

Provided with i should normally have the values 0, 1, 2, 3 , 4, ... and it is the same thing for j, but at the compilation, i takes only the values 0 and 1.

ex3.if is an example.

if.k is a program K.

Thank you very much for your help.

Samira.

2013/8/30 Moore, Brandon Michael <bmmoore AT illinois.edu>

Hi Samira.

I haven't tested it, but that looks reasonable. Are you having any problems with it?

Brandon

---

From: k-user-bounces AT cs.uiuc.edu [k-user-bounces AT cs.uiuc.edu] on behalf of samira kherfellah [samira.kherfellah AT gmail.com]
Sent: Friday, August 30, 2013 10:58 AM
To: k-user AT cs.uiuc.edu
Subject: [K-user] Variable declaration

Hi All,

I have a question about declaring variables in K. 

Here is an example of using variables in my language

var i integer ;

...

task i := i+1; 

...

The variables must be initialized to 0, the rules are defined as follows:

rule <k> var X:Id TV:Type ;  => . ...</k> 

      <tenv>... . => X |-> TV ...</tenv> 

      <store>... . => X |-> 0 ...</store> 

// lookup

rule <k> X:Id => V ...</k>

<store>... X |-> V ...</store> 

rule <k>  task X:Id := I:Int ; => . ...</k> 

<store>... X |-> (_=> I) ...</store> 

<tenv>... X |-> integer ...</tenv>

this way is it correct or there is something else to add? how to initialize variables to 0?

Thanks.

Samira.