Uncaught ModuleTransformException

[tomofumi-yuki]

Hi,

I encountered the following: [Error] Internal: Uncaught exception thrown of type ModuleTransformerException. Please rerun your program with the --debug flag to generate a stack trace, and file a bug report at https://github.com/kframework/k/issues

Here are the outputs with --debug and the input file.

kompile-out.txt test.txt

[daejunpark]

@tomofumi-yuki We recommend to enclose the cell of multiplicity=* with another cell, e.g., as follows:

<threads>
  <thread multiplicity=*>
    ...
  </thread>
</threads>

Also, you have to qualify the dot . with a proper sort name (e.g., .Bag, .List, .Map).

Please find the fixed definition in below:

module TEST-SYNTAX
  syntax Statement ::= Basic | Seq | Spawn
  syntax Basic ::= Id
  syntax Spawn ::= "spawn" "{" Basic "}"
  syntax Seq ::= Statement ";" Statement [left]


endmodule

module TEST
  imports TEST-SYNTAX
  syntax KResult ::= Int | Bool

  configuration <T>
  <threads>
                   <thread multiplicity="*">
                       <k> $PGM:Statement </k>
                       <TID>0</TID>
                   </thread>
  </threads>
                   <nextTID>1</nextTID>
                </T>

  rule S1; S2 => S1 ~> S2 [structural]

  rule
  <threads>
        <thread>
            <k> (spawn { S } => .) ...</k>
            <TID>0</TID>
         </thread>
        (.Bag =>  <thread>
            <k> S </k>
           <TID>V</TID>
               </thread>)
  </threads>
        <nextTID>V => V +Int 1</nextTID>

endmodule