K-user mailing list

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

I don't know if this is the problem or not, and I cannot test it properly as 
I am on the road trying to get back home today, but in general writing rules 
like 

  rule <k> (V:Val; ~> K:K) => K ...</k>
       <out>... . => ListItem(V) </out>
       when  V =/=K void

  rule <k> (void; ~> K:K) => K ...</k>

is very risky.  I would write them this way:

  rule <k> V:Val; => . ...</k>
       <out>... . => ListItem(V) </out>
       when  V =/=K void

  rule <k> void; => . ...</k>

These are simpler, too.

The problem with your rules is that that they are HIGHLY non-determinstic!  
Your K variables can match any
fragments of the computation that follow V, so you have n-1 matches, where n 
is the number of items in your k cell!  In this particular case it does not 
matter that much, because you should get the same results when you execute 
your definitions, but you may get an exponential blowup when you search!

Radu, the error message that Brendon got is not very nice or helpful .. but 
you know that already.

Grigore



________________________________________
From: 
k-user-bounces AT cs.uiuc.edu
 
[k-user-bounces AT cs.uiuc.edu]
 on behalf of Brandon Hill 
[bgh.list.reader AT gmail.com]
Sent: Thursday, September 27, 2012 4:09 PM
To: 
k-user AT cs.uiuc.edu
Subject: [K-user] Printing

I am trying to model a language that prints the resulting value from
each expression.  The examples show how to explicitly print with an
explicit print function, a Printable sort, and an output list.  I'm
not entirely clear how that Printable works.

Without it, I get:

[Fatal Error] :1:1: Premature end of file.
Error: Error while reading XML:Premature end of file.

or

(#ostream( 1 ))  (#buffer( (.) ))

as output.  Here is a trimmed down version of what I tried:


module RT-SYNTAX
  imports BUILTIN-SYNTAX-HOOKS

  syntax Val ::= Int

  syntax Expr ::= Id | Val
        > Id "<-" Expr  [right, strict(2)]

  syntax Stmt ::= Expr ";" [strict]
        | Stmt Stmt    [left]

  syntax Pgm ::= Stmt

endmodule

module RT
  imports RT-SYNTAX

  syntax Val ::= "void"

  syntax KResult ::= Val

  configuration <T color="yellow">
                  <k color="green"> $PGM:Pgm </k>
                  <env color="LightSkyBlue"> .Map </env>
                  <heap color="white"> .Map </heap>
                  <nextLoc color="gray"> 0 </nextLoc>
                  <out color="Orchid" stream="stdout"> .List </out>
                </T>

  rule [declaration]:
       <k> X:Id <- V:Val => void ...</k>
       <env>... Rho => Rho[L/X] ...</env>
       <heap>... . => L |-> V ...</heap>
       <nextLoc> L => L +Int 1 </nextLoc>
       when notBool(X in keys(Rho)) [transition]

  rule [lookup]: <k> X => V ...</k>
       <env>... X |-> L ...</env>
       <heap>... L |-> V ...</heap> [supercool, transition]

  rule [sequential]: (S1:Stmt S2:Stmt) => (S1 ~> S2)  [structural]

  rule <k> (V:Val; ~> K:K) => K ...</k>
       <out>... . => ListItem(V) </out>
       when  V =/=K void

  rule <k> (void; ~> K:K) => K ...</k>

endmodule


I also tried ListItem(Int2String(V)) but that doesn't work either.

Any pointers would be appreciated.

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