K-user mailing list

[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