Project

General

Profile

Revision:

Revisions

# Date Author Comment
a80babbf 11/16/2017 11:13 AM Hans-Peter Deifel

benchmarks: Rename gen.ml to aconjunctive_mu_generator.ml

Also disables the build of the corresponding executable by
default (can be reenabled with the flat 'benchmarks').

42f17c7e 11/07/2017 08:04 AM Hans-Peter Deifel

makestatic.sh: Add 'gen' binary for acmu benchmarks

4caf8f04 11/07/2017 07:59 AM Hans-Peter Deifel

makestatic.sh: Include benchmarks for aconjunctive mu

2357f98f 11/07/2017 07:59 AM Hans-Peter Deifel

benchmarks: Add README

2cccf57a 11/07/2017 07:32 AM Hans-Peter Deifel

Link ncurses bindings against libtinfo and libgpm

This is needed to produce static binaries.

80e49b79 11/02/2017 06:52 PM Hans-Peter Deifel

Revert "Update INSTALL file to reflect current state"

This reverts commit 5de20a335bdf0e0c5e7b940fe69952963720b1cd.

Wrong branch...

5de20a33 11/02/2017 06:47 PM Hans-Peter Deifel

Update INSTALL file to reflect current state

Since pgsolver is now a dependency and is not available in common
Linux distributions, we advise people to install all ocaml
dependencies with opam instead.

0655be7e 11/02/2017 06:11 PM Hans-Peter Deifel

benchmarks: Correctly parse output with REPEATS=1

In this case, no stddev is generated

6c3793cb 10/20/2017 07:09 PM Hans-Peter Deifel

benchmarks: Fix early_caching_ac formula

db56eb9d 10/20/2017 06:25 PM Hans-Peter Deifel

benchmarks: Add early_ac formulae to generator

42e43efd 10/19/2017 11:32 PM Hans-Peter Deifel

benchmarks: Ignore temporary files when collecting statistics

221a3816 10/19/2017 09:43 PM Hans-Peter Deifel

benchmarks: Set final TIMEOUT and REPEATS parameters

cf05f9f8 10/19/2017 09:42 PM Hans-Peter Deifel

benchmarks: Run mlsolver with -pgs stratimprloc2

f498e556 10/19/2017 07:31 PM Hans-Peter Deifel

benchmarks: Fork a subshell for mlsolver

Otherwise, 'perf stat' returns a zero exit code if mlsolver is killed
by a signal (e.g in case of an OOM situation)

a43cb4c2 10/19/2017 05:27 PM Hans-Peter Deifel

benchmarks: Distribute results over different directories

Allows benchmarks of two formula series to be performed in parallel
without interfering with each other.

63177472 10/19/2017 05:01 PM Hans-Peter Deifel

benchmarks: Add visual progress feedback

cf5e561d 10/19/2017 04:27 PM Hans-Peter Deifel

benchmarks: Add script to run 'bench_one_formula' on all formulas

775ab65f 10/19/2017 04:26 PM Hans-Peter Deifel

benchmarks: Output numbers with leading zeros

Some csv tools can only sort lexicographically

7a044d56 10/19/2017 04:26 PM Hans-Peter Deifel

benchmarks: Save full 'perf stat' output

who knows if we might need it

10b7fc02 10/19/2017 04:25 PM Hans-Peter Deifel

benchmarks: Set locale to C

This ensures that decimal separators are consistent.

ec2caa83 10/19/2017 10:23 AM Hans-Peter Deifel

benchmarks: Allow to have multiple directories with benchmark results

4b369edd 10/19/2017 10:21 AM Hans-Peter Deifel

benchmarks: Add script to collect results into CSV format

6d28c445 10/19/2017 10:20 AM Hans-Peter Deifel

benchmarks: Save output of programs

Allows to collect other results than just the time. For example how
many states the game has and what the result was (sat/unsat).

3fd00cf1 10/19/2017 10:19 AM Hans-Peter Deifel

benchmarks: Add cool with pgsolver support to matrix

45386aae 10/19/2017 07:56 AM Hans-Peter Deifel

Fix typo

8c274b5b 10/18/2017 11:17 PM Hans-Peter Deifel

benchmarks: Add cool without propagation

eb9bb469 10/18/2017 10:38 PM Hans-Peter Deifel

benchmarks: Add mlsolver with optimizations to tested programs

e442d62b 10/18/2017 10:28 PM Hans-Peter Deifel

benchmarks: Switch mlsolver to 'recursive' strategy

e412454f 10/18/2017 08:48 PM Hans-Peter Deifel

Make propagation rate configurable with command line flag

Adds the parameter --propagationRate

6b7a66a8 10/18/2017 07:36 PM Hans-Peter Deifel

Cache maximum priority of all nodes in graph

So it doesn't have to be recomputed for each propagation.

Unfortunately this optimization doesn't seem to make a difference for
the formulas I tested, but it doesn't hurt either.

f1eb4f7c 10/18/2017 09:17 AM Hans-Peter Deifel

Add argument checking to benchmark script

a06d5cea 10/18/2017 09:12 AM Hans-Peter Deifel

Add benchmark script to compare cool and mlsolver

dacb681b 10/18/2017 08:12 AM Hans-Peter Deifel

Remove pgsolver dependency

e765822b 10/17/2017 11:28 PM Daniel Hausmann

Implement own parity game solver

Instead of relying on pgsolver for this task.

3e877781 10/17/2017 10:53 PM Hans-Peter Deifel

Use pgsolver from opam instead of bundling it

Simplifies the installation process and allows to compare performance
with other tools that use the same pgsolver version.

994d7911 10/15/2017 05:05 PM Hans-Peter Deifel

Move aconjunctive formula generator to benchmarks/

77f7da85 10/15/2017 05:01 PM Daniel Hausmann

Add more formula families to gen.ml

682787c5 10/13/2017 10:22 PM Hans-Peter Deifel

generator: Rename formula families to something descriptive

b078517b 10/13/2017 10:14 PM Hans-Peter Deifel

Fix printing of modality of the identity functor

88a1a18b 10/13/2017 10:12 PM Hans-Peter Deifel

phi generator: Use identity modality for phi

As this speeds things up quite a bit.

fdfe3dcc 10/13/2017 06:39 PM Hans-Peter Deifel

phi generator: Add another formula family

69962164 10/13/2017 05:11 PM Hans-Peter Deifel

CoAlgMisc: Store fixpoint variable name for every deferral

This is only useful for debugging and currently not used anywhere in
the code.

467e8bbc 10/13/2017 05:03 PM Hans-Peter Deifel

phi generator: Generalize command line syntax

Allows for more variations of the formula and also is a little bit
more self-documenting.

97d89f3f 10/11/2017 10:53 PM Hans-Peter Deifel

Remove unused code

9cab822e 10/10/2017 11:52 PM Hans-Peter Deifel

Fix apply for the partial permutation tracker

- Apply all indices in the map, not only the currently tracked ones.
- Apply Stars in the same way as regular formulas

c9dbb509 10/10/2017 11:31 PM Hans-Peter Deifel

Add negation to generator for phi

7915d13f 10/10/2017 11:30 PM Hans-Peter Deifel

Fix formula generator for positive phi

3dc07cf8 10/10/2017 09:34 PM Hans-Peter Deifel

Fix bug in detClosure

ae7e01ca 10/09/2017 06:45 PM Hans-Peter Deifel

gen.ml: Change quantification order

1d36cd07 10/06/2017 09:06 PM Kristin Braun

Tried to optimize translation with fixpoint approximation; added depthFormula function in CoAlgFormula

(1-50/638) Per page: 25, 50, 100

Also available in: Atom