Skip to Content.
Sympa Menu

k-user - Re: [K-user] [k-list] matching entire configuration while also matching its components

k-user AT lists.cs.illinois.edu

Subject: K-user mailing list

List archive

Re: [K-user] [k-list] matching entire configuration while also matching its components


Chronological Thread 
  • From: "Rosu, Grigore" <grosu AT illinois.edu>
  • To: "Moore, Brandon Michael" <bmmoore AT illinois.edu>, Daniele Filaretti <dfilaretti AT gmail.com>, "k-user AT cs.uiuc.edu" <k-user AT cs.uiuc.edu>
  • Cc: "k-list AT cs.illinois.edu" <k-list AT cs.illinois.edu>
  • Subject: Re: [K-user] [k-list] matching entire configuration while also matching its components
  • Date: Wed, 9 Jul 2014 12:59:24 +0000
  • Accept-language: en-US
  • List-archive: <http://lists.cs.uiuc.edu/pipermail/k-user/>
  • List-id: <k-user.cs.uiuc.edu>

Sorry, I said that your rule would be

rule [assign-create]:
<k> X = I:Int; => . ... </k>
<env> M:Map => M[?L/X] </env>
<store> ... . => ?L |-> I ... </store>
<nextAddr> I:Int => I +Int 1 </nextAddr>)
requires notBool (X in keys(M)) andBool ?L = alloc()

which is incorrect. It would be

rule [assign-create]:
<k> X = I:Int; => . ... </k>
<env> M:Map => M[?L/X] </env>
<store> ... . => ?L |-> I ... </store>
<nextAddr> I:Int => I +Int 1 </nextAddr>)
requires notBool (X in keys(M))
ensures ?L = alloc()

Grigore



________________________________________
From:
k-list-bounces AT cs.uiuc.edu

[k-list-bounces AT cs.uiuc.edu]
on behalf of Rosu, Grigore
[grosu AT illinois.edu]
Sent: Wednesday, July 09, 2014 7:33 AM
To: Moore, Brandon Michael; Daniele Filaretti;
k-user AT cs.uiuc.edu
Cc:
k-list AT cs.illinois.edu
Subject: Re: [k-list] [K-user] matching entire configuration while also
matching its components

Brandon is right, that is an acceptable solution for now.

However, we, the K developers, should do what we discussed for a long time to
do, namely to allow functions to have access to the entire state. We will
take this task seriously over the next few weeks, and hopefully the next
release of K will include it. Here is how your example rule will look like
then:

rule [assign-create]:
<k> X = I:Int; => . ... </k>
<env> M:Map => M[?L/X] </env>
<store> ... . => ?L |-> I ... </store>
<nextAddr> I:Int => I +Int 1 </nextAddr>)
requires notBool (X in keys(M)) andBool ?L = alloc()

?L means that it is an existentially quantified "fresh" variable in the RHS
of the rule, which is further constrained by the equality ?L = alloc(). You
do not want to write alloc() twice in the RHS, because you may not want to
propagate the side-effects of the function alloc() on the state twice. For
example, alloc() can be defined something like this:

rule alloc() => "L" +String int2string(N)
<nextLoc> N => N +Int 1 </nextLoc>

Would this be acceptable?

Grigore



________________________________________
From:
k-user-bounces AT cs.uiuc.edu

[k-user-bounces AT cs.uiuc.edu]
on behalf of Moore, Brandon Michael
[bmmoore AT illinois.edu]
Sent: Tuesday, July 08, 2014 11:15 AM
To: Daniele Filaretti;
k-user AT cs.uiuc.edu
Subject: Re: [K-user] matching entire configuration while also matching its
components

I don't know of any easy way to grab everything like that. I think you just
have to explicitly name the "rest" of every cell, and put it together
yourself.

Cutting down to one call to alloc would help, if you need to explicitly
assemble the state yourself.
You can define a new kind of item to put in the K cell to hold and use the
result, like this:

rule [assign-create]:
<k> X = V:Int; => do_alloc(X

alloc(Bag(<k>KRest</k><env>M</env><store>S</store><nextAttr>I</nextAddr>),V)
KRest </k>
<env>M</env>
<store>S</store>
<nextAddr>I</nextAddr>
when notBool (X in keys(M))

(I changed "I" to "V" in the assignment, assuming you didn't mean the rule to
apply only when you were asigning a value that happened to match nextAddr).

then you give do_alloc semantics with a rule like
rule [do-alloc]:
<k> do_alloc(X,Loc,V) => . ...</k>
<env>M => M[Loc/X]</env>
<store>... . => Loc |-> V ...</store>
<nextAddr> I => I+Int 1 </nextAddr>

We've thought a little bit about whether there is some way to give rules
read-only access to the whole configuration (or maybe cell completion style
access to cells near the call?), but don't have any concrete design or plans
for it.
Maybe you could say a little more about how your alloc works, and which
information it needs.

Brandon
________________________________________
From:
k-user-bounces AT cs.uiuc.edu

[k-user-bounces AT cs.uiuc.edu]
on behalf of Daniele Filaretti
[dfilaretti AT gmail.com]
Sent: Tuesday, July 08, 2014 10:30 AM
To:
k-user AT cs.uiuc.edu
Subject: [K-user] matching entire configuration while also matching its
components

Hi All,
little technical question, in an IMP++ setting (actually only IMP, but with
environment + store).

The following is a variable assignment rule that, in case the variable
doesn’t exists, it creates it. In order to do this, it does the standard
things - adding an entry in the environment and in the store, using a fresh
allocated address.

However, I’m not using K’s builtin “fresh” predicate but I’d like to use my
own allocation function “alloc” which takes the whole configuration as an
input:

rule [assign-create]:
<k> X = I:Int; => . ... </k>
<env> M:Map => M[alloc(State)/X] </env>
<store> ... . => alloc(State) |-> I ... </store>
<nextAddr> I:Int => I +Int 1 </nextAddr>)
when notBool (X in keys(M))

As you can see, I use “alloc(State)”, where I would like “State” to match the
entire configuration. Is that even possible?
I’ve tried with

rule [assign-create]:
State:Bag(
<k> X = I:Int; => . ... </k>
<env> M:Map => M[alloc(State)/X] </env>
<store> ... . => alloc(State) |-> I ... </store>
<nextAddr> I:Int => I +Int 1 </nextAddr>)
)
when notBool (X in keys(M))

but in this case “State” matches the empty bag (I guess) as it’s parsed as
(Config1 Config2). Is there a way to match entire configuration (simply “give
it a name”) and at the same time, match part of its content - all in one rule?

Thank you very much!

Regards,

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

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

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





Archive powered by MHonArc 2.6.16.

Top of Page