FAU error

Skip to first unread message


Feb 27, 2019, 1:51:32 PM2/27/19
to PRISM model checker developers

We have been developing approximation techniques to analyze infinite-state continuous Markov chain models. When verifying the results generated by our method against Fast Adaptive Uniformization, we got inconsistent results. I am using attached infinite state model(model.prism) and property 'P=? [ true U[0,800] ((LacI<20)&(TetR>40)) ]'. 

Verification result:

Version: 4.4
Date: Wed Feb 27 11:37:34 MST 2019
Hostname: xx
Memory limits: cudd=1g, java(heap)=4.4g
Command line: prism -javamaxmem 5g -transientmethod fau -fauepsilon 1e-9 model.prism -pf 'P=? [ true U[0,800] ((LacI<20)&(TetR>40)) ]'

Parsing model file "model.prism"...

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

Type:        CTMC
Modules:     TetR_def LacI_def 
Variables:   TetR LacI 


Model checking: P=? [ true U[0,800] ((LacI<20)&(TetR>40)) ]
Starting transient probability computation using fast adaptive uniformisation...

Total probability lost is : 1.4664550684884148E-9
Maximal number of states stored during analysis : 367

Model checking completed in 0.099 secs.

Result (probability): 0.0

The actual probability value for this property is "0.7255". Is there anything I am missing while using the FAU method?

Thanks for the help!

Thakur Neupane

Joachim Klein

Feb 27, 2019, 2:51:06 PM2/27/19
to thakur....@aggiemail.usu.edu, PRISM model checker developers
Hi Thakur,

you are right: There was a bug in FAU model exploration that was fixed
after the 4.4 release. I just tried your model with the current version
of the PRISM development trunk from Github
(https://github.com/prismmodelchecker/prism), and that gets the result
you expect.

There will be a 4.5 PRISM release shortly, otherwise you can get the
source from the github repository and compile yourself.

Joachim Klein
Reply all
Reply to author
0 new messages