K-user mailing list

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

Absolutely.

Robby

On Wed, Oct 3, 2012 at 10:00 AM, Rosu, Grigore 
<grosu AT illinois.edu>
 wrote:
> Yes and Yes.
>
>
>
> Note, however, that it is quite tricky to know when you have and when you
> don't have an ambiguous choice in a semantics, so I do not expect any tool
> to do magic in all situations.  For example,  an ambiguous + is innocent
> until you allow side effects in expressions.  Similarly, an agent-based
> distributed language may be non-ambiguous until you add a construct which
> allows an agent access to its name as a string; then the particular order in
> which agents are created and given their unique names by the name-server
> starts to matter.
>
>
>
> Grigore
>
>
> ________________________________
> From: 
> robby.findler AT gmail.com
>  
> [robby.findler AT gmail.com]
>  on behalf of Robby
> Findler 
> [robby AT eecs.northwestern.edu]
> Sent: Wednesday, October 03, 2012 9:30 AM
> To: Rosu, Grigore
> Cc: Traian Florin Șerbănuță; Patrick Meredith; 
> k-user AT cs.uiuc.edu
> Subject: Re: ambiguity & seqstrict
>
> 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
>> >> >