Project

General

Profile

Statistics
| Branch: | Revision:

cool @ master

# Date Author Comment
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

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.

e919f880 04/06/2017 05:58 PM Hans-Peter Deifel

Merge branch 'aconjunctive'

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

Add command line flag for fragment

The user can now choose which fragment of the mu-calculus the reasoner
uses. More specialized fragments can have better performance
characteristics.

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

Add tests for command line option parser

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

Generalize command line argument parsing

Adds a new module CoolUtils.Args that implements a generic command
line argument parser. This makes it easier to add new options to the
main program.

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

coalg: Make 'graph' subcommand more cli-friendly

- Read only one formula, we also only generate one graph
- Don't print a prompt or the satisfiability result

This allows to redirect the output graph to a file or directly to dot.

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

tests: Add dividing example for aconjunctive fragment

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

Document tests in HACKING file

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'

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

tests: Don't use exit status 0 if tests failed

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

Fix aconjunctive fragment for rules with >1 children

Previously, the algorithm for the aconjunctive fragment would insert
many cores for each child of a modal rule and add those as children of
the rule application to the state.

This was wrong for multiple reasons:...

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

Add CoolUtils.TList.combinations function

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

Makefile: Add doc target to generate documentation

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

tests: Print summary for failed tests at the end

Makes it easier to find failing formulas for further fine-grained
analysis.

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

tests: Add example where new Algorithm should fail

This formula is not aconjunctive and should be wrongly declared as
satisfiable by the algorithm that assumes aconjunctivity.

This doesn't work right now: The new algorithm also answers with
"unsat".

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

Don't hardcode check for aconjunctive formulas

Previously, cool would simply raise an exception if the formula was
not aconjunctive. This was done to ease testing of the new reasoner
algorithm.

Now, the reasoner decides whether the formula is aconjunctive or not...

bc706b79 04/06/2017 05:56 PM Hans-Peter Deifel

Add test cases for aconjunctive fragment

This fails currently, because the check for aconjunctivity is
currently hard coded, ruling out all formulas that aren't
aconjunctive.

e7aaefa9 04/06/2017 05:56 PM Hans-Peter Deifel

Specialize deferral tracking for aconjunctive fragment

For the aconjunctive fragment, we replace the generation of a single
core with all tracked deferrals by the generation of multiple cores,
each annotated with a single deferral from the above set.

fdda99d4 04/06/2017 05:56 PM Hans-Peter Deifel

Add check for aconjunctive formulas

31038432 03/31/2017 12:00 PM Kristin Braun

.

966e1556 03/27/2017 08:42 PM Kristin Braun

nom2EA function compiles

0fe522e0 03/27/2017 08:10 PM Kristin Braun

implemented nom2fix function

8d9a2669 03/27/2017 08:48 AM Hans-Peter Deifel

Add vim modelines to more files

8c810657 03/27/2017 08:36 AM Hans-Peter Deifel

tests: Throw error if child doesn't return 0 or 1

0 and 1 are used for Sat and Unsat respectively. But if the child
throws an exception, another exit status is returned which the parent
now recognizes.

ad0b75b1 03/26/2017 09:29 AM Hans-Peter Deifel

tests: Run reasoner in new process for each formula

As it stands, cool leaks tons of memory with each `isSat` call. Until
this is fixed, the new `--slow` testsuite would need at least 16GB of
memory if all formulas are decided in one process. Thus, we now call...

b002efa8 03/26/2017 09:29 AM Hans-Peter Deifel

Add lots of test cases for CTL.

This imports some of the quickly decidable ctl comparision benchmark
formulas into the test suite.

The testsuite also gained a --slow parameter, that enables slower (but
still fairly fast) formulas.

860b962a 03/23/2017 02:59 PM Kristin Braun

Tried to implement a translation

200774f4 03/23/2017 01:26 PM Kristin Braun

added EAFormula

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.

6c61df45 03/22/2017 04:56 PM Hans-Peter Deifel

Advertise 'graph' command of command line interface

83612ae5 03/22/2017 04:54 PM Hans-Peter Deifel

debugger: Stop and print result if reasoner finishes

The 'step' command takes an optional repeat count. Now it stops
stepping and prints the result if the reasoner finishes before
reaching the specified number of steps.

86c2c2ee 03/22/2017 04:54 PM Hans-Peter Deifel

Prettify graphviz output

- Use more readable colors and proper spacing
- Differentiate between cores and states by shape
- Add a legend
- Teach debugger to optionally write graph to file instead of stdout

5f1ec830 03/22/2017 04:54 PM Hans-Peter Deifel

Add UTF-8 "Micro Sign" as syntax for 'mu'

This is easier to type with a standard compose key as opposed as the
arguably more correct "Greek Small Letter Mu".

371cb823 03/22/2017 04:54 PM Hans-Peter Deifel

Perform sat propagation in debugger step

Otherwise, the debugger would report the reasoner result to be "Sat"
when it should really be "Unsat".

bbd5d2db 03/22/2017 04:54 PM Hans-Peter Deifel

Fix command line argument check in debugger

Also shows the correct binary name in the usage output.

3a374ca4 03/22/2017 04:54 PM Hans-Peter Deifel

Whitespace fixes

cf70b199 03/22/2017 04:54 PM Hans-Peter Deifel

Show correct binary name in "Usage" of main program

e928d370 03/22/2017 04:52 PM Hans-Peter Deifel

Improve 'verify' subcommand of main program

- Show a prompt before each input.
- Don't die if the verification of a formula fails. Show an error
instead and accept the next input.

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

Merge branch 'remove-gmlmip'

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

Disable all testcases involving PML

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

Remove GMLMIP from INSTALL file

It's not needed any more

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

Replace Array.exists by Array.fold_left

Array.exists is only available since OCaml 4.03.0 and we need to
support version at least version 4.02.3.

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.

a57eb439 03/21/2017 09:12 PM Hans-Peter Deifel

Add vim modeline to all OCaml files

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

Add emacs mode lines to various files

b81e4887 03/21/2017 05:00 PM Hans-Peter Deifel

Fix whitespace

9631d5b7 03/18/2017 12:13 PM Kristin Braun

added nom2fix method

7eb41195 03/17/2017 12:11 AM Hans-Peter Deifel

Fix another compiler warning

This fixes the warning "the label idx is defined in both types state
and core." by renaming the label to idxS and idxC respectively.

885cc0df 03/16/2017 11:16 PM Hans-Peter Deifel

Add .merlin file to gitignore

This is generated by the editor completion framework called merlin:
https://github.com/ocaml/merlin

e0e6eb62 03/16/2017 11:15 PM Hans-Peter Deifel

Fix a few compiler warnings

9fdc9f4d 03/16/2017 07:08 PM Hans-Peter Deifel

Get testsuite running again

Fixes the syntax of all tests that use R and B as identifiers, which
are keywords now.

Also disables all tests involving nominals as they are currently all
throwing exceptions.

3c42e3f1 03/16/2017 07:08 PM Hans-Peter Deifel

Fix testsuite for K

R and B are now keywords and were used as identifiers. Now, r and
b (lowercase) is used instead in the testcases. For consistency, all
other identifiers were lowercased, too.

9352b45f 03/16/2017 07:08 PM Hans-Peter Deifel

Fix compilation of gmlmip with newest ocaml

The CAMLparam0() macro must be invoked at the beginning of a function
that has local variables.

fb402b0e 03/16/2017 07:00 PM Hans-Peter Deifel

Merge branch 'flatmu'

74870253 05/23/2016 01:28 AM Christoph Egger

Create random coalition for ATL operators

7d83cfb6 05/23/2016 01:28 AM Christoph Egger

use correct modal operator for ATL

07402362 05/21/2016 03:50 AM Christoph Egger

Consider also other modal operators as valid guards

edfbcc2b 05/14/2016 11:50 PM Christoph Egger

Fix deferral tracking for new CoalitionLogic code

3e2aa1b8 05/14/2016 10:16 PM Christoph Egger

Remove A( ψ R φ) as it's not supported by all CTL reasoners

d0628bb9 05/14/2016 10:16 PM Christoph Egger

fix generation for CTL

2a36974b 05/14/2016 10:16 PM Christoph Egger

Revert to fresh variable names in convertToMu

becb9ab2 05/14/2016 05:27 AM Christoph Egger

Allow creating ATL formulae in randmu

e01c4a03 05/14/2016 05:10 AM Christoph Egger

Merge remote-tracking branch 'origin/master' into flatmu

e08cd8a9 05/12/2016 05:33 PM Christoph Egger

Fix deferral tracking when "empty" least fixpoints appear

60d2d6aa 05/12/2016 04:23 PM Christoph Egger

Add support for creating CTL formulae

23f1d0e0 05/12/2016 04:23 PM Christoph Egger

Extra parens in generated formulae

Makes them not only intended alt-free but also parsed to something alt-free

c126d689 05/12/2016 04:20 PM Christoph Egger

Fix states with no children

bc8db289 05/12/2016 02:01 PM Christoph Egger

actually verify properties for sat target

de13bc0f 05/10/2016 10:02 AM Christoph Egger

Unify CTL variable name for more global caching

eff3ff0c 05/10/2016 03:07 AM Christoph Egger

make HashConsing accept ¬Var ≡ Var

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

Fix static linking

39c9b648 05/06/2016 05:02 PM Christoph Egger

Enforce monotonicity

3b329210 05/06/2016 04:50 PM Christoph Egger

Also create mlsolver-compatible versions

4eab42c3 05/04/2016 02:04 PM Christoph Egger

Add tool to generate random μ-calculus formulas

52f5465c 04/28/2016 04:13 PM Christoph Egger

Add deferral tracking for Identity

a670c5fd 04/28/2016 04:09 PM Christoph Egger

Add deferral tracking for Fusion

f40cc23c 04/28/2016 04:06 PM Christoph Egger

Add deferral tracking for Choice

40a714df 04/28/2016 03:58 PM Christoph Egger

Add deferral tracking to CoalitionLogic

f4e43751 04/27/2016 07:42 PM Christoph Egger

Add Monotone neighbourhood logic

0debe698 04/19/2016 08:07 PM Christoph Egger

Rewrap some code to fit into 90 chars width

6aa0e444 04/19/2016 08:07 PM Christoph Egger

Only deallocate solver for unsat nodes

We want to still have the solver for naive unsat propagation

e0906550 04/19/2016 06:34 PM Christoph Egger

Remove debug output