From 03/18/2017 to 04/16/2017
- 11:22 AM Revision a2ec2dfc (cool): Set states without children to Sat early
- We can set states without children to Sat right after we expand them.
- 11:19 AM Revision afeec2f2 (cool): Correctly represent root Core in parity games
- In the two games we solve, expandable cores are represented either as
themselves or as the successful node. Unfortuna...
- 11:36 AM Revision dd1db59c (cool): Change game algorithm from Stratimprlocal2 to Stratimprlocal
- As the former is not deterministic
- 11:35 AM Revision 1717d534 (cool): Add a single satisfiable game node to states without children
- 01:01 AM Revision b1e625e9 (cool): Only iterate through open states in PG solution
- 06:34 PM Revision aa97b631 (cool): Remove last call to propagateUnsatMu
- 01:46 PM Revision 30668fd9 (cool): Keep node mapping to parity game on the fly
- 07:56 PM Revision 0dd1f4ca (cool): Don't set all expandable cores to unsat
- namely those that have children
- 07:48 PM Revision 3800543c (cool): Solve game twice to accommodate for partial games
- 09:07 AM Revision 2e9e42f2 (cool): WIP: First steps towards using pgsolver
- 09:03 AM Revision 2761a943 (cool): Import pgsolver as git submodule
- A parity game solver that will be used to solve games arising from the
- Adds a new submodule unde...
- 05:58 PM Revision e919f880 (cool): Merge branch 'aconjunctive'
- 05:57 PM Revision bc28fc54 (cool): build: Use new Makefile as generated by oasis
- Adds many new targets including 'test' and 'distclean'
- 05:57 PM Revision fbe64bb7 (cool): build: Add testsuite to oasis
- Enables 'make test' and 'ocaml setup.ml -test' to run the testsuite.
- 05:57 PM Revision 256444ba (cool): tests: Add unit tests
- Adds a whole new set of tests that don't just test the whole reasoning
process on a formula, but smaller individual f...
- 05:57 PM Revision c2233aff (cool): Document tests in HACKING file
- 05:57 PM Revision c4503f4f (cool): tests: Add dividing example for aconjunctive fragment
- 05:57 PM Revision 62cbb102 (cool): 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
- 05:57 PM Revision 4c23563e (cool): 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 ...
- 05:57 PM Revision 7ed16bab (cool): Add tests for command line option parser
- 05:57 PM Revision f24367c4 (cool): 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 bett...
- 05:57 PM Revision b6653b96 (cool): 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 o...
- 05:57 PM Revision 0d6818bb (cool): tests: Add example where new Algorithm should fail
- This formula is not aconjunctive and should be wrongly declared as
satisfiable by the algorithm that assumes aconjunc...
- 05:57 PM Revision 4a20854e (cool): tests: Print summary for failed tests at the end
- Makes it easier to find failing formulas for further fine-grained
- 05:57 PM Revision f15d82e6 (cool): Makefile: Add doc target to generate documentation
- 05:57 PM Revision aa4d3606 (cool): Add CoolUtils.TList.combinations function
- 05:57 PM Revision 93ef4736 (cool): 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 ad...
- 05:57 PM Revision 3d2f5068 (cool): tests: Don't use exit status 0 if tests failed
- 05:56 PM Revision fdda99d4 (cool): Add check for aconjunctive formulas
- 05:56 PM Revision e7aaefa9 (cool): Specialize deferral tracking for aconjunctive fragment
- For the aconjunctive fragment, we replace the generation of a single
core with all tracked deferrals by the generatio...
- 05:56 PM Revision bc706b79 (cool): Add test cases for aconjunctive fragment
- This fails currently, because the check for aconjunctivity is
currently hard coded, ruling out all formulas that aren...
- 12:00 PM Revision 31038432 (cool): .
- 08:42 PM Revision 966e1556 (cool): nom2EA function compiles
- 08:10 PM Revision 0fe522e0 (cool): implemented nom2fix function
- 08:48 AM Revision 8d9a2669 (cool): Add vim modelines to more files
- 08:36 AM Revision 8c810657 (cool): tests: Throw error if child doesn't return 0 or 1
- 0 and 1 are used for Sat and Unsat respectively. But if the child
throws an exception, another exit status is returne...
- 09:29 AM Revision b002efa8 (cool): Add lots of test cases for CTL.
- This imports some of the quickly decidable ctl comparision benchmark
formulas into the test suite.
The testsuite als...
- 09:29 AM Revision ad0b75b1 (cool): tests: Run reasoner in new process for each formula
- As it stands, cool leaks tons of memory with each `isSat` call. Until
this is fixed, the new `--slow` testsuite would...
- 02:59 PM Revision 860b962a (cool): Tried to implement a translation
- 01:26 PM Revision 200774f4 (cool): added EAFormula
- 11:18 AM Revision 7451cccf (cool): Add comment on purpose of glpk_stub to various files
- 11:09 AM Revision a6f9f99f (cool): Remove libbdd and libglpk from C linker command
- Now that GMLMIP is removed, those are not needed any more. Now cool
can really be built without GMLMIPs dependencies ...
- 06:21 PM Revision 7198f96f (cool): Enable documentation generation in oasis
- Documentation can be built with: ocaml setup.ml -doc
This also fixes two documentation comments that had the wrong s...
- 04:56 PM Revision 6c61df45 (cool): Advertise 'graph' command of command line interface
- 04:54 PM Revision cf70b199 (cool): Show correct binary name in "Usage" of main program
- 04:54 PM Revision 3a374ca4 (cool): Whitespace fixes
- 04:54 PM Revision bbd5d2db (cool): Fix command line argument check in debugger
- Also shows the correct binary name in the usage output.
- 04:54 PM Revision 371cb823 (cool): Perform sat propagation in debugger step
- Otherwise, the debugger would report the reasoner result to be "Sat"
when it should really be "Unsat".
- 04:54 PM Revision 5f1ec830 (cool): 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".
- 04:54 PM Revision 86c2c2ee (cool): Prettify graphviz output
- - Use more readable colors and proper spacing
- Differentiate between cores and states by shape
- Add a legend
- 04:54 PM Revision 83612ae5 (cool): debugger: Stop and print result if reasoner finishes
- The 'step' command takes an optional repeat count. Now it stops
stepping and prints the result if the reasoner finish...
- 04:52 PM Revision e928d370 (cool): 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 ac...
- 02:09 PM Revision c9ed384b (cool): Merge branch 'remove-gmlmip'
- 02:05 PM Revision c4aee922 (cool): Remove GMLMIP
- This drops the rule implementation for GML and PML, because they were
relying on GMLMIP which complicated the build p...
- 02:05 PM Revision 5736aabb (cool): 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.
- 02:05 PM Revision 48e6299b (cool): Remove GMLMIP from INSTALL file
- It's not needed any more
- 02:05 PM Revision 2ed7312f (cool): Disable all testcases involving PML
- 09:12 PM Revision a57eb439 (cool): Add vim modeline to all OCaml files
- 07:39 PM Revision 2bda8737 (cool): Add emacs mode lines to various files
- 05:00 PM Revision b81e4887 (cool): Fix whitespace
- 02:26 PM Bug #19: GML formula takes long
- On a fast machine, one gets the correct answer within 3 minutes:...
Also available in: Atom