k-user AT lists.cs.illinois.edu

Subject: K-user mailing list

List archive

[K-user] How to check if all threads have finished execution

From: Omar Duhaiby <3omarz AT gmail.com>
To: "k-user AT cs.uiuc.edu" <k-user AT cs.uiuc.edu>
Subject: [K-user] How to check if all threads have finished execution
Date: Thu, 16 Oct 2014 10:59:29 +0300
List-archive: <http://lists.cs.uiuc.edu/pipermail/k-user/>
List-id: <k-user.cs.uiuc.edu>

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] How to check if all threads have finished execution, Omar Duhaiby, 10/16/2014
- Re: [K-user] How to check if all threads have finished execution, Traian Florin Şerbănuţă, 10/16/2014
  - Re: [K-user] How to check if all threads have finished execution, Omar Duhaiby, 10/16/2014
    - Re: [K-user] How to check if all threads have finished execution, Traian Florin Şerbănuţă, 10/16/2014