K-user mailing list

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

I'm not very sure what "first K" you are referring to, so I'll give a more complete answer:

the .K in the first rule has a dot in front of K and represents/ matches the empty computation.

The K on the left of => in the second rule matches the entire computation.  Actually you can do whatever you want there:  you can choose to match and transform only the first item in the computation (if you put ... at the end of the k cell), or you can transform the entire computation as I did, but you don't even need to match the <k> cell at all (maybe you need to trigger a reaction somewhere else, based on information which could be contained in other cells in the <thread> cell).

best wishes,

Traian

2014-10-16 12:25 GMT+03:00 Omar Duhaiby <3omarz AT gmail.com>:

Yes, you are right. I should erase such threads. But I have a question about your example rule. Is the first 'K' equivalent to '_:K'? What does it match?

Thank you

On Thu, Oct 16, 2014 at 11:48 AM, Traian Florin Şerbănuţă <traian.serbanuta AT fmi.unibuc.ro> wrote:

What one usually does (see, e.g., SIMPLE) is to erase threads which have nothing in their <k> cell, with rules like

rule <thread>...

  <k> .K </k>

...</thread> => .

This keeps the thread space clean and also makes rewriting faster.  If doing so, then you can check whether there is only one thread left by matching only one thread in the threads cell (it is always good to group similar cells like thread into a single cell, like threads).

rule <threads> <thread>... <k> K => enter_single_mode(K) </k> ...</thread> </threads>

Hope this helps,

Traian

2014-10-16 10:59 GMT+03:00 Omar Duhaiby <3omarz AT gmail.com>:

Hello,

I have one thread that is always active. The problem is that the program will not halt as long as that thread is active. It is a counter of transitions made during execution. My question is:

1- Is there a better way to count the number of transitions of a certain thread or the whole program?

2- How do I check if all other threads have nothing in their k cells? because '_' includes '.'

    I tried doing this:

    rule (some rewrite)

        <thread>...
          <k> Code:K </k>
        ...</thread>
    when Code =/=K .K

I really don't know what I'm doing here. I was just trying my luck. The idea is that this rule should only work if there is at least one thread that has something in its k cell. Question: will this match against the thread that I'm rewriting?
If all fails, I can always make a new cell to act as a flag, call it "isActive". Any ideas?

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