| Branch: | Revision:

cool / src / lib @ 40a714df

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

97d73a78 04/12/2016 02:54 PM Christoph Egger

Fix A ( φ U ψ ) and E ( φ U ψ ) translation

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

e30caa42 04/11/2016 12:13 AM Christoph Egger

Implement {A,E}( .. {R,B} ..) CTL formulas

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

f20718d2 04/09/2016 03:18 AM Christoph Egger

Add header for function used in previous commit

fe81b988 04/09/2016 03:17 AM Christoph Egger

Make real empty set for deferral (not including True)

ef0e7121 04/09/2016 03:17 AM Christoph Egger

Actually use refocused deferral in modal step

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

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

Mark deferrals bold in graphviz export

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

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

Add function to determin size of Core / State set

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

Some more comments

b9a8d969 04/05/2016 02:56 AM Christoph Egger

Space normalization

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

Add documentation on dependencies

a25a6849 02/29/2016 10:37 AM Christoph Egger

Make KD a deferral-tracking Logic

dcc8167f 02/22/2016 03:44 PM Christoph Egger

Use custom variables for CTL -> μ

Makes morally same formulas actually the same. Removes the need to
recalculate some States that have already been fully expanded but with
different variable names only (where this is possible)

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

Update deferral when revisiting formula

fbffb079 02/16/2016 12:54 PM Christoph Egger

Some seemingly missed patern-match cases

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

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

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

5e7c8aa1 01/26/2016 04:29 PM Christoph Egger

Add function to verify if deferral is still mentioned in formula

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

Whitespace cleanup

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

Whitespace cleanup

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

Unfold fixpoints when generating new states

c5c25acf 12/07/2015 04:53 PM Christoph Egger

Whitespace cleanup

No tabs any more

854e1338 12/07/2015 04:47 PM Christoph Egger

Fix fixpoint-unfolding

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?

92feed46 12/01/2015 05:04 PM Christoph Egger

Implement negation of Fixpoints also for HashConsed representation

a7ae917b 12/01/2015 05:04 PM Christoph Egger

Implement equality on (HC)μ/ν

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

cc07e93d 12/01/2015 04:43 PM Christoph Egger

Add function to substitute variables

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

some documentation wrt detClosure

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

unfold fixpoints when creating new Cores

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

Add MuF / NuF datatypes to reasoner

e156fbca 11/24/2015 12:57 PM Christoph Egger

Merge remote-tracking branch 'origin/master' into flatmu

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

Add a lot of comments about cores

939f5bab 11/18/2015 02:37 PM Christoph Egger

add fallthrough cases (CTL constructors) for verify*

26cfb2dc 11/17/2015 04:14 PM Christoph Egger

Fix guardednes check

1484d8cb 11/17/2015 03:54 PM Christoph Egger

Move verification of formula to separate step

63710593 11/17/2015 03:53 PM Christoph Egger

Implement verify functions

ff4dc786 11/16/2015 11:29 PM Christoph Egger

implement nnf for μ-Calculus

993e31e1 11/10/2015 05:12 PM Christoph Egger

allow arbitrary formulas in A(φ U ψ) and E(…)

previously only late parser steps were used so modalities were allowed
but not e.g. disjunctions. With this change all of the
CTLComparisonBenchmarks formulas successfully parse

80bbb363 11/10/2015 04:30 PM Christoph Egger

assume parens when parsing A(φ U ψ)

Example formulas from the benchmark seem to all have parens so assume
they are there

a2cd9f2a 11/09/2015 08:03 PM Christoph Egger

Add check for guardedness

d2db7e40 11/09/2015 08:02 PM Christoph Egger

Add prototypes for checker functions

We need to enforce some assumptions for μ-Calculus. Add (still empty)
checker function and call them when importing the forumla

309b71a5 11/09/2015 08:01 PM Christoph Egger

Add μ constructors to the formula iter

c3e13ca6 11/09/2015 02:43 PM Christoph Egger

Generate instance of VAR instead of AP for bound variables

80aa0b2f 11/09/2015 02:43 PM Christoph Egger

Add symbols bound in ν/μ expressions to table

0b908205 11/09/2015 02:43 PM Christoph Egger

Hand symbol table down the parser

508e3c33 11/09/2015 02:43 PM Christoph Egger

Add pattern-matching for hcFormula where obvious

Add all obvious cases for hcFormula

d29d35f7 11/09/2015 02:43 PM Christoph Egger

Actually represent variable under μ/ν as string

so it's `MU of string * formula` again. The variable within the formula
is still represented as `VAR s`

8cac0897 11/09/2015 02:43 PM Christoph Egger

CTL is expected to be removed early on

Create pattern-matching cases for all CTL language elements and raise an
error if encountered. We are assuming that CTL is replaced by plain
μ-Calculus early on

7b944a64 11/09/2015 02:43 PM Christoph Egger

Add CTL and μ-Calculus Constructors to convert_post

Needed e.g. to implement the CTL → μ conversion

87d5082f 11/09/2015 02:43 PM Christoph Egger

Add μ-constructors for hcFormula

CTL is assumed to be eliminated before the hash-consing step

17af2794 11/09/2015 02:43 PM Christoph Egger

Add gensym for CTL -> μ