K-user mailing list

[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