search

moves-rwth / storm

A Modern Probabilistic Model Checker
https://www.stormchecker.org
GNU General Public License v3.0
126 stars 73 forks source link

Fix jani functions in properties #503

Closed tquatmann closed 4 months ago

tquatmann commented 4 months ago

Previously, functions occurring in properties were not handled correctly. This was the case because all functions declared in the model were eliminated before simplifying the properties. See preprocessSymbolicInput in model-handling.h, where the SymbolicModelDescription is preprocessed before the Jani model is simplified.

Since the preprocess() method was used in the DdJaniModelBuilderTest to (also) eliminate functions, I reworked this (and for consistency, the ExplicitJaniModelBuilderTest as well).

sjunges commented 4 months ago

Looks good. May be good to avoid the now even more appearant code duplication.

tquatmann commented 4 months ago

Looks good. May be good to avoid the now even more appearant code duplication.

Absolutely! The builder tests could need a refactor and should be templated like (most of) the model checker tests.