K-user mailing list

[<tomofumi.yuki AT inria.fr>]

Hi,

I just started using the K framework a couple of days ago while looking for a
good way to express semantics for parallel languages. I was initially using
the virtual machine provided to get started with the tools, and since I was
quite happy with what I was able to achieve, I decided to actually install it
on my machine.

The problem that I currently face is that the semantics I developed within the
virtual machine, which has version 3.4, does not kompile with the most recent
version from git (4.0.1).

It appears that the accepted syntax for the rewrite rules are more strict. I
tried a heavily stripped down version of the EXP language in this article:
  http://fsl.cs.illinois.edu/index.php/The_K_Primer_(version_3.3)
copied at the end of the post, and many variants of it, but I was unable to
get thread spawning to work. (From what I can see, it seems like the problem
is around: . => )

I quickly went through the changelog, but I didn't spot any relevant changes
to the syntax. I appreciate your help on how I can update my rules to work
with 4.0.
For now, what I want to know is how to write a rule for spawning of threads.

Thanks,
Tomofumi Yuki


module EXP-SYNTAX

syntax Exp ::= Int
syntax Exp ::= "spawn" Exp

endmodule

module EXP

imports EXP-SYNTAX
syntax KResult ::= Int
configuration
  <T><k multiplicity="*">$PGM:Exp</k></T>

rule <k> spawn S => . ...</k>
     (. => <k> S </k>)

endmodule