K-user mailing list

[Patrick Meredith <pmeredit AT gmail.com>]

The quick fix, if you want to mention the threads cell explicitly, is:

  rule <threads>  <thread> <k> (spawn S => skip)  ...</k> </thread>

       (. => <thread> <k> S </k> </thread>) ...</threads>

On Tue, Oct 16, 2012 at 8:29 PM, Patrick Meredith <pmeredit AT gmail.com> wrote:

Your new rule is saying that there is somehow a <k> cell outside of the <threads> cell, and then inferring that there must be two <threads> cells.

-Patrick

On Tue, Oct 16, 2012 at 8:27 PM, Robby Findler <robby AT eecs.northwestern.edu> wrote:

Okay guys, thanks. I think I simplified too much. What is happening now?

module IMP
  syntax Stmt ::= StmtVal
                > "spawn" Stmt
  syntax StmtVal ::= "skip"

  syntax KResult ::= Bool | Int | String | StmtVal

  configuration <C color="yellow">
                  <threads>
                    <thread multiplicity="*">
                      <k color="green"> $PGM:K </k>
                    </thread>
                  </threads>
                </C>


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

       <threads> (. => <thread> <k> S </k> </thread>) ...</threads>
endmodule


Error: Cell <C> appears multiple times at the top level but its multipliciy
    does not allow that. Check the initial configuration for the definition
    matches the rule.
 Term: <_>_</_>(__(C,_=_(ellipses,"both")),<_>_</_>(__(threads,_=_(ellipses,
    "both")),<_>_</_>(__(thread,_=_(ellipses,"both")),<_>_</_>(__(k,_=_(

    ellipses,"right")),_=>_(_`(_`)('spawn_,S:K),_`(_`)('skip,.List`{K`})),k),
    thread),threads),C)
 Context:
Location: /Users/robby/git/robby/395-2012/imp.k:17:3:18:68
 Compilation phase: CONTEXT-TRANSFORMERS

_______________________________________________
k-user mailing list
k-user AT cs.uiuc.edu
http://lists.cs.uiuc.edu/mailman/listinfo/k-user

--
-Patrick

--
-Patrick