K-user mailing list

[Robby Findler <robby AT eecs.northwestern.edu>]

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 I2
>> >>   rule true and B:BExp => B
>> >>   rule false and _ => false
>> >> endmodule
>> >>
>> >>
>> >> and here's the IMP program I run:
>> >>
>> >>    false and (1/0 <= 3)
>> >>
>> >> I would have expected it to produce two out comes ("div0" and false)
>> >> because of the seqstrict annotation on the "and" production in the
>> >> grammar.
>> >> Specifically, I thought I'd get a heating/cooling rule that would apply
>> >> to
>> >> the program above that would move the (1/0 <= 3) expression to the
>> >> front of
>> >> the K cell, and the the 1/0 would move to the front and then I'd get
>> >> the
>> >> div0 result. But instead I get this:
>> >>
>> >> $ ../k/bin/krun --do-search --maude-cmd search x.impSearch results:
>> >>
>> >> Solution 1, state 0:
>> >>
>> >> <k>
>> >>  false
>> >> </k>
>> >>
>> >> I do see that if I remove the short-circuiting 'and' rule that I get
>> >> the
>> >> div0, but I cannot seem to get them both at once.
>> >>
>> >> tia,
>> >> Robby
>> >>
>> >> _______________________________________________
>> >> 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