K-user mailing list

[Traian Florin Şerbănuţă <traian.serbanuta AT gmail.com>]

Hi Soha,

I was reluctant to attempt answering this question, as I am no longer up-to-date with the latest developments in K.

The distinctCounter,  defined in the COUNTER-HOOKS module (in include/builtins/counter.k), is something arising from the implementation of K in Maude, which was  meant  as a  way to achieve fresh symbolic variables generation.

A particularity of Maude made it such that all distinct counters with the same argument *within a rule* would evaluate to the same value, which would be distinct from the value of other occurences of distinctCounter with different arguments *within the same rule*.

Hence, there is only one global counter addressed by this #distinctCounter, not multiple ones, and relying on it giving numbers in a sequence is not very advisable (in my opinion).

Nevertheless, if you want to access this global counter *at most once per rule* it would be better to do it through the #counter functional constant also defined in the COUNTER-HOOKS module.

But if you need two instances of the same counter *in the same rule* (with different valuse), then use #distinctCounter with diferent arguments for each instance you need.

this probably does not help much with your original question, but I have no easy answers in that direction, except maybe that you should reconsider your problem and find a different solution.

best wishes,

Traian

2015-01-21 9:15 GMT+02:00 Dorel Lucanu <dlucanu AT info.uaic.ro>:

Dear Soha,


sorry for not replying up to now, I was very busy.
I think Traian is the best who vam answer your questions, therefore I added him to the cc list.
If I correctly remember, he implemented that function.
From my experience, you may have only one counter, so there is no difference between  #distinctCounter(0) and #distinctCounter(1) (I remember that I did some experiments and the result was always the  same).

Best wishes,
Dorel

On 18/01/15 13:42, soha hussein wrote:

Hello Dorel,

I have been looking into the Counter module in K you've referred to, I also to a look at its interface in maude and I played with it a program but the output made me more confused. I would appreciate it if you give me some lights on:

1. what does distinctCounter(Int) do? what is the difference between #distinctCounter(0), #distinctCounter(1), #distinctCounter(#counter)?

2. #counter displays the last value of the counter, is this correct?

3. how to 

a) initialize the counter, 

b) increment it and 

c) reset it?

Thank you

Soha

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

Alright, thanks Dorel for everything.

Soha

On Jan 15, 2015, at 2:52 PM, Dorel Lucanu <dlucanu AT info.uaic.ro> wrote:

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

The definition does not mean anything, it is just there to test that functions attributed as functions applies anywhere regardless they are wrapped inside a k cell or not. Which is not the case, the function loses this ability of matching anywhere once you put it in a k cell. Is this a bug or is there a logic behind that, and any advises on ways to work around it.

As I said in a previous message, the functions cannot be matched because always the must return a value. The name of a function is not constructor of terms.
Dorel

I have completely defined my language and i have been maintaing it for a year now on k. It will be very hard and late to switch to some other tool.  Like i mentioned, the k-nightly version  3.4 behaves exactly the same.

Thanks for all the help

Soha

On Jan 15, 2015, at 2:32 PM, Dorel Lucanu <dlucanu AT info.uaic.ro> wrote:

You are right, the function rules should be applied anywhere.
Sorry, I didn't understand exactly what you want from your definition.
Dorel

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

Dorel, please bear with me, i am trying to understand. I should not be writing strictness, because I have provided attribute [function] which should match wherever. Moreover writing this (attached) reduces.

It has no strictness attributes, however it reduces. The only difference is that it is not wrapped inside a K. 

I can understand this, but not the one in the previous email. Because it is defined as a function, and therefore it ensures that all places (no matter where they are) matches. Somehow this definition does not work if i write a function rule wrapped in a K cell. The function loses its ability of matching wherever and it only matches the top computation inside K. Why is this happening. 

Soha

<Mail Attachment.png>

On Jan 15, 2015, at 1:58 PM, Dorel Lucanu <dlucanu AT info.uaic.ro> wrote:

That is a different problem. You have to declare the operator "+" strict in order to reduce its operands to values:

syntax Exp ::= "fn""(" ")" [function]
| "start"
| Exp "+" Exp [strict]
| Int

The rule
<k>… fn() => 2 </k>
<c>C:Int => C +Int 1<c>
cannot be applied because you have just one KItem element in the k cell: 1 + fn()

With strict attribute, you should obtain something like that

<k> 1 + fn() </k>

<c> 0 <c>
=>

<k>fn() ~> 1 + HOLE </k>

<c> 0 <c>
=

<k>2 ~> 1 + HOLE </k>

<c> 0 <c>
=>

<k>1 + 2 </k>

<c> 0 <c>
=>

<k>3 </k>

<c> 0 <c>

  Dorel

On 15/01/15 12:44, soha hussein wrote:

On Jan 15, 2015, at 1:11 PM, Dorel Lucanu <dlucanu AT info.uaic.ro> wrote:

On 15/01/15 09:47, soha hussein wrote:

Hi Dorel,

I crafted something for the purpose of our discussion. Below I defined fn() as a function. what you would expect with such a definition is that it is going to be applied anywhere it is found in a k cell (notice that the addition has no strictness attributes). However below if you kompile and krun it does not evaluate 1 + fn()

But if you removed the enclosed k cell, say you write the function rule as 

rule fn() => 2 ,

then the _expression_ 1 + fn() is reduced. 

My problem is that exactly that, I want to be able to write a function and access the counter cell c, and therefore the first formate of writing the function rule as 

<k>… fn() => 2 </k>

<c>C:Int => C +Int 1<c>

A function call is supposed to instantaneously reduce to a legal term, in your case a term of sort Exp. Therefore a term like "fn()" cannot never be matched.

the above rule should reduce fn() to 2 which is Int which is in turn  a sub sort of Exp, so the term should be legal.

is what i want, but it isn't working in k. My question is how to make it work. What is it that i'm doing/expecting wrong!?

module TEST

syntax Exp ::= "fn""(" ")" [function]

| "start"

| Exp "+" Exp

| Int

configuration<k>start</k> 

<c>0</c> 

rule <k>start => (1 + fn()) ...</k>

<c>C:Int => 0</c>

After the above rule is applied, the content of the cel k will be 1 + 2, because fn() is instantaneously reduced to 2.

No, this is not what happens it does not reduce. After running the above i get the following "1+fn()" in the k cell. I am attaching a screenshot of what is happening. Also, i installed the k-nightly version and ran the same program, same thing happened the k cell does not reduce 1+ fn().

rule <k>...fn() => 2 ... </k>

<c>C:Int => (C +Int 1)</c>

  

rule V1:Int + V2:Int => V1 +Int V2

endmodule

There is only one counter in K (see builtins/counter.k) that generates the non-zero natural numbers.
Here is an example how it can be used:

module TEST
 
  syntax Pgm ::= "st1" | "st2"

  syntax Int ::= "f" "(" ")" [function]

  rule f() => #counter

  rule st1 => st2 ~> f()  // f() is reduced to 1
  rule st2 => f() +Int f()   // f() is reduced to 2
 
  configuration
    <k> st1  </k>

endmodule

Dorel

<Mail Attachment.png>

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

On 14/01/15 11:19, soha hussein wrote:

I think the key of what you have done is that you have another K cell for the counter. But why do you need that for ?

Just to simulate the function on counters.
May be the solution I sent is too complicated. I think that you may have just one cell

<counters> .Map </counters>

(or <globals> .Map </globals>, if you prefer), where a counter (global variable) is written as "cntrA -> val", and add your needed functions over maps.
For instance, you may write
//  reading and incrementing cntrA
  rule <k> stmt1 => .K ...</k>
       <out> .List => ListItem(val(cntrA, CNTRS)) ...</out>
      <counters> CNTRS => inc(cntrA, CNTRS) </counters>

Dorel

Soha 

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

With the version you work with, the only solution to your problem I see now is to define the counters as subconfigurations.
Here is an example (it should be self-explained, if you have questions don't hesitate to ask):

====
module TEST
 
  syntax Pgm ::=  "stmt1" | "stmt2" | "stmt3" | "createCounter"

  syntax CounterName ::= "cntrA"   // for counters name
  syntax CounterCmd ::= "inc" | "reset"  // commands for counters

// create a counter
  rule <k> createCounter => .K ...</k>
      (.Bag
        =>
       <cntr>
         <name> cntrA </name>
         <cmd> .K </cmd>
         <val> 0 </val>
       </cntr>)


//  reading cntrA
  rule <k> stmt1 => .K ...</k>
       <out> .List => ListItem(V) ...</out>
      <name> cntrA </name>
      <val> V:Int </val>

//  incrementing cntrA as a side-effect
  rule <k> stmt2 => .K ...</k>
      <name> cntrA </name>
      <cmd> .K => inc </cmd>

//  reseting cntrA as a side-effect
  rule <k> stmt3 => .K ...</k>
      <name> cntrA </name>
      <cmd> .K => reset </cmd>




// operations with counters (simulating the function handling the counter)

  rule <cmd> inc => .K </cmd>
       <val> V:Int => V +Int 1 </val>
    [anywhere]

  rule <cmd> reset => .K </cmd>
       <val> V:Int => 0 </val>
    [anywhere]


  configuration
    <k> createCounter ~> stmt1 ~> stmt2 ~> stmt1 ~> stmt3 ~> stmt1 </k>
    <out> .List </out>
    <counters>
      <cntr multiplicity="*"> 
        <name> cntrA </name>
        <cmd> .K </cmd>
        <val> 0 </val>
      </cntr>
    </counters>


endmodule

and the output is like this:

$ krun
<k>
    .K
</k>
<out>
    ListItem(0)
    ListItem(1)
    ListItem(0)
</out>
<counters>
    <cntr>
        <val>
            0
        </val>
        <name>
            cntrA
        </name>
        <cmd>
            .K
        </cmd>
    </cntr>
</counters>

=====

Note that using "counter" as cell name, it may cause some ambiguities.

The solution is not the most elegant, but I hope it could solve your problem.

Dorel

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

I am not using the k-nightly version, i am using version 3.0. I remember trying to upgrade to the nightly version but my used-to-run-and-compile code raised exceptions in the nightly version. So I restored the older version of K. 

I do know about fresh but what I know from trying it out is that I does not generate numbers in sequence, and in my case i want a counter that would generate from 1 to 10 and to be able to reset it and reuse it. 

I am stuck, i also tried randomRandom(Int), it is generating large random numbers. Any other suggestions?

Soha

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

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