K-user mailing list

[Omar Duhaiby <3omarz AT gmail.com>]

Thanks for the workaround. But I think I did something better. I didn't split the rule into two. I just replaced the contents of the K cell of the second thread with a special function that I defined:
    syntax K ::= getNewId(K) [function]
    rule
        <k> getNewId(E) => E </k>
        <tid> _ => !NewId:Int </tid>
    [structural]

On Fri, Nov 7, 2014 at 9:41 PM, Andrei Stefanescu <andreistef AT gmail.com> wrote:

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