K-user mailing list

[Andrei Stefanescu <andreistef AT gmail.com>]

Omar, this is a bug. Thank you for reporting it. I'm looking into it now.

Andrei 

On Fri, Nov 7, 2014 at 12:24 PM, Moore, Brandon Michael <bmmoore AT illinois.edu> wrote:

That looks like a bug, but you can probably work around it with an extra step if you need to.
Something like:

rule <k> iWantChildren => iWantSecondChild ...</k>
       (. => <thread> <tid> !NewId1:Int </tid> </thread>)
rule <k> iWantSecondChild => . ...</k>
       (. => <thread> <tid> !NewId2:Int </tid> </thread>)

that does take a second step, maybe opens up unwanted interleavings, etc.,
but hopefully it will get your definition going again.

Brandon

---

From: k-user-bounces AT cs.uiuc.edu [k-user-bounces AT cs.uiuc.edu] on behalf of Omar Duhaiby [3omarz AT gmail.com]
Sent: Thursday, November 06, 2014 3:55 AM
To: k-user AT cs.uiuc.edu
Cc: Traian Șerbănuță; Musab A. AlTurki; Dwight Guth
Subject: [K-user] multiple fresh Ints in one rule

I didn't have a problem in the older version using the fresh function, but now using '!' like the following example gives the same value twice:

rule <k> iWantChildren </k>

(. => <thread> <tid> !NewId1:Int </tid> </thread>
        <thread> <tid> !NewId2:Int </tid> </thread>
)

this makes two threads with the same value. How should I do it?

Thank you

Omar Alzuhaibi

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