Project

General

Profile

Statistics
| Branch: | Revision:

cool / src / lib / CoAlgMisc.ml @ def3763d

History | View | Annotate | Download (48.1 KB)

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

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

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.

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

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

Add vim modeline to all OCaml files

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

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

Fix deferral tracking when "empty" least fixpoints appear

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

actually verify properties for sat target

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
formulas

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

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
ruleEnumerations,

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