how multiple matched rules are dealt with

[ngasoft]

Sorry for an naive question. I try to understand what happens two or more rules are matched? do they all fired to give rise to different runs?

For example, I have the following K program:

module TEST-SYNTAX

  syntax STM ::= "i" | "a" | "b" 

endmodule

module TEST

  imports TEST-SYNTAX

  configuration
  <T>
    <k> $PGM:STM </k>
    <out> .K </out>
  </T>

  rule <k> i => b </k>
  rule <k> i => a </k>
  rule <k> b => .K </k> <out> _ => "b" </out>
  rule <k> a => .K </k> <out> _ => "a" </out>

endmodule

A program for this language contain only "i" (without quotes).

If I kruns this program with the option --search, there is only solution (also I wish to have two). Do I misunderstand K at some point? how to obtain both expected runs from this program?

Here is the output of krun (I use k 3.5.2)

krun test.t --search
Search results:

Solution 1:
<T>
    <k>
        .K
    </k>
    <out>
        "a"
    </out>
</T>

Thank you very much.

[cos]

Sorry for an naive question. I try to understand what happens two or more rules are matched? do they all fired to give rise to different runs?

Yes. With regular execution you will only see one of the runs, while --search will give you all possible runs.

For your example, it does look like it should give two solutions. It might be a bug in K 3.5. Could you try it with K 4.0?

[andreiarusoaie]

Have you tried to add the [transition] tag to your rules? Syntax: rule Left => Right [transition]

[cos]

@andreiarusoaie, right :-)

We had been defaulting to [transition] in the Java backend for a while but, yes, it was needed before, and it is still needed in the latest version.

[grosu]

Guys, let me remind you that we do not encourage you to use the "transition" attribute. Instead, you should use the --transition option to kompile, and include all the rules that you want to consider as transitions there. If you want all the rules to be transitions, then add "computational" to the list of transitions (--transition "computational")..

[ngasoft]

Hello, thank you for your answers. Also a similar question about how multiple applicable rules are dealt with, but now, in the definition of a function? when two or more rules in the definition of a function are applicable at the same time, is there an implicit priority determining which rule is applied? Can we specify an explicit priority for the application of these rules?

For example, consider the following k definition

module RULEINFUN-SYNTAX

  syntax STM ::= "i" | "a" | "b"

endmodule

module RULEINFUN

  imports RULEINFUN-SYNTAX

  configuration
  <T>
    <k> $PGM:STM </k>
  </T>

  rule <k> i => fun(i) </k>

  syntax STM ::= fun(STM) [function]
  rule fun(i) => b
  rule fun(i) => a 

endmodule

And an input file

i

When kruning this input file, I have the result:

<T>
    <k>
        a
    </k>
</T>

Can we explicitly specify in K definition that the first rule of "fun" to have a higher priority than the second?

Thank you.

[cos]

The rules are applied non-deterministically. While some earlier versions of K did follow some conventions for rule application order, it would be best to not rely on them.

The cleanest way to prioritize rules is to use rewriting strategies. We have experimental support for them in K 4.0. If using the latest version of K is not an option for you, there was some limited support for strategies before. @andreistefanescu, do you know more about it by any chance?