Transition rules fail to apply on supercooled expressions. Unsound?

[cos]

When tagging a rule with [transition], it doesn't apply on supercooled expressions anymore. In the example below I'm playing with adding [transition] after rule b 1 => c

module TEST
  syntax L ::= "a" | "b" | "c" | "1"
  syntax Exp ::= L L [strict, superheat]

  rule a => b [supercool]
  rule b 1 => c [transition]
endmodule

The input is a 1.

Without [transition]:

Solution 1, State 1:
<k>
    c
</k>

Solution 2, State 2:
<k>
    1 ~> a HOLE
</k>

With [transition]:

Solution 1, State 2:
<k>
    1 ~> a HOLE
</k>

Solution 2, State 3:
<k>
    b ~> HOLE 1
</k>

Solution 3, State 4:
<k>
    1 ~> b HOLE
</k>

It looks like b 1 is heated before the rule is allowed to apply. I guess the transitions (implemented as Maude rules) only apply after the cooling->heating (implemented as Maude equations) is finished. Still, it looks unsound.

(don't read too much into the example :)

[cos]

Minimized the example.

[cos]

A simpler example:

module TEST
  syntax L ::= "a" | "b" | "c" | "1"
  syntax Exp ::= L L [strict]

  rule a 1 => b 1 [transition] 
  rule a 1 => c 1 [transition]
endmodule

on the same input (a 1) gives:

Solution 1, State 0:
<k>
    a ~> HOLE 1
</k>

This means it is impossible (or not obvious to me) to explore behaviors that vary depending on structural rules applied before heating. In the above example, we can convince one of the rules to apply by removing the transition tag, but we cannot explore both.

[cos]

One way to force the behavior is to tag the syntax Exp rule with transition, thus putting a backtracking point there. But this makes supercooling fail for some reason:

module TEST
  syntax L ::= "a" | "b" | "c" | "1" | "d"
  syntax Exp ::= L L [strict, transition]

  rule a => d [supercool]

  rule d 1 => b 1 
endmodule

Outputs:

Solution 1, State 1:
<k>
    d ~> HOLE 1
</k>

Solution 2, State 2:
<k>
    1 ~> a HOLE
</k>

Instead of:

Solution 1, State 0:
<k>
    b ~> HOLE 1
</k>

Solution 2, State 2:
<k>
    1 ~> a HOLE
</k>

[cos]

I nagged @andreistefanescu and we looked into it:

For the example, the cooling rule: syntax Exp ::= L L [strict, transition] generates a transition that that requires the the cooled expression to be a KResult, as expected.

The problem is that supercool should inhibit this requirement and it doesn't - my guess is the supercooling mechanism simply doesn't work with cooling transitions. We didn't look into this.

We looked into how to bypass the problem. For now, the simplest solutions are to either write the heating/cooling rules manually (including ugly freezer wrappers), or change the source to make the cooling not require KResults. This will break krun for non-search but will work for my purpose. @traiansf, could you help me with this by any chance? At least knowing where to look in the k sources would be helpful.

[cos]

Test this when strategies are in place.