gistfile2.txt

SIMPLE_spawn.maude

eq pSpawn = --- should output 1-10 and 11-20 interleaved
  function main() {
    spawn(for x = 11 to 20 do write(x);)
    for x = 1 to 10 do write(x);
  } .

mb configuration < T > 
                   < threads >
                     < thread >
                       < k > K </ k >
                       < fstack > .List </ fstack >
                       < xstack > .List </ xstack >
                       < env > .Map </ env >
                     </ thread >
                   </ threads >
                   < genv > .Map </ genv >
                   < store > .Map </ store >
                   < in > .List </ in >
                   < out > .List </ out >
                   < nextLoc > 0 </ nextLoc >
                 </ T > : KSentence .

mb rule
  < thread >...
    < k > [spawn S => .K] ...</ k >
    < env > Env </ env >
  ...</ thread >
  [.Bag =>
    < thread >
      < k > S </ k >
      < env > Env </ env >
      < fstack > .List </ fstack >
      < xstack > .List </ xstack >
    </ thread >
  ] : KSentence .