K-user mailing list

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

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