K-user mailing list

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

I was able to make progress on this question with the following solution 
(which I am sending to the list in case it helps someone in the future, and 
for the sake of keeping documentation).

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

  // (Mw[Z])[ (choice(keys((Mw[Z])) -Set Ss)) ]
  rule <k> load Z:Id => aux(Mw,Ss,Z) ... </k>
       <S> Ss:Set </S>
       <W> Mw:Map </W>
  syntax K ::= aux(Map,Set,Id)
             | aux2(K,Set)
             | aux3(K,K,Set)
             | aux4(K,K)
             | aux5(K,K)
  rule aux(M,S,I)     => aux2(M[I],S)                   [structural]
  rule aux2(M2,S)     => aux3(keys(M2),M2,S)            [structural]
  rule aux3(S2,M2,S)  => aux4(S2:Set -Set S, M2)        [structural]
  rule aux4(S3,M2)    => aux5(choice(S3:Set),M2)        [structural]
  rule aux5(K,M2)     => (M2:Map)[K]                    [structural]

endmodule


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