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, 3 Jun 2017 11:59:42 +0300

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