K-user mailing list

[Brandon Hill <bgh.list.reader AT gmail.com>]

Ok, I tried it with both:

java version "1.6.0_24"
OpenJDK Runtime Environment (IcedTea6 1.11.4 (6b24-1.11.4-1ubuntu0.12.04.1)
OpenJDK 64-Bit Server VM (build 20.0-b12, mixed mode

and

java version "1.7.0_07"
OpenJDK Runtime Environment (IcedTea7 2.3.2) (7u7-2.3.2a-0ubuntu0.12.04.1)
OpenJDK 64-Bit Server VM (build 23.2-b09, mixed mode)

with the same results.  I'm not quite sure what to try beyond that.
I'm not suggesting that it must be fixed, I can work on the Mac.  I'm
just trying to give data in case someone else runs into a similar
issue.

Thanks,
Brandon

On Fri, Sep 28, 2012 at 1:10 AM, Radu Mereuta 
<headness13 AT gmail.com>
 wrote:
> That error messages comes from somewhere in Java. It tries to read a badly
> formated XML and it throws an exception. But as we have multiple points that
> uses XML, I'm not really sure where it comes from. Could be kompile, krun
> and kast in equal matters.
>
> But since you only get it on one machine, might be the problem there. Please
> check the java installation too.
>
> Radu
>
> On Fri, Sep 28, 2012 at 3:02 AM, Brandon Hill 
> <bgh.list.reader AT gmail.com>
> wrote:
>>
>> This does seem to work on the Mac from both the binary and the SVN
>> build.  This makes me wonder if it is a system library that behaves
>> differently than expected on my Ubuntu installation.
>>
>> Thanks,
>> Brandon
>>
>>
>>
>> On Thu, Sep 27, 2012 at 4:22 PM, Brandon Hill 
>> <bgh.list.reader AT gmail.com>
>> wrote:
>> > The latest from  http://k-framework.googlecode.com/svn/tags/latest/
>> > gives me the same error.  I will move on to trying this on another
>> > platform.
>> >
>> > Thanks,
>> > Brandon
>> >
>> >
>> >
>> > On Thu, Sep 27, 2012 at 4:02 PM, Brandon Hill
>> > <bgh.list.reader AT gmail.com>
>> >  wrote:
>> >> Interesting.  I just made sure I was using the 28-Sep-2012 release.  I
>> >> cut and pasted the code above into a file.  I kompiled it, but my test
>> >> case of:
>> >>
>> >> x <- 5;
>> >> x;
>> >>
>> >> Still gives:
>> >>
>> >> [Fatal Error] :1:1: Premature end of file.
>> >> Error: Error while reading XML:Premature end of file
>> >>
>> >> I even uninstalled any pre-existing Maude because it was a year newer
>> >> than what is in your binary, and I wanted to be sure the system wasn't
>> >> using it instead.  I also tried it with the earlier recommended
>> >> changes, but they gave the same result.  I am running on Ubuntu 12.04
>> >> 64-bits.  Does that imply that some other environment variable could
>> >> be making our runs differ?  I can try getting the latest from SVN and
>> >> building that as a sanity check.  Sorry for any hassle.
>> >>
>> >> My intention was for assignments to print nothing, but reductions of
>> >> all other expressions to print.  That was why I had assignments reduce
>> >> to void so I could capture and ignore those expressions.
>> >>
>> >> Thank you,
>> >> -Brandon
>> >>
>> >> P.S.  Thanks for the tutorial videos, they are really helpful.
>> >> On Thu, Sep 27, 2012 at 3:11 PM, Rosu, Grigore 
>> >> <grosu AT illinois.edu>
>> >> wrote:
>> >>> Ok, my flight is late, so I tried your example.  It works on my
>> >>> machine, I mean, it kompiles.  Also, it kruns, or at least on the 
>> >>> program
>> >>> test.rt, which is
>> >>>
>> >>> x <- 10;
>> >>>
>> >>> However, it does not do what you want, which is to print 10, because
>> >>> your definition is actually not correct.
>> >>> (if you get compilation errors, then please make sure you downloaded
>> >>> the k latest built).
>> >>>
>> >>> You have two competing rules that can apply when a value is on top of
>> >>> K: the cooling rule for your assignment, and the printing rule.  It 
>> >>> happens
>> >>> that the first one applies, so the value V is moved back into its 
>> >>> context,
>> >>> and then the printing rule gets no chance to apply anymore, since 
>> >>> there is
>> >>> no value for it on the computation.  If the printing rule applied 
>> >>> first,
>> >>> then things would be a lot worse!  That's because you are also 
>> >>> consuming the
>> >>> value once you print it, so the cooling rule of assignment would get no
>> >>> value to cool, so it would get stuck.
>> >>>
>> >>> The above does not give you a solution for your problem, but hopefully
>> >>> makes you think through these interesting issues.
>> >>>
>> >>> Grigore
>> >>>
>> >>>
>> >>>
>> >>> ________________________________________
>> >>> From: Brandon Hill 
>> >>> [bgh.list.reader AT gmail.com]
>> >>> Sent: Thursday, September 27, 2012 4:47 PM
>> >>> To: Rosu, Grigore
>> >>> Cc: 
>> >>> k-user AT cs.uiuc.edu
>> >>> Subject: Re: [K-user] Printing
>> >>>
>> >>> Thank you for the pointer on the better rules.  I thought I had tried
>> >>> something like that and got errors, but it seems to work currently.
>> >>>
>> >>> The cleaner rules don't seem to solve the printing issue, even when I
>> >>> change the sort to I:Int and eliminate the side rule.  I was going
>> >>> with V because it will contain more sorts in the future, but making
>> >>> different rules for each result sort will be fine if that can be made
>> >>> to work.
>> >>>
>> >>> Thanks,
>> >>> Brandon
>> >>>
>> >>> On Thu, Sep 27, 2012 at 2:25 PM, Rosu, Grigore 
>> >>> <grosu AT illinois.edu>
>> >>> wrote:
>> >>>> Did you try I:Int instead of V:Val and remove the side condition?
>> >>>>
>> >>>> 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
>>
>> _______________________________________________
>> k-user mailing list
>> k-user AT cs.uiuc.edu
>> http://lists.cs.uiuc.edu/mailman/listinfo/k-user
>
>