Global state: Settings used throughout the code

[sjunges]

As a midterm goal, it would be good to clarify the use of command line settings throughout the code. For this, we have adapted environments as a more transparant solution. The following image shows, however, that we still have quite a way to go. (This simply searches for the occurrence of "settings", I have a longer more detailled list somewhere). Occurrences of settings in the settings is clear, and in the environment constructor is something that could be easily resolved.

To be clear: a limited use of a global state is fine, but right now there are too many variables occurring at too many places. I think that a global state object should have a limited set of well documented variables and that settings should be a CLI thing.

Lets focus on the easier targets first

• Api
• Builder (Requires dont fix deadlocks as a builder option)
• Generator
• Modelchecker
• Solver
• Storage
• Utility

For utility, the difficult cases seem to be:

• ProgressMeasurement (settings to determine whether to output something, relates to STORM_PRINT vs STORM_LOG_INFO outside CLI #272)
• ConstantsComparator (settings to determine the precision to use, fixed by ConstantsComparator no longer depends on global state #830)
• VectorHelper (settings to determine whether to use TBB), relates to Newer versions of Intel TBB are incompatible #133

[sjunges]

Update:

[sjunges]

While I still need to provide an updated picture, here are two points worth discussing, related to the SMT solver.

The SMT solver is currently often hardcoded, mostly to be z3 (this makes somewhat sense as the only other solver we currently support is mathsat). The generic factory that builds this from settings, is, however also used in some places deep down>

• Various NativePolytope checks
• Various PrismProgram/JaniModel routines, some of them deep down.

I would currently suggest to use a DefaultFactory for these deep-down methods that are most likely not very performance critical (although the code for nativepolytope could be), where the default order is decided at compile time and cannot be changed by setting the environment.

The alternative is to pass the environment or the factory through many layers of code. That feels very disruptive for a run-time flag that isnt that important to us.

@tquatmann I would in particular like your perspective on the NativePolytope.