Exception in selecting Gauss-Seidel and power options for CTMC analysis

[zgzn]

@brettjepsen Running the command below generated null pointer exception. The same happened to the power option.

$ stamina -gaussseidel toggle_IPTG_0_tmp.prism toggle_IPTG_0.csl
Picked up _JAVA_OPTIONS: -Xmx80g
PRISM

Version: 4.5
Date: Fri Apr 03 02:31:22 MDT 2020
Hostname: el176-deeplearning
Memory limits: cudd=64g, java(heap)=80g

Type: CTMC
Modules: TetR_def LacI_def
Variables: TetR LacI

Generator: stamina.InfCTMCModelGenerator
Type: CTMC

========================================================================
Approximation<1> : kappa = 1.0E-6

---

Building model...
18 2351 states

Time for model construction: 0.411 seconds.

Type: CTMC
States: 2351 (1 initial)
Transitions: 8650

Rate matrix: 8229 nodes (731 terminal), 8650 minterms, vars: 16r/16c
Exception in thread "main" java.lang.NullPointerException
at explicit.StateValues.(StateValues.java:115)
at explicit.StateModelChecker.checkExpressionLiteral(StateModelChecker.java:852)
at explicit.StateModelChecker.checkExpression(StateModelChecker.java:617)
at explicit.NonProbModelChecker.checkExpression(NonProbModelChecker.java:76)
at explicit.ProbModelChecker.checkExpression(ProbModelChecker.java:510)
at stamina.StaminaModelChecker.modelCheckStamina(StaminaModelChecker.java:200)
at stamina.StaminaCL.run(StaminaCL.java:171)
at stamina.StaminaCL.main(StaminaCL.java:91)

[brettjepsen]

@zgzn this seems to be a prism error:

PRISM
=====

Version: 4.5
Date: Fri Apr 03 19:12:01 MDT 2020
Hostname: Bretts-MacBook-Pro-Work.local
Memory limits: cudd=1g, java(heap)=1g
Command line: prism ../../stamina/case-studies/Toggle/toggle_IPTG_0.prism ../../stamina/case-studies/Toggle/toggle_IPTG_0.csl -gaussseidel

Parsing model file "../../stamina/case-studies/Toggle/toggle_IPTG_0.prism"...

Parsing properties file "../../stamina/case-studies/Toggle/toggle_IPTG_0.csl"...

1 property:
(1) P=? [ true U[0,2100] ((LacI<20)&(TetR>40)) ]

Type:        CTMC
Modules:     TetR_def LacI_def 
Variables:   TetR LacI 

---------------------------------------------------------------------

Model checking: P=? [ true U[0,2100] ((LacI<20)&(TetR>40)) ]

Building model...

Error: Cannot build a model that contains a variable with unbounded range (try the explicit engine instead).```

[zgzn]

@brettjepsen Sorry, I forgot to mention that you need to bound the variables. See attached PRISM file. You can use the same property file. @brettjepsen Actually,

toggle_IPTG_0_tmp.txt

[zgzn]

@brettjepsen It looks like the same error occurs on the hazard circuit model. Currently, with the updated circuit model, I do not need the Gauss-Seidel option.
Command: stamina -gaussseidel -cuddmaxmem 55g Circuit0x8E_flat_10.sm hazard.csl
PRISM

Version: 4.5
Date: Wed Apr 08 11:41:21 MDT 2020
Hostname: el176-deeplearning
Memory limits: cudd=55g, java(heap)=2g

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

========================================================================
Approximation<1> : kappa = 1.0E-6

---

Building model...
4 5342 states

Time for model construction: 12.756 seconds.

Type: CTMC
States: 5342 (1 initial)
Transitions: 42567

Rate matrix: 277317 nodes (1050 terminal), 42567 minterms, vars: 150r/150c
Exception in thread "main" java.lang.NullPointerException
at explicit.StateValues.(StateValues.java:115)
at explicit.StateModelChecker.checkExpressionLiteral(StateModelChecker.java:852)
at explicit.StateModelChecker.checkExpression(StateModelChecker.java:617)
at explicit.NonProbModelChecker.checkExpression(NonProbModelChecker.java:76)
at explicit.ProbModelChecker.checkExpression(ProbModelChecker.java:510)
at stamina.StaminaModelChecker.modelCheckStamina(StaminaModelChecker.java:219)
at stamina.StaminaCL.run(StaminaCL.java:172)
at stamina.StaminaCL.main(StaminaCL.java:91)