Non-termination behavior of java backend when forgetting declaring function

[liyili2]

I am not sure if there is a bug or not: When I have the following set of rules:

module TEST

     syntax KItem ::= print(String)

     rule print(S:String) => #write(#stdout,S)

endmodule

If I compile it as maude backend defintion, it runs fine. The output is like:

success<k>
    .K
</k>

If I compile it as java backend definition and try to run it. It will not terminate:

However, if I add a function label, it terminates again:

module TEST

     syntax KItem ::= print(String) [function]

     rule print(S:String) => #write(#stdout,S)

endmodule

The output has problem but it is not related to the non-termination problem here:

[0, 2.768 ms]
<k>
    #write ( #stdout , "success" )
</k>

[andreistefanescu]

This is actually the intended behavior.

[liyili2]

This is a opposite behavior here: If I have this set of rules:

module TEST

     configuration 
<T>
     <k color="green"> 
          loadMergeObj($OBJ1:Bag, $OBJ2:Bag)
          ~> $PGM:K ~> link
     </k>
<options> $OPTIONS:Set </options>

</T>

syntax KItem ::= loadMergeObj(Bag,Bag) [function]
        | print(String) [function]
        | "link"
        | Int

rule loadMergeObj(B1:Bag,B2:Bag) => .K
rule 1 => .K
rule <k> link => print("success!\n") ...</k>
rule print(S:String) => #write(1,S)

endmodule

and if I have program: "1" and I use this command to run the program:

krun --smt=none -cOPTIONS="(SetItem(NOLINK) .Set)" -cOBJ1=".Bag" -cOBJ2=".Bag" program

The krun will go into non-termination. However if I eliminate the [function] in the print method as:

module TEST

     configuration 
<T>
     <k color="green"> 
          loadMergeObj($OBJ1:Bag, $OBJ2:Bag)
          ~> $PGM:K ~> link
     </k>
<options> $OPTIONS:Set </options>

</T>

syntax KItem ::= loadMergeObj(Bag,Bag) [function]
        | print(String) [function]
        | "link"
        | Int

rule loadMergeObj(B1:Bag,B2:Bag) => .K
rule 1 => .K
rule <k> link => print("success!\n") ...</k>
rule print(S:String) => #write(1,S)

endmodule

It can run fine and the output is expected:

success!
[3, 13.78 ms]
<T>
    <k>
        .K
    </k>
    <options>
        SetItem ( NOLINK )
    </options>
</T>

[dwightguth]

First issue fixed #666. Second issue duplicate of #654. Will resolve when #666 is merged.