| Branch: | Revision:

cool / src / lib @ de84f40d

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

c5105465 11/03/2015 04:52 PM Christoph Egger

Add function to convert CTL -> μ Calculus

Needs a #'gensym implementation for variable names still

0aa34675 10/30/2015 06:24 PM Christoph Egger

Read/Write CTL

b179a57f 10/30/2015 05:57 PM Christoph Egger

Add new datatypes for CTL

a5f60450 10/28/2015 05:16 PM Christoph Egger

sizeFormula function for μ-Calculus

8334c748 10/28/2015 05:14 PM Christoph Egger

Read/Write μ-Calculus formulas

TODO: differentiate between APs and VARs on use. VAR is only used during
declaration so far

b2f18312 10/28/2015 05:11 PM Christoph Egger

Add μ / ν symbols to the lexer

9a3b23cc 10/28/2015 05:10 PM Christoph Egger

Add New datatypes for μ-Calculus

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

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

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

Add basic debugging repl

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

Remove old annbitset code

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

Disable annotated bitsets "annbitset"

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

Added Identity Functor and Skeleton for Default Implication

93cbaa2e 01/23/2015 08:07 AM Dirk Pattinson

Implement constant functor

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

Implement functor parameters for Const

77644d14 01/22/2015 07:30 PM Thorsten Wißmann

Allow functors to get parameters in the syntax

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

69a71d22 01/22/2015 01:15 PM Thorsten Wißmann

Add more documentatoin about installing and hacking

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.

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

Implement the REAL box of PML

25fb6e92 07/21/2014 12:21 PM Thorsten Wißmann

Glue GMLMIP and Cool together for PML purposes

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

d193f4aa 07/20/2014 04:54 PM Thorsten Wißmann

Remove debug output

36bfdafd 07/20/2014 04:04 PM Thorsten Wißmann

Implement parsing of composition of functors

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

Add formula constructors for PML

4bfb63a1 07/20/2014 11:05 AM Thorsten Wißmann

Remove unneeded variables

bc6db513 07/20/2014 11:04 AM Thorsten Wißmann

Fix equal_hcFormula_node for CL

81435cc4 07/19/2014 06:38 PM Thorsten Wißmann

Add syntax for PML

e5422169 07/19/2014 06:36 PM Thorsten Wißmann

Add syntax for PML

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

Add more comments to the reasoner core

d1c3e8ff 07/17/2014 01:43 AM Dominik Paulus

Port glpk_stub.c to GLPK 4.54 and add it to _oasis

Some options and functions are still missing, e.g. MILP support

21b7f7bc 07/17/2014 01:41 AM Dominik Paulus

run astyle on glpk_stub.c