K-user mailing list

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

So, thinking about this a little bit: would you say that this is a place that errors can creep into the specification? That is, say I don't recognize that there is this ambiguous choice in my semantics. And, on most days, there isn't one; I get the one behavior that I was expecting and the other choice doesn't show up because krun/kompile somehow avoid it. Then one day, either krun or kompile decides it likes the other choice and now my semantics behaves differently, perhaps well after it has been deployed or whatever.

With my K hat on (not that I'm sure I get wear such a hat :), I guess that the right answer to such a problem is tool suport. That is, some kind of a tool where I could specify the shape of valid configurations (perhaps just the configuration declaration, but I guess there are also context sensitive constraints that can go into this too) and then it would search for ones that have multiple transitions?

Robby

On Wednesday, October 3, 2012, Rosu, Grigore wrote:

I expected this answer ...  We already had 3 requests by now to give heating/cooling the same priority as the other rules, so it is time to fix it.  We are now in the middle of a transition of the kompiler to Java; as we do it, let's also try to fix this issue.

Thanks Robby!  However, there is one thing, related to the first problem that Traian mentioned, which I would like to elaborate a bit, because you may not be familiar with it and may come up soon in your class.  By default, kompile optimizes for execution performance, not for exhaustive model analysis.  In other words, if you have this trivial choice definition:

module IMP
  syntax S ::= Int | S "|" S

  rule I | _ => I
  rule _ | I => I
endmodule

and do

kompile imp
krun p.imp --search    (where p.imp contains 3|7)

then you will still only get one solution.

kompile and krun are disconnected, and what happened above is that kompile did not put enough information in the generated language model for krun to find all behaviors.

To tell kompile that you really want the two rules to generate transitions, then you need to use its option "--transition", which typically means that you should also tag the rules; something like this:

module IMP
  syntax S ::= Int | S "|" S

  rule I | _ => I  [first]
  rule _ | I => I  [second]
endmodule

and do

kompile imp --transition="first second"
krun p.imp --search

Now you should see both solutions.

Rules can also have the same tag; for example, you can replace both "first" and "second" with "choice".  You can also use the tag "transition", in which case you do not even have to give kompile the option anymore, but I personally do not encourage this last thing, because (1) it may give people the wrong idea that "transition" is part of the semantics, instead of a kompilation directive; and (2) it will always generate a slower model, whether you really need the transitions or not.

I hope this helps a bit until we fix the other issue.

K was always driven by user requests and by performance.

Thanks,
Grigore



________________________________________
From: k-user-bounces AT cs.uiuc.edu [k-user-bounces AT cs.uiuc.edu] on behalf of Traian Florin Șerbănuță [traian.serbanuta AT info.uaic.ro]
Sent: Wednesday, October 03, 2012 12:48 AM
To: Patrick Meredith
Cc: k-user AT cs.uiuc.edu
Subject: Re: [K-user] ambiguity & seqstrict

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
>> >