Skip to Content.
Sympa Menu

k-user - Re: [[K-user] ] non-deterministic ("random" ?) choice vs symbolic constraints on fresh variables

k-user AT lists.cs.illinois.edu

Subject: K-user mailing list

List archive

Re: [[K-user] ] non-deterministic ("random" ?) choice vs symbolic constraints on fresh variables


Chronological Thread 
  • From: Christos Kloukinas <c.kloukinas AT gmail.com>
  • To: Everett Hildenbrandt <hildenb2 AT illinois.edu>
  • Cc: k-user AT lists.cs.illinois.edu
  • Subject: Re: [[K-user] ] non-deterministic ("random" ?) choice vs symbolic constraints on fresh variables
  • Date: Sat, 10 Jun 2017 14:24:12 +0300
Hi, I've tried to run the example here that looked to me as if it's extracting a model from the SMT prover: k/k-distribution/tests/regression/java-rewrite-engine/smt_model/


The most recent version of K kompiles test.k but when I try to krun program.test it crashes :-(

$ krun program.test
(error "line 2 column 31: unknown sort 'Int@INT-SYNTAX'")
com.microsoft.z3.Z3Exception: parser error
at com.microsoft.z3.Native.parseSmtlib2String(Native.java:3052)

Any ideas on what the problem is? Should I be looking elsewhere in the distribution for an example of how to extract a model from the SMT engine?


Best,

Christos

P.S. I've finally managed to get the non-deterministic choice work with plain values - I had to label the rules with [transition]:

syntax Exp ::= "$upto" // K3.6 accepts Id ::= "$upto" but K 4.0's krun crashes with it - a bug?
/*(2)*/ //@ Base case AND 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>ASet:Set => SetItem(N)</upto>
requires N <=Int M [//uptonow1,
transition]
/*(3)*/ //@ General case for N < M, advances to N+1:
rule <k> (N:Int upto M:Int) => ((1 +Int N) upto M) ... </k>
<upto>ASet:Set => SetItem(N)</upto>
requires N <Int M [//uptonow2,
transition]
/*(4)*/ //@ Pick a value from the interval [N upto M]:
rule <k>($upto => I) ...</k>
<upto> (SetItem(I:Int) Rest:Set) => .Set </upto>

Note: The set inside <upto></upto> holds at most one element.

On 04/06/2017 13:32, Christos Kloukinas wrote:
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



Archive powered by MHonArc 2.6.19.

Top of Page