K-user mailing list

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

We're planning to add owise to function declarations for now,  but it
will probably take a while until we add it to all rules in their full
generality.

One problem with it is that while [owise] is perfectly fine in a
functional context with no side effects, it is not that ok when you
have non-determinism, and it's semantics usually requires a global
predicate on configurations.

But let's bring back this subject in our meetings and see what comes out of 
it.

BTW Ulrich, I'm coming to Bremen next week from Monday to Wednesday to
attend and present at ICGT'12.  It seems I'll be giving a short
tutorial on K, too.   If you want to meet in person and talk about K,
please let me know :-)

best wishes,
- traian

2012/9/20 David Lazar 
<lazar6 AT illinois.edu>:
> On Wed, Sep 19, 2012 at 9:35 AM, Ulrich Kühne
> <ulrichk AT informatik.uni-bremen.de>
>  wrote:
>> Hi,
>>
>> As far as I know, in Maude, there is the owise keyword, meaning that an
>> equation is only tried if no other applies. This comes handy for default
>> transitions. How can I do this in K? Is there some annotation that I can 
>> add
>> like [transition] such that my rule is only applied if all others fail?
>>
>> What I would like to do is some sort of cleaning up after all rules get
>> stuck, but of course I do not want to see half-complete results. So I need
>> to avoid the cleaning up in a state where still rules could be applied.
>> Maybe I could do this with guards ("when ..."), but since the conditions of
>> my rules depend on deeply nested structures, this would be a big pain.
>
> I've also needed this many times.
>
> Can we add this functionality to K?
>
> Cheers,
> David
>
> _______________________________________________
> k-user mailing list
> k-user AT cs.uiuc.edu
> http://lists.cs.uiuc.edu/mailman/listinfo/k-user