Support JANI's Forall and Exists Quantifiers

[Philipp15b]

Hello! I am working on the probabilistic program deductive verifier Caesar, and I have recently added support to generate JANI files from HeyVL files, Caesar's input. The idea is to replace the recently deleted storm-pgcl. Caesar's feature is documented here. To enable model-checking probabilistic programs with infinity-wlp semantics, i.e. using the greatest fixpoint for the while loop's fixpoint iteration starting at infinity, I need to check whether there exists a path that does not reach the sink (not just with probability 1).

JANI has the Boolean quantifiers Exists and Forall, which seem ideal for this purpose. However, they are not implemented right now as far as I can tell. It would be great if Storm added support for them :)

[Philipp15b]

Another motivation for this would be checking for over-approximations from the --build:state limit option (in the currently unmerged PR #521) by checking whether unexplored states are reachable.

[sjunges]

So this is basically asking for (regular) CTL model checking support? 👍

[Philipp15b]

I’m not an expert in the JANI spec, but I’d guess that’s what it is I’m asking for :)