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 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.
Fix a few compiler warnings
Fix deferral tracking when "empty" least fixpoints appear
actually verify properties for sat target
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
Do propagation only after 100 iterations
First implementation of propagateUnsat
Fix syntax error introduced in last commit
Fix bug in FL calculation and refocusing after states
Mark deferrals bold in graphviz export
Add function to determin size of Core / State set
Add documentation on dependencies
Update deferral when revisiting formula
Color-code core/state status in graph output
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 deferrals to reasoner array
Calculate deferral when building FL-Closure
Add Closure for plain Variables
As there should never be free variables in formulas within theFL-Closure maybe we should rather signal an error here?
Implement initTables for μ-Calculus
Make following state of a fixpoint it's unfold
Add fixpoint-unfold to detClosure
should now properly calculate the FL-Closure
some documentation wrt detClosure
Add MuF / NuF datatypes to reasoner
Add a lot of comments about cores
Use different state sets for different sorts
Patch by Florian Widmann In order to fix the behaviour for the K*Kformulas
[pi1]<R>c0 | [pi1]<S>c1 | [pi2]<T>c3 [pi1]<R>c0 | [pi1]<S>c1 | [pi2]<T>c3 | [pi1][U]c4
Removed Negation Normal Form of Choice as Choice is Self-Dual
Also show parent nodes in debugger
Implement queue printing
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