| Branch: | Revision:

cool / src / coalg @ 946e8213

# Date Author Comment
946e8213 06/20/2017 07:41 PM Kristin Braun

translation from nominal to EG AF works for K

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

Translation for K

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

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

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.

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

coalg: Make 'graph' subcommand more cli-friendly

- Read only one formula, we also only generate one graph
- Don't print a prompt or the satisfiability result

This allows to redirect the output graph to a file or directly to dot.

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

6c61df45 03/22/2017 04:56 PM Hans-Peter Deifel

Advertise 'graph' command of command line interface

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

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

Show correct binary name in "Usage" of main program

e928d370 03/22/2017 04:52 PM Hans-Peter Deifel

Improve 'verify' subcommand of main program

- Show a prompt before each input.
- Don't die if the verification of a formula fails. Show an error
instead and accept the next input.

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

Merge branch 'remove-gmlmip'

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

Replace Array.exists by Array.fold_left

Array.exists is only available since OCaml 4.03.0 and we need to
support version at least version 4.02.3.

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

b81e4887 03/21/2017 05:00 PM Hans-Peter Deifel

Fix whitespace

9631d5b7 03/18/2017 12:13 PM Kristin Braun

added nom2fix method

f4e43751 04/27/2016 07:42 PM Christoph Egger

Add Monotone neighbourhood logic

4942adb7 04/11/2016 02:43 AM Christoph Egger

Add graph subcommand to coalg

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

Move verification of formula to separate step

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

Added Identity Functor and Skeleton for Default Implication

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

3e5fbf7e 07/21/2014 12:47 PM Thorsten Wißmann

Update helper message

a9243a88 07/16/2014 03:35 PM Thorsten Wißmann

Fixup coalg-example call

b03cc745 07/16/2014 02:59 PM Thorsten Wißmann

Use generic functor parsing in coalg

3879f710 07/16/2014 01:53 PM Thorsten Wißmann

Implement parsing of complex functors

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

Separate cool into library and coalg frontend