Project

General

Profile

Statistics
| Branch: | Revision:

cool / _oasis @ 2cccf57a

History | View | Annotate | Download (5.13 KB)

# Date Author Comment
2cccf57a 11/07/2017 07:32 AM Hans-Peter Deifel

Link ncurses bindings against libtinfo and libgpm

This is needed to produce static binaries.

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

Remove pgsolver dependency

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/

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

oasis: Correctly declare TCSLib dependency for pgsolver

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

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

Modularize reasoner by focus tracking strategy

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

Only iterate through open states in PG solution

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

Solve game twice to accommodate for partial games

2761a943 04/10/2017 09:03 AM Hans-Peter Deifel

Import pgsolver as git submodule

A parity game solver that will be used to solve games arising from the
full mu-calculus.

- Adds a new submodule under `vendor/` for pgsolver. Linking without
including it in the source proved difficult at the moment.
- Adds a new library `libpgsolver` to _oasis that contains the files...

256444ba 04/06/2017 05:57 PM Hans-Peter Deifel

tests: Add unit tests

Adds a whole new set of tests that don't just test the whole reasoning
process on a formula, but smaller individual functions.

Right now there are only two tests but more should follow.

fbe64bb7 04/06/2017 05:57 PM Hans-Peter Deifel

build: Add testsuite to oasis

Enables 'make test' and 'ocaml setup.ml -test' to run the testsuite.

bc28fc54 04/06/2017 05:57 PM Hans-Peter Deifel

build: Use new Makefile as generated by oasis

Adds many new targets including 'test' and 'distclean'

7451cccf 03/23/2017 11:18 AM Hans-Peter Deifel

Add comment on purpose of glpk_stub to various files

a6f9f99f 03/23/2017 11:09 AM Hans-Peter Deifel

Remove libbdd and libglpk from C linker command

Now that GMLMIP is removed, those are not needed any more. Now cool
can really be built without GMLMIPs dependencies (as is now advertised
by the INSTALL file).

7198f96f 03/22/2017 06:21 PM Hans-Peter Deifel

Enable documentation generation in oasis

Documentation can be built with: ocaml setup.ml -doc

This also fixes two documentation comments that had the wrong syntax.

c9ed384b 03/22/2017 02:09 PM Hans-Peter Deifel

Merge branch 'remove-gmlmip'

c4aee922 03/22/2017 02:05 PM Hans-Peter Deifel

Remove GMLMIP

This drops the rule implementation for GML and PML, because they were
relying on GMLMIP which complicated the build process and didn't work
completely. See Issue 19.

GML and PML are still implemented as functors but currently disabled.
To re-instantiate them, an OCaml implementation is needed.

2bda8737 03/21/2017 07:39 PM Hans-Peter Deifel

Add emacs mode lines to various files

1ecf0388 05/09/2016 04:47 PM Christoph Egger

Fix static linking

c2cc0c2e 02/05/2015 04:00 AM Thorsten Wißmann

Add basic debugging repl

c49eea11 01/22/2015 06:58 PM Thorsten Wißmann

Implement raw syntax for constant functors

8c423c7a 07/27/2014 07:43 PM Thorsten Wißmann

Add curses painting basics

c14c011a 07/27/2014 05:02 PM Thorsten Wißmann

Add basic curses and readline bindings

ab7dc651 07/20/2014 12:05 PM Thorsten Wißmann

Disable glpk_stub.c until we do not need GMLMIP anymore

d1c3e8ff 07/17/2014 01:43 AM Dominik Paulus

Port glpk_stub.c to GLPK 4.54 and add it to _oasis

Some options and functions are still missing, e.g. MILP support

3879f710 07/16/2014 01:53 PM Thorsten Wißmann

Implement parsing of complex functors

b33c1f3f 05/16/2014 07:22 PM Thorsten Wißmann

Add basic testsuite skeleton

59b6a7fd 05/05/2014 11:38 AM Thorsten Wißmann

Make if conditions in _oasis more conform

ed3a7d47 05/03/2014 04:06 PM Thorsten Wißmann

Explicitly name all internal moduls

edf5c0ed 05/03/2014 03:33 PM Thorsten Wißmann

Compile entiere GMLMIP-0.1 into cool

77125941 05/03/2014 03:12 PM Thorsten Wißmann

Move more cpp to c

21e4bb67 05/03/2014 12:50 PM Thorsten Wißmann

Use -cc g++ everywhere in oasis file

cac42fce 05/01/2014 05:09 PM Thorsten Wißmann

Add build flat for static linking

f82f09b7 05/01/2014 04:46 PM Thorsten Wißmann

Add coalgcompare frontend

7f2800d0 04/23/2014 12:37 PM Thorsten Wißmann

Add OWL frontend

7b8150bd 04/23/2014 11:33 AM Thorsten Wißmann

Improve _oasis file

7c4d2eb4 04/23/2014 11:21 AM Thorsten Wißmann

Separate cool into library and coalg frontend

0fe95cdc 04/23/2014 10:20 AM Thorsten Wißmann

Minor _oasis file cleanups

c2f74310 04/23/2014 10:04 AM Thorsten Wißmann

Make coalg build with oasis

b925131a 04/23/2014 12:34 AM Thorsten Wißmann

Make c++ sources compile with oasis

aad01c19 04/22/2014 11:58 PM Thorsten Wißmann

Add first not-yet-working _oasis