K-user mailing list

["Rosu, Grigore" <grosu AT illinois.edu>]

I just sent the message below to Robby, but I think that others may also be interested in (one possible way of)

how to manually do heating/cooling in a way to circumvent the tool's current limitation and have direct control over the generated model.

 

One thing I forgot to say in the previous message: the isSort predicates only evaluate to true; they do not evaluate to false, to ensure semantic consistency.  Indeed, you can say it for sure that a computation that parses as Int is an integer, but you never know when it is not an integer (semantically speaking), because you may have forgotten a rule, or your rules are not confluent, etc.  That's why I used the really dirty trick isInt(E) =/=K true.

 

Grigore

----------------

 

Hi Robby,

I hacked a bit and, via some dirty tricks, I made it work with manual heating/cooling rules pretty much in the style of what happens internally in the tool. You may try to use this as a start.

So here is my TRY "language", in file try.k:

module TRY
syntax Exp ::= Int | String | Exp "/" Exp | Exp "&&" Exp | "(" Exp ")" [bracket]
syntax Frozen ::= "[" "]" "&&" Exp | Exp "&&" "[" "]"

rule <k> _:Int / 0 ...</k> => <k> "div0" </k> [div-zero]
rule 0 && _ => 0 [shortcircuit]

// Exp && Exp [strict]
rule E1 && E2 => E1 ~> [] && E2 when isInt(E1) =/=K true [heat]
rule E1 ~> [] && E2 ~> E1 && [] when isInt(E1) [cool]
rule E1 && E2 => E2 ~> E1 && [] when isInt(E2) =/=K true [heat]
rule E2 ~> E1 && [] => E1 && E2 when isInt(E2) [cool]
endmodule

So I introduced explicit syntax for the freezers, with a Frozen syntactic category. You can use K instead of Frozen as well, but I wanted it to look more "syntactic". You should also be able to just add "[]" to Exp, but I have not tried it (you may need to add additional side conditions in the heating rules).

I also tagged all the rules (none of those tags are builtin). Now, if you just kompile it normally,

kompile try

then you will see only one behavior when you execute the program

krun pgm.try --search

where pgm.try is "0 && (0/1)".

However, if you kompile with

kompile try --transition="shortcircuit heat"

you will see two behaviors:

Solution 1, state 1:
<k>
0
</k>
Solution 2, state 2:
<k>
"div0"
</k>

So I did two things above: I make the heating/cooling rules associated to strictness explicit, and I manually fixed the bug that we have in the tool by adding the heating rules to the set of transitions.

Note that using =/=K (different as K terms) is very unsafe and fragile, because it compares the normal forms of the two terms syntactically (so it is NOT semantics equality ---that is undecidable).

I hope this helps as a start.

Ah, one more thing. Since here I know the results of my computations (Int in this case), I did not need to define KResults. The KResult is needed when you declare things strict, because K cannot know by default what the results are.

Grigore

 

 

 

---

From: k-user-bounces AT cs.uiuc.edu [k-user-bounces AT cs.uiuc.edu] on behalf of Robby Findler [robby AT eecs.northwestern.edu]
Sent: Wednesday, October 03, 2012 11:17 AM
To: Patrick Meredith
Cc: k-user AT cs.uiuc.edu
Subject: Re: [K-user] ambiguity & seqstrict

Just to clarify from my side on this issue: I believe the model I've posted is buggy. It should say "strict(1)" in the and production in the grammar, not seqstrict. And, IIUC, K would respond exactly how I'd like it to respond when this is fixed.

The reason I posted this is that in the class I'm running, we came up with this model via suggestions I took from the class. I then expected the buggy model to behave a certain way, but I didn't see that behavior, so I wanted to confirm that my understanding of K was correct. Turns out I was missing something and I now understand what I'm missing and so I can explain this to the class and then we can fix the bug and continue on, building our IMP model (and our understanding of K).

Hope that clarifies.

Robby

On Wednesday, October 3, 2012, Patrick Meredith wrote:

You are definitely right, and don't worry, we often use a hole notation too.

My only thinking here is that we *do* want the ability to write a short circuiting and that will not evaluate that div/0.  The fact that this should be nondeterministic bothers me.  If this gets changed as Traian mentions, it seems that then we would need to write manual heating and cooling rules to make sure that and correctly short circuits.

-Patrick

On Wed, Oct 3, 2012 at 6:22 AM, Robby Findler <robby AT eecs.northwestern.edu> wrote:

What would this mean from the standpoint of the rules that seqstrict
generates? (I understand the seqstrict annotation as a shorthand for
generating rules, but I'm not sure that's right.)

I thought it would generate a rule something like

  A:KResult and B:BExp ~> everythingelse => A ~> (hole and B) ~> everythingelse

(apologies for my bad notation here "(hole and B)" is really something
with a freezer around it and some substitutions and I'm not sure how
to write "everythingelse" properly)

Such a rule should fire!

And indeed, if I just remove the 'and' shortcircuiting rule, then I do
see the heating rule fire.

Robby

On Tue, Oct 2, 2012 at 10:36 PM, Patrick Meredith <pmeredit AT gmail.com> wrote:
> Actually, that is a good point, and I'm not sure.  This is the behavior you
> would normally want, but I'm not sure why it is working.  My best guess is
> that seqstrict always plugs the heated value back in (cool) before it heats
> the second value, deterministically, and that is where it is reducing your
> short circuit (which doesn't care about the sort of the second argument).
> This is what we'd want, so my guess is that is how it works.  I haven't used
> seqstrict in any of my definitions.  Someone more knowledgeable can probably
> confirm if I am correct.
>
> -Patrick
>
> On Oct 2, 2012 10:27 PM, "Robby Findler" <robby AT eecs.northwestern.edu>
> wrote:
>>
>> But why should that preclude the heating/cooling from applying?
>>
>> Robby
>>
>> On Tue, Oct 2, 2012 at 10:26 PM, Patrick Meredith <pmeredit AT gmail.com>
>> wrote:
>> > One definite issue is bool is in your syntax, so false and _ can be
>> > applied
>> > before any heating or cooling ever occurs.
>> >
>> > -Patrick
>> >
>> > On Oct 2, 2012 10:20 PM, "Robby Findler" <robby AT eecs.northwestern.edu>
>> > wrote:
>> >>
>> >> Yes, but the left is already a KResult so the heating (or is it
>> >> cooling?) rule should still fire. No?
>> >>
>> >> Robby
>> >>
>> >> On Tue, Oct 2, 2012 at 10:16 PM, Patrick Meredith <pmeredit AT gmail.com>
>> >> wrote:
>> >> > Hi Robby,
>> >> >
>> >> > Replace seqstrict with strict.  Seqstrict is deterministic
>> >> > sequentially
>> >> > (left to right)
>> >> >
>> >> > -Patrick
>> >> >
>> >> > On Oct 2, 2012 7:12 PM, "Robby Findler" <robby AT eecs.northwestern.edu>
>> >> > wrote:
>> >> >>
>> >> >> Hi all: I'm having trouble understanding a K program's behavior and
>> >> >> I
>> >> >> wondered if I could get some help.
>> >> >>
>> >> >> Here's the program:
>> >> >>
>> >> >> module IMP
>> >> >>   syntax AExp ::= Int
>> >> >>                 | "(" AExp ")"    [bracket]
>> >> >>                 | AExp "/" AExp   [seqstrict, left]
>> >> >>   syntax BExp ::= Bool
>> >> >>                 | "(" BExp ")"    [bracket]
>> >> >>                 | AExp "<=" AExp  [seqstrict]
>> >> >>                 > BExp "and" BExp [seqstrict]
>> >> >>
>> >> >>   syntax KResult ::= Bool | Int
>> >> >>
>> >> >>   rule <k> I1:Int / 0 ...</k> => <k> "div0" </k>
>> >> >>   rule I1:Int <= I2:Int => I1 <=Int

--
-Patrick