COOL issueshttps://git8.cs.fau.de/software/cool/-/issues2023-11-10T15:29:03Zhttps://git8.cs.fau.de/software/cool/-/issues/65Investigate out of memory2023-11-10T15:29:03ZMerlinInvestigate out of memoryInvestigate where the memory is leaked in our the ocaml-minisat usage.
Job [#34894](https://git8.cs.fau.de/software/cool/-/jobs/34894) failed for 7108bb19ee9342cc64dc168b4cb254e8120dadd8:Investigate where the memory is leaked in our the ocaml-minisat usage.
Job [#34894](https://git8.cs.fau.de/software/cool/-/jobs/34894) failed for 7108bb19ee9342cc64dc168b4cb254e8120dadd8:https://git8.cs.fau.de/software/cool/-/issues/64Reasoner for Aconjunctive Fragment decides formula incorrectly2023-08-07T14:16:29ZFrederik HennigReasoner for Aconjunctive Fragment decides formula incorrectlyThe following nearly identical formulas are both unsatisfiable (even in the classical sense), but COOL's reasoner for the aconjunctive fragment classifies the second formula as satisfiable.
```
f1 := ~(( ( νx.µy. ((q1 => []x) & (q2 => []...The following nearly identical formulas are both unsatisfiable (even in the classical sense), but COOL's reasoner for the aconjunctive fragment classifies the second formula as satisfiable.
```
f1 := ~(( ( νx.µy. ((q1 => []x) & (q2 => []y)) ) <=> ( νx.µy. ((q1 => []x) & (q2 => []y)) ) ))
f2 := ~(( ( νx.µy. ((q1 => []y) & (q2 => []x)) ) <=> ( νx.µy. ((q1 => []y) & (q2 => []x)) ) ))
```
COOL (`f1`):
```
$ cool-coalg sat K --fragment altfreeaconj <<< "~(( ( νx.µy. ((q1 => []x) & (q2 => []y)) ) <=> ( νx.µy. ((q1 => []x) & (q2 => []y)) ) ))"
Formula 1:
Both onestep and tableau implementation available
unsatisfiable
```
COOL (`f2`):
```
$ cool-coalg sat K --fragment altfreeaconj <<< "~(( ( νx.µy. ((q1 => []y) & (q2 => []x)) ) <=> ( νx.µy. ((q1 => []y) & (q2 => []x)) ) ))"
Formula 1:
Both onestep and tableau implementation available
satisfiable
```
Their NNFs, which are the formulas the reasoner actually works on, are identical, except for the order of appearance of fixpoint literals:
NNF (`f1`):
```
(νx.(μw.(~(q1) | [ ](x)) & (~(q2) | [ ](w)))) & (μy.(νz.q1 & < >(y) | q2 & < >(z))) | (νy.(μz.(~(q1) | [ ](y)) & (~(q2) | [ ](z)))) & (μx.(νw.q1 & < >(x) | q2 & < >(w)))
```
NNF (`f2`):
```
(νx.(μw.(~(q1) | [ ](w)) & (~(q2) | [ ](x)))) & (μy.(νz.q1 & < >(z) | q2 & < >(y))) | (νy.(μz.(~(q1) | [ ](z)) & (~(q2) | [ ](y)))) & (μx.(νw.q1 & < >(w) | q2 & < >(x)))
```
The second formula is decided wrongly only by the permutation-game reasoner; the more general Safra-tree-based reasoner correctly classifies both as unsatisfiable.https://git8.cs.fau.de/software/cool/-/issues/63Richer specification language for models2023-08-01T13:41:38ZMerlinRicher specification language for modelsCurrently, COOL models are specified simply as the coalgebra structure however other model checkers typically do not give explicit per-state models but rather some generating system description.
It is for example quite common to specify...Currently, COOL models are specified simply as the coalgebra structure however other model checkers typically do not give explicit per-state models but rather some generating system description.
It is for example quite common to specify typed variables (bounded) and some guarded mechanism of how their values evolve. Some specification languages also have forms of modularization and macro mechanisms. These features are only syntactic sugar on top of the underlying coalgebra structure and can hence be compiled into bare model structures.
#### Specification languages
1. AUT https://cadp.inria.fr/man/aut.html LTS as a list of triples
2. MoDeST https://www.researchgate.net/profile/Pedro-Dargenio/publication/28552328_MODEST_A_modelling_language_for_stochastic_timed_systems/links/0deec522297224620f000000/MODEST-A-modelling-language-for-stochastic-timed-systems.pdf
3. mCRL2 https://www.mcrl2.org/web/user_manual/language_reference/mcrl2.html
4. SMV https://nusmv.fbk.eu/NuSMV/papers/sttt_j/html/node7.html -\> NuSMV/nuXmv
5. GPF -\> GPUExplore https://www.win.tue.nl/\~awijs/articles/GPUexplore-tacas14.pdf
6. DVE/mDVE https://is.muni.cz/www/bauch/meandve.pdf -\> BEEM benchmark set available in mDVE https://paradise.fi.muni.cz/beem/
7. JANI https://jani-spec.org/ -\> many benchmarks available in JANI
8. BIR https://bogor.projects.cs.ksu.edu/manual/ch02.html -\> BOGOR https://bogor.projects.cs.ksu.edu/manual/
9. UPPAAL https://docs.uppaal.org/language-reference/
#### Vision
My goal would be to have a modular architecture where various input language features can be implemented as individual compiler passes over the input structure until it arrives at the bare coalgebra structurehttps://git8.cs.fau.de/software/cool/-/issues/62Implement game logic2023-08-01T12:32:22ZMerlinImplement game logicGiven that we now support the full mu-calculus, game logic should be encodable into the monotone mu-calculus.Given that we now support the full mu-calculus, game logic should be encodable into the monotone mu-calculus.https://git8.cs.fau.de/software/cool/-/issues/61Implement modal cube2023-08-01T12:32:31ZMerlinImplement modal cubeIn Cláudia Nalon, Ullrich Hustadt, Fabio Papacchini and Clare Dixon: Buy One Get 14 Free: Evaluating Local Reductions for Modal Logic (CADE 2023) there are encodings of the modal cube into K. It might be worth investigating whether this ...In Cláudia Nalon, Ullrich Hustadt, Fabio Papacchini and Clare Dixon: Buy One Get 14 Free: Evaluating Local Reductions for Modal Logic (CADE 2023) there are encodings of the modal cube into K. It might be worth investigating whether this extends to our fixpoint calculi.https://git8.cs.fau.de/software/cool/-/issues/60Implement ATL*2023-08-01T12:32:41ZMerlinImplement ATL*The AMC subsumes ATL*, so we could also introduce syntactic sugar for ATL* syntax like we do for ATL syntax.
Details should be in Thm 6.1 https://www.cis.upenn.edu/~alur/Jacm02.pdfThe AMC subsumes ATL*, so we could also introduce syntactic sugar for ATL* syntax like we do for ATL syntax.
Details should be in Thm 6.1 https://www.cis.upenn.edu/~alur/Jacm02.pdfhttps://git8.cs.fau.de/software/cool/-/issues/59Validation task in COOL2023-05-23T12:02:28ZMerlinValidation task in COOLAs COOL started as an ontology reasoner it is natural to look at SHACL (a standard language for validating ontologies). The underlying logic itself (similar to PDL + grades + nominals) is maybe not that interesting for COOL however the v...As COOL started as an ontology reasoner it is natural to look at SHACL (a standard language for validating ontologies). The underlying logic itself (similar to PDL + grades + nominals) is maybe not that interesting for COOL however the validation task they use might be incorporated into COOL to make COOL usable for a range of new applications.
The validation task essentially takes a frame without valuation and a specification and checks whether a satisfying valuation can be found. Given that in the coalgebraic view, atoms can be seen as nullary modalities and hence part of the functor/world structure this task can be seen as simply leaving out part of the structure and trying to find a satisfying filler.
This task conceptually lives somewhere in between model checking and satisfiability checking. When the completed model is constructed and returned there are different semantics to decide dependency loops in the specification and there are different semantics (e.g. well-founded or stable) similar to abstract argumentation semantics.
See e.g. https://www.vldb.org/pvldb/vol15/p2284-ahmetaj.pdf
I see at least the following use cases that would be enabled by having such a generic implementation:
- AMCDES open model checking
- Abstract argumentation labelling semanticshttps://git8.cs.fau.de/software/cool/-/issues/58Incorporate standard library extensions2023-08-01T12:33:52ZMerlinIncorporate standard library extensionsWe maintain our own CoolUtils module as an extension of the standard library, however, there are big libraries available in the community. It might be beneficial to choose and incorporate such a library instead of rolling our own.We maintain our own CoolUtils module as an extension of the standard library, however, there are big libraries available in the community. It might be beneficial to choose and incorporate such a library instead of rolling our own.https://git8.cs.fau.de/software/cool/-/issues/57Cmd API: functor argument2023-08-01T12:33:29ZMerlinCmd API: functor argumentThe used functor is specified as a cmd argument however in many cases the functor could be inferred from the parsing result of the given formula. The argument could hence be only required when it is not clear from the logic.
Another pos...The used functor is specified as a cmd argument however in many cases the functor could be inferred from the parsing result of the given formula. The argument could hence be only required when it is not clear from the logic.
Another possibility I see would be to give the functor to the parser to allow overlapping syntax or do automated embeddings of e.g. K modalities into CL.https://git8.cs.fau.de/software/cool/-/issues/56Cost constrained ATL2023-02-28T09:59:04ZMerlinCost constrained ATLCan we sensibly implement cost-constrained modal logics (e.g. cost constrained ATL)
The idea here is that the edges/moves have a cost and the modalities specify a budget. There are also variants where transitions can produce gains/incr...Can we sensibly implement cost-constrained modal logics (e.g. cost constrained ATL)
The idea here is that the edges/moves have a cost and the modalities specify a budget. There are also variants where transitions can produce gains/increase the budget are also available. Different semantics can be envisioned based on the granularity of the cost calculation (e.g. do individual moves have cost or only the joint move has a cost) as well as the scope of the budget (e.g. does the budget only affect the coalition in the modality of the system as a whole)https://git8.cs.fau.de/software/cool/-/issues/55Cmd API cleanup2023-01-20T15:20:50ZMerlinCmd API cleanupCurrently COOL consists of the `cool-coalg` executable which does a bunch of loosely related things as well as a bunch of other small executables with varying naming schemes. I suggest we give the executables a unified naming scheme and ...Currently COOL consists of the `cool-coalg` executable which does a bunch of loosely related things as well as a bunch of other small executables with varying naming schemes. I suggest we give the executables a unified naming scheme and split the `cool-coalg` executable into multiple executables that have a single usage domain. E.g. the SAT and model-checking functionality doesn't have to be in the same executable as they share almost no parameters or use-caseshttps://git8.cs.fau.de/software/cool/-/issues/54Graded ATL2023-08-01T12:34:32ZMerlinGraded ATLNow that we have ATL as well as GML support it might be worth investigating whether graded ATL can be nicely encoded in coalgebras and implemented in COOL.
https://www.researchgate.net/publication/220444447_Graded_Alternating-Time_Tempo...Now that we have ATL as well as GML support it might be worth investigating whether graded ATL can be nicely encoded in coalgebras and implemented in COOL.
https://www.researchgate.net/publication/220444447_Graded_Alternating-Time_Temporal_Logichttps://git8.cs.fau.de/software/cool/-/issues/53Implement LTL encoding2023-08-01T12:34:47ZMerlinImplement LTL encodingLTL should be implementable on functional Kripke frames.LTL should be implementable on functional Kripke frames.https://git8.cs.fau.de/software/cool/-/issues/52Drop CTL quantifiers from formula type2022-12-22T08:39:59ZMerlinDrop CTL quantifiers from formula typeCOOL handles CTL formulas by translating them to fixpoint formulas. This should be done directly in the parser as done for CTL.COOL handles CTL formulas by translating them to fixpoint formulas. This should be done directly in the parser as done for CTL.https://git8.cs.fau.de/software/cool/-/issues/51Test also other propagation strategies2022-10-12T15:39:08ZMerlinTest also other propagation strategiesCurrently, the whole test suite uses the `Adaptive` on-the-fly propagation strategy however COOL also offers other strategies that should also be tested.
Ideally, we write a property-based test checking that the propagation strategy par...Currently, the whole test suite uses the `Adaptive` on-the-fly propagation strategy however COOL also offers other strategies that should also be tested.
Ideally, we write a property-based test checking that the propagation strategy parameter doesn't affect SAT results.https://git8.cs.fau.de/software/cool/-/issues/50Generated parsers for rest of COOL2023-07-06T12:17:41ZMerlinGenerated parsers for rest of COOLCurrently the following functionality still uses hand-written lexers and parsers:
- [ ] the `ALCFormula` module
- [x] the functor expression parser
They should be refactored to use ocamllex and menhir like the rest of cool.Currently the following functionality still uses hand-written lexers and parsers:
- [ ] the `ALCFormula` module
- [x] the functor expression parser
They should be refactored to use ocamllex and menhir like the rest of cool.https://git8.cs.fau.de/software/cool/-/issues/49Lin-Smolka Fixpoint Computation2022-10-12T09:25:33ZLutz SchröderLin-Smolka Fixpoint ComputationOne may consider basing propagation on fixpoint computation in the style of Lin and Smolka, see Kupke et al. 2022 "Coalgebraic Reasoning with Global Assumptions in Arithmetic Modal Logics", https://arxiv.org/abs/2009.00971One may consider basing propagation on fixpoint computation in the style of Lin and Smolka, see Kupke et al. 2022 "Coalgebraic Reasoning with Global Assumptions in Arithmetic Modal Logics", https://arxiv.org/abs/2009.00971https://git8.cs.fau.de/software/cool/-/issues/48Experiment with OINK as a PGSolver alternative2022-10-12T08:26:34ZMerlinExperiment with OINK as a PGSolver alternativeThe usage of the optimized solver [OINK](https://github.com/trolando/oink) should be similar to PGSolver but might give a performance gain.
We should implement offloading the solving to OINK as an alternative to PGSolver and check if th...The usage of the optimized solver [OINK](https://github.com/trolando/oink) should be similar to PGSolver but might give a performance gain.
We should implement offloading the solving to OINK as an alternative to PGSolver and check if this improves performance.https://git8.cs.fau.de/software/cool/-/issues/47Simplify the agent mechanism2023-07-06T12:13:06ZMerlinSimplify the agent mechanismCurrently, the set of agents e.g. for CL is stored globally as an `int array` in COOL and accessed through `cl_{get,set}_agents` from the `CoolUtils`. I would argue that we should change it to just the number of agents. This would lose t...Currently, the set of agents e.g. for CL is stored globally as an `int array` in COOL and accessed through `cl_{get,set}_agents` from the `CoolUtils`. I would argue that we should change it to just the number of agents. This would lose the feature of having agents 1,7, and 12 without having the agent numbers in between for the gain of simplicity and making the code less error-prone.https://git8.cs.fau.de/software/cool/-/issues/46Formula printer has its own precedence mechanism2022-09-05T12:32:12ZMerlinFormula printer has its own precedence mechanismThe formula printer has its own precedence mechanism independent of the formula parser to determine where braces should be placed. Given that those two things are completely independent of one another we might run into cases where the br...The formula printer has its own precedence mechanism independent of the formula parser to determine where braces should be placed. Given that those two things are completely independent of one another we might run into cases where the bracketing leads to mismatches.
Related to #37