K-user mailing list

[Dorel Lucanu <dlucanu AT info.uaic.ro>]

On 13/01/15 13:22, soha hussein wrote:

Hi Dorel,

I am not sure I understand what you are proposing. 

1. what does !A mean? and where is it defined? I actually tried to compile your code and it didn't pass, the compiler did not recognize ! symbol.

What version of K do you use?
In the latest version of K (k-nightly) ! is used for fresh variables.
In the previous versions of K,  we used
  rule start => A:Counter
    requires fresh(A:Counter)
But, in that case, the output is a bit different.

2. in  syntax Counter ::= myCounter(Int)    [freshGenerator, function] 

did you mean it as

  syntax Counter ::= "myCounter" "("Int")"  [freshGenerator, function]  ? if not then where is myCounter(Int) defined?

Yes, the two definitions of "myCounter" are equivalent. "Counter" and "myCounter" are just two examples of sort and function, respectively.

3. when you executed the module you didn't provide a program on which the definition is going to run? In other words what does CounterA(2) and Counter(1) results from?

You have to provide a program name for krun only if the specification of the configuration include $PGM variable, in that case the AST obtained by parsing the program replace the name of this variable. In that case, "krun prog-name" is similar to "krun -c PGM=prog-name".

4. where is the place where the counter gets incremented? 

This is done automatically by the K tool.

Dorel

Soha

On Jan 13, 2015, at 12:05 PM, Dorel Lucanu <dlucanu AT info.uaic.ro> wrote:

Hi Soha,

Here is a solution I use to generate fresh symbolic variables:

module TEST
 
  syntax Counter ::= "CounterA" "(" Int ")" | "start" | Counter Counter [left]
  syntax Counter ::= myCounter(Int)    [freshGenerator, function]
  rule myCounter(I) => CounterA(I)

  configuration <k> start </k>

  rule start => !A:Counter
  rule CounterA(1) => !A:Counter CounterA(1)
endmodule

The output of the execution of the above module is:

$ kompile test.k
$ krun
<k>
    CounterA ( 2 ) CounterA ( 1 )
</k>

Regarding the random function, here is an extract from a message that circulated some time ago un k-user list:

Check the random.k module in /include/modules/builtins

If I remember correctly, randomRandom(I)  generates the ith random number in the sequence.

best wishes,

Traian

2014-05-18 22:32 GMT+03:00 Omar Duhaiby <3omarz AT gmail.com>:
Does K have a random number generator? How can I simulate random behavior?

I hope that this help you.

Dorel


Dorels-MacBook-Pro:test dlucanu$

On 13/01/15 07:08, soha hussein wrote:

Any Ideas? replies?


Thanks

Soha

On Jan 12, 2015, at 12:12 PM, soha hussein <husseinsoh AT gmail.com> wrote:

Just to clarify the last question, i mean Can I call a K definition, that is complete (contains, its definition, KResults, rules) from another K definition? I know that we can include one definition into another, but I do not want that, because in my case both definitions have contradicting terminals, KResults. So somehow I want them to operate disjointly without having the same terminals.


Soha


On Jan 12, 2015, at 11:50 AM, soha hussein <husseinsoh AT gmail.com> wrote:

Hello, 

I have a problem and I am wondering if you can help me. What i want to do is actually very simple. I want a global variable (counter) and a function (Exp -> Exp) that checks the counter and update its value accordingly. 

What I have done is I created the counter in a new cell <c>C:Int<c>, but then writing a function rule like:

rule <k> f(C) => E:Exp </k>
	<c>C:Int => C +Int 1</c>


does not work, because K will match it when f is on top of the computation, which I do not want, i want it to apply wherever it exists.


I tried another way, I changed the function into a new internal _expression_ construct, but then I had a problem of defining the KResult; since the f: Exp -> Exp then KResult will include Exp, but then computation on Exp will stop since it is in the Exp.


I am looping in the same issue over and over, I have another way to do it, but it is so complicated for the purpose I want it. 


So my questions are:

1. Can anybody tell me how to create a global counter and have it accessible through other functions? 
2. Are there other ways of defining a global variable?
3. Is there a built in counter, like fresh or random?
4. Are there any other way of defining terminals other than including them in KResult?
5. Can I call a K program from another? How?



Thanks

Soha

_______________________________________________
k-user mailing list
k-user AT cs.uiuc.edu
http://lists.cs.uiuc.edu/mailman/listinfo/k-user