K-user mailing list

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

oops, last minute edit to the email caused a confusing typo.

The $x was in this line here:
>  rule <k> load Z:Id => $x </k>

As opposed to 
>  rule <k> load Z:Id => Mw[Z] </k>

Thanks,

Daniel


> On 15 Feb 2017, at 12:51, Daniel Schnetzer Fava 
> <danielsf AT ifi.uio.no>
>  wrote:
> 
> 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