Project

General

Profile

Activity

From 03/18/2017 to 04/16/2017

04/14/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. Hans-Peter Deifel
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...
Hans-Peter Deifel

04/13/2017

11:36 AM Revision dd1db59c (cool): Change game algorithm from Stratimprlocal2 to Stratimprlocal
As the former is not deterministic Hans-Peter Deifel
11:35 AM Revision 1717d534 (cool): Add a single satisfiable game node to states without children
Hans-Peter Deifel

04/12/2017

01:01 AM Revision b1e625e9 (cool): Only iterate through open states in PG solution
Hans-Peter Deifel
06:34 PM Revision aa97b631 (cool): Remove last call to propagateUnsatMu
Hans-Peter Deifel
01:46 PM Revision 30668fd9 (cool): Keep node mapping to parity game on the fly
Hans-Peter Deifel

04/11/2017

07:56 PM Revision 0dd1f4ca (cool): Don't set all expandable cores to unsat
namely those that have children Hans-Peter Deifel
07:48 PM Revision 3800543c (cool): Solve game twice to accommodate for partial games
Hans-Peter Deifel

04/10/2017

09:07 AM Revision 2e9e42f2 (cool): WIP: First steps towards using pgsolver
Hans-Peter Deifel
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
full mu-calculus.
- Adds a new submodule unde...
Hans-Peter Deifel

04/06/2017

05:58 PM Revision e919f880 (cool): Merge branch 'aconjunctive'
Hans-Peter Deifel
05:57 PM Revision bc28fc54 (cool): build: Use new Makefile as generated by oasis
Adds many new targets including 'test' and 'distclean' Hans-Peter Deifel
05:57 PM Revision fbe64bb7 (cool): build: Add testsuite to oasis
Enables 'make test' and 'ocaml setup.ml -test' to run the testsuite. Hans-Peter Deifel
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...
Hans-Peter Deifel
05:57 PM Revision c2233aff (cool): Document tests in HACKING file
Hans-Peter Deifel
05:57 PM Revision c4503f4f (cool): tests: Add dividing example for aconjunctive fragment
Hans-Peter Deifel
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
This al...
Hans-Peter Deifel
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 ...
Hans-Peter Deifel
05:57 PM Revision 7ed16bab (cool): Add tests for command line option parser
Hans-Peter Deifel
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...
Hans-Peter Deifel
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...
Hans-Peter Deifel
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...
Hans-Peter Deifel
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
analysis.
Hans-Peter Deifel
05:57 PM Revision f15d82e6 (cool): Makefile: Add doc target to generate documentation
Hans-Peter Deifel
05:57 PM Revision aa4d3606 (cool): Add CoolUtils.TList.combinations function
Hans-Peter Deifel
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...
Hans-Peter Deifel
05:57 PM Revision 3d2f5068 (cool): tests: Don't use exit status 0 if tests failed
Hans-Peter Deifel
05:56 PM Revision fdda99d4 (cool): Add check for aconjunctive formulas
Hans-Peter Deifel
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...
Hans-Peter Deifel
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...
Hans-Peter Deifel

03/31/2017

12:00 PM Revision 31038432 (cool): .
Kristin Braun

03/27/2017

08:42 PM Revision 966e1556 (cool): nom2EA function compiles
Kristin Braun
08:10 PM Revision 0fe522e0 (cool): implemented nom2fix function
Kristin Braun
08:48 AM Revision 8d9a2669 (cool): Add vim modelines to more files
Hans-Peter Deifel
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...
Hans-Peter Deifel

03/26/2017

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...
Hans-Peter Deifel
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...
Hans-Peter Deifel

03/23/2017

02:59 PM Revision 860b962a (cool): Tried to implement a translation
Kristin Braun
01:26 PM Revision 200774f4 (cool): added EAFormula
Kristin Braun
11:18 AM Revision 7451cccf (cool): Add comment on purpose of glpk_stub to various files
Hans-Peter Deifel
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 ...
Hans-Peter Deifel

03/22/2017

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...
Hans-Peter Deifel
04:56 PM Revision 6c61df45 (cool): Advertise 'graph' command of command line interface
Hans-Peter Deifel
04:54 PM Revision cf70b199 (cool): Show correct binary name in "Usage" of main program
Hans-Peter Deifel
04:54 PM Revision 3a374ca4 (cool): Whitespace fixes
Hans-Peter Deifel
04:54 PM Revision bbd5d2db (cool): Fix command line argument check in debugger
Also shows the correct binary name in the usage output. Hans-Peter Deifel
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".
Hans-Peter Deifel
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".
Hans-Peter Deifel
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
- Teac...
Hans-Peter Deifel
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...
Hans-Peter Deifel
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...
Hans-Peter Deifel
02:09 PM Revision c9ed384b (cool): Merge branch 'remove-gmlmip'
Hans-Peter Deifel
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...
Hans-Peter Deifel
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.
Hans-Peter Deifel
02:05 PM Revision 48e6299b (cool): Remove GMLMIP from INSTALL file
It's not needed any more Hans-Peter Deifel
02:05 PM Revision 2ed7312f (cool): Disable all testcases involving PML
Hans-Peter Deifel

03/21/2017

09:12 PM Revision a57eb439 (cool): Add vim modeline to all OCaml files
Hans-Peter Deifel
07:39 PM Revision 2bda8737 (cool): Add emacs mode lines to various files
Hans-Peter Deifel
05:00 PM Revision b81e4887 (cool): Fix whitespace
Hans-Peter Deifel

03/20/2017

02:26 PM Bug #19: GML formula takes long
On a fast machine, one gets the correct answer within 3 minutes:... Thorsten Wißmann

03/18/2017

12:13 PM Revision 9631d5b7 (cool): added nom2fix method
Kristin Braun
 

Also available in: Atom