| Branch: | Revision:

cool / src / lib / @ 40a714df

History | View | Annotate | Download (46.4 KB)

# Date Author Comment
f4e43751 04/27/2016 07:42 PM Christoph Egger

Add Monotone neighbourhood logic

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

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

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

de84f40d 04/08/2016 08:08 PM Christoph Egger

Mark deferrals bold in graphviz export

50df1dc2 04/07/2016 02:34 AM Christoph Egger

Add function to determin size of Core / State set

f4498ed1 04/05/2016 02:55 AM Christoph Egger

Add documentation on dependencies

653eaa4b 02/16/2016 02:32 PM Christoph Egger

Update deferral when revisiting formula

c13029a3 02/16/2016 12:47 PM Christoph Egger

Color-code core/state status in graph output

16af388e 02/15/2016 04:57 PM Christoph Egger

Make reasoner nodes include deferrals

This makes the identifying information be of type bset*bset instead of
bset and adds tracking of deferrals for propositional reasoning and --
in case of K -- for modal reasoning

8d6bf016 02/15/2016 04:52 PM Christoph Egger

Add basic graphviz export feature

3285ac30 02/09/2016 12:00 AM Christoph Egger

Add deferral flags to core/state data structure

c67aca42 02/01/2016 05:10 PM Christoph Egger

Add deferral accessor function

d9f4e4af 01/26/2016 04:32 PM Christoph Egger

Add deferrals to reasoner array

cb12f8a5 01/26/2016 04:32 PM Christoph Egger

Calculate deferral when building FL-Closure

034a8dea 12/07/2015 04:58 PM Christoph Egger

Whitespace cleanup

43194ed2 12/01/2015 05:07 PM Christoph Egger

Add Closure for plain Variables

As there should never be free variables in formulas within the
FL-Closure maybe we should rather signal an error here?

5ec97220 12/01/2015 05:01 PM Christoph Egger

Implement initTables for μ-Calculus

Make following state of a fixpoint it's unfold

6553983f 12/01/2015 04:48 PM Christoph Egger

Add fixpoint-unfold to detClosure

should now properly calculate the FL-Closure

4b0d0388 12/01/2015 04:41 PM Christoph Egger

some documentation wrt detClosure

3b407438 12/01/2015 04:41 PM Christoph Egger

Add MuF / NuF datatypes to reasoner

e0f19999 11/24/2015 12:53 PM Thorsten Wißmann

Add a lot of comments about cores

d283bf7a 07/06/2015 04:36 PM Thorsten Wißmann

Use different state sets for different sorts

Patch by Florian Widmann In order to fix the behaviour for the K*K

[pi1]<R>c0 | [pi1]<S>c1 | [pi2]<T>c3
[pi1]<R>c0 | [pi1]<S>c1 | [pi2]<T>c3 | [pi1][U]c4
d58bba0f 02/05/2015 07:02 AM Dirk Pattinson

Removed Negation Normal Form of Choice as Choice is Self-Dual

4164c8e1 02/05/2015 06:36 AM Thorsten Wißmann

Also show parent nodes in debugger

488cea0f 02/05/2015 06:11 AM Thorsten Wißmann

Implement queue printing

73762b19 02/05/2015 05:39 AM Thorsten Wißmann

Implement state listing for debugger

f335015f 02/05/2015 05:08 AM Thorsten Wißmann

Implement lscores for debugger

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

Add basic debugging repl

19f5dad0 02/04/2015 05:02 AM Dirk Pattinson

Added Identity Functor and Skeleton for Default Implication

5e0983fe 01/22/2015 08:23 PM Thorsten Wißmann

Implement functor parameters for Const

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

Implement raw syntax for constant functors

3b055ae8 01/22/2015 06:10 PM dirk

Change ConstF to TrueFalseF

9bae2c4f 07/21/2014 01:49 PM Thorsten Wißmann

Implement the REAL box of PML

c855ba91 07/21/2014 11:34 AM Thorsten Wißmann

Change AtMostProbable to LessProbableThan

The actual box of PML (in GMLMIP) is: less probable than. The Diamond
is: At least Probable than.

So now you have ¬[p] C = <p> C.

eda515b6 07/21/2014 11:05 AM Thorsten Wißmann

Add ocaml part of PML rule application

86b07be8 07/20/2014 11:05 AM Thorsten Wißmann

Add formula constructors for PML

db23edf7 07/16/2014 02:50 PM Thorsten Wißmann

Implement more generic functor parsing/printing

672429b4 07/16/2014 12:08 PM Thorsten Wißmann

Make Or-step in And-Or-rules lazy

a9949a25 07/16/2014 12:08 PM Thorsten Wißmann

Use lazylists to remove redudancy

69243f7f 07/16/2014 12:08 PM Thorsten Wißmann

Generalize ruleEnumeration by introducing lazylist

Introduce a new generic data type lazylist, e.g. used for lazy rule

b36e57bc 07/16/2014 12:08 PM Thorsten Wißmann

Remove Disjunctive ruleEnumerations

Propagation of satisfiability and unsatisfiability does not cover
disjunctions and I don't get how propagation works, so I won't touch it
yet. So this reverts the only partially implemented Disjunctive

269d93e5 07/16/2014 12:08 PM Thorsten Wißmann

Introduce junctions (Disjunction, Conjunction)

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

Separate cool into library and coalg frontend