Rather than using the ModelModify class to change property modification, we could use something within storm::logic::Formula or storm::*::Expression. This was originally written in a (somewhat buried) commit, but was not used because there were some issues with passing that expression into the model checker. If we were able to get this to work, it would present these benefits:
Reduced memory footprint in CompressedStates (by 1 bit per state)
Reduced code complexity in stamina::util::ModelModify
Reduced hard drive impact (minor)
This is marked as "enhancement" as it does not affect the results of STAMINA/STORM
Rather than using the
ModelModify
class to change property modification, we could use something withinstorm::logic::Formula
orstorm::*::Expression
. This was originally written in a (somewhat buried) commit, but was not used because there were some issues with passing that expression into the model checker. If we were able to get this to work, it would present these benefits:CompressedStates
(by 1 bit per state)stamina::util::ModelModify
This is marked as "enhancement" as it does not affect the results of STAMINA/STORM