COOL merge requestshttps://git8.cs.fau.de/software/cool/-/merge_requests2023-06-10T16:14:52Zhttps://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 Hennig