k-user AT lists.cs.illinois.edu

Subject: K-user mailing list

List archive

Re: [[K-user] ] A Maps of Id to Set

From: Daniel Schnetzer Fava <danielsf AT ifi.uio.no>
To: Lucas Pena <lpena7 AT illinois.edu>
Cc: Daniel Schnetzer Fava <danielsf AT ifi.uio.no>, "k-user AT lists.cs.illinois.edu" <k-user AT lists.cs.illinois.edu>, Dorel Lucanu <dlucanu AT info.uaic.ro>
Subject: Re: [[K-user] ] A Maps of Id to Set
Date: Tue, 14 Feb 2017 00:02:46 +0000
Accept-language: en-US, nb-NO

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)

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)

[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

[[K-user] ] A Maps of Id to List of Nat, danielsf, 02/13/2017
- Re: [[K-user] ] A Maps of Id to List of Nat, Dorel Lucanu, 02/13/2017
  - Message not available
    - Message not available
      - [[K-user] ] A Maps of Id to Set, Daniel Schnetzer Fava, 02/13/2017
  - Message not available
    - Message not available
      - Message not available
        
        Re: [[K-user] ] A Maps of Id to Set, Lucas Pena, 02/13/2017
        
        Re: [[K-user] ] A Maps of Id to Set, Daniel Schnetzer Fava, 02/13/2017
        
        Message not available
        
        Re: [[K-user] ] A Maps of Id to Set, Lucas Pena, 02/13/2017
        Re: [[K-user] ] A Maps of Id to Set, Daniel Schnetzer Fava, 02/13/2017
        
        Message not available
        Re: [[K-user] ] A Maps of Id to Set, Lucas Pena, 02/13/2017
        Re: [[K-user] ] A Maps of Id to Set, Daniel Schnetzer Fava, 02/13/2017
        Re: [[K-user] ] A Maps of Id to Set, Saxena, Manasvi, 02/13/2017
        Re: [[K-user] ] A Maps of Id to Set, Daniel Schnetzer Fava, 02/13/2017
        
        Message not available
        Re: [[K-user] ] A Maps of Id to Set, Lucas Pena, 02/13/2017
        Re: [[K-user] ] A Maps of Id to Set, Saxena, Manasvi, 02/13/2017
        Message not available
        Re: [[K-user] ] A Maps of Id to Set, Saxena, Manasvi, 02/13/2017
        Re: [[K-user] ] A Maps of Id to Set, Daniel Schnetzer Fava, 02/13/2017