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.
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
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.
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
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
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
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
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.
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.
Consider also other modal operators as valid guards
Fix deferral tracking for new CoalitionLogic code
Revert to fresh variable names in convertToMu
Merge remote-tracking branch 'origin/master' into flatmu
Fix deferral tracking when "empty" least fixpoints appear
Fix states with no children
actually verify properties for sat target
Unify CTL variable name for more global caching
make HashConsing accept ¬Var ≡ Var
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
Only remove solver after Unsat Propagation
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...
Use proper number of open States when calculating frequency
Instead of some calculation based of finishing on normal Cores reallycount proper Open States
substract number of finishing/Sat nodes when calculating propagation frequency
Remove nominal propagation for now
Make number of waves between propagation depend on #openCores
Do propagation only after 100 iterations
Do both sat and unsat propagation
Remove debug output from propagateSatMu
Do a final propagation round at the end
Fix typo in propagateUnsatMu function name
Expandable states are always acceptable Finishing states for Unsat propagation
Switch to only unsat propagation for testing
If root is Sat, formula is unconditionally Sat
First implementation of propagateUnsat
Fix syntax error introduced in last commit
Fix bug in FL calculation and refocusing after states
Some adjustment to AB / EB
Fixup for last commit