search

fluentverification / stamina-prism

STAMINA - STochastic Approximate Model-checker for INfinite-state Analysis, integrated with the PRISM model checking engine
https://staminachecker.org
MIT License
4 stars 3 forks source link

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

Open zgzn opened 4 years ago

zgzn commented 4 years ago

@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 commented 4 years ago

@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 commented 4 years ago

@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 commented 4 years ago

@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_subpBAD Circuit10_10_AmtR_module_subpHlyIIR Circuit10_10_PhIF_module_subpAmtR Circuit10_10_PhIF_module_subpTac Circuit10_10_BetI_module_subpHlyIIR Circuit10_10_BetI_module_subpTet Circuit10_10_YFP_module_subpBetI Circuit10_10_YFP_module_subpPhlF Circuit10_10_HIyIIR_module_subpTet Circuit10_10_HIyIIR_module_subpBAD reaction_rates Variables: YFP_protein BetI_protein PhlF_protein HlyIIR_protein AmtR_protein Circuit10_10_AmtR_module_subpBAD Circuit10_10_AmtR_module_subpHlyIIR Circuit10_10_PhIF_module_subpAmtR Circuit10_10_PhIF_module_subpTac Circuit10_10_BetI_module_subpHlyIIR Circuit10_10_BetI_module_subpTet Circuit10_10_YFP_module_subpBetI Circuit10_10_YFP_module_subpPhlF Circuit10_10_HIyIIR_module_subpTet Circuit10_10_HIyIIR_module_subpBAD

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)