K-user mailing list

[Everett Hildenbrandt <hildenb2 AT illinois.edu>]

Hello,

The syntax with the question mark `?` produces a fresh existentially bound 
variable, so that is what you want.

```k
    rule freshInt => ?I:Int
```

You can add constraints to it as well:

```k
    rule freshInt(N, M) => ?I:Int requires I >=Int N andBool I <=Int M
```

Manipulating the constraints directly may be challenging though, I'm not 
entirely sure how to do that.
I know that there is a way to at least get the engine to print out 
constraints (usually it just prints out structural information about the 
state, without the added constraints).

Perhaps someone who knows how to print/manipulate the constraints directly 
can chime in.

If you want to reason about them using interval arithmetic (or some other 
decision methods), you may have to "hold" the constraints yourself.
You're always free to define your own data-structures for managing 
constraints and put all your own reasoning about them in yourself.
This won't be as efficient as handing the constraint reasoning to an SMT 
solver (eg. dReal) directly though.

```k
    syntax IntInterval ::= "[" Int "," Int "]"
                         | IntInterval "+IntInterval" IntInterval [function]
                         | ...

   rule [ I1 , I2 ] +IntInterval [ I3 , I4 ] => [ I1 +Int I3 , I2 +Int I4 ]
   ...
```

Does this help?
Everett H.

On Fri, Jun 02, 2017 at 04:25:36PM +0300, Christos Kloukinas wrote:
> 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