| Branch: | Revision:

cool / src / lib @ bc0691dc

# Date Author Comment
bc0691dc 08/10/2017 12:48 PM Kristin Braun

translation only uses subformulas if their negation is not a subformula

2d58f46f 07/18/2017 11:16 AM Kristin Braun

added optimized translation

97b76edf 06/29/2017 05:03 PM Kristin Braun

deleted conjunction

946e8213 06/20/2017 07:41 PM Kristin Braun

translation from nominal to EG AF works for K

2da28579 06/20/2017 05:50 PM Kristin Braun

added VAR to patternmatching

def3763d 06/19/2017 01:18 PM Kristin Braun

Translation for K

e3cf4ca2 05/16/2017 07:39 PM Kristin Braun

translation calculates fisher ladner closure correctly

267e3fcf 05/16/2017 02:03 PM Kristin Braun


89613c41 05/11/2017 03:52 PM Kristin Braun

tried to use Fischer-Ladner Closure but not working yet

0f9140ab 05/04/2017 04:06 PM Kristin Braun

part 1 and 3 of translation

a91110f4 05/03/2017 03:47 PM Kristin Braun

first part of translations is implemented

3cd07e5d 05/03/2017 03:26 PM Hans-Peter Deifel

Replace String.split_on_char with custom implementation

String.split_on_char was introduced in OCaml 4.04, but we want to
support 4.02.

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

7ed16bab 04/06/2017 05:57 PM Hans-Peter Deifel

Add tests for command line option parser

4c23563e 04/06/2017 05:57 PM Hans-Peter Deifel

Generalize command line argument parsing

Adds a new module CoolUtils.Args that implements a generic command
line argument parser. This makes it easier to add new options to the
main program.

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

aa4d3606 04/06/2017 05:57 PM Hans-Peter Deifel

Add CoolUtils.TList.combinations function

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

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.

fdda99d4 04/06/2017 05:56 PM Hans-Peter Deifel

Add check for aconjunctive formulas

31038432 03/31/2017 12:00 PM Kristin Braun


966e1556 03/27/2017 08:42 PM Kristin Braun

nom2EA function compiles

0fe522e0 03/27/2017 08:10 PM Kristin Braun

implemented nom2fix function

860b962a 03/23/2017 02:59 PM Kristin Braun

Tried to implement a translation

200774f4 03/23/2017 01:26 PM Kristin Braun

added EAFormula

7451cccf 03/23/2017 11:18 AM Hans-Peter Deifel

Add comment on purpose of glpk_stub to various files

7198f96f 03/22/2017 06:21 PM Hans-Peter Deifel

Enable documentation generation in oasis

Documentation can be built with: ocaml -doc

This also fixes two documentation comments that had the wrong syntax.

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

5f1ec830 03/22/2017 04:54 PM Hans-Peter Deifel

Add UTF-8 "Micro Sign" as syntax for 'mu'

This is easier to type with a standard compose key as opposed as the
arguably more correct "Greek Small Letter Mu".

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

c9ed384b 03/22/2017 02:09 PM Hans-Peter Deifel

Merge branch 'remove-gmlmip'

c4aee922 03/22/2017 02:05 PM Hans-Peter Deifel


This drops the rule implementation for GML and PML, because they were
relying on GMLMIP which complicated the build process and didn't work
completely. See Issue 19.

GML and PML are still implemented as functors but currently disabled.
To re-instantiate them, an OCaml implementation is needed.

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

9352b45f 03/16/2017 07:08 PM Hans-Peter Deifel

Fix compilation of gmlmip with newest ocaml

The CAMLparam0() macro must be invoked at the beginning of a function
that has local variables.

07402362 05/21/2016 03:50 AM Christoph Egger

Consider also other modal operators as valid guards

edfbcc2b 05/14/2016 11:50 PM Christoph Egger

Fix deferral tracking for new CoalitionLogic code

2a36974b 05/14/2016 10:16 PM Christoph Egger

Revert to fresh variable names in convertToMu

e01c4a03 05/14/2016 05:10 AM Christoph Egger

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

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

Fix deferral tracking when "empty" least fixpoints appear

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

Fix states with no children

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

actually verify properties for sat target

de13bc0f 05/10/2016 10:02 AM Christoph Egger

Unify CTL variable name for more global caching

eff3ff0c 05/10/2016 03:07 AM Christoph Egger

make HashConsing accept ¬Var ≡ Var

52f5465c 04/28/2016 04:13 PM Christoph Egger

Add deferral tracking for Identity

a670c5fd 04/28/2016 04:09 PM Christoph Egger

Add deferral tracking for Fusion

f40cc23c 04/28/2016 04:06 PM Christoph Egger

Add deferral tracking for Choice

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