Project

General

Profile

Statistics
| Branch: | Revision:

cool / src / lib / CoAlgReasoner.ml @ de84f40d

History | View | Annotate | Download (33.3 KB)

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