K-user mailing list

[Traian Florin Șerbănuță <traian.serbanuta AT info.uaic.ro>]

Hi Robby,

I'm sorry to inform you that we have a (tool) problem with that.
Although in theory both states are reachable, the tool does some
simplifications:
(1) By default in the interpreter all rules are "abstracted" to
structural.  therefore to see nondeterministic behavior you would need
to annotate some rules with transition (informing the tool that they
matter in the transition system).  For example, in your case, you
might want to annotate the and-false rule with 'transition'

However, then we reach another problem:
(2) Currently the beginning of the heating/cooling process (given by
strictness annotations) takes precedence over transitions, not giving
them a chance to apply.

Besides your example, this seems to pose a problem in lazy languages,
too, and has been reported before.  However, the tool development is
guided by feature requests, and we did not have enough requests in
this direction until now.  But it comes at a good time, as we're
redesigning the strictness implementation these days anyway.

As it stands, the only solution I would see, which is not elegant,
would be to write the heating/cooling rules for 'and' manually and
annotate them with transition.




2012/10/3 Patrick Meredith 
<pmeredit AT gmail.com>:
> 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 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
>
>
> _______________________________________________
> k-user mailing list
> k-user AT cs.uiuc.edu
> http://lists.cs.uiuc.edu/mailman/listinfo/k-user
>