COOL merge requestshttps://git8.cs.fau.de/software/cool/-/merge_requests2024-03-18T13:16:36Zhttps://git8.cs.fau.de/software/cool/-/merge_requests/17Draft: Tl star2024-03-18T13:16:36ZMerlinDraft: Tl starImplemented ATL* encodingImplemented ATL* encodinghttps://git8.cs.fau.de/software/cool/-/merge_requests/16AMCDES Implementation2023-11-06T13:01:50ZMerlinAMCDES ImplementationSet valued resolution based AMCDES implementation described in Sebastian Dietlmeiers BA.Set valued resolution based AMCDES implementation described in Sebastian Dietlmeiers BA.MerlinMerlinhttps://git8.cs.fau.de/software/cool/-/merge_requests/15Draft: Modelchecking in COOL2023-12-07T20:32:16ZMerlinDraft: Modelchecking in COOLAttempt to get the long-standing modelchecking branch ready for merging.Attempt to get the long-standing modelchecking branch ready for merging.https://git8.cs.fau.de/software/cool/-/merge_requests/14SAT Checking for the full guarded fragment of the coalgebraic mu-calculus, us...2023-06-10T16:14:52ZFrederik HennigSAT Checking for the full guarded fragment of the coalgebraic mu-calculus, using Compact Safra TreesThis merge request introduces a SAT decision procedure for the entire guarded fragment of the coalgebraic mu calculus,
by extending the existing Tableau- and OneStep-function-based reasoners with a parity game construction using Compact ...This merge request introduces a SAT decision procedure for the entire guarded fragment of the coalgebraic mu calculus,
by extending the existing Tableau- and OneStep-function-based reasoners with a parity game construction using Compact Safra Trees as states.
This implements the procedure described in https://doi.org/10.1007/978-3-030-17127-8_16.
**Primary Contribution:** `SafraTreeTracking.ml(i)` provides `CstTracker` as a new implementation of `FocusTracking.FocusTracker`, which uses compact safra trees as described by Piterman (https://arxiv.org/pdf/0705.2205.pdf).
**Secondary Changes:**
- The `cool-coalg` executable is updated; its `--fragment` parameter is now respected by selecting the reasoner implementation at runtime.
- The `fragSpec` argument to `CoAlgReasoner.isSat` and `CoAlgReasoner.initReasoner` is removed. Instead, all `FocusTracker` implementations are annotated with a `fragment`, against which compatibility of formulas is checked in `initReasoner`. This ensures that the fragment used in the reasoner is always compatible with the selected focus tracking, and the formulas actually lie in that fragment.
- `Series.ml` and `cool-gen_exec` are extended with new, non-aconjunctive formula series describing Streett games.Frederik HennigFrederik Hennighttps://git8.cs.fau.de/software/cool/-/merge_requests/13Atl benchmark series2023-05-12T07:39:57ZMerlinAtl benchmark serieshttps://git8.cs.fau.de/software/cool/-/merge_requests/12Model checking via Effectivity Frames2023-07-21T11:16:31ZSimon PruckerModel checking via Effectivity FramesWe extended the model checking implementation for Coalition Logic with Effectivity Frame Semantics.We extended the model checking implementation for Coalition Logic with Effectivity Frame Semantics.Simon PruckerSimon Pruckerhttps://git8.cs.fau.de/software/cool/-/merge_requests/11Integrated benchmarks and switch to incremental generated parser2022-10-20T15:37:52ZMerlinIntegrated benchmarks and switch to incremental generated parserIntegrated some of the benchmark series as well as new ones.
Furthermore, we switched to the generated parser which got ported to the incremental API for better error messages.Integrated some of the benchmark series as well as new ones.
Furthermore, we switched to the generated parser which got ported to the incremental API for better error messages.https://git8.cs.fau.de/software/cool/-/merge_requests/10Refactoring2022-08-23T11:29:39ZMerlinRefactoringfixes #37
fixes #21fixes #37
fixes #21https://git8.cs.fau.de/software/cool/-/merge_requests/9Onestep2022-06-29T13:17:58ZMerlinOnestepThis merge request implements general one-step satisfiability (see [Oliver Grosch BA](https://git8.cs.fau.de/theses/oliver-grosch-ba)).
ToDos:
- [x] Cleanup (see comments below)
- [x] Implement a flag to explicitly switch to one-step sa...This merge request implements general one-step satisfiability (see [Oliver Grosch BA](https://git8.cs.fau.de/theses/oliver-grosch-ba)).
ToDos:
- [x] Cleanup (see comments below)
- [x] Implement a flag to explicitly switch to one-step satisfiability as it is very inefficient when other procedures are available.v2.1 - One-Step COOLhttps://git8.cs.fau.de/software/cool/-/merge_requests/8Generator Executable2021-12-09T09:13:56ZSimon PruckerGenerator ExecutableThe gen_exec generator executable is able to generate formulas for various functors of variable size with optional fixpoint support.The gen_exec generator executable is able to generate formulas for various functors of variable size with optional fixpoint support.https://git8.cs.fau.de/software/cool/-/merge_requests/7Generators2021-12-09T09:14:15ZSimon PruckerGeneratorsQCheck generators for formulas intended for property based tests in an extra libraryQCheck generators for formulas intended for property based tests in an extra libraryhttps://git8.cs.fau.de/software/cool/-/merge_requests/6Readme with user facing examples and install/build instructions2021-06-22T12:35:55ZMerlinReadme with user facing examples and install/build instructionswill adress:
- #9
- #12
- #18will adress:
- #9
- #12
- #18v1.0 - The first "real" releaseMerlinMerlinhttps://git8.cs.fau.de/software/cool/-/merge_requests/5Selective/Parallel test execution2019-08-06T11:53:47ZMerlinSelective/Parallel test executionThe new "--only" parameter on `cool-testsuite` allows having a job per test case set.The new "--only" parameter on `cool-testsuite` allows having a job per test case set.Hans-Peter DeifelHans-Peter Deifelhttps://git8.cs.fau.de/software/cool/-/merge_requests/4Documentation update2019-08-02T11:03:50ZMerlinDocumentation updateGitlab renders asciidoc into HTML is file endings are specified.Gitlab renders asciidoc into HTML is file endings are specified.Hans-Peter DeifelHans-Peter Deifelhttps://git8.cs.fau.de/software/cool/-/merge_requests/3Add licensing info2019-08-05T13:23:21ZMerlinAdd licensing info_oasis file said the project is GPL licensed but no LICENSE file was included_oasis file said the project is GPL licensed but no LICENSE file was includedHans-Peter DeifelHans-Peter Deifelhttps://git8.cs.fau.de/software/cool/-/merge_requests/2CI Improvements2019-08-01T13:58:08ZMerlinCI ImprovementsCI improvements as done originally in the cln branch.
---
Improvements:
* run tests
* separated build and tests
* optional compiler cross-compilation
---
The optional cross-compilation stages have the purpose of providing an easy w...CI improvements as done originally in the cln branch.
---
Improvements:
* run tests
* separated build and tests
* optional compiler cross-compilation
---
The optional cross-compilation stages have the purpose of providing an easy way to check if and how fast cool would compile under different OCaml versions.Hans-Peter DeifelHans-Peter Deifelhttps://git8.cs.fau.de/software/cool/-/merge_requests/1Add dune build system2021-05-21T14:15:37ZHans-Peter DeifelAdd dune build system*dune* is a newer build system for ocaml that tries to unify the different build systems of ocaml by invocation of [xkcd 927](https://xkcd.com/927/). Success is imminent, the majority of opam packages now use dune!
Advantages over oasis...*dune* is a newer build system for ocaml that tries to unify the different build systems of ocaml by invocation of [xkcd 927](https://xkcd.com/927/). Success is imminent, the majority of opam packages now use dune!
Advantages over oasis:
- tight integration with opam, if we ever want to publish cool there
- reportedly much faster than oasis
- doesn't need hacks to detect C code, build documentation or format source code
- can generate `.merlin` files
- subjectively, oasis seems unfinished around the edges and breaks when trying to use it in non-standard ways.
Disadvantages:
- Build definition spread out over individual files instead of being in one place (disadvantage status is subjective)
- No built-in concept of `configure` step and flags (but [easy workaround](https://github.com/ocaml/dune/tree/main/example/with-configure-step.t))
This is in preparation for making the pgsolver dependency optional and therefore being able to merge the pgsolver branch to master. I hope that this will be easier with dune than with oasis.v1.0 - The first "real" releaseMerlinMerlin