K-user mailing list

[Christos Kloukinas <c.kloukinas AT gmail.com>]

Hi,

I'm using the latest version from github and trying to write a model 
checker for a language that allows non-deterministic assignment:
int i := 8 upto 17 ; // i gets a value in the interval [8, 17]

Currently we're translating this to Spin's select 
(http://spinroot.com/spin/Man/select.html), if this helps, which is a macro:
select (i : 8..17);
// equivalent to:
i = 8;
do
:: i < 17 -> i++
:: break // can break from the loop at any time, so all values in [8,17] 
are checked
od

(1) not sure how to write this in K. I've tried with randomInt (and 
randomRandom) but it doesn't work (kompiles fine but krun produces error 
messages about bad types...).
I modified kool-typed-dynamic.k with:
  syntax Exp ::= .... | Exp "upto" Exp         [seqstrict]    // KOOL
  rule <k> ( I1:Int upto I2:Int =>
       I1 +Int randomInt(I2 -Int I1) ) ... </k>
       requires I1 <=Int I2

Any idea why random doesn't work?

(2) I actually would much rather have a constraint on a fresh variable 
like this instead of random:
rule I1:Int upto I2:Int => !N:Int requires ?N >=Int I1 && ?N <=Int I2
The reason for preferring this rule is that I hope that such a 
constraint would allow me to do some symbolic interval computations 
instead of considering each value in the interval in isolation.
Currently it fails to reduce, since !N is 1 and the constraint fails for 
an expression like: cat random-test.kool
class Main {
  void Main() {
    int e = ( 10 upto 12 );
    print(e);
  }
}

Rule "rule I1:Int upto I2:Int => !N:Int " executes fine but N is 
assigned the value of 1.

Is there a plan to support symbolic constraints on fresh variables (or 
something that adds symbolic constraints)?
Or is there some other way to get symbolic constraints?

BTW - what's the difference between ?N:Int and !N:Int ? (any plans on 
updating the primer to help newbies? :-) )

Best,
Christos