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

1a213985 09/27/2017 01:02 AM Kristin Braun

added translation for Const

78ab3383 09/19/2017 11:10 PM Hans-Peter Deifel

oasis: Correctly declare TCSLib dependency for pgsolver

bc0691dc 08/10/2017 12:48 PM Kristin Braun

translation only uses subformulas if their negation is not a subformula

2d58f46f 07/18/2017 11:16 AM Kristin Braun

added optimized translation

97b76edf 06/29/2017 05:03 PM Kristin Braun

deleted conjunction

d5e292c6 06/20/2017 09:28 PM Kristin Braun

nom2fix and solveNom

946e8213 06/20/2017 07:41 PM Kristin Braun

translation from nominal to EG AF works for K

2da28579 06/20/2017 05:50 PM Kristin Braun

added VAR to patternmatching

def3763d 06/19/2017 01:18 PM Kristin Braun

Translation for K

e3cf4ca2 05/16/2017 07:39 PM Kristin Braun

translation calculates fisher ladner closure correctly

267e3fcf 05/16/2017 02:03 PM Kristin Braun

.

89613c41 05/11/2017 03:52 PM Kristin Braun

tried to use Fischer-Ladner Closure but not working yet

0f9140ab 05/04/2017 04:06 PM Kristin Braun

part 1 and 3 of translation

a91110f4 05/03/2017 03:47 PM Kristin Braun

first part of translations is implemented

3cd07e5d 05/03/2017 03:26 PM Hans-Peter Deifel

Replace String.split_on_char with custom implementation

String.split_on_char was introduced in OCaml 4.04, but we want to
support 4.02.

7776135e 04/22/2017 12:52 AM Hans-Peter Deifel

Move verifyFormula after simplification

a60f4851 04/21/2017 11:16 PM Hans-Peter Deifel

Enforce aconjunctivity globally

In the future, we would need a switch for that

867cefeb 04/21/2017 10:24 PM Hans-Peter Deifel

Add script to generate test formulas

- gen.ml: Generates a specific set of formulas, usable for
benchmarking cool against pgsolver

64adaa3d 04/21/2017 10:23 PM Hans-Peter Deifel

Disable debug output

2400280e 04/21/2017 10:23 PM Hans-Peter Deifel

Fix alternation level computation

c6fcba65 04/21/2017 10:22 PM Hans-Peter Deifel

Disable backjumping for now

acd285b4 04/21/2017 02:10 PM Hans-Peter Deifel

Temporarily add some debug output

ac55ab4a 04/21/2017 02:10 PM Hans-Peter Deifel

Fix priority for empty foci

83e87153 04/21/2017 11:43 AM Hans-Peter Deifel

Swap priorities of partial permutations

Since the automaton must be complemented, our priorities have to be
just the other way round.

e3905995 04/21/2017 11:39 AM Hans-Peter Deifel

Include priority of nodes in dot output

af2f4755 04/21/2017 11:39 AM Hans-Peter Deifel

Correctly add new formulas if deferral changes

6054c1ec 04/21/2017 08:25 AM Hans-Peter Deifel

Enable new focus tracking by default

- In the future this should only happen if the formula is not
alternation free, but aconjunctive (or via a cli-switch)

a2b07f24 04/21/2017 08:17 AM Hans-Peter Deifel

Fix a few bugs with the new focus tracker

f4bfec73 04/21/2017 12:20 AM Hans-Peter Deifel

Actually use depth first tracking

e3a4d293 04/21/2017 12:05 AM Hans-Peter Deifel

Implement depth-first tracking for deferral sets

9b05e638 04/21/2017 12:04 AM Hans-Peter Deifel

Initialize arrayAlternationLevel

was accidentally left uninitialized

65e44e2d 04/20/2017 11:45 PM Hans-Peter Deifel

First try at depth first tracking

6bfe1352 04/20/2017 06:28 PM Hans-Peter Deifel

Properly calculate priority for partial permutations

- Compute n based on the size of the Fischer-Ladner-Closure and
maximum alternation depth of the input formula
- Handle the case where no formula has been removed or is active

5a7548b8 04/20/2017 06:18 PM Hans-Peter Deifel

Calculate and save alternation depth of input formula

6c039e3a 04/20/2017 04:24 PM Hans-Peter Deifel

Implement equality and hashing for partial permutations

dc5d9271 04/20/2017 03:44 PM Hans-Peter Deifel

First implementation of tracking for partial permutation

d517658d 04/20/2017 03:44 PM Hans-Peter Deifel

Expose computed alternation level for other modules

cd0ce0b5 04/20/2017 08:25 AM Hans-Peter Deifel

Calculate alternation level for every formula

38828d40 04/19/2017 05:16 PM Hans-Peter Deifel

Actually used polymorphic focus tracking

af6ede09 04/19/2017 09:16 AM Hans-Peter Deifel

Modularize reasoner by focus tracking strategy

a2ec2dfc 04/14/2017 11:22 AM Hans-Peter Deifel

Set states without children to Sat early

We can set states without children to Sat right after we expand them.

afeec2f2 04/14/2017 11:19 AM Hans-Peter Deifel

Correctly represent root Core in parity games

In the two games we solve, expandable cores are represented either as
themselves or as the successful node. Unfortunately the root node was
always represented as itself, leading to wrong results. This is now
fixed.

dd1db59c 04/13/2017 11:36 AM Hans-Peter Deifel

Change game algorithm from Stratimprlocal2 to Stratimprlocal

As the former is not deterministic

1717d534 04/13/2017 11:35 AM Hans-Peter Deifel

Add a single satisfiable game node to states without children

b1e625e9 04/13/2017 01:01 AM Hans-Peter Deifel

Only iterate through open states in PG solution

aa97b631 04/12/2017 06:34 PM Hans-Peter Deifel

Remove last call to propagateUnsatMu

30668fd9 04/12/2017 01:46 PM Hans-Peter Deifel

Keep node mapping to parity game on the fly

0dd1f4ca 04/11/2017 07:56 PM Hans-Peter Deifel

Don't set all expandable cores to unsat

namely those that have children

3800543c 04/11/2017 07:48 PM Hans-Peter Deifel

Solve game twice to accommodate for partial games

2e9e42f2 04/10/2017 09:07 AM Hans-Peter Deifel

WIP: First steps towards using pgsolver

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

Also available in: Atom