Tried to optimize translation with fixpoint approximation; added depthFormula function in CoAlgFormula
added translation for Const
translation only uses subformulas if their negation is not a subformula
added optimized translation
nom2fix and solveNom
translation from nominal to EG AF works for K
added VAR to patternmatching
Translation for K
translation calculates fisher ladner closure correctly
tried to use Fischer-Ladner Closure but not working yet
part 1 and 3 of translation
first part of translations is implemented
Replace String.split_on_char with custom implementation
String.split_on_char was introduced in OCaml 4.04, but we want tosupport 4.02.
Merge branch 'aconjunctive'
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.
Add tests for command line option parser
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.
tests: Add dividing example for aconjunctive fragment
Document tests in HACKING file
tests: Add unit tests
Adds a whole new set of tests that don't just test the whole reasoningprocess on a formula, but smaller individual functions.
Right now there are only two tests but more should follow.
build: Add testsuite to oasis
Enables 'make test' and 'ocaml setup.ml -test' to run the testsuite.
build: Use new Makefile as generated by oasis
Adds many new targets including 'test' and 'distclean'
tests: Don't use exit status 0 if tests failed
Fix aconjunctive fragment for rules with >1 children
Previously, the algorithm for the aconjunctive fragment would insertmany cores for each child of a modal rule and add those as children ofthe rule application to the state.
This was wrong for multiple reasons:...
Add CoolUtils.TList.combinations function
Makefile: Add doc target to generate documentation
tests: Print summary for failed tests at the end
Makes it easier to find failing formulas for further fine-grainedanalysis.
tests: Add example where new Algorithm should fail
This formula is not aconjunctive and should be wrongly declared assatisfiable by the algorithm that assumes aconjunctivity.
This doesn't work right now: The new algorithm also answers with"unsat".
Don't hardcode check for aconjunctive formulas
Previously, cool would simply raise an exception if the formula wasnot aconjunctive. This was done to ease testing of the new reasoneralgorithm.
Now, the reasoner decides whether the formula is aconjunctive or not...
Add test cases for aconjunctive fragment
This fails currently, because the check for aconjunctivity iscurrently hard coded, ruling out all formulas that aren'taconjunctive.
Specialize deferral tracking for aconjunctive fragment
For the aconjunctive fragment, we replace the generation of a singlecore with all tracked deferrals by the generation of multiple cores,each annotated with a single deferral from the above set.
Add check for aconjunctive formulas
nom2EA function compiles
implemented nom2fix function
Add vim modelines to more files
tests: Throw error if child doesn't return 0 or 1
0 and 1 are used for Sat and Unsat respectively. But if the childthrows an exception, another exit status is returned which the parentnow recognizes.
tests: Run reasoner in new process for each formula
As it stands, cool leaks tons of memory with each `isSat` call. Untilthis is fixed, the new `--slow` testsuite would need at least 16GB ofmemory if all formulas are decided in one process. Thus, we now call...
Add lots of test cases for CTL.
This imports some of the quickly decidable ctl comparision benchmarkformulas into the test suite.
The testsuite also gained a --slow parameter, that enables slower (butstill fairly fast) formulas.
Tried to implement a translation
Add comment on purpose of glpk_stub to various files
Remove libbdd and libglpk from C linker command
Now that GMLMIP is removed, those are not needed any more. Now coolcan really be built without GMLMIPs dependencies (as is now advertisedby the INSTALL file).
Enable documentation generation in oasis
Documentation can be built with: ocaml setup.ml -doc
This also fixes two documentation comments that had the wrong syntax.
Advertise 'graph' command of command line interface
debugger: Stop and print result if reasoner finishes
The 'step' command takes an optional repeat count. Now it stopsstepping and prints the result if the reasoner finishes beforereaching the specified number of steps.
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
Add UTF-8 "Micro Sign" as syntax for 'mu'
This is easier to type with a standard compose key as opposed as thearguably more correct "Greek Small Letter Mu".
Perform sat propagation in debugger step
Otherwise, the debugger would report the reasoner result to be "Sat" when it should really be "Unsat".
Fix command line argument check in debugger
Also shows the correct binary name in the usage output.
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'
Disable all testcases involving PML
Remove GMLMIP from INSTALL file
It's not needed any more
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
Add emacs mode lines to various files
added nom2fix method
Fix another compiler warning
This fixes the warning "the label idx is defined in both types stateand core." by renaming the label to idxS and idxC respectively.
Add .merlin file to gitignore
This is generated by the editor completion framework called merlin:https://github.com/ocaml/merlin
Fix a few compiler warnings
Get testsuite running again
Fixes the syntax of all tests that use R and B as identifiers, whichare keywords now.
Also disables all tests involving nominals as they are currently allthrowing exceptions.
Fix testsuite for K
R and B are now keywords and were used as identifiers. Now, r andb (lowercase) is used instead in the testcases. For consistency, allother identifiers were lowercased, too.
Fix compilation of gmlmip with newest ocaml
The CAMLparam0() macro must be invoked at the beginning of a functionthat has local variables.
Merge branch 'flatmu'
Create random coalition for ATL operators
use correct modal operator for ATL
Consider also other modal operators as valid guards
Fix deferral tracking for new CoalitionLogic code
Remove A( ψ R φ) as it's not supported by all CTL reasoners
fix generation for CTL
Revert to fresh variable names in convertToMu
Allow creating ATL formulae in randmu
Merge remote-tracking branch 'origin/master' into flatmu
Fix deferral tracking when "empty" least fixpoints appear
Add support for creating CTL formulae
Extra parens in generated formulae
Makes them not only intended alt-free but also parsed to something alt-free
Fix states with no children
actually verify properties for sat target
Unify CTL variable name for more global caching
make HashConsing accept ¬Var ≡ Var
Fix static linking
Also create mlsolver-compatible versions
Add tool to generate random μ-calculus formulas
Add deferral tracking for Identity
Add deferral tracking for Fusion
Add deferral tracking for Choice
Add deferral tracking to CoalitionLogic
Add Monotone neighbourhood logic
Rewrap some code to fit into 90 chars width
Only deallocate solver for unsat nodes
We want to still have the solver for naive unsat propagation
Remove debug output