K-user mailing list

[Daniel Schnetzer Fava <danielsf AT ifi.uio.no>]

Sorry I didn’t notice the non ascii character from the copy/paste.  It works now, with the character removed from the comment, thanks.

I filed an issue like you suggested:

https://github.com/kframework/k/issues/2280

Thanks again,

Daniel

On 14 Feb 2017, at 04:09, Saxena, Manasvi <msaxena2 AT illinois.edu> wrote:

Hi Daniel,

Seems like the issue occurs since our parser cannot correctly parse the comment. Could you try removing the comment "//Notice how generation of fresh Ints can be done by prepending “!” to the variable” from the definition, and running kompile + run again? This should fix the problem. 

Sorry for the trouble. I added the comment while writing the email, and didn’t realize it’d cause this weird issue. 

It’d also be great if you could open an issue regarding this on github. Just copy the definition, with the comment included, and the error you encountered. The definition shouldn’t have parsed correctly in the first place. 

Manasvi

On Feb 13, 2017, at 8:30 PM, Daniel Schnetzer Fava <danielsf AT ifi.uio.no> wrote:

Hi Manasvi,

Thanks for the new definition!  Indeed I was able to kompile simple.k by copy/pasting from your previous email.

But when I ran on the same program (nat a, b, c), I got an exception (this time from krun):

$ cat test.simple

nat a, b, c

$ krun test.simple

Exception in thread "main" org.kframework.utils.errorsystem.KEMException: [Error] Critical: Failed to parse Kore file: ./simple-kompiled/kore.txt

ERROR: Unexpected error while parsing: java.lang.IllegalArgumentException: Less than 4 hex digits in unicode value: '\u' due to end of CharSequence

at org.kframework.utils.errorsystem.KEMException.create(KEMException.java:109)

at org.kframework.utils.errorsystem.KEMException.criticalError(KEMException.java:30)

at org.kframework.utils.inject.DefinitionLoadingModule.parseKore(DefinitionLoadingModule.java:62)

at org.kframework.utils.inject.DefinitionLoadingModule.koreDefinition(DefinitionLoadingModule.java:82)

at org.kframework.main.Main.runApplication(Main.java:228)

at org.kframework.main.Main.main(Main.java:74)

I’m attaching simple-kompiled/kore.txt in case it helps.

and got - 

<T> <k> nat .Globals </k> <H> c |-> SetItem ( 3 ) b |-> SetItem ( 2 ) a |-> SetItem ( 1 ) </H> </T>.

Is this consistent with the behavior you were intending to capture? 

Yes, that is the output I would like to get.

Thank you,

Daniel

<kore.txt>

On 14 Feb 2017, at 03:15, Saxena, Manasvi <msaxena2 AT illinois.edu> wrote:

Hi Daniel, 

I think K 4.0 doesn’t implicitly have support for “Nats”. I rewrote your definition as follows - 

module SIMPLE-SYNTAX

    syntax Globals ::= List{Id,","}

    syntax Pgm ::= "nat" Globals

endmodule

module SIMPLE

imports SIMPLE-SYNTAX

configuration <T><k> $PGM:Pgm </k><H> .Map </H></T>

//Notice how generation of fresh Ints can be done by prepending “!” to the variable

rule <k> nat (Z:Id,Zs:Globals => Zs) </k>

     <H> HMap => HMap[Z <- SetItem(!N:Int)] </H>

     requires notBool(Z in keys(HMap)) // no repeated declaration

endmodule

Then I ran krun on the following program - 

"nat a, b, c”

and got - 

<T> <k> nat .Globals </k> <H> c |-> SetItem ( 3 ) b |-> SetItem ( 2 ) a |-> SetItem ( 1 ) </H> </T>.

Is this consistent with the behavior you were intending to capture? 

On Feb 13, 2017, at 8:07 PM, Lucas Pena <lpena7 AT illinois.edu> wrote:

I'm sorry, it seems I am getting the same errors as you. I had saved your file as "test.k" on my system and I had another file named "simple.k" from before. For your program, try removing the "require ...", replacing the N with ?N, and removing the fresh(N) part of the requires clause. That seemed to work for me.

On Mon, Feb 13, 2017 at 7:58 PM, Daniel Schnetzer Fava <danielsf AT ifi.uio.no> wrote:

Hi Manasvi,

Without the require, kompile seems to complain about Nat:

$ kompile simple.k

[Error] Compiler: Had 1 parsing errors.

[Error] Inner Parser: Parse error: unexpected character ':'.

Source(./simple.k)

Location(10,24,10,25)

The location is the «N» for Nat right after the «:» 

I also tried replacing the require builtins/int.k with require "builtins/domains.k" but the NoSuchElementException still happens.

Thanks,

Daniel

On 14 Feb 2017, at 02:53, Saxena, Manasvi <msaxena2 AT illinois.edu> wrote:

Hi Daniel,

This may be occurring due to the presence of “require builtins/int.k”. Do you still get the same error when you try running kompile without it?

Manasvi

On Feb 13, 2017, at 7:44 PM, Daniel Schnetzer Fava <danielsf AT ifi.uio.no> wrote:

Hi Lucas,

I cloned the repo and built it.  I also ran the tests, which took about half an hour just like the instructions said.

Everything looked good, but when I try to kompile simple.k, I get the following exception:

$ kompile simple.k --debug

java.util.NoSuchElementException: No value present

at java.util.Optional.get(Optional.java:135)

at org.kframework.parser.concrete2kore.ParserUtils.slurp(ParserUtils.java:152)

at org.kframework.parser.concrete2kore.ParserUtils.slurp(ParserUtils.java:119)

at org.kframework.parser.concrete2kore.ParserUtils.loadModules(ParserUtils.java:207)

at org.kframework.parser.concrete2kore.ParserUtils.loadDefinition(ParserUtils.java:254)

at org.kframework.kompile.DefinitionParsing.parseDefinition(DefinitionParsing.java:169)

at org.kframework.kompile.DefinitionParsing.parseDefinitionAndResolveBubbles(DefinitionParsing.java:153)

at org.kframework.kompile.DefinitionParsing.parseDefinitionAndResolveBubbles(DefinitionParsing.java:149)

at org.kframework.kompile.Kompile.parseDefinition(Kompile.java:140)

at org.kframework.kompile.KompileFrontEnd.run(KompileFrontEnd.java:54)

at org.kframework.main.FrontEnd.main(FrontEnd.java:34)

at org.kframework.main.Main.runApplication(Main.java:414)

at org.kframework.main.Main.runApplication(Main.java:132)

at org.kframework.main.Main.main(Main.java:74)

java.util.NoSuchElementException: No value present

at java.util.Optional.get(Optional.java:135)

at org.kframework.parser.concrete2kore.ParserUtils.slurp(ParserUtils.java:152)

at org.kframework.parser.concrete2kore.ParserUtils.slurp(ParserUtils.java:119)

at org.kframework.parser.concrete2kore.ParserUtils.loadModules(ParserUtils.java:207)

at org.kframework.parser.concrete2kore.ParserUtils.loadDefinition(ParserUtils.java:254)

at org.kframework.kompile.DefinitionParsing.parseDefinition(DefinitionParsing.java:169)

at org.kframework.kompile.DefinitionParsing.parseDefinitionAndResolveBubbles(DefinitionParsing.java:153)

at org.kframework.kompile.DefinitionParsing.parseDefinitionAndResolveBubbles(DefinitionParsing.java:149)

at org.kframework.kompile.Kompile.parseDefinition(Kompile.java:140)

at org.kframework.kompile.KompileFrontEnd.run(KompileFrontEnd.java:54)

at org.kframework.main.FrontEnd.main(FrontEnd.java:34)

at org.kframework.main.Main.runApplication(Main.java:414)

at org.kframework.main.Main.runApplication(Main.java:132)

at org.kframework.main.Main.main(Main.java:74)

[Error] Internal: Uncaught exception thrown of type NoSuchElementException.

Please rerun your program with the --debug flag to generate a stack trace, and

file a bug report at https://github.com/kframework/k/issues

I’m using the latest java (8u121).

Thanks in advance,

Daniel

On 14 Feb 2017, at 01:44, Lucas Pena <lpena7 AT illinois.edu> wrote:

Yes, I'd go ahead and clone the repo and build it yourself. Please let me know if you're still experiencing issues. 

On Mon, Feb 13, 2017 at 6:39 PM, Daniel Schnetzer Fava <danielsf AT ifi.uio.no> wrote:

 Copying your code verbatim seems to kompile fine on my machine.

That’s excellent news.  It sounds like I just need to replicate your setup.

 Did you make sure you pulled the latest version from the repo, and rebuilt the project (using mvn clean and mvn package)?

I am using the binaries that came with k-distribution-4.0.0.zip from:

https://github.com/kframework/k/releases

Do you recommend cloning the repo and building myself?

Also, for what it's worth, the file you likely want to require is "domains.k" now, but you don't have to put the requires clause at all since it is included in the prelude.

Good to know.

Thanks,

Daniel

On 14 Feb 2017, at 01:27, Lucas Pena <lpena7 AT illinois.edu> wrote:

Hm, I'm not sure what causes that. Copying your code verbatim seems to kompile fine on my machine. Did you make sure you pulled the latest version from the repo, and rebuilt the project (using mvn clean and mvn package)? Also, for what it's worth, the file you likely want to require is "domains.k" now, but you don't have to put the requires clause at all since it is included in the prelude.

On Mon, Feb 13, 2017 at 6:02 PM, Daniel Schnetzer Fava <danielsf AT ifi.uio.no> wrote:

That’s very understandable.  It would be very hard to maintain both.

I am eager to switch to 4.0, but I’ve see a fair share of:

[Error] Internal: Uncaught exception thrown of type OutOfMemoryError.

Do you mind helping me diagnose this?  The same file kompiles ok with 3.4, but I guess lots has changed since.

Here is simple.k

$ cat simple.k

require "builtins/int.k"

module SIMPLE

  syntax Globals ::= List{Id,","}

  syntax Pgm ::= "nat" Globals

  configuration <T><k> $PGM:Pgm </k><H> .Map </H></T>

  rule <k> nat (Z:Id,Zs:Globals => Zs) </k>

       //<H> HMap:Map (. => Z |-> .Set ) </H>

       <H> HMap:Map (. => Z |-> SetItem(N) ) </H>

       requires fresh(N:Nat) andBool

        notBool(Z in keys(HMap)) // no repeated declaration

And here is the stack trace when the error happens:

$ ~/k-4/bin/kompile simple.k -I ~/k-4/include --debug

java.lang.OutOfMemoryError: GC overhead limit exceeded

at org.kframework.utils.Poset.<init>(Poset.java:110)

at org.kframework.utils.Poset.create(Poset.java:27)

at org.kframework.kil.loader.ModuleContext.<init>(ModuleContext.java:33)

at org.kframework.kil.Module.<init>(Module.java:22)

at org.kframework.parser.outer.Outer.Module(Outer.java:789)

at org.kframework.parser.outer.Outer.Start(Outer.java:758)

at org.kframework.parser.outer.Outer.parse(Outer.java:79)

at org.kframework.parser.concrete2kore.ParserUtils.slurp(ParserUtils.java:119)

at org.kframework.parser.concrete2kore.ParserUtils.slurp(ParserUtils.java:147)

at org.kframework.parser.concrete2kore.ParserUtils.slurp(ParserUtils.java:147)

at org.kframework.parser.concrete2kore.ParserUtils.slurp(ParserUtils.java:147)

at org.kframework.parser.concrete2kore.ParserUtils.slurp(ParserUtils.java:147)

at org.kframework.parser.concrete2kore.ParserUtils.slurp(ParserUtils.java:147)

at org.kframework.parser.concrete2kore.ParserUtils.slurp(ParserUtils.java:147)

at org.kframework.parser.concrete2kore.ParserUtils.slurp(ParserUtils.java:147)

at org.kframework.parser.concrete2kore.ParserUtils.slurp(ParserUtils.java:147)

at org.kframework.parser.concrete2kore.ParserUtils.slurp(ParserUtils.java:147)

at org.kframework.parser.concrete2kore.ParserUtils.slurp(ParserUtils.java:147)

at org.kframework.parser.concrete2kore.ParserUtils.slurp(ParserUtils.java:147)

at org.kframework.parser.concrete2kore.ParserUtils.slurp(ParserUtils.java:147)

at org.kframework.parser.concrete2kore.ParserUtils.slurp(ParserUtils.java:147)

at org.kframework.parser.concrete2kore.ParserUtils.slurp(ParserUtils.java:147)

at org.kframework.parser.concrete2kore.ParserUtils.slurp(ParserUtils.java:147)

at org.kframework.parser.concrete2kore.ParserUtils.slurp(ParserUtils.java:147)

at org.kframework.parser.concrete2kore.ParserUtils.slurp(ParserUtils.java:147)

at org.kframework.parser.concrete2kore.ParserUtils.slurp(ParserUtils.java:147)

at org.kframework.parser.concrete2kore.ParserUtils.slurp(ParserUtils.java:147)

at org.kframework.parser.concrete2kore.ParserUtils.slurp(ParserUtils.java:147)

at org.kframework.parser.concrete2kore.ParserUtils.slurp(ParserUtils.java:147)

at org.kframework.parser.concrete2kore.ParserUtils.slurp(ParserUtils.java:147)

at org.kframework.parser.concrete2kore.ParserUtils.slurp(ParserUtils.java:147)

at org.kframework.parser.concrete2kore.ParserUtils.slurp(ParserUtils.java:147)

java.lang.OutOfMemoryError: GC overhead limit exceeded

at org.kframework.utils.Poset.<init>(Poset.java:110)

at org.kframework.utils.Poset.create(Poset.java:27)

at org.kframework.kil.loader.ModuleContext.<init>(ModuleContext.java:33)

at org.kframework.kil.Module.<init>(Module.java:22)

at org.kframework.parser.outer.Outer.Module(Outer.java:789)

at org.kframework.parser.outer.Outer.Start(Outer.java:758)

at org.kframework.parser.outer.Outer.parse(Outer.java:79)

at org.kframework.parser.concrete2kore.ParserUtils.slurp(ParserUtils.java:119)

at org.kframework.parser.concrete2kore.ParserUtils.slurp(ParserUtils.java:147)

at org.kframework.parser.concrete2kore.ParserUtils.slurp(ParserUtils.java:147)

at org.kframework.parser.concrete2kore.ParserUtils.slurp(ParserUtils.java:147)

at org.kframework.parser.concrete2kore.ParserUtils.slurp(ParserUtils.java:147)

at org.kframework.parser.concrete2kore.ParserUtils.slurp(ParserUtils.java:147)

at org.kframework.parser.concrete2kore.ParserUtils.slurp(ParserUtils.java:147)

at org.kframework.parser.concrete2kore.ParserUtils.slurp(ParserUtils.java:147)

at org.kframework.parser.concrete2kore.ParserUtils.slurp(ParserUtils.java:147)

at org.kframework.parser.concrete2kore.ParserUtils.slurp(ParserUtils.java:147)

at org.kframework.parser.concrete2kore.ParserUtils.slurp(ParserUtils.java:147)

at org.kframework.parser.concrete2kore.ParserUtils.slurp(ParserUtils.java:147)

at org.kframework.parser.concrete2kore.ParserUtils.slurp(ParserUtils.java:147)

at org.kframework.parser.concrete2kore.ParserUtils.slurp(ParserUtils.java:147)

at org.kframework.parser.concrete2kore.ParserUtils.slurp(ParserUtils.java:147)

at org.kframework.parser.concrete2kore.ParserUtils.slurp(ParserUtils.java:147)

at org.kframework.parser.concrete2kore.ParserUtils.slurp(ParserUtils.java:147)

at org.kframework.parser.concrete2kore.ParserUtils.slurp(ParserUtils.java:147)

at org.kframework.parser.concrete2kore.ParserUtils.slurp(ParserUtils.java:147)

at org.kframework.parser.concrete2kore.ParserUtils.slurp(ParserUtils.java:147)

at org.kframework.parser.concrete2kore.ParserUtils.slurp(ParserUtils.java:147)

at org.kframework.parser.concrete2kore.ParserUtils.slurp(ParserUtils.java:147)

at org.kframework.parser.concrete2kore.ParserUtils.slurp(ParserUtils.java:147)

at org.kframework.parser.concrete2kore.ParserUtils.slurp(ParserUtils.java:147)

at org.kframework.parser.concrete2kore.ParserUtils.slurp(ParserUtils.java:147)

[Error] Internal: Uncaught exception thrown of type OutOfMemoryError.

Please rerun your program with the --debug flag to generate a stack trace, and

file a bug report at https://github.com/kframework/k/issues

Let me know whether I should file a bug report on github (as the error message suggests).

Thank you!

Daniel

On 14 Feb 2017, at 00:18, Lucas Pena <lpena7 AT illinois.edu> wrote:

I'm not sure why that doesn't work, but please note K 3.4 is no longer supported or maintained, and we encourage all users to switch to K 4.0, the newest version.

On Mon, Feb 13, 2017 at 12:10 PM, Daniel Schnetzer Fava <danielsf AT ifi.uio.no> wrote:

I have a similar question to my previous one:

https://lists.cs.illinois.edu/lists/arc/k-user/2017-02/msg00015.html

but now initializing a map of Id to Set (as opposed to List of Nat)

Following the same idea, it seems like I would do the following to initialize it to an empty set:

       <H> HMap:Map (. => Z |-> .Set ) </H>

And something like this to initialize it to a Set with one item (that item being N):

       <H> HMap:Map (. => Z |-> SetItem(N) ) </H>

But neighter of these work.

It seems like kompile complais about the last parenthesis of those lines:

[Error] Critical: Parse error: Syntax error near unexpected character ‘)'

Thanks again,

Daniel

On 13 Feb 2017, at 13:23, Dorel Lucanu <dlucanu AT info.uaic.ro> wrote:

You may initialize with any value you want, so it should work.
Dorel

On 13/02/2017 14:15, Daniel Schnetzer Fava wrote:

Indeed, its 3.4.

The list of nats does work, though I have a follow up question.
Can it be initialized to a non-empty list? For example:

       <H> HMap:Map (. => Z |-> N,.NatList ) </H>   requires fresh(N:Nat)

Does this seem legitimate?
Assuming .NatList is the empty list of nats and , is cons.

Thanks Dorel!

On 13 Feb 2017, at 13:02, Dorel Lucanu <dlucanu AT info.uaic.ro> wrote:

What version of K do you use? It seems to me that it is 3.4, correct?

A possible solution is:
- declare a sort for list of naturals

 syntax NatList ::= List{Nat,"","}

- initialize the store with the empty lists:
rule <k> nat (Z:Id,Zs:Globals => Zs) </k>
      <H> HMap:Map (. => Z |-> .NatList ) </H>

Dorel

On 13/02/2017 13:44, danielsf AT ifi.uio.no wrote:

What would be a good way to create a store from Id to List[Nat] as opposed to
Id to Nat?

I created a simple example where it parses
    nat x, y, z
and creates a configuration:
<H>
        x |-> #symNat(1)
        y |-> #symNat(2)
        z |-> #symNat(3)
</H>

But I would like x, y, and z to map to lists of Nats as opposed to a Nat.

Can you point me in the right direction?

Thanks!

Daniel

module SIMPLE
  syntax Globals ::= List{Id,","}
  syntax Pgm ::= "nat" Globals
  configuration <T><k> $PGM:Pgm </k><H> .Map </H></T>

  rule <k> nat (Z:Id,Zs:Globals => Zs) </k>
       // I would like to somehow say this instead:
       // <H> HMap:Map (. => Z|-> ListItem(N) ) </H>
       <H> HMap:Map (. => Z|-> N ) </H>
       requires fresh(N:Nat) andBool
        notBool(Z in keys(HMap)) // no repeated declaration
endmodule

--

Lucas Peña

University of Illinois at Urbana-Champaign

lpena7 AT illinois.edu

(954) 882-7070

--

Lucas Peña

University of Illinois at Urbana-Champaign

lpena7 AT illinois.edu

(954) 882-7070

--

Lucas Peña

University of Illinois at Urbana-Champaign

lpena7 AT illinois.edu

(954) 882-7070

--

Lucas Peña

University of Illinois at Urbana-Champaign

lpena7 AT illinois.edu

(954) 882-7070