k-user AT lists.cs.illinois.edu

Subject: K-user mailing list

List archive

Re: [K-user] k local rewrite could not be eliminated here.

From: Robby Findler <robby AT eecs.northwestern.edu>
To: "Rosu, Grigore" <grosu AT illinois.edu>
Cc: "k-user AT cs.uiuc.edu" <k-user AT cs.uiuc.edu>
Subject: Re: [K-user] k local rewrite could not be eliminated here.
Date: Tue, 16 Oct 2012 20:27:49 -0500
List-archive: <http://lists.cs.uiuc.edu/pipermail/k-user/>
List-id: <k-user.cs.uiuc.edu>

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] k local rewrite could not be eliminated here., Robby Findler, 10/16/2012
- <Possible follow-up(s)>
- Re: [K-user] k local rewrite could not be eliminated here., Patrick Meredith, 10/16/2012
  - Re: [K-user] k local rewrite could not be eliminated here., Robby Findler, 10/16/2012
- Re: [K-user] k local rewrite could not be eliminated here., Rosu, Grigore, 10/16/2012
  - Re: [K-user] k local rewrite could not be eliminated here., Robby Findler, 10/16/2012
  - Message not available
    - Re: [K-user] k local rewrite could not be eliminated here., Patrick Meredith, 10/16/2012
  - Message not available
    - Message not available
      - Re: [K-user] k local rewrite could not be eliminated here., Patrick Meredith, 10/16/2012
        
        Re: [K-user] k local rewrite could not be eliminated here., Robby Findler, 10/16/2012
        
        Re: [K-user] k local rewrite could not be eliminated here., Rosu, Grigore, 10/16/2012