K-user mailing list

[Everett Hildenbrandt <hildenb2 AT illinois.edu>]

Hey Christos,

I'm not sure how to get K to output the generated model, but it shouldn't 
output the solution unless it has already queried Z3 for a model to check for 
feasibility.
So it is generating a model for you, but it's not outputting it for you; 
short of hacking on K I'm not sure how to get it to output it for you.
Do you actually need a model in hand though? I would think it's enough to 
just know that the solution is feasible.

The syntax `!I` is used to generate a concrete fresh integer, so it can be 
used as a counter/nonce; it doesn't generate a symbolic value.
So what you're seeing in `test3.fresh` is `!I` gets the value 1, and `!J` 
gets the value 2.

If you don't supply the `--search` flag, K won't split execution state for 
you when a branch is hit (it will just pick one of the branches).
For your program this doesn't mean anything, but if you later had two rules 
that could apply but have non-overlapping requires clause, K will split that 
into two solutions for you and explore both.
I think K should print out the constraints anyway (even without `--search`) 
because it really is always doing symbolic execution.
As it is right now though, adding `--search` puts it into "symbolic execution 
mode" and which also starts printing out the constraints.

Everett H.

On Sat, Jun 03, 2017 at 11:59:42AM +0300, Christos Kloukinas wrote:
> 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
>