Project

General

Profile

Statistics
| Branch: | Revision:

cool / src / lib / CoAlgReasoner.ml @ 946e8213

History | View | Annotate | Download (40 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.

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

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.

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

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

Whitespace fixes

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

Add vim modeline to all OCaml files

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

Fix a few compiler warnings

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

Fix states with no children

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

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

2f126161 04/11/2016 01:46 PM Christoph Egger

Add some comments to propagateSatMu

3c05e89f 04/11/2016 01:29 AM Christoph Egger

Allow finishing cycles depending on only Sat states

92102c11 04/10/2016 11:23 PM Christoph Egger

Don't assume Open means Sat when finished

Assumption doesn't hold true currently

3f073372 04/10/2016 11:12 PM Christoph Egger

Treat Sat states like finishing states

With Sat states only treated like other states in the second fixpoint
iteration, the outer fixpoint was not ncessarily monononously decreasing
causing wrong results when in the first round the same number of nodes
got removed as added due to sat states.

080482ac 04/09/2016 10:15 PM Christoph Egger

Consider expanable Cores (but not states)

Acceptance test for cores is ∃ which is safe to use when non or only
some child states are created tus far

9fb4b019 04/09/2016 10:15 PM Christoph Egger

Turn inner fixpoint inside-out

215ad4d7 04/08/2016 08:09 PM Christoph Egger

Mark `True` only node as Sat

1e781c93 04/08/2016 08:08 PM Christoph Egger

For now, don't consider Expandable states

0a6a3df5 04/08/2016 02:29 AM Christoph Egger

Fix inclusion condition for A_x

2fba43c0 04/08/2016 02:28 AM Christoph Egger

Make Sat children actually propagate their state to the parents

46cd6856 04/08/2016 02:26 AM Christoph Egger

Preliminarily mark States with no childs Sat in propagateSatMu

Should actually happen when the State changes from `Expandable` to
`Open` and trigger the propagateSatMu but for now just do it in
propagateSatMu so we can observe the algorithm working.

07a36b24 04/07/2016 05:35 PM Christoph Egger

Reorganize code, start from Sat nodes as well

Not only finishing cycles but also plain sat nodes may cause a node to
be satisfiable

67b07e54 04/07/2016 04:16 AM Christoph Egger

Restrict finishing nodes used as startingpoint

Only finishing nodes with enough Open / Sat children are to be
considered as startingpoints

Also accept already Satisfiable nodes when finding paths

1d5d9896 04/07/2016 02:38 AM Christoph Egger

Call new propagateSatMu instead of old propagateSat

6bbde09c 04/07/2016 02:37 AM Christoph Egger

preliminary propafateSat for μ-Calculus

This still produces wrong results: It assumes every node with empty
focus to be sat.

6d64bc5a 04/07/2016 02:35 AM Christoph Egger

whitespace cleanup

7b21fbae 04/05/2016 04:57 PM Christoph Egger

Some more comments

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

b395c870 02/09/2016 11:45 AM Christoph Egger

track deferrals across propositional reasoning

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

Add deferral flags to core/state data structure

3eb8fabd 12/07/2015 05:00 PM Christoph Egger

Whitespace cleanup

5c638a53 12/07/2015 04:56 PM Christoph Egger

Unfold fixpoints when generating new states

9b6bdd74 12/01/2015 04:41 PM Christoph Egger

unfold fixpoints when creating new Cores

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

Add a lot of comments about cores

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

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

One debugger step takes one element from the queue

Now one step in the debugger removes exactly one element from the queue
(if it's not empty). If this action empties the queue, nominals are
propagated.

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

Add basic debugging repl

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

Change ConstF to TrueFalseF

433c8a2e 07/21/2014 02:48 PM Thorsten Wißmann

Reset CoAlgReasoner to the version ee45f2f

This fixes an assertion that failed for the PML+K formula

sat "({>= 3/5} (False + <R1> True & <R2> True) & {>= 2/5} ({>= 1/10} p0 & {>= 1/10} (~ p0) + False ) + False)"

which is satisfiable.

da0ea00b 07/19/2014 05:27 PM Thorsten Wißmann

Add more comments to the reasoner core

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

Make Or-step in And-Or-rules lazy

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,

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

Add more comments to CoAlgReasoner.ml

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

Add many comments in CoAlgReasoner.ml

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

Make insertRule more disjunctive-aware

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

Introduce junctions (Disjunction, Conjunction)

c78c1ce0 05/06/2014 08:00 AM Thorsten Wißmann

Connect OWL ontologies with CoAlgReasoner

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

Separate cool into library and coalg frontend