K-user mailing list

["Rosu, Grigore" <grosu AT illinois.edu>]

Indeed, as Pat said, there is no way to complete the partial configuration that you mentioned in your rule, in the sense that there is no way to add more cells over the already given cells in order to satisfy the configuration "contract" (i.e., k inside thread inside threads, and only thread can multiply).  Of course, we could give a better error message here.  Radu, I hope you are taking notes :)

But the simplest and most compact way to write your rule is:

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

Note that you do not need parentheses around (spawn S => skip), because <k> and 

...</k>, which we call "(cell) membranes", are thought of as "parentheses".  A membrane with ... in it is also called "open membrane".  In other words, <k> spawn S => skip  ...</k> does not grab the ... as part of the skip RHS.

Two more observations: you should normally not need the ">" before the syntax declaration of "spawn".  That is needed only when there could be parsing ambiguities.  For such a simple language there should not be any ambiguities.  I typically put no ">" until I really have to.

Finally, you can be more specific with the type of $PGM, for example $PGM:Stmt instead of $PGM:K.  This will help the parser, because it will consider Stmt to be the start symbol of the grammar; otherwise, it assumes that any symbol can be start, so there could be more parsing ambiguities.

Grigore

 

 

---

From: k-user-bounces AT cs.uiuc.edu [k-user-bounces AT cs.uiuc.edu] on behalf of Patrick Meredith [pmeredit AT gmail.com]
Sent: Tuesday, October 16, 2012 8:31 PM
To: Robby Findler
Cc: k-user AT cs.uiuc.edu
Subject: Re: [K-user] k local rewrite could not be eliminated here.

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