State generation gets stuck when analyzing inverted until property

[zgzn]

STAMINA seems to be stuck at (or before) the first iteration of state generation, when the CSL property is P=? [!(true U[0,1000] (YFP_protein > 30)) ] for the hazard circuit model (both included in the attached zip file).

$ stamina -noproprefine -maxapproxcount 70 Circuit0x8E_flat_10_010to111_unbounded.sm hazard_glitch_zero.csl
STAMINA

hazardCctModelAndCSL.zip

Version: 1.1

PRISM

Version: 4.5
Date: Sat May 30 13:48:03 MDT 2020
Hostname: el176-deeplearning
Memory limits: cudd=1g, java(heap)=120g

Type: CTMC
Modules: YFP_protein BetI_protein PhlF_protein HlyIIR_protein AmtR_protein Circuit10_10_AmtR_module_sub__pBAD Circuit10_10_AmtR_module_sub__pHlyIIR Circuit10_10_PhIF_module_sub__pAmtR Circuit10_10_PhIF_module_sub__pTac Circuit10_10_BetI_module_sub__pHlyIIR Circuit10_10_BetI_module_sub__pTet Circuit10_10_YFP_module_sub__pBetI Circuit10_10_YFP_module_sub__pPhlF Circuit10_10_HIyIIR_module_sub__pTet Circuit10_10_HIyIIR_module_sub__pBAD reaction_rates
Variables: YFP_protein BetI_protein PhlF_protein HlyIIR_protein AmtR_protein Circuit10_10_AmtR_module_sub__pBAD Circuit10_10_AmtR_module_sub__pHlyIIR Circuit10_10_PhIF_module_sub__pAmtR Circuit10_10_PhIF_module_sub__pTac Circuit10_10_BetI_module_sub__pHlyIIR Circuit10_10_BetI_module_sub__pTet Circuit10_10_YFP_module_sub__pBetI Circuit10_10_YFP_module_sub__pPhlF Circuit10_10_HIyIIR_module_sub__pTet Circuit10_10_HIyIIR_module_sub__pBAD

Generator: stamina.InfCTMCModelGenerator
Type: CTMC