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.
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...
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.
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 vim modeline to all OCaml files
Fix a few compiler warnings
Add Monotone neighbourhood logic
Deallocate satsolver once core becomes `Open`
The satsolver is reatined and only updated with new clauses for everystate that is generated out of a core. Once the core becomes Open (asopposed to expandable), the solver is no longer needed.
This patch makes the solver a `Solver option` and gets it deallocated...
Make number of waves between propagation depend on #openCores
First implementation of propagateUnsat
Add header for function used in previous commit
Add function to determin size of Core / State set
Make reasoner nodes include deferrals
This makes the identifying information be of type bset*bset instead ofbset and adds tracking of deferrals for propositional reasoning and --in case of K -- for modal reasoning
Add basic graphviz export feature
Add deferral flags to core/state data structure
Add deferral accessor function
Add MuF / NuF datatypes to reasoner
Implement state listing for debugger
Implement lscores for debugger
Add basic debugging repl
Added Identity Functor and Skeleton for Default Implication
Implement functor parameters for Const
Implement raw syntax for constant functors
Change ConstF to TrueFalseF
Implement the REAL box of PML
Change AtMostProbable to LessProbableThan
The actual box of PML (in GMLMIP) is: less probable than. The Diamondis: At least Probable than.
So now you have ¬[p] C = <p> C.
Add ocaml part of PML rule application
Add formula constructors for PML
Implement more generic functor parsing/printing
Make Or-step in And-Or-rules lazy
Use lazylists to remove redudancy
Generalize ruleEnumeration by introducing lazylist
Introduce a new generic data type lazylist, e.g. used for lazy ruleenumerations.
Remove Disjunctive ruleEnumerations
Propagation of satisfiability and unsatisfiability does not coverdisjunctions and I don't get how propagation works, so I won't touch ityet. So this reverts the only partially implemented DisjunctiveruleEnumerations,
Introduce junctions (Disjunction, Conjunction)
Separate cool into library and coalg frontend