K-user mailing list

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

Hi Everett, thanks for your response!

Please see below inline.


On 03/06/2017 19:33, Everett Hildenbrandt wrote:
> 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.

Thanks! Had not realised that K is doing this, it's quite cool.
> 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.

Well, I need the model if I'm going to do model-checking - have 
something to present back to the end-user that is simpler than a long 
constraint.
*** Actually in a perfect world I'd like to have access through K to 
*both* the constraints and the model(s) of these constraints *and* be 
able to make decisions based on them, manipulate them (strengthen/weaken 
the constraints), etc.


In general I think that if the K tool is going to the trouble to 
implement such an advanced analysis technique that is quasi-magical (to 
the eyes of non-experts like myself), then it should allow users to 
access and manipulate the analysis results. Hiding these internally 
reduces the technique's utility substantially in my view - like 
preparing an amazing meal only to show me a photo of it... :-/
=> If you have it, flaunt it!!! ;-)

> 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.

?!? K only splits the search when two rules have non-overlapping 
requires? So it doesn't split when their requires are overlapping/are 
the same?
This is biting me - I'm trying at the same time to implement a 
non-deterministic choice based on the concrete values in the interval 
like Spin, so as to have the ability to get a model without going 
through the SMT constraints.
I've written this code (which works for K 3.6 - having trouble with 4.0...):

  syntax Exp ::= Int | Bool | String | Id
               | "this"                                 // KOOL
               | "super"                                // KOOL
               | "(" Exp ")"             [bracket]
               | Exp "upto" Exp         [seqstrict]  // **** interval ****
               | "++" Exp
               | ....
  syntax Id ::= "$upto"
  /*(1)*/ //@ Base case - interval of a single point:
  rule <k> (N:Int upto N => $upto) ... </k>
       <upto>... .Set => SetItem(N) ...</upto>
  /*(2)*/ //@ General case for N < M, early stop at N (introduces a 
non-deterministic choice for ending the evaluation early, to allow 
searching all values in the interval):
  rule <k> (N:Int upto M:Int) => ($upto) ... </k>
       <upto>... .Set => SetItem(N) ...</upto>
      requires N <Int M
  /*(3)*/ //@ General case for N < M, advances to N+1:
  rule <k> (N:Int upto M:Int) => ((1 +Int N) upto M) ... </k>
       <upto>... .Set  => SetItem(N) ...</upto>
       requires N <Int M
  /*(4)*/ //@ Pick a value from the interval [N upto M]:
  //** K 4.0 version - doesn't work in K 3.6 because sets have no 
"choice". Choice always picks the minimum element! :-(
  // rule <k>(($upto) => (choice(Upto))) ...</k>
  //      <upto>Upto:Set => .Set </upto>
  //** K 3.6 version - doesn't work in K 4.0! krun barfs with errors... :-(
  rule <k>($upto => I) ...</k>
       <upto> (SetItem(I:Int) Rest:Set) => .Set </upto>


Rule (1) is the base case for [N upto N] - stores N into the 
thread-local cell upto.
Rule (4) "picks" a number from the set in cell upto (*always* picks the 
minimum member... :-( would have loved if it could split here on the 
different set members when searching!) and deletes the set's contents so 
that the thread can evaluate another interval.
Rule (3) adds another number into the set, advancing N for [N upto M] 
when N < M.
And Rule (2) tries to introduce a split point so that the search for a 
member can end at any point in the interval - also with a requires 
clause of N < M like rule (3).

K 3.6 does not do any splitting at all here - it behaves exactly as if 
rule (2) was missing.
How can I add a splitting point in there, to ask K to try both rules (2) 
& (3) when searching?

I'm quite stuck here - using constraints I cannot get a model and using 
the concrete values I cannot get K to split on them... :-(

Notes:

a) K 4.0 krun barfs with errors on rule (4) when using the version of K 3.6.

b) For some crazy reason, K 4.0 works sometimes with its own version of 
rule (4) - the one commented out that uses "choice" - and barfs in other 
cases (on the same input file) - I must have hit upon some very nasty 
bug in the implementation there !!!

I'm attaching the versions I've got for both K 3.6 & K 4.0 in case they 
can help identify the bug in K (or in my rules that drive K 4.0 nuts). 
My changes to Kool are where "upto" appears.
Hope the zip file does not get removed from the list - if it gets 
removed and someone wants it, please email me directly.
Its contents are:
$ unzip -l unroll-kool.zip
Archive:  unroll-kool.zip
  Length      Date    Time    Name
---------  ---------- -----   ----
    29608  06-04-2017 13:15   unroll-kool-3.6/kool-typed-dynamic.k
    32611  06-04-2017 13:14   unroll-kool-4.0/kool-typed-dynamic.k
       65  06-04-2017 01:27   unroll-kool-3.6/unroll-upto-3_3.kool
       87  06-04-2017 02:59 
unroll-kool-3.6/unroll-upto-3_5-plus-upto-6_9.kool
       88  06-04-2017 03:46   unroll-kool-3.6/unroll-upto-3_5.kool
       65  06-04-2017 02:03   unroll-kool-3.6/unroll-upto-5_3.kool
       65  06-04-2017 01:27   unroll-kool-4.0/unroll-upto-3_3.kool
       87  06-04-2017 02:59 
unroll-kool-4.0/unroll-upto-3_5-plus-upto-6_9.kool
       88  06-04-2017 03:46   unroll-kool-4.0/unroll-upto-3_5.kool
       65  06-04-2017 02:03   unroll-kool-4.0/unroll-upto-5_3.kool
---------                     -------
    62829                     10 files


Sorry for the long email...

Best,
Christos

> 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

Attachment: unroll-kool.zip
Description: Zip archive