K-user mailing list

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

Hi, thanks for this, it does help!

Here's a small example I've created that shows how this might work (had 
to use ?I in the constraints as well, since it complains about unbound 
variables otherwise - added a case with !I to better understand how it 
differs from ?I):
cat fresh.k
module FRESH-SYNTAX
    syntax P ::= "freshInt" "(" Int "," Int ")" | "freshInt" | "phreshInt"
endmodule
module FRESH
    imports FRESH-SYNTAX
        rule (phreshInt => !I:Int +Int !J:Int)
        rule (freshInt => ?I:Int)
        rule freshInt(N:Int , M:Int ) => ?I:Int requires ?I >=Int N 
andBool ?I <=Int M
endmodule

cat test[123].fresh
freshInt
freshInt(2, 4)
phreshInt

kompile fresh.k && krun --bound 3 --search test1.fresh && krun --bound 3 
--search test2.fresh && krun --bound 3 --search test3.fresh
Solution 1
<k> V0 </k>
Solution 1
<k> V0 </k>
 AND ( V0 >=Int 2 ) ==K true andBool ( V0 <=Int 4 ) ==K true
Solution 1
<k> 3 </k>

So for freshInt(2, 4) it produces an integer V0 with the correct 
constraints (V0 \in [2, 4]).

But it doesn't attempt to find specific models for it with "--search" 
(without this switch it doesn't output the constraints at all).

Does anyone know if there's some way of asking it to produce models that 
satisfy these constraints?

Best,
Christos

On 03/06/2017 00:02, Everett Hildenbrandt wrote:
> 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