translation from nominal to EG AF works for K
Translation for K
tried to use Fischer-Ladner Closure but not working yet
Add command line flag for fragment
The user can now choose which fragment of the mu-calculus the reasoneruses. More specialized fragments can have better performancecharacteristics.
Generalize command line argument parsing
Adds a new module CoolUtils.Args that implements a generic commandline argument parser. This makes it easier to add new options to themain program.
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.
implemented nom2fix function
Tried to implement a translation
Advertise 'graph' command of command line interface
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
Show correct binary name in "Usage" of main program
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.
Merge branch 'remove-gmlmip'
Replace Array.exists by Array.fold_left
Array.exists is only available since OCaml 4.03.0 and we need tosupport version at least version 4.02.3.
This drops the rule implementation for GML and PML, because they wererelying on GMLMIP which complicated the build process and didn't workcompletely. See Issue 19.
GML and PML are still implemented as functors but currently disabled.To re-instantiate them, an OCaml implementation is needed.
Add vim modeline to all OCaml files
added nom2fix method
Add Monotone neighbourhood logic
Add graph subcommand to coalg
Move verification of formula to separate step
Added Identity Functor and Skeleton for Default Implication
Implement functor parameters for Const
Allow functors to get parameters in the syntax
Implement raw syntax for constant functors
Update helper message
Fixup coalg-example call
Use generic functor parsing in coalg
Implement parsing of complex functors
Separate cool into library and coalg frontend