K-user mailing list

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

Hi,

I'm trying to express
  (Mw[Z])[ (choice(keys((Mw[Z])) -Set Ss)) ]
in a rule, where Mw is a Map of Id to Map of Int to Int, and Ss is a set of 
Ints.

If you think of Mw as a time-stamped history of writes to variables, and Ss 
as a set of discarded time stamps, then I would like to express "load Z:Id" 
as follows:

Pick a random value in Mw[Z] (i.e. a value that was previously writen to Z) 
but that is not in Ss (i.e., a value that was not yet discarded).

Here is a small example:

module Q2-SYNTAX
  syntax Id ::= "x" | "y" | "z" | "$x"
  syntax Val ::= Id | Int
  syntax Pgm ::= Val | "load" Id
  syntax KResult ::= Val
endmodule

module Q2
  imports Q2-SYNTAX
  syntax KVariable ::= Id
  configuration <T color="yellow">
                  <k color="green"> $PGM:Pgm </k>
                  <S color="Orchid"> SetItem(1) SetItem(2)  </S> // Set of 
Ints
                </T>
                <W color="Aquamarine"> (x |-> ((1|->0)[3<-1][4<-2])) [y <- 
(2|->0) ] </W>  // Map of Id to a Map of Int to Val

  rule <k> load Z:Id => Mw[Z] </k>
       <S> Ss:Set </S>
       <W> Mw:Map </W>
endmodule

I would like to replace the $x above.  Replacing it with (Mw[Z])[ 
(choice(keys((Mw[Z])) -Set Ss)) ] doesn't kompile.  I had able to get it to 
compile by breaking the expression down into several smaller structural 
rules. But it still didn't work as it caused errors when krun’ing (see below).

Can you point me in a good direction?

Thank you in advace,

Daniel


$ cat test.q2
load x
$ krun test.q2 --debug
java.util.NoSuchElementException: key not found: index
        at scala.collection.MapLike.default$(MapLike.scala:232)
        at scala.collection.MapLike.default(MapLike.scala:231)
        at scala.collection.MapLike.apply$(MapLike.scala:141)
        at scala.collection.MapLike.apply(MapLike.scala:140)
        at 
org.kframework.unparser.KOREToTreeNodes$.apply(KOREToTreeNodes.scala:20)
        at 
org.kframework.unparser.KOREToTreeNodes$.$anonfun$apply$3(KOREToTreeNodes.scala:21)
        at 
scala.collection.TraversableLike.$anonfun$map$1(TraversableLike.scala:234)
        at scala.collection.Iterator.foreach$(Iterator.scala:932)
        at scala.collection.Iterator.foreach(Iterator.scala:932)
        at scala.collection.IterableLike.foreach$(IterableLike.scala:71)
        at scala.collection.IterableLike.foreach(IterableLike.scala:70)
        at scala.collection.TraversableLike.map$(TraversableLike.scala:234)
        at scala.collection.TraversableLike.map(TraversableLike.scala:227)
        at 
org.kframework.unparser.KOREToTreeNodes$.apply(KOREToTreeNodes.scala:21)
        at 
org.kframework.unparser.KOREToTreeNodes$.$anonfun$apply$3(KOREToTreeNodes.scala:21)
        at 
scala.collection.TraversableLike.$anonfun$map$1(TraversableLike.scala:234)
        at scala.collection.Iterator.foreach$(Iterator.scala:932)
        at scala.collection.Iterator.foreach(Iterator.scala:932)
        at scala.collection.IterableLike.foreach$(IterableLike.scala:71)
        at scala.collection.IterableLike.foreach(IterableLike.scala:70)
        at scala.collection.TraversableLike.map$(TraversableLike.scala:234)
        at scala.collection.TraversableLike.map(TraversableLike.scala:227)
        at 
org.kframework.unparser.KOREToTreeNodes$.apply(KOREToTreeNodes.scala:21)
        at 
org.kframework.unparser.KOREToTreeNodes$.$anonfun$apply$3(KOREToTreeNodes.scala:21)
        at 
scala.collection.TraversableLike.$anonfun$map$1(TraversableLike.scala:234)
        at scala.collection.Iterator.foreach$(Iterator.scala:932)
        at scala.collection.Iterator.foreach(Iterator.scala:932)
        at scala.collection.IterableLike.foreach$(IterableLike.scala:71)
        at scala.collection.IterableLike.foreach(IterableLike.scala:70)
        at scala.collection.TraversableLike.map$(TraversableLike.scala:234)
        at scala.collection.TraversableLike.map(TraversableLike.scala:227)
        at 
org.kframework.unparser.KOREToTreeNodes$.apply(KOREToTreeNodes.scala:21)
        at 
org.kframework.unparser.KOREToTreeNodes$.$anonfun$apply$3(KOREToTreeNodes.scala:21)
        at 
scala.collection.TraversableLike.$anonfun$map$1(TraversableLike.scala:234)
        at scala.collection.Iterator.foreach$(Iterator.scala:932)
        at scala.collection.Iterator.foreach(Iterator.scala:932)
        at scala.collection.IterableLike.foreach$(IterableLike.scala:71)
        at scala.collection.IterableLike.foreach(IterableLike.scala:70)
        at scala.collection.TraversableLike.map$(TraversableLike.scala:234)
        at scala.collection.TraversableLike.map(TraversableLike.scala:227)
        at 
org.kframework.unparser.KOREToTreeNodes$.apply(KOREToTreeNodes.scala:21)
        at 
org.kframework.unparser.KOREToTreeNodes.apply(KOREToTreeNodes.scala)
        at org.kframework.krun.KRun.unparseTerm(KRun.java:431)
        at org.kframework.krun.KRun.prettyPrint(KRun.java:313)
        at org.kframework.krun.KRun.filterAnonVarsAndPrint(KRun.java:163)
        at org.kframework.krun.KRun.printK(KRun.java:214)
        at org.kframework.krun.KRun.run(KRun.java:107)
        at org.kframework.krun.KRunFrontEnd.run(KRunFrontEnd.java:68)
        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:265)
        at org.kframework.main.Main.main(Main.java:74)
java.util.NoSuchElementException: key not found: index
        at scala.collection.MapLike.default$(MapLike.scala:232)
        at scala.collection.MapLike.default(MapLike.scala:231)
        at scala.collection.MapLike.apply$(MapLike.scala:141)
        at scala.collection.MapLike.apply(MapLike.scala:140)
        at 
org.kframework.unparser.KOREToTreeNodes$.apply(KOREToTreeNodes.scala:20)
        at 
org.kframework.unparser.KOREToTreeNodes$.$anonfun$apply$3(KOREToTreeNodes.scala:21)
        at 
scala.collection.TraversableLike.$anonfun$map$1(TraversableLike.scala:234)
        at scala.collection.Iterator.foreach$(Iterator.scala:932)
        at scala.collection.Iterator.foreach(Iterator.scala:932)
        at scala.collection.IterableLike.foreach$(IterableLike.scala:71)
        at scala.collection.IterableLike.foreach(IterableLike.scala:70)
        at scala.collection.TraversableLike.map$(TraversableLike.scala:234)
        at scala.collection.TraversableLike.map(TraversableLike.scala:227)
        at 
org.kframework.unparser.KOREToTreeNodes$.apply(KOREToTreeNodes.scala:21)
        at 
org.kframework.unparser.KOREToTreeNodes$.$anonfun$apply$3(KOREToTreeNodes.scala:21)
        at 
scala.collection.TraversableLike.$anonfun$map$1(TraversableLike.scala:234)
        at scala.collection.Iterator.foreach$(Iterator.scala:932)
        at scala.collection.Iterator.foreach(Iterator.scala:932)
        at scala.collection.IterableLike.foreach$(IterableLike.scala:71)
        at scala.collection.IterableLike.foreach(IterableLike.scala:70)
        at scala.collection.TraversableLike.map$(TraversableLike.scala:234)
        at scala.collection.TraversableLike.map(TraversableLike.scala:227)
        at 
org.kframework.unparser.KOREToTreeNodes$.apply(KOREToTreeNodes.scala:21)
        at 
org.kframework.unparser.KOREToTreeNodes$.$anonfun$apply$3(KOREToTreeNodes.scala:21)
        at 
scala.collection.TraversableLike.$anonfun$map$1(TraversableLike.scala:234)
        at scala.collection.Iterator.foreach$(Iterator.scala:932)
        at scala.collection.Iterator.foreach(Iterator.scala:932)
        at scala.collection.IterableLike.foreach$(IterableLike.scala:71)
        at scala.collection.IterableLike.foreach(IterableLike.scala:70)
        at scala.collection.TraversableLike.map$(TraversableLike.scala:234)
        at scala.collection.TraversableLike.map(TraversableLike.scala:227)
        at 
org.kframework.unparser.KOREToTreeNodes$.apply(KOREToTreeNodes.scala:21)
        at 
org.kframework.unparser.KOREToTreeNodes$.$anonfun$apply$3(KOREToTreeNodes.scala:21)
        at 
scala.collection.TraversableLike.$anonfun$map$1(TraversableLike.scala:234)
        at scala.collection.Iterator.foreach$(Iterator.scala:932)
        at scala.collection.Iterator.foreach(Iterator.scala:932)
        at scala.collection.IterableLike.foreach$(IterableLike.scala:71)
        at scala.collection.IterableLike.foreach(IterableLike.scala:70)
        at scala.collection.TraversableLike.map$(TraversableLike.scala:234)
        at scala.collection.TraversableLike.map(TraversableLike.scala:227)
        at 
org.kframework.unparser.KOREToTreeNodes$.apply(KOREToTreeNodes.scala:21)
        at 
org.kframework.unparser.KOREToTreeNodes.apply(KOREToTreeNodes.scala)
        at org.kframework.krun.KRun.unparseTerm(KRun.java:431)
        at org.kframework.krun.KRun.prettyPrint(KRun.java:313)
        at org.kframework.krun.KRun.filterAnonVarsAndPrint(KRun.java:163)
        at org.kframework.krun.KRun.printK(KRun.java:214)
        at org.kframework.krun.KRun.run(KRun.java:107)
        at org.kframework.krun.KRunFrontEnd.run(KRunFrontEnd.java:68)
        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:265)
        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