| Branch: | Revision:

cool / src @ 1d36cd07

# 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.

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

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

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.

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

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

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

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

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

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

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

Enable documentation generation in oasis

Documentation can be built with: ocaml -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

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


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

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.

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.

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

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

Revert to fresh variable names in convertToMu

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

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

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

54c89878 04/19/2016 06:32 PM Christoph Egger

Only remove solver after Unsat Propagation

9f1263ec 04/19/2016 10:30 AM Christoph Egger

Deallocate satsolver once core becomes `Open`

The satsolver is reatined and only updated with new clauses for every
state that is generated out of a core. Once the core becomes Open (as
opposed to expandable), the solver is no longer needed.

This patch makes the solver a `Solver option` and gets it deallocated...

dce4e4aa 04/18/2016 07:09 PM Christoph Egger

Use proper number of open States when calculating frequency

Instead of some calculation based of finishing on normal Cores really
count proper Open States

4f821479 04/14/2016 06:37 PM Christoph Egger

substract number of finishing/Sat nodes when calculating propagation frequency

1c26e356 04/14/2016 06:30 PM Christoph Egger

Remove nominal propagation for now

55dc0a64 04/14/2016 06:18 PM Christoph Egger

Make number of waves between propagation depend on #openCores

61c5af02 04/14/2016 05:53 PM Christoph Egger

Do propagation only after 100 iterations

07c71f1c 04/14/2016 05:44 PM Christoph Egger

Add comment

31229254 04/14/2016 04:23 PM Christoph Egger

Do both sat and unsat propagation

9c174a95 04/14/2016 04:13 PM Christoph Egger

Remove debug output from propagateSatMu

e4faff97 04/13/2016 11:43 PM Christoph Egger

Do a final propagation round at the end

012c092c 04/13/2016 10:18 PM Christoph Egger

Obvious simplification

8ab82480 04/13/2016 10:07 PM Christoph Egger

Fix typo in propagateUnsatMu function name

e1489b0d 04/13/2016 09:54 PM Christoph Egger

Expandable states are always acceptable Finishing states for Unsat propagation

86948fae 04/13/2016 09:33 PM Christoph Egger

Switch to only unsat propagation for testing

c4142480 04/13/2016 09:31 PM Christoph Egger

If root is Sat, formula is unconditionally Sat

5956a56d 04/13/2016 03:04 AM Christoph Egger

First implementation of propagateUnsat

066ed7b8 04/13/2016 02:35 AM Christoph Egger

Fix syntax error introduced in last commit

1b17ef3c 04/13/2016 02:20 AM Christoph Egger

Fix bug in FL calculation and refocusing after states

435390a8 04/12/2016 03:51 PM Christoph Egger

Some adjustment to AB / EB

22fef65c 04/12/2016 03:02 PM Christoph Egger

Fixup for last commit