Dienstag, 4. Dezember 2012

How to run Alloy from the command line

I've recently started evaluating my Alloy models by script. This is a challenge, because Alloy does not offer simple command line parameters in order to be run from promt. However, there is a way, and Felix Chang tells us:
You can invoke it like this: (it will execute every command
in every Alloy file you specified, and if an assertion
has a counterexample, it will show the values of every sig
and every relation in that counterexample)
Here's a sample promt:
java -cp alloy4.jar edu.mit.csail.sdg.alloy4whole.ExampleUsingTheCompiler file1.als file2.als
And the same thing for Alloy 4.2:
java -cp alloy4.2-rc.jar edu.mit.csail.sdg.alloy4whole.ExampleUsingTheCompiler file1.als file2.als
This is actually a different program and it's important to account for the differences.

Mittwoch, 28. November 2012

How to build Z3 for Linux (for non-roots)

Now, suppose you are a normal user without root and you would like to run Z3 on Linux. How should you go about it? This blog posts documents what worked for me and I hope it will for you, too.

Set up a place for Z3 to be downloaded and built:
cd ~  # change to home folder
mkdir repositories  # create a folder called "repositories"
cd repositories  # go there
Once we are there, we can basically follow the readme instructions:
git clone https://git01.codeplex.com/z3  # downloads z3 source code
autoconf
./configure
python scripts/mk_make.py
cd build
make
The last step is setting execute permissions on Z3:
chmod 751 z3
That's it! Now you can run Z3 from this path. Try it now:
~/repositories/z3/build/z3 -version

Montag, 19. November 2012

Verifiying proofs with Z3

The Z3 theorem prover has a command for constructing proofs: (get-proof). The resulting files are not meant "for human consumption" and you can probably see why:

unsat
((set-logic <null>)
(proof
(let ((@x41 (monotonicity (rewrite (= (<= 2 a) (>= a 2))) (= (not (<= 2 a)) (not (>= a 2))))))
(let (($x19 (<= 2 a)))
(let (($x20 (not $x19)))
(let ((@x26 (monotonicity (rewrite (= $x19 $x19)) (= $x20 $x20))))
(let ((@x27 (trans (rewrite (= (< a 2) $x20)) @x26 (= (< a 2) $x20))))
(let (($x7 (< a 2)))
(let ((@x29 (mp (mp (|and-elim| (asserted (and (> a 3) $x7)) $x7) @x27 $x20) @x26 $x20)))
(let ((@x42 (mp (mp (mp @x29 (|rewrite*| (= $x20 $x20)) $x20) @x26 $x20) @x41 (not (>= a 2)))))
(let (($x39 (>= a 2)))
(let (($x15 (not (<= a 3))))
(let ((@x18 (mp (|and-elim| (asserted (and (> a 3) $x7)) (> a 3)) (rewrite (= (> a 3) $x15)) $x15)))
(let ((@x64 (|unit-resolution| ((_ |th-lemma| arith farkas 1 1) (or $x39 (<= a 3))) (mp @x18 (|rewrite*| (= $x15 $x15)) $x15) $x39)))
(|unit-resolution| @x64 @x42 false)))))))))))))))
Looking good, right? Well, hardly.
Even with nicer formatting, line breaks, etc. the proof is not quite readable. Now, it looks like people have actually managed to work with these proofs and I'm quite curious about how they accomplished that. There is a description of all the symbols used in the proof, but what I'm lacking is some kind of command line parameter which simply feeds the proof back into Z3.

If I ever find one (or build one), I'll write down here.